IndisputableMonolith.Gravity.SevenGaps.Gap5MomentumAdditivityComposition
The chart system's recognition cost obeys the Recognition Composition Law, inherited from symplectic area preservation (σ = 0). The module also packages imbalance and absolute-imbalance facts and proves that momentum additivity is independent of the composition law. Gravity Gap-5 consumers cite it when separating ledger composition from momentum bookkeeping. Arguments are mostly import wrappers plus short algebraic and continuity lemmas.
claimThe chart recognition cost $J$ satisfies the composition law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. Absolute imbalance is continuous, normalized, vanishes on balance, and is not additive; ordinary imbalance is additive on the debit axis. Momentum additivity is independent of the composition law.
background
Recognition Science forces the unique cost $J(x)=\frac12(x+x^{-1})-1$ from the Recognition Composition Law (RCL) together with reciprocity, normalization, calibration, and continuity. Upstream, the symplectic-action module identifies $J$ as the action of the double-entry ledger: vanishing symplectic area ($\sigma=0$) supplies the trace identity that is exactly RCL for $J$.
This module sits in Gravity Gap 5, after the EnergyEqualsCost derivation. That upstream no-go shows EnergyEqualsCost is independent of Hamiltonian data and lands only after one extra input. Here the focus shifts to how chart cost composes and how imbalance (net debit/credit mismatch) behaves under addition, absolute value, and continuity.
Sibling material packages unit, balance-vanishing, continuity, and (non)additivity for imbalance and absolute imbalance, then isolates momentum additivity from the composition law itself.
proof idea
The composition-law claim is imported from the symplectic derivation: area preservation yields the trace identity that is SatisfiesCompositionLaw for chart $J$-cost, so the main lemma is essentially a one-line wrapper of that identity.
A companion result records that the composition law does not mention momentum, so momentum bookkeeping cannot be read off RCL alone. Imbalance lemmas establish unit normalization, vanishing on balanced postings, and additivity on the debit axis; absolute-imbalance lemmas add continuity and a non-additivity counterexample. These are bundled into two small packages (additive imbalance and absolute imbalance). The headline independence statement then combines the composition-law fact with the imbalance packages to separate momentum additivity from RCL.
why it matters in Recognition Science
Gap 5 is closing the ledger-to-energy bridge for gravity. Downstream, Gap5NetImbalanceDerivation consumes this module: its verdict is that the net-imbalance package from posting-level incidence lands, with a supporting no-go, while full derivation of the remaining charged outcome does not. That consumer needs ReadsNetImbalance and AdditiveOnDebitAxis (with continuity and unit) to force consolidation additivity and EnergyEqualsCost.
By proving chart cost satisfies RCL via symplectic $\sigma=0$, and by showing momentum additivity is independent of that law, this module supplies the composition half of the Gap-5 interface without smuggling momentum structure into $J$. It sits on the T5 J-uniqueness landmark and the RCL identity, and keeps the EnergyEqualsCost path honest about which extra inputs are still required.
scope and limits
- Does not derive EnergyEqualsCost or close the full Gap-5 energy bridge.
- Does not force momentum additivity from the composition law alone.
- Does not claim absolute imbalance is additive; it proves the opposite.
- Does not re-derive J-uniqueness; it imports the symplectic RCL identity.
- Does not address spatial dimension, eight-tick structure, or the alpha band.
used by (1)
depends on (2)
declarations in this module (26)
-
theorem
chart_cost_satisfies_composition_law -
theorem
composition_law_ignores_momentum -
theorem
imbalance_unit -
theorem
imbalance_balance_vanishing -
theorem
abs_imbalance_continuous -
theorem
abs_imbalance_balance_vanishing -
theorem
abs_imbalance_unit -
theorem
abs_imbalance_not_additive -
theorem
imbalance_additive_package -
theorem
abs_imbalance_package -
theorem
momentum_additivity_independent_of_composition_law -
def
nlPUnit -
theorem
nlPUnit_continuous -
theorem
nlPUnit_swap_odd -
theorem
nlPUnit_balance_vanishing -
theorem
nlPUnit_unit -
theorem
nlPUnit_not_additive -
theorem
nlPUnit_package -
def
ReadsNetImbalance -
def
AdditiveOnDebitAxis -
theorem
balance_vanishing_of_net_imbalance_reading -
theorem
continuous_additive_real -
theorem
energyEqualsCost_of_net_imbalance_reading_additive_unit -
theorem
imbalance_reads_net_and_additive_on_axis -
structure
MomentumAdditivityCompositionVerdict -
theorem
momentumAdditivityCompositionVerdict