Foundation Hierarchy Realization No Moduli Forces Uniform Ratios

The uniformity theorem

A hierarchy is a stack of levels, each one a step up in scale from the last. Think of a ladder whose rungs are numbered by size. The question at issue is whether the spacing between rungs can vary: can the jump from rung 1 to rung 2 be a different proportion than the jump from rung 2 to rung 3? The theorem no_moduli_forces_uniform_ratios answers no, under one precise condition. The condition is that the system's carrier, the underlying set of possible states, cannot host a continuous range of distinct values. If it cannot, then every adjacent ratio in the hierarchy must equal every other adjacent ratio.

The proof works by contradiction. Suppose two adjacent ratios differ. Then one can build an injective map from the real numbers into the carrier, one that assigns a distinct internal state to every real number. That injection is a continuous modulus: a continuously varying parameter encoded in the carrier's states. But the framework's defining assumption forbids exactly that. The carrier has no room for such a continuum, so the supposition fails, and the ratios must be uniform.

This result is a theorem in the framework's machine-checked library of formal theorems. It does not stand alone. It relies on two earlier ingredients: the levels must be positive, and the observable that reads the levels must be able to realize every positive value as some carrier state. Those are hypotheses of the theorem, not conclusions. The theorem also does not say what the common ratio is. It only says the ratios are all equal. The value of that ratio, the golden ratio φ, comes from a separate result that adds the Fibonacci recurrence as a further premise.

What the theorem changes is the shape of the hierarchy problem. Before it, one might have hoped for a family of hierarchies with different spacings. After it, that family collapses to a single uniform ladder. The freedom to vary the ratios is not a real freedom at all, once the carrier is finite in the relevant sense. The uniformity is forced, not chosen.

In Recognition Science, this theorem is the bridge that lets the framework derive the golden ratio from its own primitives. The framework models a hierarchy as a realized structure on a closed observable framework, with dynamics that preserve the inter-level ratio and additive posting that composes adjacent levels. From those two fields, uniform scaling and the Fibonacci recurrence follow as theorems. The uniformity theorem is the keystone: it shows that the self-similar dynamics is not one option among many, but the only option consistent with the absence of continuous moduli.

/-- **Corollary**: In a `ClosedObservableFramework` where the observable
can realize all positive values, non-uniform ratios are impossible. -/
theorem no_moduli_forces_uniform_ratios
    (F : ClosedObservableFramework)
    (levels : ℕ → ℝ)
    (levels_pos : ∀ k, 0 < levels k)
    (_levels_from_carrier : ∀ k, ∃ s : F.S, F.r s = levels k)
    (carrier_lifts_perturbations :
      ∀ (_k : ℕ) (v : ℝ), 0 < v → ∃ s : F.S, F.r s = v) :
    ∀ j k, levels (j + 1) / levels j = levels (k + 1) / levels k := by
  by_contra h
  push_neg at h
  have ⟨embed, h_inj⟩ := nonuniform_ratios_yield_moduli
    F levels levels_pos _levels_from_carrier carrier_lifts_perturbations h
  exact F.no_continuous_moduli embed h_inj

/-- If hierarchy levels have non-uniform ratios and the observable
separates hierarchy states, then continuous moduli exist in the carrier.

This internalizes the `sensitivity` bridge: the perturbation family
`ScalePerturbed` lifts to carrier states via the observable `r`. -/
theorem nonuniform_ratios_yield_moduli
    (F : ClosedObservableFramework)
    (levels : ℕ → ℝ)
    (levels_pos : ∀ k, 0 < levels k)
    (_levels_from_carrier : ∀ k, ∃ s : F.S, F.r s = levels k)
    (carrier_lifts_perturbations :
      ∀ (_k : ℕ) (v : ℝ), 0 < v →
        ∃ s : F.S, F.r s = v) :
    (∃ j k, levels (j + 1) / levels j ≠ levels (k + 1) / levels k) →
    ∃ (embed : ℝ → F.S), Function.Injective embed := by
  intro ⟨j, _, _⟩
  have h_pos : 0 < levels (j + 1) := levels_pos (j + 1)
  have h_ne : levels (j + 1) ≠ 0 := ne_of_gt h_pos
  choose lift h_lift using fun (t : ℝ) =>
    carrier_lifts_perturbations (j + 1) (levels (j + 1) * Real.exp t)
      (mul_pos h_pos (Real.exp_pos t))
  refine ⟨lift, fun t₁ t₂ h_eq => ?_⟩
  have h1 : F.r (lift t₁) = levels (j + 1) * Real.exp t₁ := h_lift t₁
  have h2 : F.r (lift t₂) = levels (j + 1) * Real.exp t₂ := h_lift t₂
  have h3 : F.r (lift t₁) = F.r (lift t₂) := by rw [h_eq]
  rw [h1, h2] at h3
  exact Real.exp_injective (mul_left_cancel₀ h_ne h3)

/-- **Corollary**: In a `ClosedObservableFramework` where the observable
can realize all positive values, non-uniform ratios are impossible. -/
theorem no_moduli_forces_uniform_ratios
    (F : ClosedObservableFramework)
    (levels : ℕ → ℝ)
    (levels_pos : ∀ k, 0 < levels k)
    (_levels_from_carrier : ∀ k, ∃ s : F.S, F.r s = levels k)
    (carrier_lifts_perturbations :
      ∀ (_k : ℕ) (v : ℝ), 0 < v → ∃ s : F.S, F.r s = v) :
    ∀ j k, levels (j + 1) / levels j = levels (k + 1) / levels k := by
  by_contra h
  push_neg at h
  have ⟨embed, h_inj⟩ := nonuniform_ratios_yield_moduli
    F levels levels_pos _levels_from_carrier carrier_lifts_perturbations h
  exact F.no_continuous_moduli embed h_inj

/-- **End-to-end theorem**: A realized hierarchy on a closed observable
framework forces the scale ratio to be φ.

This replaces the old bridge that required external `sensitivity` and
`HasAdditiveComposition` hypotheses. Both are now derived from
the realization's `ratio_self_similar` and `additive_posting` fields,
which are RS-native physical principles. -/
theorem realized_hierarchy_forces_phi (F : ClosedObservableFramework)
    (H : RealizedHierarchy F) :
    (realized_to_ladder F H).ratio = PhiForcing.φ :=
  hierarchy_emergence_forces_phi
    (realized_to_ladder F H)
    (realized_additive_closure F H)

What this page does not claim

The theorem does not prove that the common ratio is the golden ratio. The theorem does not apply to hierarchies whose observable cannot realize all positive values. The theorem does not claim that all hierarchies in nature are uniform, only those meeting its stated conditions.

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/HierarchyRealization.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: