TypedSeedPostingSemantics
plain-language theorem explainer
Typed seed-posting semantics is a Prop-structure that keeps two hierarchy observables rigorously separate: additive level size (equal to the multilevel composition's level sequence) and a posting-potential control surface given by the shifted J-cost of powers of a positive seed scale σ. Seed-step additivity is required only on level size; the potential must obey the RCL/d'Alembert identity. Anyone proving the canonical seed-size law or the T5→T6 self-similarity bridge cites this interface. It is a definitional package, not a theorem.
Claim. Given a nontrivial multilevel composition $M$, maps $L,P_{\mathrm{obs}}:\mathbb{N}\to\mathbb{R}$, and $\sigma\in\mathbb{R}$, typed seed-posting semantics holds when: $L(k)$ equals the hierarchy level sequence of $M$ for every $k$; $P_{\mathrm{obs}}(k)$ equals the posting potential (shifted $J$-cost) of $\sigma^k$; $\sigma>0$; level size is additive at the canonical seed index, $L(n_{\mathrm{seed}})=L(0)+L(1)$; and the posting potential $P$ satisfies $P(xy)+P(x/y)=2P(x)P(y)$ for all $x,y>0$.
background
The Unified Forcing Chain module aims to force the full T0–T8 ladder from the cost foundation (Recognition Composition Law, normalization, calibration). The T5→T6 step needs a discrete hierarchy whose scale ratio is self-similar; that step is easy to mis-state if one treats the J-cost surface as if it were additive at the seed step.
Posting potential is the shifted J-cost control quantity used so that the RCL takes the pure d'Alembert product form $P(xy)+P(x/y)=2P(x)P(y)$, rather than the expanded form with linear terms in $J$. Level size is a separate additive observable read from the hierarchy's level sequence (or from event sizes in a lower ledger model). The seed scale $\sigma>0$ indexes the geometric ladder $\sigma^k$ on which the potential is evaluated.
Upstream ledger and coarsening language supplies the event picture: recognition events carry positive ratios, and total cost is a weighted sum of those ratios. The structure here does not rebuild that ledger; it only records the two surfaces a hierarchy must expose for seed-posting arguments.
proof idea
No proof body: this is a structure (Prop bundle). The five fields are the entire content. Equality fields pin $L$ to $M$'s levels and $P_{\mathrm{obs}}$ to posting potential of $\sigma^k$. Positivity of $\sigma$ is a plain inequality. Seed additivity is a single numeric identity on $L$ at the canonical seed index. The RCL field is a universal quantification over positive reals for the posting-potential function, not for $L$. Downstream constructors (additive event models, seed-closed hierarchies, seed recognition-work) inhabit the structure by discharging these five obligations.
why it matters
This interface exists to block a false shortcut on the T5→T6 path. The doc-comment states the point bluntly: the tempting identity that posting potential itself is additive at $\sigma^2$ versus $\sigma^0$ and $\sigma^1$ is false; conflating the two surfaces would smuggle a wrong algebraic step into φ-forcing.
Downstream, canonical_seed_size_law_of_typed_seed_posting derives the canonical seed-size law from the additive $L$ surface alone while leaving the potential as pure RCL control. Constructors from additive posting models, seed-closed multilevel compositions, and seed recognition-work supply concrete inhabitants. The T5→T6 self-similarity bridge certificate routes through hierarchy dynamics that need exactly this typed separation (ratio self-similarity plus additive posting) rather than bare closed-observable fields.
In the primer landmarks, this sits between T5 (unique $J$ from d'Alembert plus normalization/calibration) and T6 (φ as the self-similar fixed point of the discrete ledger). It does not itself force φ; it is the typed contract those forcing theorems consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.