Recog Spec Phi Selection Core

The golden ratio selector

The golden ratio, usually written φ, is the positive number that satisfies φ² = φ + 1. Solving the quadratic gives φ = (1 + √5)/2 ≈ 1.618. Euclid described it around 300 BCE as the extreme and mean ratio: a line divided so the whole is to the longer part as the longer part is to the shorter. It appears in the regular pentagon, where diagonals cut each other in this ratio, and in the Fibonacci sequence, where successive ratios approach φ.

The defining equation has two solutions: the positive root ≈ 1.618 and the negative root ≈ −0.618. The negative root is the reciprocal of the positive one, up to sign. The selector rule in the framework's machine-checked library of formal theorems, called recognition (the cost of recording an event in a discrete ledger), is simply the conjunction of the equation and the positivity condition. It is a definition, not a theorem: it chooses which root counts as the golden ratio.

In Recognition Science, this selector appears as the unique self-similar scaling forced by the cost function J(x) = (x + 1/x)/2 − 1. The framework proves that any cost function satisfying five plain conditions must equal J, and from J the golden ratio emerges as the only scale that maps the cost to itself. The selector module pins down which root that is: the positive one. Without the positivity condition, the equation alone would admit both roots and the framework's chain of consequences would lose its unique anchor.

The practical consequence is that the framework's constants and particle mass ladder all inherit the positive root. The selector is the gate that lets the golden ratio enter the framework's derivations. It does not derive φ from anything deeper; it fixes the convention so that later theorems can rely on a single value.

/-- φ selection criterion: φ² = φ + 1 and φ > 0. -/
def PhiSelection (φ : ℝ) : Prop :=
  φ ^ 2 = φ + 1 ∧ φ > 0

What this page does not claim

This module does not prove that the golden ratio exists; it defines which root is selected. The selector does not derive φ from the cost function; the forcing chain does that separately. The module does not state or prove any theorem about the golden ratio's properties.

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/RecogSpec/PhiSelectionCore.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: