canonical_seed_post_index_holds
plain-language theorem explainer
The canonical index for posting adjacent seed levels 0 and 1 is certified, at theorem level, to equal 2. Hierarchy-bridge constructions cite this certificate so the seed-posting operation need not carry a free index parameter. The proof is pure reflexivity on the definition of that index.
Claim. The natural number $2$ carries a seed-posting index certificate: it equals the canonical seed-posting index, which is defined to be $2$.
background
The Unified Forcing Chain derives T-1 through T8 as forced steps from the Recognition Composition Law together with normalization and calibration. In that setting, a local second-order hierarchy begins with seed levels 0 and 1; their first local closure is the next level.
The canonical seed-posting index is the natural number 2. A seed-posting index certificate for a proposed index is the proposition that the proposal equals this canonical value. Downstream hierarchy-bridge lemmas consume such a certificate to pin the seed-posting operation at level 2 instead of leaving an arbitrary parameter.
proof idea
One-line structure instance. The sole field of the certificate asks that the supplied index equal the canonical index; both sides are definitionally 2, so rfl closes it. No upstream lemmas are invoked beyond the definition of the canonical index.
why it matters
Supplies the seed_index field for the two constructors that build a seed-posting operation on a nontrivial multilevel composition: one from an explicit level-two size identity, and one from the canonical seed-size law. Those parents remove the free post-index from the hierarchy bridge by always using the canonical value 2. Within the forcing chain this is bookkeeping for the local closure of seed levels 0 and 1, a discrete-hierarchy step that later supports the self-similar fixed point (T6), the eight-tick octave (T7), and D = 3 (T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.