IndisputableMonolith.Gravity.SevenGaps.Gap5MomentumAdditivity
Algebraic and sign lemmas for ledger imbalance under swap, addition, and scaling, plus a root classification of the kinetic condition. The kinetic condition equates squared momentum to squared net imbalance; on orbits it follows from cost exactness, globally it is a named premise. Downstream magnitude-bridge work cites these facts to reduce the global identity to a single energy-cost hypothesis on the positive quadrant.
claimThe kinetic condition asserts $p(z)^2 = I(z)^2$ for ledger states $z$, with $I$ the net imbalance. The module proves $I$ is odd under swap, additive, and homogeneous; imbalance segments keep constant sign on unit intervals; and roots of the kinetic identity are classified via vanishing of the balance term.
background
Gap 5 sits in the Seven Gaps gravity program: whether classical momentum and the half-imbalance chart arise from recognition primitives rather than stipulation. The upstream chart module records a failed derivation verdict: the half-imbalance chart is stipulated, and with the geometry route closed, Pillar 1 has no surviving named route from a recognition primitive to classical gravity.
This module isolates the kinetic condition: the momentum observable squared equals the squared net ledger imbalance. On an orbit that identity is forced by exactness of the recognition cost; as a global statement on all ledger states it is only a named premise. Sibling definitions package the condition itself, swap-oddness, and elementary imbalance calculus (swap, add, scalar multiply, positive/negative segments).
Sign lemmas then lock the imbalance to a constant sign on each unit interval with no interior zero-crossing, which feeds the root classification: when the kinetic identity holds, balance vanishing characterizes the roots.
proof idea
Not a single theorem wrapper. The module is a short lemma stack. First, pure algebraic identities for imbalance under swap, addition, and scalar multiplication. Segment lemmas treat positive and negative pieces separately. Sign constancy on the unit interval is proved by ruling out a sign change (no interior root on that interval), yielding constant-positive and constant-negative corollaries. Balance vanishing of the kinetic identity and the kinetic root classification then combine those facts: if the squared-momentum equals squared-imbalance relation holds, the balance term vanishes exactly at the classified roots. No deep analytic machinery; elementary real one-variable sign and homogeneity arguments.
why it matters in Recognition Science
Feeds the momentum-magnitude bridge module, which states that 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 control of imbalance, that exact reduction cannot be stated cleanly.
In the broader Gap 5 arc, the upstream chart-from-ledger verdict already closed the geometry route and marked the half-imbalance chart as stipulated. This module does not reopen that route. It supplies the algebraic substrate so the residual gap can be named precisely: discharge the global kinetic identity, or accept EnergyEqualsCost as an independent physical premise. Framework landmarks (T5 J-cost, RCL) sit one layer below; here the issue is whether ledger imbalance behaves like classical momentum magnitude under the kinetic square identity.
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 imbalance algebra for that residual.
- Does not address spatial dimension, eight-tick structure, or Newtonian limit matching.
- Does not claim classical gravity follows from Gap 5 alone.
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