cubeDiff
plain-language theorem explainer
Cube-difference sends a ledger state (debit, credit) to debit cubed minus credit cubed. It is the continuous, swap-odd, column-incident witness that posting incidence does not force net-imbalance reading or debit-axis additivity. Downstream no-go lemmas cite it to keep the 1D Cauchy obligation on the debit axis as a separate named input toward EnergyEqualsCost.
Claim. For a ledger state $z=(d,c)\in\mathbb{R}^2$, define the cube-difference observable by $\mathrm{cubeDiff}(z):=d^3-c^3$.
background
This module works in the Gap-5 net-imbalance package for gravity. A ledger state is a pair of real columns (debit, credit). The consumer upstream wants two properties on an observable $F$: reading net imbalance alone (P1) and additivity on the pure-debit axis (P2). With continuity and unit normalization those force consolidation additivity and EnergyEqualsCost.
Column posting incidence is the named hypothesis that $F(d,c)=F(d,0)+F(0,c)$: momentum is the sum of pure-debit and pure-credit postings. Swap-oddness is debit-credit parity, $F(c,d)=-F(d,c)$. Under incidence plus swap-oddness, P1 and P2 become equivalent, collapsing the frontier to a single 1D Cauchy problem on the debit axis.
The module doc states the verdict up front: incidence does not by itself force that Cauchy obligation. Cube-difference is the concrete package witness on the stated LedgerState carrier.
proof idea
Pure definition: evaluate the first component cubed minus the second component cubed. No lemmas, no tactics.
why it matters
Cube-difference is the explicit counterexample that pins the module verdict. Downstream theorems record that it is continuous, swap-odd, balance-vanishing, unit-normalizable, and posting-incident, yet fails both ReadsNetImbalance and AdditiveOnDebitAxis (e.g. at (1,0)+(1,0) vs (2,0), and at (2,1)).
Those no-gos feed NetImbalanceDerivationVerdict: incidence plus parity collapses P1 with P2 but does not discharge the remaining 1D debit-axis additivity. Flags 6 and 12 still rest on EnergyEqualsCost; deriving posting incidence from deeper substrate (RCL or symplectic structure) remains open. Scope note in the module: this is a carrier witness, not a class theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.