kinetic_root_mem_four
plain-language theorem explainer
Any continuous momentum observable whose square equals the squared ledger imbalance must be one of four functions: imbalance, its negative, its absolute value, or the negative absolute value. Gravity and ledger-chart authors cite this as the exhaustive continuous kinetic class on the two-coordinate ledger plane. The proof reads half-plane signs from the classification lemma, then matches each of the four unit sign patterns to one named function by case analysis.
Claim. Let $p:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ be continuous and satisfy $p(z)^2=(\mathrm{imbalance}\,z)^2$ for every ledger state $z$. Then $p$ equals one of $\mathrm{imbalance}$, $-\mathrm{imbalance}$, $|\mathrm{imbalance}|$, or $-|\mathrm{imbalance}|$.
background
Track B step B1 studies momentum additivity under ledger consolidation on the chart carrier $\mathrm{LedgerState}:=\mathbb{R}\times\mathbb{R}$. The kinetic condition is the global modeling premise $p(z)^2=(\mathrm{imbalance},z)^2$: the observable's square matches the squared net debit-credit imbalance. Continuity is a separate regularity premise.
On orbits the kinetic identity is forced by exactness of the recognition cost composed with an energy-equals-cost identification; as a statewise identity it remains named, not derived. The module's central claim is that, inside the continuous kinetic class, additivity under consolidation is equivalent to swap-oddness (oddness under debit-credit exchange).
The sibling classification lemma already pins half-plane behaviour: on the positive-imbalance cone $p$ is a fixed unit times imbalance, on the negative cone another unit times imbalance, and $p$ vanishes on balanced states. The present theorem turns those half-plane data into a global four-way exhaustive list.
proof idea
Invoke kinetic_root_classification to obtain the two unit-square evaluations $p(1,0)^2=1$ and $p(0,1)^2=1$, the positive- and negative-cone formulae, and vanishing on balanced states. From the squares, each of $p(1,0)$ and $p(0,1)$ is $\pm 1$.
Build a single piecewise key identity: for every $z$, $p(z)$ equals $p(1,0)\cdot\mathrm{imbalance},z$ when imbalance is nonnegative and $-p(0,1)\cdot\mathrm{imbalance},z$ otherwise, by trichotomy plus the classification clauses.
Case-split on the four sign pairs $(p(1,0),p(0,1))\in{\pm 1}^2$. Each pair, substituted into the key identity and simplified with absolute-value identities on the two half-planes, yields exactly one of the four named functions via funext.
why it matters
This is the formal exhaustiveness advertised for the continuous kinetic class: only four observables survive. The two signed members are the additive (swap-odd) branch; the two unsigned members are the swap-even branch. Downstream, momentumAdditivityVerdict packages the arc: additivity follows from kinetic plus continuous plus swap-odd, and the momentum is then the imbalance coordinate itself.
The module is a conditional closure of B1, not a derivation of the chart. A hostile referee accepted the kernel mathematics while noting that the kinetic premise is already the magnitude half of the chart conclusion, so what is truly derived is the parity equivalence. The magnitude bridge and the energy-equals-cost identification remain named hypotheses.
In the broader Recognition gravity track this pins why extensivity is a substrate parity (signed charge under debit-credit exchange) rather than a free regularity or functional-equation assumption, answering the chart module's open question on additivity without smuggling in linearity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.