ScaleClosureAtWithNonnegative
plain-language theorem explainer
Predicate asserting that a nonnegative-work binary operation, applied to the base and first scales of a geometric scale sequence, recovers the n-th scale as a real. Cited by the T5→T6 self-similarity bridge and by the ledger-compose equivalence lemmas. Pure definitional packaging: subtype-wrap the positive scales, apply op, project, and equate.
Claim. Fix a binary operation $\mathrm{op}$ on nonnegative reals and a geometric scale sequence $S$ (ratio $r>0$, $r\neq 1$) with positive scales $S_k$. Closure at index $n$ holds when $\mathrm{op}(S_0,S_1)=S_n$ as real numbers (after forgetting the nonnegativity witness).
background
The module builds the complete inevitability chain T-1 through T8 from the Recognition Composition Law plus normalization and calibration. T5 pins the unique cost $J$; T6 forces $\varphi$ as the self-similar scale ratio in a discrete ledger.
NonnegativeWork is the subtype ${x:\mathbb{R}\mid x\ge 0}$, the actual range of recognition costs. Geometric scale sequences carry a positive nontrivial ratio and a scale map; positivity of each scale is recorded so the values inject into nonnegative work. The classical ledger composition on bare reals is ordinary addition.
This predicate is the domain-correct stand-in for scale closure: costs are nonnegative and geometric scales are positive, so composition must live on nonnegative work rather than on all of $\mathbb{R}$.
proof idea
Definitional, not a proved theorem. The body subtype-wraps $S.{\rm scale},0$ and $S.{\rm scale},1$ using the positivity lemmas, feeds them to the supplied operation $\mathrm{op}:{\rm NonnegativeWork}\to{\rm NonnegativeWork}\to{\rm NonnegativeWork}$, projects the result to its underlying real, and asserts equality with $S.{\rm scale},n$. No tactics or lemmas beyond le_of_lt for the subtype witnesses.
why it matters
Sits on the T5→T6 bridge path that forces $\varphi$ as the self-similar fixed point of the discrete ledger (primer landmark T6). Downstream, scaleClosureAtWithNonnegative_iff_ledgerCompose shows any recognition-work nonnegative composition model yields the same closure predicate as additive ledger composition; canonical_nonnegative_work_closure_iff_ledger specializes that to the canonical model. The bridge certificate T5_To_T6_SelfSimilarity_Bridge routes hierarchy dynamics through this nonnegative packaging so no all-real composition fantasy is smuggled into the chain. Without it, scale closure would be stated on the wrong domain relative to cost values.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.