SeedRecognitionWorkPostingModel
plain-language theorem explainer
A Prop-structure packaging the minimal seed-pair data needed for the T5→T6 bridge: hierarchy levels equal recognition-work costs, levels 0 and 1 compose by configuration-space join to the canonical seed event, and that pair is independent. Anyone citing the seed size law or the self-similarity bridge uses this interface. It is a pure definitional bundle of four fields, not a proved theorem.
Claim. A seed recognition-work posting model for a nontrivial multilevel composition $M$, an event type with configuration-space structure, a cost $\kappa$, a level map $k \mapsto e_k$, and a binary compose operation, is the conjunction of: (i) $M.{\rm levels}(k) = \kappa.C(e_k)$ for all $k$; (ii) $e_{\rm seed} = {\rm compose}(e_0,e_1)$; (iii) ${\rm compose}(e_0,e_1)$ equals the configuration-space join of $e_0$ and $e_1$; (iv) $e_0$ and $e_1$ are independent in the configuration space.
background
The Unified Forcing Chain module aims to force every landmark T-1 through T8 from the Recognition Composition Law plus normalization and calibration. T5 pins the unique cost $J(x)=(x+x^{-1})/2-1$; T6 forces $\varphi$ as the self-similar fixed point of a discrete ledger hierarchy.
Between those steps one needs a concrete posting semantics: hierarchy level sizes must be recognition-work costs of events, and composing the two seed levels must be an independent join so that cost additivity applies. ConfigSpace supplies a join and an independence predicate; a CostFunction assigns the work $\kappa.C$. The full all-pairs independence package is stronger than the bridge needs, so this structure isolates only the seed pair $(e_0,e_1)$.
Upstream, support-event models and support-disjointness certificates supply concrete instances where independence follows from disjoint atom supports, because abstract configuration spaces do not expose supports by themselves.
proof idea
No proof body: this is a structure (definitional Prop bundle). The four fields are the exact hypotheses later theorems discharge. Downstream constructors such as seed_recognition_work_model_of_support and canonical_seed_recognition_work_model_of_support_events build inhabitants by setting level sizes to support costs, identifying compose with join, and deriving seed independence from a support-disjointness certificate rather than from level separation alone.
why it matters
This is the minimal interface the T5→T6 self-similarity bridge actually consumes. Downstream, canonical_seed_size_law_of_seed_recognition_work turns an inhabitant into the seed size law; typed_seed_posting_of_seed_recognition_work upgrades it to typed seed-posting semantics; and T5_To_T6_SelfSimilarity_Bridge routes through hierarchy dynamics that need additive seed posting to force the scale ratio $\varphi$ (primer landmark T6).
By requiring only seed-pair independence rather than all-pairs independence, the chain avoids smuggling a stronger hypothesis into the forcing argument. The parent bridge structure explicitly records that bare closed-observable data do not force hierarchy fields, so this model is the honest place where posting and additivity enter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.