no_free_scale_forces_uniform
plain-language theorem explainer
Equal adjacent ratios in a positive real sequence with first ratio exceeding one yield a uniform scale ladder. Researchers deriving hierarchy emergence from zero-parameter ledgers cite this when closing scale data without free parameters. The definition constructs the UniformScaleLadder record and verifies uniform scaling by algebraic reduction of the equal-ratios hypothesis.
Claim. Let $(L_k)_{k=0}^∞$ be positive reals such that $L_{j+1}/L_j = L_{k+1}/L_k$ for all $j,k$ and $L_1/L_0 > 1$. Then the sequence forms a uniform scale ladder: there exists $r = L_1/L_0 > 1$ with $L_{k+1} = r L_k$ for every $k$.
background
UniformScaleLadder is the structure recording a sequence of positive level sizes, a fixed ratio greater than one, and the property that every consecutive pair scales by that ratio. The HierarchyEmergence module derives minimal hierarchies from zero-parameter scale closure: multilevel composition induces a ladder, absence of free parameters forces uniformity, locality forces a recurrence, and minimality forces the Fibonacci relation whose fixed point is φ. The definition supplies the second step of that chain.
proof idea
One-line wrapper that assembles the UniformScaleLadder record. It copies the input levels and positivity, sets ratio to levels 1 / levels 0, and proves uniform_scaling by specializing the equal-ratios hypothesis at (k,0), rewriting the division equality, and applying field_simp followed by linarith to obtain the required scaling identity.
why it matters
It closes the no-free-scale step in the four-step hierarchy emergence argument of the module doc-comment. The result is invoked by realized_to_ladder in HierarchyRealization to lift a realized hierarchy to the uniform ladder. Within Recognition Science it supplies the uniform ratio needed for the subsequent locality theorem that forces the Fibonacci recurrence and therefore φ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.