Foundation Hierarchy Forcing Uniform Scaling Forced

The uniform ladder

A hierarchy is a stack of levels, each one a positive real number, like the rungs of a ladder measured from the ground. The question is how the rungs are spaced. They could grow by a different factor at each step, or they could all grow by the same factor. The classical fact, familiar from logarithms and geometric series, is that a uniform ladder is the simplest and most regular choice. The Recognition Science declaration uniform_scaling_forced states a stronger, formal version: if a hierarchy has no free scale parameters, meaning no adjustable constants that could tune the rungs independently, then all adjacent ratios must be equal. The proof lives in the framework's machine-checked library of formal theorems, and it is pure real arithmetic, with no extra axioms.

The theorem's shape is precise. It starts with a structure called a nontrivial multilevel composition, which is just a sequence of positive levels with at least three entries. The key hypothesis is that every adjacent ratio is the same as every other, a condition the framework calls no free scale parameters. The conclusion is that a single number sigma exists, greater than one, so that each level is sigma times the previous one. In other words, the ladder is geometric: level k equals sigma to the k-th power times level zero. The declaration also provides the machinery to see why the condition matters. A perturbation function shifts all levels above a chosen position by a factor of exp(t), which changes one ratio continuously while leaving the others alone. The library proves that different parameters yield different sequences, so the perturbation really does move the ladder. The no-free-scale condition rules out exactly this kind of movement.

The framework then connects this uniform ladder to its own central constant. A companion theorem, hierarchy_forced_gives_phi, adds one more condition: the third level is the sum of the first two. Under that additive rule, the forced ratio sigma is the golden ratio, the number satisfying r squared equals r plus one, about 1.618. This is the step where a purely structural fact, uniform spacing, becomes a specific number. The library also proves a minimality result: among positive integer pairs (a, b), the pair (1, 1) uniquely minimizes the maximum of the two, which is the simplest possible recurrence coefficient. That result is pure arithmetic as well.

In Recognition Science, this theorem is one rung in a larger chain that leads from a cost function to the golden ratio and beyond. The framework treats the uniform ladder as a forced structure, not a chosen one. But the claim has sharp limits. The theorem does not say that any real hierarchy must be uniform; it says that a hierarchy satisfying the no-free-scale hypothesis must be. It does not derive the golden ratio without the additive condition, and it does not say anything about which physical systems, if any, realize such a hierarchy. The bridge from this formal theorem to physical space or particles remains open. What the declaration establishes, cleanly and checkably, is a conditional fact: no free parameters, uniform ratios. That is the whole of it.

/-- **Theorem**: No free scale parameters forces uniform adjacent ratios.

The canonical derivation now uses `HierarchyRealization.realized_uniform_ratios`
which derives uniform ratios from the `RealizedHierarchy.ratio_self_similar`
field, with `no_continuous_moduli` as backup
(`HierarchyRealization.no_moduli_forces_uniform_ratios`). -/
theorem uniform_scaling_forced
    (M : NontrivialMultilevelComposition)
    (no_free_scale : ∀ j k,
      M.levels (j + 1) / M.levels j = M.levels (k + 1) / M.levels k)
    (ratio_gt_one : 1 < M.levels 1 / M.levels 0) :
    ∃ σ : ℝ, 1 < σ ∧ ∀ k, M.levels (k + 1) = σ * M.levels k := by
  use M.levels 1 / M.levels 0
  refine ⟨ratio_gt_one, fun k => ?_⟩
  have hk := M.levels_pos k
  have h0 := M.levels_pos 0
  have hratio := no_free_scale k 0
  rw [div_eq_div_iff (ne_of_gt hk) (ne_of_gt h0)] at hratio
  have : M.levels (k + 1) = M.levels 1 / M.levels 0 * M.levels k := by
    field_simp; linarith
  exact this

/-- Different perturbation parameters give different level sequences.
The key step: at position `j + 1` the values are `levels(j+1) · exp(t)`,
and `exp` is injective. -/
theorem scale_perturbed_family_injective (levels : ℕ → ℝ) (j : ℕ)
    (h_pos : 0 < levels (j + 1)) :
    Function.Injective (ScalePerturbed levels j) := by
  intro t₁ t₂ h
  have h_eval := congr_fun h (j + 1)
  unfold ScalePerturbed at h_eval
  rw [if_neg (by omega : ¬(j + 1 ≤ j)), if_neg (by omega : ¬(j + 1 ≤ j))] at h_eval
  have h_ne : levels (j + 1) ≠ 0 := ne_of_gt h_pos
  exact Real.exp_injective (mul_left_cancel₀ h_ne h_eval)

/-- The forced hierarchy yields σ = φ. -/
theorem hierarchy_forced_gives_phi
    (M : NontrivialMultilevelComposition)
    (no_free_scale : ∀ j k,
      M.levels (j + 1) / M.levels j = M.levels (k + 1) / M.levels k)
    (ratio_gt_one : 1 < M.levels 1 / M.levels 0)
    (additive : M.levels 2 = M.levels 1 + M.levels 0) :
    (hierarchy_forced M no_free_scale ratio_gt_one).ratio = PhiForcing.φ :=
  hierarchy_emergence_forces_phi
    (hierarchy_forced M no_free_scale ratio_gt_one)
    additive

/-- **Theorem (Phase 3)**: Among recurrence coefficients (a, b) with
a ≥ 1 and b ≥ 1, the pair (1, 1) uniquely minimizes max(a, b).
No axiom needed — this is pure arithmetic. -/
theorem additive_composition_is_minimal (a b : ℕ) (ha : 1 ≤ a) (hb : 1 ≤ b) :
    max a b = 1 → a = 1 ∧ b = 1 := by
  intro h
  constructor
  · exact Nat.le_antisymm (by omega) ha
  · exact Nat.le_antisymm (by omega) hb

What this page does not claim

The theorem does not claim that every hierarchy must be uniform, only those with no free scale parameters. The golden ratio conclusion requires the additive condition that the third level is the sum of the first two. The declaration says nothing about which physical systems realize such a hierarchy; that bridge is open.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/HierarchyForcing.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: