hierarchy_forced
plain-language theorem explainer
Definition that assembles a UniformScaleLadder record from a NontrivialMultilevelComposition once all adjacent ratios are forced equal and the base ratio exceeds one. Researchers closing the zero-parameter ledger to hierarchical structure in Recognition Science cite it when moving from Gap 2 to self-similar scaling. The construction is a direct record literal that copies levels and proves the uniform_scaling field by algebraic rearrangement of the no_free_scale hypothesis.
Claim. Let $M$ be a nontrivial multilevel composition: a function levels $: ℕ → ℝ$ with levels$(k) > 0$ for all $k$ and at least three positive initial values. Assume adjacent ratios are position-independent, i.e., $∀ j,k, levels(j+1)/levels(j) = levels(k+1)/levels(k)$, and the base ratio satisfies $1 < levels(1)/levels(0)$. Then there exists a uniform scale ladder whose level sequence coincides with that of $M$, whose ratio is the base ratio, and whose scaling property holds for every step.
background
UniformScaleLadder is the structure that packages a positive real sequence, a ratio greater than one, and the exact scaling relation levels$(k+1) = ratio · levels(k)$ for all $k$. NontrivialMultilevelComposition is the structure that supplies such a sequence together with the guarantee of at least three levels. The present definition belongs to the module that treats Gap 2 of the axiom-closure plan: the step that forces hierarchical structure from a nontrivial zero-parameter ledger.
proof idea
The definition is a direct structure constructor. It sets levels and levels_pos to the corresponding fields of $M$, sets ratio to the first adjacent ratio, and supplies the uniform_scaling proof by applying the no_free_scale hypothesis at $(k,0)$, rewriting via div_eq_div_iff, then simplifying with field_simp and linarith.
why it matters
The definition supplies the UniformScaleLadder instance required by the downstream theorem hierarchy_forced_gives_phi, which concludes that the forced ratio equals φ. It therefore advances the derivation of self-similar fixed points from the zero-parameter condition inside the HierarchyForcing module. The construction closes the uniform-scaling half of the Gap-2 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.