canonicalPhiScaleSequence
plain-language theorem explainer
Packages the golden ratio φ as the ratio of a geometric scale sequence (positive, not 1). Anyone citing the canonical minimal hierarchy or first-closure law for φ-scales uses this object. The body is a structure instance: ratio is φ, positivity and nontriviality come from the standard φ lemmas.
Claim. The canonical geometric scale sequence is the geometric scale sequence whose common ratio is $\varphi$ (the unique positive solution of $x^2 = x + 1$), with $0 < \varphi$ and $\varphi \neq 1$.
background
The Unified Forcing Chain module argues that T0–T8 are forced from the Recognition Composition Law plus normalization and calibration. T6 is the step that pins $\varphi$ as the self-similar fixed point of the discrete ledger.
Upstream, GeometricScaleSequence is the structure of a geometric scale sequence: a real ratio $r > 0$ with $r \neq 1$ (nontrivial scaling), together with the $n$-th scale $r^n$. Elsewhere in RS, discrete scales often appear as $\varphi^k$ (e.g. cosmological scale ladders).
This definition simply names the canonical choice of that structure: ratio equal to the forced constant $\varphi$ from PhiForcing. It is the scale object later fed into minimal-hierarchy and first-closure statements.
proof idea
Definitional structure instance, not a proof. The ratio field is set to $\varphi$. Positivity is discharged by PhiForcing.phi_pos. Nontriviality ($\varphi \neq 1$) is ne_of_gt applied to PhiForcing.phi_gt_one. No further algebraic work occurs here.
why it matters
This is the named $\varphi$-scale object for the T6 segment of the forcing chain. Downstream, canonicalPhiScaleSequence_closed shows the sequence is minimally closed (using $\varphi^2 = \varphi + 1$), and canonicalPhiScaleSequence_first_closure_law packages that as a first-closure law. Those feed canonicalMinimalHierarchy: the $\varphi$ geometric sequence with first closure.
In framework terms it is the concrete scale ladder realizing T6 ($\varphi$ forced by self-similarity). Parent results then connect hierarchy minimality to the claim that every minimal hierarchy has ratio $\varphi$, tying discrete ledger self-similarity to the unique nontrivial geometric ratio.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.