IndisputableMonolith.Gravity.SevenGaps.Gap5MomentumAdditivity
Module developing the kinetic condition: squared momentum equals squared net ledger imbalance, together with additivity and sign-constancy lemmas for that imbalance. Gravity auditors cite it when reducing global kinetic identities to local chart statements. The argument is algebraic: imbalance transforms linearly under swap, scale, and segment operations, then root classification pins when balance vanishes.
claimThe kinetic condition asserts $p(z)^2 = I(z)^2$ for ledger states $z$, where $I$ is net ledger imbalance and $p$ is the momentum observable. The module proves $I$ is additive and homogeneous, invariant (up to sign) under odd swaps, and sign-constant on unit intervals without zero crossings; balance vanishing and kinetic root classification follow.
background
Gap 5 in the Seven Gaps gravity program asks whether classical momentum and energy identities drop out of recognition ledger structure or must be named as premises. The upstream chart module already records a negative verdict: the half-imbalance chart is stipulated, not derived, so Pillar 1 has no surviving named route from a recognition primitive to classical gravity.
Against that backdrop this module isolates the kinetic condition itself. On an orbit, $p^2 = I^2$ is forced by exactness of the recognition cost; as a global identity on all ledger states it is only a named premise. The supporting objects are the imbalance functional $I$ and elementary operations on it: odd swap, addition, scalar multiplication, and restriction to positive or negative segments.
Sign analysis on the unit interval (no sign change unless a root is hit) supplies the bridge from local algebraic identities to global root classification of the kinetic equation.
proof idea
Not a single theorem: a cluster of elementary lemmas. Imbalance is shown additive and $\mathbb{R}$-homogeneous, and odd under the swap that exchanges the two ledger sides. Segment restrictions inherit positivity or negativity. A no-sign-change lemma on the unit interval yields constant-sign corollaries away from zeros. Those feed balance-vanishing-of-kinetic and a root classification for the kinetic condition. No deep analytic machinery; pure algebraic bookkeeping on the ledger imbalance.
why it matters in Recognition Science
Feeds the downstream momentum-magnitude bridge module, whose doc-comment states the global kinetic condition is not derived from substrate structure, yet on the open positive quadrant is exactly equivalent to the named premise EnergyEqualsCost. Without additivity, homogeneity, and sign constancy of imbalance, that exact reduction cannot be stated. In the broader Seven Gaps audit this module therefore sharpens what remains open: the kinetic identity is isolated as a residual premise rather than smuggled into chart geometry. It does not reopen the closed geometry route of the upstream chart module; it only organizes the algebraic residue that later bridge work must either discharge or keep named.
scope and limits
- Does not derive the global kinetic condition from recognition cost or substrate axioms.
- Does not construct or justify the half-imbalance chart; that remains stipulated upstream.
- Does not prove EnergyEqualsCost; only prepares algebraic lemmas used in its equivalence analysis.
- Does not address spatial dimension, eight-tick structure, or other forcing-chain landmarks.
- Does not close Gap 5 or restore a named Pillar 1 route to classical gravity.
used by (1)
depends on (1)
declarations in this module (21)
-
def
KineticCondition -
def
SwapOdd -
theorem
imbalance_swap -
theorem
imbalance_add -
theorem
imbalance_smul -
theorem
imbalance_seg_pos -
theorem
imbalance_seg_neg -
theorem
no_sign_change_on_unit_interval -
theorem
sign_const_pos -
theorem
sign_const_neg -
theorem
balance_vanishing_of_kinetic -
theorem
kinetic_root_classification -
theorem
kinetic_root_mem_four -
theorem
kinetic_root_additive_iff -
theorem
kinetic_root_additive_iff_swap_odd -
theorem
momentum_additivity_from_swap -
theorem
kinetic_on_orbit -
theorem
nlP_countermodel -
theorem
abs_countermodel -
structure
MomentumAdditivityVerdict -
theorem
momentumAdditivityVerdict