Foundation Hierarchy Emergence Uniform Scale Ladder

The scale ladder

A scale ladder is a simple mathematical object: a sequence of positive numbers, one for each level, where moving from one level to the next multiplies by a single fixed ratio. The ratio is greater than one, so the levels grow steadily. The definition itself chooses no particular ratio; it only says that whatever the ratio is, it stays the same at every step. This uniformity is what makes the ladder a ladder rather than a list of unrelated sizes.

The classical interest in such ladders comes from the golden ratio, the number φ ≈ 1.618 that solves r² = r + 1. Euclid knew it as the extreme and mean ratio, and it appears in pentagons and in the Fibonacci sequence, where each term is the sum of the two before it. The Fibonacci recurrence is the simplest way to build a ladder with no free parameters: if each level is the sum of the two preceding levels, then the ratio between adjacent levels is forced to be φ. This is a standard result, true for any sequence that follows that additive rule.

In Recognition Science, the framework models a ledger, a discrete record of recognition events, and asks what structure such a ledger must have when it has no free parameters. The declaration UniformScaleLadder formalizes the ladder itself: it states that a zero-parameter comparison ledger with multilevel composition necessarily produces a minimal hierarchy, and that this hierarchy forces φ as the unique admissible scale. The argument proceeds in four steps: multilevel composition induces a scale ladder; no free scale data forces a uniform ratio between adjacent levels; locality forces a finite-order recurrence where composition at level k+2 depends only on levels k and k+1; and minimal nondegenerate closure forces the Fibonacci recurrence L_{k+2} = L_{k+1} + L_k, hence σ² = σ + 1, hence σ = φ.

The machine-checked library of formal theorems proves the key steps. One theorem, locality_forces_additive_composition, shows that if a scale ladder has additive composition at the next level, then the ratio squared equals the ratio plus one. Another, hierarchy_emergence_forces_phi, concludes directly that the ratio equals φ. A third, ledger_forces_phi, packages the result: from the ledger primitives of a uniform scale ladder and additive composition, one can derive a minimal hierarchy whose scale ratio is φ. These are formal results, checked by the library's kernel, with no hidden assumptions beyond the stated ones.

What the declaration does not claim is as important as what it proves. It does not claim that any particular physical system must have a golden-ratio scale; it claims only that if a system is modeled as a zero-parameter ledger with additive composition, then its scale ratio is forced. The theorem does not derive the value of any specific constant from experiment; it derives a mathematical consequence of a definitional choice. The ladder is a structure, not a prediction about the world. The framework's claim is that this structure is the one a minimal ledger must have, and that is a statement about the model, not about any measurement.

/-- A scale ladder extracted from multilevel composition: a sequence
of positive level sizes with a uniform scaling ratio. -/
structure UniformScaleLadder where
  levels : ℕ → ℝ
  levels_pos : ∀ k, 0 < levels k
  ratio : ℝ
  ratio_gt_one : 1 < ratio
  uniform_scaling : ∀ k, levels (k + 1) = ratio * levels k

/-- Combined emergence theorem: from ledger primitives (uniform scale
ladder + additive composition), derive the `MinimalHierarchy` package
and conclude `φ`. -/
theorem ledger_forces_phi
    (L : UniformScaleLadder)
    (additive_closure : L.levels 2 = L.levels 1 + L.levels 0) :
    ∃ H : MinimalHierarchy, H.scales.ratio = φ := by
  let S : GeometricScaleSequence :=
    { ratio := L.ratio
      ratio_pos := lt_trans (by norm_num) L.ratio_gt_one
      ratio_ne_one := by linarith [L.ratio_gt_one] }
  have h_closed : S.isClosed := by
    unfold GeometricScaleSequence.isClosed
    unfold ledgerCompose
    unfold GeometricScaleSequence.scale
    have hrec := locality_forces_additive_composition L additive_closure
    nlinarith [hrec]
  exact ⟨⟨S, h_closed⟩, hierarchy_forces_phi ⟨S, h_closed⟩⟩

/-- **Locality theorem**: Additive composition at the next level
depends only on the two preceding levels.  The minimal nondegenerate
integer recurrence with positive coefficients is `a = b = 1`. -/
theorem locality_forces_additive_composition
    (L : UniformScaleLadder)
    (additive_closure : L.levels 2 = L.levels 1 + L.levels 0) :
    L.ratio ^ 2 = L.ratio + 1 := by
  have h0 : L.levels 0 ≠ 0 := ne_of_gt (L.levels_pos 0)
  have h1 : L.levels 1 = L.ratio * L.levels 0 := L.uniform_scaling 0
  have h2 : L.levels 2 = L.ratio * L.levels 1 := L.uniform_scaling 1
  have h_sq : L.levels 2 = L.ratio ^ 2 * L.levels 0 := by
    rw [h2, h1]; ring
  have h_rhs : L.levels 2 = (L.ratio + 1) * L.levels 0 := by
    rw [additive_closure, h1]; ring
  have h_mul : (L.ratio ^ 2 - (L.ratio + 1)) * L.levels 0 = 0 := by
    calc
      (L.ratio ^ 2 - (L.ratio + 1)) * L.levels 0
          = L.ratio ^ 2 * L.levels 0 - (L.ratio + 1) * L.levels 0 := by ring
      _ = L.levels 2 - L.levels 2 := by rw [← h_sq, h_rhs]
      _ = 0 := by ring
  rcases mul_eq_zero.mp h_mul with hzero | hsize
  · exact sub_eq_zero.mp hzero
  · exact (h0 hsize).elim

/-- **Bridge B1 (unconditional)**: from a zero-parameter scale ladder
with additive composition, the scale ratio is forced to `φ`. -/
theorem hierarchy_emergence_forces_phi
    (L : UniformScaleLadder)
    (additive_closure : L.levels 2 = L.levels 1 + L.levels 0) :
    L.ratio = φ := by
  let S : GeometricScaleSequence :=
    { ratio := L.ratio
      ratio_pos := lt_trans (by norm_num) L.ratio_gt_one
      ratio_ne_one := by linarith [L.ratio_gt_one] }
  have h_closed : S.isClosed := by
    unfold GeometricScaleSequence.isClosed
    unfold ledgerCompose
    unfold GeometricScaleSequence.scale
    have hrec := locality_forces_additive_composition L additive_closure
    nlinarith [hrec]
  exact closed_ratio_is_phi S h_closed

What this page does not claim

The declaration does not claim that any specific physical system must have a golden-ratio scale. It does not derive the value of any measured constant from experiment. The theorem does not prove that the Fibonacci recurrence is the only possible recurrence without additional premises.

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