RecognitionWorkScaleCompositionModel
plain-language theorem explainer
A Prop-structure that packages when a real binary operation on work values is realized by recognition events: each real is an event of that cost, event composition matches the real operation, composition is config-space join, and the events are independent. Downstream work-extensivity and the T5→T6 self-similarity bridge cite it. Pure definitional packaging; propositional uniqueness is immediate (Subsingleton by rfl).
Claim. Fix a type of events with a configuration-space structure and a recognition cost $\kappa$. Given a realization map $w:\mathbb{R}\to\mathrm{Event}$, an event composition $\circ$, and a real binary operation $\oplus$, the data form a recognition-work scale-composition model when: (i) $\kappa(w(a))=a$ for every real $a$; (ii) $w(a\oplus b)=w(a)\circ w(b)$; (iii) $w(a)\circ w(b)$ equals the configuration-space join of $w(a)$ and $w(b)$; (iv) $w(a)$ and $w(b)$ are independent for all $a,b$. Under those hypotheses, cost additivity forces $\oplus$ to be ordinary addition.
background
The ambient module is the Unified Forcing Chain: T-1 through T8 are derived as inevitabilities from the cost foundation (Recognition Composition Law, normalization $F(1)=0$, calibration $F''(1)=1$). T5 pins the unique cost $J(x)=(x+x^{-1})/2-1$; T6 forces $\varphi$ as the self-similar fixed point of the discrete ledger.
CostFromDistinction supplies the local primitives: a configuration space of events with a join operation and an independence predicate, plus a nonnegative cost function $\kappa$ that is additive on independent joins. The structure here is the interface that says a real scale-composition law is faithfully represented inside that event algebra: each real work value is the cost of some event, and composing those events realizes the real operation via join.
Upstream cosmology helpers (scale, rung-coarsen Event/cost) illustrate the same work-on-events pattern at large scales, but the structure itself is foundation-level and does not depend on $\varphi$-ladder numerics.
proof idea
Definitional, not a proved theorem. The structure is a bundled Prop with four fields (cost realization, composition representation, join identification, independence). No construction or existence proof is given here.
A companion Subsingleton instance records propositional uniqueness for fixed parameters: any two inhabitants are equal by rfl, because a structure of pure propositions has at most one proof. Downstream theorems (work-extensivity, impossibility of a global all-real model) unpack the fields and apply CostFunction additivity / nonnegativity.
why it matters
This is the interface lemma-bundle for the scale-composition half of the T5→T6 bridge. Once a model exists, work_extensive_of_recognition_work_scale_model concludes that the real operation must be addition (work-extensivity). canonical_scale_composition_of_recognition_work then names that forced operation as the canonical scale composition. Separately, no_global_recognition_work_scale_composition_model shows no such model can cover all of $\mathbb{R}$, because costs are nonnegative—so the representation is local/partial, not a global embedding of every real work value.
In the forcing chain this matters for self-similarity: T6 needs a realized hierarchy whose scale ratio is forced to $\varphi$. The bridge certificate T5_To_T6_SelfSimilarity_Bridge routes through hierarchy dynamics that presuppose additive posting of recognition work; this structure is the precise hypothesis package that makes “additive posting” a theorem rather than an extra axiom. It does not itself force $\varphi$; it forces the arithmetic shape of work composition that the $\varphi$ step consumes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.