CanonicalSeedPostIndex
plain-language theorem explainer
Certificate that a proposed natural number is the canonical seed-posting index for adjacent hierarchy levels 0 and 1. Cited by anyone assembling the T5→T6 bridge or local second-order closure. It is a one-field Prop structure requiring equality with the fixed index 2.
Claim. A natural number $n$ is a canonical seed-posting index precisely when $n=2$. Here $2$ is the first local closure level of the seed pair $(0,1)$ in a second-order hierarchy: levels $0$ and $1$ post together and land at the next level.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. Within that chain, multilevel composition needs a local posting law for the lowest hierarchy seeds.
A local second-order hierarchy begins with seed levels $0$ and $1$. Their first local closure is the next level, written as the constant index $2$. The companion definition fixes that canonical seed-posting index to $2$; the present structure packages the claim that a proposed index equals that constant.
Several other "canonical" objects appear upstream (Peano arithmetic, dyadic real protocols, completed traces, self-similar dressings). They share the naming pattern of a preferred representative, but this certificate is specifically about hierarchy posting, not about those constructions.
proof idea
Definitional structure, not a proved theorem. It is a Prop-valued structure on a natural number post01 with a single field: equality of that number with the constant canonical seed-posting index (which is definitionally $2$). Inhabitation is immediate by reflexivity once the candidate is that constant; uniqueness of any inhabited certificate is discharged downstream by rewriting the field.
why it matters
This certificate is the index half of the canonical seed posting operation used on the T5→T6 bridge. Downstream, the posting operation isolates the exact local datum the hierarchy recurrence needs: level $0$ posted with level $1$ closes at level $2$, with posted size the sum of the two seed sizes, rather than a full all-pairs posting law.
Sibling theorems show the constant itself carries a certificate and that any certificate forces the index to equal $2$. In the forcing chain, T5 pins the unique cost $J$ and T6 forces $\varphi$ as the self-similar fixed point; the seed-posting index is the discrete bookkeeping step that lets the multilevel composition talk about that self-similarity at the lowest nontrivial level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.