bridge_B1_hierarchy_implies_phi
plain-language theorem explainer
Any hierarchical ledger whose successive level sizes scale by a fixed factor σ > 1 and obey the two-step composition law must have σ equal to the golden ratio φ. Exclusivity and phi-forcing arguments cite this as Bridge B1. The proof packages the ledger as a closed geometric scale sequence and invokes the existing minimal-hierarchy uniqueness theorem.
Claim. Let $L$ be a hierarchical ledger: a real scale $\sigma > 1$, positive level sizes $\ell(k)$, uniform scaling $\ell(k+1) = \sigma\,\ell(k)$, and the composition identity $\ell(2) = \ell(1) + \ell(0)$. Then $\sigma = \varphi$, where $\varphi = (1+\sqrt{5})/2$ is the unique positive root greater than $1$ of $x^2 = x + 1$.
background
A HierarchicalLedger packages discrete recognition levels with a single scale factor: each level size is the previous times $\sigma > 1$, and the two-step composition law identifies level 2 with the sum of levels 1 and 0. That sum is the ledger composition operation used throughout the phi-forcing stack.
Upstream, a GeometricScaleSequence is a positive ratio $r \neq 1$ together with its geometric powers. Closure under ledger composition means the ratio satisfies the Fibonacci recurrence $r^2 = r + 1$. The HierarchyMinimality result states that "minimal closure already forces the unique positive self-similar ratio $\varphi$".
This module sits in Verification.Exclusivity: it turns the abstract hierarchical ledger interface into a concrete bridge that pins the scale to $\varphi$, matching the T6 landmark that $\varphi$ is the forced self-similar fixed point.
proof idea
Build a GeometricScaleSequence whose ratio is $L$.scale. Positivity and $r \neq 1$ follow from $\sigma > 1$ by lt_trans/norm_num and linarith.
Unfold closure (ledger composition on consecutive scales) and feed in the sibling lemma hierarchy_forces_fibonacci_recurrence, which extracts $\sigma^2 = \sigma + 1$ from uniform scaling plus the composition identity; nlinarith discharges the algebraic match.
Package the closed sequence as a MinimalHierarchy and apply hierarchy_forces_phi, which reduces to the existing closed-ratio uniqueness for $\varphi$.
why it matters
Bridge B1 is the exclusivity step that converts hierarchical ledger structure into the forced scale $\varphi$. It sits on the T6 phi-forcing landmark: once levels compose by addition and scale geometrically, the only admissible ratio is the golden ratio.
Downstream exclusivity arguments that assume a hierarchical ledger can therefore replace the free scale parameter by $\varphi$ without extra hypotheses. The proof reuses HierarchyMinimality rather than re-deriving root uniqueness, keeping the verification layer thin over the foundation stack.
No used_by edges are recorded yet; the declaration is the named B1 bridge for the exclusivity hierarchy theorem family and the sibling Fibonacci-recurrence extraction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.