AdditiveSeedPostingModel
plain-language theorem explainer
An additive seed-posting model packages three axioms: hierarchy level values equal sizes of chosen events, levels 0 and 1 post to the canonical seed level, and event size is additive under posting. Anyone proving the T5→T6 self-similarity bridge or the canonical seed-size law cites it as the lower-level ledger semantics. It is a pure structure definition (Prop bundle), not a proved theorem.
Claim. Fix a nontrivial multilevel composition $M$, a type of events, a level-to-event map $\ell$, a size map $s$, and a binary posting operation $\circ$. An additive seed-posting model asserts: (i) $M.{\rm levels}(k)=s(\ell(k))$ for every $k$; (ii) $\ell(2)=\ell(0)\circ\ell(1)$ (canonical seed index); (iii) $s(a\circ b)=s(a)+s(b)$ for all events $a,b$.
background
The Unified Forcing Chain module aims to force T0–T8 from the cost foundation (Recognition Composition Law plus normalization and calibration). The T5→T6 step needs self-similarity on a discrete ledger hierarchy; that requires a precise notion of how hierarchy levels arise by posting seed events and how level sizes add.
NontrivialMultilevelComposition supplies the hierarchy skeleton (level values and composition structure). Events are the primitive ledger postings; in related modules a recognition event is a directed source→target posting carrying a positive ratio. A CostFunction on a configuration space satisfies dichotomy (zero cost iff consistent) and independent additivity over joins of disjoint configurations. The recognition-work posting model later specializes size to such a cost and compose to configuration join, so additivity becomes a theorem rather than an extra axiom.
This structure is the lower-level interface: level sizes are read from event sizes, seeds 0 and 1 compose to the canonical seed level (index 2), and size is additive under posting.
proof idea
No proof body: this is a structure definition packing three propositional fields. Instantiation is by supplying level_size_eq, seed_event_composes, and size_additive. Downstream, additive_seed_posting_model_of_recognition_work builds an instance from a recognition-work posting model plus seed-event interpretation, using CostFunction additivity for the size field. Other consumers treat the three fields as hypotheses and rewrite.
why it matters
This interface is the ledger semantics under the T5→T6 self-similarity bridge. Downstream, canonical_seed_size_law_of_additive_posting_model shows these axioms force the canonical seed-size law; typed_seed_posting_of_additive_model lifts them (with a posting-potential control surface) to typed seed-posting semantics where level size is additive as an event-size observable and the potential carries the RCL/d'Alembert control law. The bridge certificate T5_To_T6_SelfSimilarity_Bridge records that bare closed-observable data do not force hierarchy fields such as additive posting, so this model is the explicit extra structure that makes φ-forcing honest rather than smuggled. In the primer chain, T5 is J-uniqueness and T6 is φ as the self-similar fixed point; additive seed posting is the discrete ledger step that turns uniqueness of J into a forced scale ratio φ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.