uniform_scaling_forced
The theorem establishes that a nontrivial multilevel composition with identical adjacent ratios across all levels must scale uniformly by a fixed factor greater than one. A researcher deriving hierarchical structure from zero-parameter ledgers in Recognition Science would cite it to close the gap between the ledger and self-similar levels. The proof selects the first ratio as the common factor and propagates it to every index via the equality hypothesis and field arithmetic.
claimLet $M$ be a nontrivial multilevel composition: a map $l:ℕ→ℝ_{>0}$ with at least three positive values. Assume the adjacent ratios are level-independent, $l_{j+1}/l_j=l_{k+1}/l_k$ for all $j,k$, and $l_1/l_0>1$. Then there exists $σ>1$ such that $l_{k+1}=σ⋅l_k$ for every $k$.
background
The module HierarchyForcing treats Gap 2 of the axiom-closure plan: passage from a nontrivial zero-parameter ledger to forced hierarchical structure. NontrivialMultilevelComposition is the structure whose fields are a level map $l:ℕ→ℝ$, the positivity predicate $∀k,0<l_k$, and the witness $0<l_0∧0<l_1∧0<l_2$. The hypothesis no_free_scale asserts that every pair of adjacent ratios coincides; ratio_gt_one supplies the strict increase at the base.
proof idea
The proof is a direct tactic sequence. It instantiates the witness σ with the concrete ratio $l_1/l_0$. For arbitrary $k$ it obtains the positivity facts $l_k>0$ and $l_0>0$, applies no_free_scale at the pair $(k,0)$, rewrites the ratio equality via div_eq_div_iff, and finishes with field_simp followed by linarith to recover the scaling identity.
why it matters in Recognition Science
The result is the first theorem listed in the module documentation for Phase 3 and supplies the uniform-ratio step required by later siblings such as hierarchy_forced and hierarchy_forced_gives_phi. It eliminates free scale parameters inside the zero-parameter ledger, aligning with the self-similar fixed point of the forcing chain (T6) and the eight-tick octave. No downstream use sites are recorded yet; the declaration therefore functions as an internal bridge within the HierarchyForcing block.
scope and limits
- Does not prove existence of any multilevel composition.
- Does not treat continuous scale perturbations or their injectivity.
- Does not invoke the Recognition Composition Law or any physical constants.
- Does not address non-adjacent or higher-dimensional compositions.
formal statement (Lean)
89theorem uniform_scaling_forced
90 (M : NontrivialMultilevelComposition)
91 (no_free_scale : ∀ j k,
92 M.levels (j + 1) / M.levels j = M.levels (k + 1) / M.levels k)
93 (ratio_gt_one : 1 < M.levels 1 / M.levels 0) :
94 ∃ σ : ℝ, 1 < σ ∧ ∀ k, M.levels (k + 1) = σ * M.levels k := by
proof body
Tactic-mode proof.
95 use M.levels 1 / M.levels 0
96 refine ⟨ratio_gt_one, fun k => ?_⟩
97 have hk := M.levels_pos k
98 have h0 := M.levels_pos 0
99 have hratio := no_free_scale k 0
100 rw [div_eq_div_iff (ne_of_gt hk) (ne_of_gt h0)] at hratio
101 have : M.levels (k + 1) = M.levels 1 / M.levels 0 * M.levels k := by
102 field_simp; linarith
103 exact this
104
105/-- **Theorem (Phase 3)**: Among recurrence coefficients (a, b) with
106a ≥ 1 and b ≥ 1, the pair (1, 1) uniquely minimizes max(a, b).
107No axiom needed — this is pure arithmetic. -/