ledger_forces_phi
plain-language theorem explainer
A uniform scale ladder with additive closure at the second level forces existence of a minimal hierarchy whose scale ratio equals the golden ratio φ. Researchers deriving zero-parameter scale hierarchies from ledger composition would cite this result. The proof builds a geometric scale sequence from the ladder, verifies closure with the locality lemma, and applies the hierarchy forcing theorem.
Claim. Let $L$ be a uniform scale ladder: a sequence of positive reals $L_k$ with uniform ratio $r>1$ satisfying $L_{k+1}=r L_k$ for all $k$. Given additive closure $L_2=L_1+L_0$, there exists a minimal hierarchy $H$ such that the scale ratio of $H$ equals the golden ratio $φ$.
background
UniformScaleLadder is a structure of positive level sizes equipped with a single uniform scaling ratio greater than one; the module shows that multilevel composition in a zero-parameter ledger produces such a ladder, with uniformity enforced because differing adjacent ratios would introduce free parameters. The local theoretical setting is the four-step emergence argument: composition induces the ladder, no free scales force uniformity, locality forces a finite recurrence on level sizes, and minimal nondegenerate closure forces the Fibonacci relation hence $σ=φ$ (MODULE_DOC). Upstream, locality_forces_additive_composition states that additive composition at the next level depends only on the two preceding levels and yields the minimal recurrence with positive coefficients (doc: 'The minimal nondegenerate integer recurrence with positive coefficients is a=b=1'). hierarchy_forces_phi from HierarchyMinimality packages the closed sequence into MinimalHierarchy.
proof idea
Construct GeometricScaleSequence S by copying the ratio from L and using lt_trans for positivity together with linarith for the ratio not equal to one. Prove S.isClosed by unfolding isClosed, ledgerCompose and scale, then invoke locality_forces_additive_composition on the additive_closure hypothesis and close with nlinarith. Apply hierarchy_forces_phi to the resulting closed sequence to obtain the required minimal hierarchy with ratio φ.
why it matters
This combined emergence theorem completes the derivation of φ from ledger primitives inside the HierarchyEmergence module, directly supplying the MinimalHierarchy package whose scale ratio is forced to φ. It realizes the fourth step of the module argument (minimal closure forces Fibonacci recurrence hence σ=φ) and aligns with the self-similar fixed point T6 in the forcing chain. No downstream uses are recorded, so the result stands as a terminal step in the zero-parameter scale closure chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.