AdditiveOnDebitAxis
plain-language theorem explainer
Defines 1D Cauchy additivity for a momentum observable along pure-debit ledger states: p(m,0)+p(n,0)=p(m+n,0). Gravity and Gap-5 authors cite it as the weakened additivity premise that, with net-imbalance reading, continuity, and unit normalization, forces EnergyEqualsCost. The body is a one-line Prop abbreviation, not a proved theorem.
Claim. A real-valued map $p$ on ledger states is additive on the pure-debit axis when, for all $m,n\in\mathbb{R}$, $p(m,0)+p(n,0)=p(m+n,0)$.
background
Gap 5 studies momentum observables $p:\mathrm{LedgerState}\to\mathbb{R}$ on the two-component ledger chart (debit, credit). The net imbalance $z\mapsto z_1-z_2$ is the canonical candidate: defined by subtraction alone, with no cost functional in the formula.
The module attacks unconditional consolidation additivity from the recognition composition law (RCL). Ambient cost is $J$-cost, which satisfies RCL independently of any choice of $p$. Companion packages (continuity, balance-vanishing, unit normalization) admit both additive imbalance and non-additive absolute imbalance, so RCL alone does not select additivity.
This definition isolates the 1D restriction of additivity to the pure-debit ray $(m,0)$, the Cauchy equation along that axis. Downstream results pair it with net-imbalance reading to recover full balance-vanishing and EnergyEqualsCost without a kinetic hypothesis.
proof idea
Definitional Prop, not a proof. The body is the universal quantification $\forall m,n,, p(m,0)+p(n,0)=p(m+n,0)$: ordinary Cauchy additivity of $p$ restricted to states with vanishing credit coordinate. No tactics, lemmas, or sorry.
why it matters
This is the sharp 1D additivity premise in the Gap-5 momentum-additivity composition attack. It feeds balance_vanishing_of_net_imbalance_reading (net-imbalance reading plus this axis additivity imply balance-vanishing) and the sharper discharge energyEqualsCost_of_net_imbalance_reading_additive_unit (reading + 1D additivity + continuity + unit force $p=\pm$ imbalance, hence full consolidation additivity and EnergyEqualsCost, with no kinetic input).
It also appears in the packaged verdict MomentumAdditivityCompositionVerdict as the constructive corollary (c), and in the momentum bridge via scaledImbalance_additiveOnDebitAxis and ScaleFreeMomentumPackage. Relative to the module no-go (composition law does not select additivity), this predicate is the minimal Cauchy fragment that still closes EnergyEqualsCost once net-imbalance reading is assumed. Landmark context: RCL on $J$-cost is ambient and $p$-independent; the eight-tick and $D=3$ scaffolding sit upstream of the ledger chart but are not used in the definition itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.