hierarchy_forced
The definition assembles a UniformScaleLadder record from a NontrivialMultilevelComposition whose adjacent ratios are all forced equal. Researchers closing the zero-parameter ledger in the Recognition hierarchy would cite it to obtain a uniform scaling structure before deriving the fixed-point ratio. The construction copies the level sequence and ratio directly, then verifies the scaling relation by reducing the equal-ratio hypothesis at base index 0 via division rewriting and linear arithmetic.
claimLet $M$ be a nontrivial multilevel composition with positive level sizes $ell_k > 0$ ($k in mathbb{N}$) and at least three levels. Given the hypothesis that all adjacent ratios coincide, $frac{ell_{j+1}}{ell_j} = frac{ell_{k+1}}{ell_k}$ for every $j,k$, together with $frac{ell_1}{ell_0} > 1$, the uniform scale ladder is the structure whose levels are exactly those of $M$, whose ratio is $r = frac{ell_1}{ell_0}$, and which satisfies $ell_{k+1} = r cdot ell_k$ for all $k$.
background
NontrivialMultilevelComposition is the structure consisting of a sequence of positive reals with at least three levels; its doc-comment states that the no-free-scale condition forces uniform adjacent ratios. UniformScaleLadder is the target structure: a positive sequence equipped with a fixed ratio greater than one and the exact scaling relation levels(k+1) = ratio * levels(k). The module treats Gap 2 of the axiom-closure plan, forcing hierarchical structure from a zero-parameter ledger; the upstream UniformScaleLadder definition supplies the codomain while the no-free-scale hypothesis eliminates continuous moduli.
proof idea
The definition is a direct record constructor. It sets levels and levels_pos to the corresponding fields of M, sets ratio to the first adjacent ratio of M, copies the ratio_gt_one hypothesis, and proves the uniform_scaling field by instantiating no_free_scale at k and 0, rewriting the ratio equality via div_eq_div_iff, applying field_simp, and closing with linarith.
why it matters in Recognition Science
The definition supplies the UniformScaleLadder instance required by the downstream theorem hierarchy_forced_gives_phi, which adds the additive composition hypothesis levels(2) = levels(1) + levels(0) to conclude that the common ratio equals phi. It therefore completes the uniform-scaling step inside the HierarchyForcing module that advances the forcing chain from the zero-parameter ledger toward the self-similar fixed point. In the Recognition framework this step precedes extraction of the eight-tick octave and the phi-ladder mass formula.
scope and limits
- Does not determine the numerical value of the common ratio.
- Does not assume or use additive composition of levels.
- Does not treat perturbed or non-uniform level sequences.
- Does not invoke the Recognition structure M or Cycle3.
formal statement (Lean)
123noncomputable def hierarchy_forced
124 (M : NontrivialMultilevelComposition)
125 (no_free_scale : ∀ j k,
126 M.levels (j + 1) / M.levels j = M.levels (k + 1) / M.levels k)
127 (ratio_gt_one : 1 < M.levels 1 / M.levels 0) :
128 UniformScaleLadder :=
proof body
Definition body.
129 { levels := M.levels
130 levels_pos := M.levels_pos
131 ratio := M.levels 1 / M.levels 0
132 ratio_gt_one := ratio_gt_one
133 uniform_scaling := fun k => by
134 have hk := M.levels_pos k
135 have h0 := M.levels_pos 0
136 have hratio := no_free_scale k 0
137 rw [div_eq_div_iff (ne_of_gt hk) (ne_of_gt h0)] at hratio
138 field_simp; linarith }
139
140/-- The forced hierarchy yields σ = φ. -/