abs_imbalance_continuous
plain-language theorem explainer
Absolute net imbalance of a ledger state is continuous as a real-valued map on the chart. Authors of the Gap5 momentum packages cite it when assembling the non-additive absolute-imbalance observable beside the additive imbalance. The proof is a one-line term: continuous projections, their difference, then absolute value.
Claim. The map sending a ledger state $z=(x,y)$ to $|x-y|$ is continuous as a function from the ledger-state chart into $\mathbb{R}$.
background
On the Gap5 ledger chart a state is a real pair. Net imbalance is the plain difference of the two coordinates; no cost functional enters the definition. Absolute imbalance is the ordinary absolute value of that difference.
This module asks whether the recognition composition law forces unconditional momentum additivity. Ambient cost is $J$-cost, known to satisfy the composition law independently of any momentum observable $p$. The same carrier admits two continuous, balance-vanishing, unit-normalized candidates: plain imbalance (additive under consolidation) and absolute imbalance (not additive). Continuity is one of the companion hypotheses still required by the consumer that derives EnergyEqualsCost from additivity plus those companions.
proof idea
Pure term proof on Mathlib's Continuous API. First and second projections on the product are continuous; their difference is continuous, so imbalance is continuous; absolute value on $\mathbb{R}$ is continuous. The chain is written (continuous_fst.sub continuous_snd).abs.
why it matters
Supplies the continuity conjunct of the absolute-imbalance package, which asserts continuity, balance-vanishing, unit normalization at $(1,0)$, and failure of additivity under consolidation. Paired with the additive imbalance package on the same carrier and the same RCL cost, that package is the constructive half of the module's no-go: composition law plus continuity, balance-vanishing, and unit normalization do not select additivity. The consumer energyEqualsCost_of_additive_continuous_balanced_unit therefore still needs additivity as an independent premise; B1's kinetic-conditional additivity is not smuggled in.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.