scaleClosureAtWithNonnegative_iff_ledgerCompose
plain-language theorem explainer
Under a recognition-work model on nonnegative costs, scale closure defined by an arbitrary nonnegative composition op is equivalent to ordinary ledgerCompose closure of a geometric scale sequence. Anyone proving the T5–T6 self-similarity bridge or specializing to the canonical additive work model cites this. The proof is a two-sided rewrite: extensivity of the model identifies the op on seed scales with ledgerCompose.
Claim. Fix a configuration space of events with cost $\kappa$, maps embedding nonnegative work into events, event composition, and a binary operation $\mathrm{op}$ on nonnegative reals, such that the data form a recognition-work nonnegative scale-composition model. For any geometric scale sequence $S$ and index $n\in\mathbb{N}$, $$\mathrm{op}(S_0,S_1)=S_n \quad\Longleftrightarrow\quad \mathrm{ledgerCompose}(S_0,S_1)=S_n.$$
background
The module UnifiedForcingChain aims to force the full T0–T8 chain from the Recognition Composition Law plus normalization and calibration. The T5–T6 step needs a bridge from unique $J$ to $\varphi$ via self-similarity on a discrete ledger of scales.
Nonnegative work is the subtype ${x:\mathbb{R}\mid x\ge 0}$, the actual range of recognition costs. A recognition-work nonnegative scale-composition model packages: every nonnegative work value is realized as the cost of some event; composition of those events represents a chosen binary operation $\mathrm{op}$ on nonnegative work. This replaces an impossible all-real model: costs are nonnegative and geometric scales are positive.
ScaleClosureAt says the ledger composition of the seed scales $S_0$ and $S_1$ equals $S_n$. ScaleClosureAtWithNonnegative is the same statement with $\mathrm{op}$ in place of ledgerCompose. Geometric scale sequences supply positive scales (as in the $\varphi^k$ ladder used cosmologically).
proof idea
Term-mode constructor proof of the biconditional.
Forward: assume closure under $\mathrm{op}$. Unfold both predicates. Apply nonnegative_work_extensive_of_recognition_work_model at the two seed scales $\langle S.scale,0,\ldots\rangle$ and $\langle S.scale,1,\ldots\rangle$ (positivity from S.scale_pos). That lemma rewrites $\mathrm{op}$ on those seeds to ledgerCompose, so the hypothesis is exactly ScaleClosureAt.
Reverse: symmetric. Unfold the nonnegative closure predicate, rewrite via the same extensivity identity, and discharge with the ledger closure hypothesis.
No induction or uniqueness of $J$ is used; only model extensivity at the two seeds.
why it matters
This is the abstract equivalence that lets scale-closure arguments move between the ledger language (additive ledgerCompose) and any realizable nonnegative work composition. Downstream, canonical_nonnegative_work_closure_iff_ledger specializes it to the canonical additive model and cost, giving the same closure predicate as ledgerCompose.
That specialization feeds the T5-to-T6 self-similarity bridge (t5_to_t6_bridge_holds), whose doc states the bridge is theorem-backed: uniqueness of $J$ plus realized closed-scale forcing of $\varphi$. In the forcing chain, T5 is $J$-uniqueness ($J(x)=(x+x^{-1})/2-1$) and T6 is $\varphi$ as the self-similar fixed point; closed geometric scales are the concrete self-similarity data.
Without this iff, nonnegative work models and ledgerCompose would be separate closure notions, blocking the realized-closed-scale route from T5 to T6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.