cubeDiff_continuous
plain-language theorem explainer
The cube-difference map on ledger states, sending a pair to the difference of cubes of its two components, is continuous as a real-valued function. Gravity and ledger-posting arguments cite this when assembling the concrete witness that column incidence plus swap-oddness still leave a free 1D Cauchy gap. The proof is a one-line term built from continuity of the projections, cubing, and subtraction.
Claim. The map $z \mapsto z_1^3 - z_2^3$ from ledger states $\mathbb{R}^2$ to $\mathbb{R}$ is continuous.
background
In the Gap5 net-imbalance module, the consumer package needs ReadsNetImbalance (P1) and AdditiveOnDebitAxis (P2); with continuity and unit normalization these force full consolidation additivity and EnergyEqualsCost. Column posting incidence (momentum equals pure-debit plus pure-credit contributions) is a named posting-level hypothesis, not derived from RCL. Under incidence and debit-credit parity (swap-oddness), P1 and P2 become equivalent, collapsing the frontier to a single 1D Cauchy obligation on the debit axis.
The cube-difference observable is defined by $z \mapsto z_1^3 - z_2^3$. It is column-separable and swap-odd, yet not a function of net imbalance alone. The module uses it as a concrete package witness on the stated LedgerState carrier: continuous, swap-odd, balance-vanishing, unit-normalized, and column-incident, while failing both P1 and P2.
proof idea
Term-mode composition of standard continuity facts. The first and second projections are continuous; cubing is continuous on $\mathbb{R}$; their difference is continuous. Explicitly: continuous first-projection raised to the third power, minus continuous second-projection raised to the third power. No Recognition-specific lemmas are required beyond the definition of the cube-difference map.
why it matters
This continuity fact is a required conjunct in the no-go theorem posting_incidence_does_not_force_debit_axis_additivity. That theorem states that on the stated LedgerState carrier there exists a continuous, swap-odd, balance-vanishing, unit-normalized, column-incident momentum (namely cube-difference) that fails both ReadsNetImbalance and AdditiveOnDebitAxis. Hence column posting incidence plus debit-credit parity plus the three consumer companions cannot force the remaining 1D Cauchy input.
In the broader SevenGaps gravity program this keeps Flags 6 and 12 resting on EnergyEqualsCost with the named remaining input still being 1D debit-axis additivity under incidence and swap-oddness. Deriving incidence itself from deeper substrate structure remains open. The result is a package witness on a concrete carrier, not a class theorem over all observables.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.