canonical_admissible_orbit_normal_form_reflection
plain-language theorem explainer
Any closed observable framework that admits an orbit with growth and ratio self-similarity carries a full φ-uniform normal-form certificate on that orbit. Citers of the T5→T6 self-similarity bridge and the closed-scale admissible-orbit bridges use this packing. The proof is a pure structure assembly: each certificate field is discharged by a named canonical lemma on the admissible orbit.
Claim. Let $F$ be a closed observable framework and $b\in F.S$ a base state. If the orbit of $b$ under $F.T$ is admissible (first step grows, adjacent ratios are self-similar, and the remaining seed/posting data hold), then that orbit supplies the full normal-form reflection: canonical uniform scaling, growth orientation, seed closure, base ratio equal to $\varphi$, level equivalence with the $\varphi$-uniform ladder, and realized-hierarchy normal-form equivalence.
background
The module UnifiedForcingChain aims to force the entire T0–T8 chain from the Recognition Composition Law plus normalization and calibration. The local step here sits between T5 (unique cost $J$) and T6 ($\varphi$ as the self-similar fixed point): one must turn bare closed dynamics into a $\varphi$-uniform discrete ladder.
A closed observable framework supplies a state space $S$, a step map $T$, and a positive ratio observable $r$, with nontriviality and no external input. An admissible-orbit reflection on a base $b$ is the missing exact data: the first orbit step grows ($r(Tb)/r(b)>1$), adjacent orbit ratios are constant (self-similar), and seed posting closes. The normal-form reflection is the stronger certificate that this orbit realizes the canonical uniform scale law, growth orientation, seed size, base ratio $\varphi$, and equivalence of levels with the $\varphi$-uniform hierarchy.
Upstream, admissibleOrbit_canonical_base_ratio_phi already pins the canonical base ratio to $\varphi$ once uniformity and seed hold; the multilevel composition of the admissible orbit is the carrier on which those canonical predicates are stated.
proof idea
Term-mode structure construction, not a tactic script. Each field of the normal-form reflection is filled by a dedicated lemma on the same admissible orbit:
- uniform from
admissibleOrbit_canonical_uniform; - growth from
admissibleOrbit_canonical_growth; - seed from
admissibleOrbit_canonical_seed_size; - base_ratio from
admissibleOrbit_canonical_base_ratio_phi(which reduces to the uniform-seed base-ratio identity equaling $\varphi$); - level_equiv from
admissibleOrbit_levels_eq_phiUniform; - realized_equivalence by applying
canonical_realized_hierarchy_normal_form_equivalenceto the realized hierarchy obtained from the admissible orbit viaadmissibleOrbitToRealizedHierarchy.
No new arithmetic is done here; the theorem is the packing of those six results into one certificate.
why it matters
This certificate is the reusable normal-form handle for admissible orbits inside the complete inevitability chain. Downstream it feeds canonical_realized_closed_scale_admissible_orbit_bridge (closed-scale models supply admissible-orbit reflection fields directly), canonical_minimal_closed_scale_orbit_bridge (minimal closed-scale orbit data enter the $\varphi$-uniform route), and ultimately t5_to_t6_bridge_holds, whose doc states that the T5-to-T6 self-similarity bridge is theorem-backed.
In primer terms this is the T5→T6 joint: once $J$ is unique, self-similarity on a discrete closed ledger forces $\varphi$ as the base ratio of the admissible orbit. Without this packing, later bridges would reassemble the same six fields ad hoc. It does not itself prove T6 from T5; it standardizes the orbit data those bridges consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.