Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generated
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.

Variable-mass momentum balance: from m′=rin−rout and (mv)′=F+rinwin−routwout to mv′=F+rin(win−v)−rout(wout−v)

Statement

Let I⊆R be an interval with nonempty interior (Intervals of R: the nine order-convex forms, nondegeneracy, and length), let m:I→(0,∞) and v:I→R3 be differentiable (The derivative f′(c)=lim⁡x→cf(x)−f(c)x−c of f:A→R at a point c∈A that is a limit point of A, and differentiability on a set, The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral), and let F:I→R3, rin,rout:I→[0,∞) and win,wout:I→R3 be maps. Suppose the two material balance identities

m′(t)=rin(t)−rout(t),(mv)′(t)=F(t)+rin(t)win(t)−rout(t)wout(t)

hold for every t∈I, where mv denotes the pointwise scalar multiple. Then

m(t)v′(t)=F(t)+rin(t)(win(t)−v(t))−rout(t)(wout(t)−v(t))(t∈I).

In particular, if F≡0, rin≡0 and rout≡r for a constant r≥0, then mv′=−r(wout−v): the acceleration is governed by the momentum carried away per unit time relative to the body, not by (mv)′=0.

The two balance identities are the adopted content of the material momentum accounting — the mathematical rendering of "gains rin dt of matter with velocity win, loses rout dt with velocity wout, and feels the external force F". They are not derived here from any closed-system law; the deduction below is their product-rule consequence.

Facts & Assumptions

Given: An interval I with nonempty interior, a differentiable positive real function m and vector curve v, maps F,win,wout into R3, nonnegative functions rin,rout, and the two material balance identities on I.

Proof

technique · direct
1.1givenL1

By [L1] the product rule applies coordinatewise to mv: (mv)′=m′v+mv′, since (mv)k=mvk and (mvk)′=m′vk+mvk′ for each coordinate k.

2.1step 1.1givenL1algebra∎

Substituting the first balance identity into the second and using step 1.1, mv′=(mv)′−m′v=F+rinwin−routwout−(rin−rout)v=F+rin(win−v)−rout(wout−v), the last step grouping the rin-terms and the rout-terms and using bilinearity of scalar multiplication. This is the displayed conclusion; the special case F≡0, rin≡0, rout≡r is its immediate substitution, in that case the assumed momentum balance is (mv)′=−rwout, so (mv)′=0 at a time t exactly when rwout(t)=0.

Depends on

Dependency tree · 2 levels

Sources