Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-adapted
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A declared smooth open flow: the uniform scaling ρ=ρ0e−3αt, u=αx satisfies the control-volume identities on fixed and material regions, and elbow port data illustrate the inlet/outlet decomposition

Physical scope

Two declared checks of the finite-regularity open-flow bookkeeping: (i) the exact uniform-scaling model ρ(t)=ρ0e−3αt, u(t,x)=αx, p=p0−ρα2∣x∣2/2, with the control maps specified and the units of α,ρ0,p0 declared; (ii) a conditional steady-elbow calculation with declared inlet/outlet data, where the balance gives mass flow 0.4 kg s−1 and requires a net external resultant on the fluid of magnitude about 3.578 N. No pressure-free momentum-flux force decomposition is inferred, since no boundary-stress data are given. Both are computations on declared model data; the example reports no measurement and does not solve a boundary-value problem.

Example

(i) Declared uniform scaling. Fix constants ρ0>0, α≠0 and p0, with [ρ0]=μℓ−3, [α]=τ−1 and [p0]=μℓ−1τ−2. On an open interval I∋0 use uniform scaling, meaning expansion for α>0 and contraction for α<0, and set ρ(t)=ρ0e−3αt,u(t,x)=αx,σ(t,x)=−p(t,x) Id,p(t,x)=p0−ρ(t)α22∣x∣2,b≡0, and fix radii R0>0 and R>0 with units ℓ. Let the material region be a ball BRB with radius RB>max⁡(R,R0). Define the material motion χ(t,X)=eαtX on a neighbourhood of BRB‾. More precisely, choose an open ball O=BRO with RO>RB and define χ:I×O→R3 by this formula. Its restriction to BR0 has current radius R(t)=R0eαt. Define the fixed-ball control motion by ψR(t,X)=X for X∈O, with control region BR, and the material-ball control motion by ψmat(t,X)=eαtX for X∈O, with control region BR0. Each map is a C2 motion on the open reference domain O and has positive spatial Jacobian. Take the fields on a common open neighbourhood of the closed sweep of χ and the closed sweeps of these controls. The fields satisfy the adopted balances of The finite-regularity open-flow model: moving-control-region mass and momentum balances, their material and fixed special cases, and the inlet/outlet decomposition reproducing the open-body and rocket laws (the density is spatially uniform, the velocity is αx, and the pressure is quadratic).

(ii) Declared elbow control-volume data. Take a material region B with motion χ and associated spatial velocity field u as in Continuum motions, spatial velocity, material acceleration and swept regions, and a material subregion B′⊆B with C1 boundary. On an open reference neighbourhood O⊃B′‾, define the fixed control motion ψ:I×O→R3 by ψ(t,X)=X; its control region is Ct=C:=B′ and its boundary velocity is w=0. Adopt the material balances of The finite-regularity open-flow model: moving-control-region mass and momentum balances, their material and fixed special cases, and the inlet/outlet decomposition reproducing the open-body and rocket laws for this model and the local mass and momentum equations on an open field neighbourhood of the closed control region, as allowed by that theorem's local-equation alternative.

Assume ρ=1000 kg m−3 is constant and the fields are time-independent on that neighbourhood. The bounded C1 boundary of C is partitioned into finitely many C1 boundary pieces, up to surface-measure-zero edges; designate an inlet patch Σin, an outlet patch Σout, and let the remaining pieces form an impermeable remainder Σ0. The outward unit normals on the ports are −x^ and +y^. On the ports take u=qinx^ and u=qouty^, respectively, where each q is a nonnegative, nonzero C1 profile supported compactly inside its port, with units ℓτ−1; take u⋅ν=0 on the remainder. These traces vanish near the port edges and are compatible with a C1 field and continuous boundary normal. For either port define Q:=∫Σq dS>0,veff:=∫Σq2 dSQ,Aeff:=Q2∫Σq2 dS, so Q=Aeffveff, the mass rate is ρQ, and the flux-averaged velocity is veff in the port direction. Declare Aeff,in=10−4 m2, Aeff,out=5×10−5 m2 and veff,in=4 m s−1; the outlet effective speed is unknown. The effective areas are defined by these integrals, not the geometric patch areas. Assume the time-independent velocity field is C1 on the common neighbourhood. Set the body-force field to b=0 and assume the stress field is C1 on the same neighbourhood. These are conditional model premises for a balance calculation; no existence claim for a boundary-value solution or decomposition of the boundary stress is made. The calculation determines only the net external resultant required by the steady balance.

Facts & Assumptions

[L1]

Balance and control-volume identities (The finite-regularity open-flow model: moving-control-region mass and momentum balances, their material and fixed special cases, and the inlet/outlet decomposition reproducing the open-body and rocket laws clauses 1-3, Control-volume balance: mass and momentum rates for a moving non-material region, Continuum motions, spatial velocity, material acceleration and swept regions, Euclidean spatial calculus: gradient, divergence and material derivative, Variable-mass momentum balance: from m′=rin−rout and (mv)′=F+rinwin−routwout to mv′=F+rin(win−v)−rout(wout−v)): for a model satisfying the adopted local mass and momentum balances, (CV1) and (CV2) hold for every control motion with bounded C1 control regions whose closed sweep lies inside the common field domain where those local equations hold; if the boundary splits into inlet and outlet with the stated signs, then m′=rin−rout and P′=Fext+rinwin−routwout.

[L2]

Elementary calculus and algebra (Intervals of R: the nine order-convex forms, nondegeneracy, and length, Ck Euclidean maps and diffeomorphisms, The Euclidean inner product ⟨x,y⟩=∑k<nxkyk on Rn, Dimensions and SI unit conventions of the non-relativistic classical mechanics framework): ddte−3αt=−3αe−3αt; for the field u=αx, div⁡u=3α, u⋅∇u=α2x and ∇∣x∣2=2x; the surface integral of the unit normal over a sphere vanishes, and odd integrands over a centred ball integrate to zero.

