RecognitionWorkPostingModel
plain-language theorem explainer
A recognition-work posting model packages two axioms on a configuration space of events: posting is the ConfigSpace join, and every pair of events is Independent. Anyone proving size additivity for recognition costs, or building the T5→T6 self-similarity bridge, cites this interface. It is a pure Prop structure (definitional packaging), not a proved theorem.
Claim. A recognition-work posting model on a type of events $E$ equipped with a configuration-space structure, a cost function $\kappa$, and a binary operation $\mathrm{compose}: E\times E\to E$ is the conjunction of: (i) $\mathrm{compose}(a,b)$ equals the configuration-space join of $a$ and $b$ for all $a,b\in E$; (ii) every pair $a,b$ is independent in the configuration-space sense. Event sizes are the recognition-work costs $\kappa.C$; additivity of size under posting is then a consequence of the cost-function additivity axiom, not an extra hypothesis.
background
The module UnifiedForcingChain aims at a complete inevitability chain T-1 through T8 from the cost foundation (Recognition Composition Law, normalization, calibration). Mid-chain, T5 forces the unique J-cost $J(x)=(x+x^{-1})/2-1$; T6 forces $\varphi$ as the self-similar fixed point of a discrete ledger hierarchy. Bridging those steps needs a clean notion of additive posting of recognition work.
Upstream, CostFromDistinction supplies a configuration space on events with a join operation and an Independence predicate, plus a CostFunction whose additivity axiom says independent joins have additive cost. Cosmology-side Event types (directed postings carrying a positive ratio) and total recognition cost under a ratio weight illustrate the intended semantics: posting combines events, and cost is summed work.
This structure freezes exactly those two geometric hypotheses (compose = join; universal independence) so that size additivity becomes a derived theorem rather than a free parameter in the hierarchy dynamics.
proof idea
No proof body: the declaration is a Prop-valued structure (definitional interface). Its two fields are the hypotheses later consumers discharge or assume. Downstream, recognition_work_posting_size_additive is the one-line consequence: under the model, $\kappa.C(\mathrm{compose},a,b)=\kappa.C,a+\kappa.C,b$ by rewriting compose to join and applying CostFunction additivity on Independent pairs. The structure itself only packages those assumptions.
why it matters
In the forcing chain, T6 ($\varphi$ forced by self-similarity in a discrete ledger) needs additive posting of hierarchical seed events. This model is the recognition-work side of that interface: it feeds recognition_work_posting_size_additive and additive_seed_posting_model_of_recognition_work, which build the additive seed posting model used by hierarchy dynamics. The T5→T6 bridge certificate explicitly records that bare closed-observable data do not force hierarchy fields such as additive posting; this structure is the named place where that additive-posting obligation is stated without smuggling it into T5 J-uniqueness. It therefore keeps the Complete Inevitability Chain honest at the T5–T6 seam while tying event size to recognition-work cost rather than an ad hoc measure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.