cubeDiff_unit
plain-language theorem explainer
The cube-difference observable is unit-normalized on the pure-debit ledger state (1,0): its square equals 1. The incidence no-go cites this fact as the unit companion in the counterexample package. Proof is a one-line numerical unfolding of the definition.
Claim. Let the cube-difference observable on ledger states be $z \mapsto z_1^3 - z_2^3$. Then $\bigl(1^3 - 0^3\bigr)^2 = 1$, i.e. the observable is unit-normalized at the pure-debit state $(1,0)$.
background
This module works at the posting-incidence layer of the ledger: a state's momentum is the sum of pure-debit and pure-credit column contributions. That incidence structure is named, not derived from RCL or $\sigma=0$. Under incidence plus debit-credit parity (swap-oddness), the two consumer properties ReadsNetImbalance and AdditiveOnDebitAxis become equivalent, collapsing the frontier to a single 1D Cauchy obligation on the debit axis.
The cube-difference map $z \mapsto z_1^3 - z_2^3$ is the concrete witness used against overclaiming. Its doc-comment records it as column-separable and swap-odd, yet not a function of net imbalance alone. Unit normalization at $(1,0)$ is one of the five companion properties the no-go packages with continuity, balance-vanishing, swap-oddness, and incidence.
proof idea
One-line wrapper: unfold the definition of the cube-difference observable and discharge $1^3 - 0^3 = 1$ (hence squared equals 1) by norm_num. No lemmas beyond the definition are required.
why it matters
Feeds the headline no-go posting_incidence_does_not_force_debit_axis_additivity, which packages cube-difference as a continuous, swap-odd, balance-vanishing, unit-normalized, column-incident momentum that still fails both ReadsNetImbalance and AdditiveOnDebitAxis. That no-go is the module's supporting landed result (b): incidence plus parity plus the three consumer companions cannot force the remaining 1D Cauchy input on the stated LedgerState carrier.
In the broader SevenGaps gravity attack, Flags 6 and 12 still rest on EnergyEqualsCost; the open named input remains 1D debit-axis additivity under incidence. This unit fact is bookkeeping inside the witness package, not a selection principle. Deriving column incidence from deeper substrate structure stays OPEN.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.