Verification

technique · direct
1.1givenA1L1L2algebra

Local balances for (i): ∂tρ+div⁡(ρu)=−3αρ+ρ div⁡u=−3αρ+3αρ=0, and ρ Dtu=ρ(0+α2x)=ρα2x while ρb+div⁡σ=−∇p=ρα2x; hence the declared fields satisfy the local balances (K) and (KM) of The finite-regularity open-flow model: moving-control-region mass and momentum balances, their material and fixed special cases, and the inlet/outlet decomposition reproducing the open-body and rocket laws. For each admissible material subregion, applying Control-volume balance: mass and momentum rates for a moving non-material region with control motion ψ=χ makes w=u and gives the adopted material balances; thus the premises of The finite-regularity open-flow model: moving-control-region mass and momentum balances, their material and fixed special cases, and the inlet/outlet decomposition reproducing the open-body and rocket laws hold. The fixed and material balls stay in the stipulated neighbourhoods of their closed sweeps, so its control-volume identities apply to them. For (ii), the fixed elbow control region stays in its declared common field domain, its boundary has nonpositive flux on the inlet patch, nonnegative flux on the outlet patch and zero flux on the remainder. The local equations are adopted there, so (CV1) and (CV2) of [L1] apply. Splitting their integrals over these patches remains valid when a profile vanishes: those subsets contribute zero.

1.2givenL1L2algebra

Inlet/outlet data for (ii): the fixed-region mass identity (CV1), steady density and velocity, and u⋅ν=0 on Σ0 give equal inlet and outlet rates, ρAeff,inveff,in=ρAeff,outveff,out. Hence m˙=1000⋅10−4⋅4=25 kg s−1=ρAeff,outveff,out, so veff,out=25/(1000⋅5×10−5)=8 m s−1; thus rin=rout=25 kg s−1 and the flux-averaged velocities are win=4x^, wout=8y^ in m s−1.

2.1step 1.1L1L2algebra

Fixed-ball check: for C=BR one has mC=4π3ρ(t)R3 and hence mC′=4π3(−3αρ)R3=−4παρR3; on the other hand (u−0)⋅ν=αR on ∂BR, so −∫∂Cρ(u−0)⋅ν dS=−ραR⋅4πR2=−4παρR3, which is (CV1). For (CV2): PC=∫BRραx dx=0 (odd integrand) and ∫∂Cρu(u⋅ν)dS=ρα2R∫∂Cx dS=0 and ∫∂Cσν dS=−p(R)∫∂Cν dS=0, with ∫BRρb=0; both sides of (CV2) vanish. At ρ0=1000 kg m−3, R=110 m, α=110 s−1, t=0: mC=4π3 kg and mC′=−2π5 kg s−1, agreeing with the flux value.

2.2step 1.2L1L2algebra

Net external resultant on the fluid: for steady fields on a fixed control region with zero body force, the fixed-control momentum identity (CV2) of The finite-regularity open-flow model: moving-control-region mass and momentum balances, their material and fixed special cases, and the inlet/outlet decomposition reproducing the open-body and rocket laws, split over the three patches, gives 0=Fext+m˙ win−m˙ wout. Hence the net external resultant required by the adopted balance is Fext=m˙(wout−win)=25(8y^−4x^) N=(−85x^+165y^) N, with magnitude 855 N≈3.578 N. This is the resultant of all external tractions on the fluid under the stated model equations; no pressure or wall-traction decomposition, and no device-force value, is determined by the supplied data.

3.1step 1.1L1L2algebra

Material-ball check: use the material control motion ψmat(t,X)=eαtX on BR0, so Ct=BR(t) with R(t)=R0eαt. For x=ψmat(t,X) on the boundary, w=∂tψmat(t,X)=αx=u(t,x), so (u−w)⋅ν=0; then (CV1) gives mC′=0, and indeed mC=4π3ρ(t)R(t)3=4π3ρ0R03 is constant. In (CV2), PC′=∫Ctρb+∫∂Ctσν with both sides zero as in step 2.1 (now at the moving radius), consistent with PC=0. This is the material special case of The finite-regularity open-flow model: moving-control-region mass and momentum balances, their material and fixed special cases, and the inlet/outlet decomposition reproducing the open-body and rocket laws clause 2.

4.1givenL1L2∎

Reading: the uniform-scaling fields are an exact solution of the adopted balances, so steps 2.1 and 3.1 check the control-volume identities for the explicitly specified fixed and material control motions. In the elbow calculation, the vector and its magnitude are the conditional net external resultant required by the steady momentum balance; the example supplies no boundary stresses with which to decompose that resultant into pressure and wall contributions. It is not a solution of the full boundary-value problem. All data are model data; no measurement, apparatus or uncertainty is involved.

Remarks

  • What the exact solution does and does not solve. The uniform scaling satisfies the local balances and therefore the control-volume identities; it does not satisfy any particular boundary condition on a wall, because the velocity field is defined on all of space. The material ball is a material region of the declared motion, consistent with Continuum motions, spatial velocity, material acceleration and swept regions.

  • Boundary forces in the elbow. The number 3.578 N is the magnitude of the net external resultant on the fluid required by the adopted steady balance. Equal inlet and outlet pressures and inviscid-wall language would not by themselves determine the wall pressure traction; no pressure-free flux force or device force is isolated here. The example illustrates the inlet/outlet decomposition and is not a design formula.

Depends on

Dependency tree · 2 levels

Sources