canonicalPhiScaleSequence_closed
plain-language theorem explainer
The canonical geometric scale sequence with ratio φ is closed under ledger composition. Hierarchy and first-closure results in the unified forcing chain cite this fact. The proof unfolds the closure predicate and finishes by simp with the identity φ² = φ + 1.
Claim. The canonical geometric scale sequence with common ratio $\varphi$ is closed under ledger composition: composing successive scales stays inside the sequence, using the self-similarity relation $\varphi^2 = \varphi + 1$.
background
The module UnifiedForcingChain assembles the complete inevitability chain T-1 through T8 from the cost foundation (Recognition Composition Law, normalization, calibration). T6 is the step that forces φ as the self-similar fixed point of the discrete ledger.
A geometric scale sequence is a φ-powered ladder of scales. Closure means ledger composition of scales remains on that ladder. The defining algebraic fact is the golden-ratio equation $\varphi^2 = \varphi + 1$, proved as phi_equation in PhiForcing / PhiRing: it equates two multiplicative steps with one step plus the unit scale.
canonicalPhiScaleSequence is the concrete instance of GeometricScaleSequence used as the default hierarchy of scales in the chain. Downstream, minimal hierarchies are exactly such sequences equipped with a proof of this closure.
proof idea
Term-mode proof by unfolding. Expand isClosed, then ledgerCompose and scale, so the goal is an equality among powers of φ. Invoke PhiForcing.phi_equation to obtain $\varphi^2 = \varphi + 1$. A single simp with the definition of the canonical sequence, that equation, and add_comm discharges the residual arithmetic.
why it matters
This is the algebraic seal on the canonical φ ladder inside the forcing chain. It is the minimalClosure field of canonicalMinimalHierarchy, the default minimal hierarchy (φ geometric sequence with first closure). It also feeds canonicalPhiScaleSequence_first_closure_law, which rephrases closure as existence of a first-closure index via the iff lemma canonical_first_closure_law_iff_isClosed.
In framework terms this sits at T6: φ forced by self-similarity on the discrete ledger. Without closure, the scale ladder would not be a minimal hierarchy, and later constant and mass constructions that ride the φ-ladder would lack their canonical scale object. The result is fully proved (no sorry).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.