canonical_nonnegative_work_closure_iff_ledger
plain-language theorem explainer
For any geometric scale sequence and index n, closure under canonical nonnegative-work addition is equivalent to closure under ledger composition. Anyone proving the T5-to-T6 self-similarity bridge cites this to swap work-addition language for ledger language without changing the predicate. The proof is a one-line specialization of the general nonnegative-work/ledger equivalence to the canonical cost and addition model.
Claim. Let $S$ be a geometric scale sequence with positive ratio $r \neq 1$, and let $n \in \mathbb{N}$. Writing $s_k$ for the $k$-th scale of $S$, the equality $s_0 + s_1 = s_n$ in the canonical nonnegative-work monoid holds if and only if $\mathrm{ledgerCompose}(s_0,s_1) = s_n$.
background
The module UnifiedForcingChain derives the full T0-T8 forcing chain from the Recognition Composition Law plus normalization and calibration. Near T5-T6 one needs a precise notion of when two seed scales close at a later rung of a geometric scale sequence.
A GeometricScaleSequence is a sequence of positive real scales with fixed ratio $r > 0$, $r \neq 1$. Ordinary scale closure at index $n$ asserts that ledger composition of the first two scales recovers the $n$-th scale. The nonnegative-work variant replaces ledger composition by an arbitrary binary operation on nonnegative work values (here canonical addition: the sum of the underlying reals, which stays nonnegative).
Canonical nonnegative-work cost is the identity cost $C(a) = a$ on those values. Upstream, the theorem that this cost, the identity embedding, and addition form a recognition-work nonnegative scale-composition model supplies the algebraic hypotheses needed to identify the two closure predicates.
proof idea
One-line term proof. Apply the general equivalence scaleClosureAtWithNonnegative_iff_ledgerCompose to the canonical nonnegative-work cost function and to the already-proved fact that this cost, together with identity and nonnegative-work addition, is a recognition-work nonnegative scale-composition model. Instantiating at the given geometric scale sequence $S$ and index $n$ yields the biconditional directly.
why it matters
This lemma is a bookkeeping bridge inside the T5-to-T6 step of the unified forcing chain. Downstream, t5_to_t6_bridge_holds packages the self-similarity bridge from unique $J$ (T5) to forced $\varphi$ (T6); one of its clauses equates realized closed-scale normal forms, and that argument needs the work-addition and ledger-compose closure predicates to be interchangeable.
In the primer landmarks, T5 pins $J(x) = (x+x^{-1})/2 - 1$ and T6 forces $\varphi$ as the self-similar fixed point of the discrete ledger. Identifying the two closure languages lets the hierarchy-dynamics arguments speak in either cost/work or ledger coordinates without introducing a second notion of closed scale. No open scaffold remains: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.