Cost Frequency Ladder Is Self Similar Ratio

The self-similar ratio

A self-similar ratio is a number that equals one plus its reciprocal. This property has exactly one positive solution: the golden ratio, approximately 1.618. This number has been known since antiquity as the extreme and mean ratio, and it appears throughout geometry, for example in the proportions of a regular pentagon.

To see why, consider a positive number r that satisfies the self-similarity equation r = 1 + 1/r. Multiplying both sides by r gives r² = r + 1, which is a quadratic equation with two roots. One root is positive, the golden ratio, and the other is negative, approximately −0.618. When ratios of positive quantities are considered, only the positive root is relevant.

In Recognition Science, the framework models physical structure through a ledger, a discrete record of recognition events, where the cost of a ratio is measured by the function J(r) = ½(r + 1/r) − 1. This cost is zero when the ratio is 1, meaning no change, and grows as the ratio moves away from 1. The framework's library, a machine-checked collection of formal theorems, proves that among all positive ratios greater than 1 that satisfy the self-similarity equation r² = r + 1, the golden ratio is the unique one. This is the declaration IsSelfSimilarRatio, which defines the property, and the theorem phi_unique_self_similar, which proves its uniqueness.

The consequence is a statement about frequency ratios. For any positive frequency f, the ratio f × φ is the first φ-harmonic above f. The framework's theorem phi_harmonic_forced shows that this harmonic is forced: it is the minimal-cost non-trivial resonance, the next frequency above f that the cost function selects. This is not a claim about how any physical system actually oscillates; it is a statement about what the cost function, once assumed, picks out as the next step in a ladder of frequencies.

The declaration itself does not claim that any real oscillator follows this ladder, nor that the golden ratio is the only possible ratio in any system. It only establishes the uniqueness of φ as the positive solution to r² = r + 1, and from that, the forced nature of the first φ-harmonic for any positive frequency. The step from this mathematical fact to a description of physical resonances in the world is a modeling choice, not a theorem.

/-- φ is the UNIQUE positive self-similar ratio.
    Proof: r² = r + 1 and φ² = φ + 1 give (r−φ)(r+φ) = r−φ,
    so (r−φ)(r+φ−1) = 0. Since r > 0 and φ > 1, r+φ−1 > 0,
    so r = φ. -/
theorem phi_unique_self_similar {r : ℝ} (hr_pos : 0 < r)
    (hr_ss : IsSelfSimilarRatio r) : r = phi := by
  unfold IsSelfSimilarRatio at hr_ss
  have hphi_sq := phi_sq_eq
  have hphi_pos := phi_pos
  have hphi_gt1 := one_lt_phi
  have hdiff : (r - phi) * (r + phi - 1) = 0 := by nlinarith
  rcases mul_eq_zero.mp hdiff with h | h
  · linarith
  · exfalso; nlinarith

/-- The φ-harmonic is forced for any positive frequency. -/
noncomputable def phi_harmonic_forced {f : ℝ} (hf : 0 < f) : PhiHarmonicForced f where
  harmonic := f * phi
  harmonic_eq := rfl
  ratio_is_phi := by rw [mul_div_cancel_left₀ _ (ne_of_gt hf)]
  ratio_self_similar := by
    rw [mul_div_cancel_left₀ _ (ne_of_gt hf)]
    exact phi_is_self_similar
  ratio_unique := fun r hr_pos hr_ss => phi_unique_self_similar hr_pos hr_ss

/-- The J-cost of a frequency ratio r = f₂/f₁. -/
noncomputable def frequencyRatioCost (r : ℝ) : ℝ := Jcost r

What this page does not claim

No claim that any real physical oscillator follows the φ-ladder. No claim that the golden ratio is the only possible ratio in any system. No claim that the step from the mathematical theorem to physical resonance is itself proved.

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/Cost/FrequencyLadder.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: