Foundation Pair Kernel Source Grammar Golden Ratio Is Algebraic

The golden ratio's algebraic status

The golden ratio φ is the positive solution of x² = x + 1, so it is algebraic: it satisfies a polynomial equation with rational coefficients. This is a classical fact, known since antiquity as the extreme and mean ratio. The equation x² - x - 1 = 0 has two real roots, (1 ± √5)/2; the positive one is φ ≈ 1.618. Because it solves a quadratic with rational coefficients, φ is algebraic of degree 2, and it is not rational, as √5 is irrational. Its continued fraction is all ones, [1; 1, 1, 1, ...], which is the slowest possible convergence among continued fractions.

The golden ratio appears throughout classical mathematics: in the regular pentagon, where diagonals cut each other in golden ratio; in the Fibonacci sequence, where consecutive ratios converge to φ; and in the spiral growth of many plants. These appearances are not coincidences but consequences of the same quadratic relation. The algebraic nature of φ is what makes it computable exactly in symbolic systems: it can be represented as a root of a polynomial, not merely approximated.

In Recognition Science, the declaration goldenRatio_isAlgebraic is part of a machine-checked library of formal theorems. The library proves that φ is algebraic over the rationals, using the polynomial X² - X - 1. This is not a new discovery; it is a formal verification of a known fact. The declaration belongs to a broader grammar: a source-strength certificate language that allows rational numbers, the golden ratio, and field operations (addition, multiplication, negation, inversion). Every expression in this language evaluates to a real number, and the library proves that every such evaluated value is algebraic over the rationals. The circle constant π has no constructor in this grammar; its absence is structural, not accidental. The grammar is deliberately kept free of downstream physical constants, so that certificates remain purely algebraic.

What this establishes, in plain terms, is a clean boundary: the certificate language can express φ and all its field combinations, but it cannot express π or any transcendental number. This matters because it gives a precise, machine-checked answer to the question of which numbers are representable in the source-strength ledger. The declaration does not claim that φ is irrational, though that is true and follows from the same polynomial; it does not claim that the golden ratio is the only algebraic number in the grammar, which is false; and it does not claim anything about the physical constants that live outside the grammar. The theorem is a small, exact fact that anchors the whole certificate system.

/-- The golden-ratio seed is algebraic over the rationals. -/
theorem goldenRatio_isAlgebraic : IsAlgebraic ℚ Real.goldenRatio := by
  refine ⟨Polynomial.X ^ 2 - Polynomial.X - 1, ?_, ?_⟩
  · intro h
    have hcoeff := congrArg (fun p : Polynomial ℚ => p.coeff 2) h
    norm_num [Polynomial.coeff_X, Polynomial.coeff_one] at hcoeff
  · norm_num [Real.goldenRatio_sq]

/-- Every value generated by the grammar is algebraic over the rationals. -/
theorem eval_isAlgebraic (e : LedgerExpr) : IsAlgebraic ℚ e.eval := by
  induction e with
  | ofRat q =>
      exact isAlgebraic_rat ℚ q
  | phi =>
      exact goldenRatio_isAlgebraic
  | add a b ha hb =>
      exact ha.add hb
  | mul a b ha hb =>
      exact ha.mul hb
  | neg a ha =>
      exact ha.neg
  | inv a ha =>
      exact ha.inv

/-- Expressions generated by rational constants, the golden ratio, and field
operations. The constructor list is the machine-checked source whitelist. -/
inductive LedgerExpr where
  | ofRat : ℚ → LedgerExpr
  | phi : LedgerExpr
  | add : LedgerExpr → LedgerExpr → LedgerExpr
  | mul : LedgerExpr → LedgerExpr → LedgerExpr
  | neg : LedgerExpr → LedgerExpr
  | inv : LedgerExpr → LedgerExpr
  deriving Repr, DecidableEq

What this page does not claim

The declaration does not prove that φ is irrational, though that follows from the same polynomial. It does not claim that φ is the only algebraic number in the grammar. It does not claim anything about the physical constants outside the grammar.

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