RecognitionWorkNonnegativeScaleCompositionModel
plain-language theorem explainer
A Prop-structure packaging when nonnegative recognition work embeds into a configuration space so that work values match costs, binary work composition is realized by event join, and the joined events are independent. Anyone proving scale-closure or the T5→T6 self-similarity bridge cites it as the admissible domain (nonnegative costs, positive scales). It is a definitional interface; uniqueness is immediate by Subsingleton.
Claim. Fix a configuration space of events with cost function $\kappa$, a map from nonnegative work values $a\ge 0$ to events, a binary event operation, and a binary operation $\oplus$ on nonnegative work. The data form a recognition-work nonnegative scale-composition model when: (i) $\kappa$ of the event for $a$ equals $a$; (ii) the event for $a\oplus b$ equals the composite of the events for $a$ and $b$; (iii) that composite is the configuration-space join; (iv) the two events are independent. Any two such models on the same data are propositionally equal.
background
In the Unified Forcing Chain, T0–T8 are forced from the Recognition Composition Law plus normalization and calibration. Scale closure and the T5→T6 bridge need a composition law on geometric scales, but raw real-valued “work” is the wrong domain: recognition costs are nonnegative and geometric scales are positive.
Nonnegative work is the subtype ${x\in\mathbb{R}: x\ge 0}$. A configuration space supplies empty config, binary join, consistency, and an independence relation (no shared predicates); join is a commutative monoid. A cost function $\kappa$ assigns a real cost to each configuration. The structure ties a work-to-event embedding, an event composite, and a work-level operation so that costs, joins, and independence line up.
Upstream, Cosmology uses $\mathrm{scale}(k)=\varphi^k$ and recognition events carrying positive ratios; total cost is a weighted sum of doubled $J$-costs. This model is the foundation-side interface those scale facts must satisfy when routed through CostFromDistinction.
proof idea
Definitional structure: four fields, no proof obligations beyond inhabiting the Prop. The companion Subsingleton instance is a one-line rfl on allEq, so any two proofs of the structure on fixed parameters are definitionally equal as propositions. Downstream theorems (extensivity, uniqueness of the work operation, scale-closure equivalence) unpack the four fields and apply cost additivity on independent joins; they are not part of this declaration.
why it matters
This is the realizable replacement for an impossible all-real work model, and the domain the scale-closure bridge actually needs. Downstream: canonical_nonnegative_work_scale_composition_model exhibits a canonical inhabitant; nonnegative_work_extensive_of_recognition_work_model shows recognition-work additivity forces the work operation to be addition on values; nonnegative_work_composition_unique uniqueness of that operation; scaleClosureAtWithNonnegative_iff_ledgerCompose equates the nonnegative composition model’s scale-closure predicate with ledger composition.
It feeds T5_To_T6_SelfSimilarity_Bridge, which routes T5 $J$-uniqueness into self-similarity forcing $\varphi$ (primer T5–T6) via realized hierarchy dynamics rather than bare closed-observable fields. Without a nonnegative work model, the scale-closure half of that bridge has no admissible carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.