Foundation Pair Kernel Source Grammar

The certificate language

A ledger, a discrete record of recognition events, needs a way to certify the strength of a source. The foundation pair kernel source grammar is the formal language that writes those certificates. It is a whitelist of expressions built from rational numbers, the golden ratio, and the field operations of addition, multiplication, negation, and inversion. That is the entire vocabulary: no trigonometric functions, no exponentials, no logarithms, and no circle constant. The grammar is a machine-checked inductive type, meaning every valid expression is constructed from exactly these allowed forms and nothing else.

The grammar's defining property is algebraic closure. Every expression evaluates to a real number that is algebraic over the rationals, meaning it is the root of some polynomial with rational coefficients. The golden ratio itself is algebraic, since it solves x² − x − 1 = 0. Because the grammar only combines algebraic numbers with field operations, the result is always algebraic. The circle constant π is transcendental, so it can never appear as the value of a certificate expression. This absence is structural, not accidental: the grammar has no constructor that could produce it.

In Recognition Science, the framework models source strength through this certificate language. The grammar's role is to keep the certificate system closed under its own operations while excluding constants that belong to downstream physical models. The wider constants module contains physical constants like the gravitational constant, but the grammar deliberately does not import them. A certificate can only assert what its own language can express.

The module proves three things in its machine-checked library of formal theorems: the golden ratio is algebraic over the rationals, every expression in the grammar evaluates to an algebraic number, and every expression certifies its own evaluated value. The third point is the practical payoff. When a certificate names a number, the expression itself is the proof that the number is legitimate. A reader can check the certificate by evaluating the expression, and the grammar guarantees the result is a well-formed algebraic value.

The consequence is a clean separation of concerns. Certificate values stay in the algebraic world where they can be checked exactly, while transcendental constants like π are reserved for the physical theories that need them. This keeps the certificate layer self-contained and auditable, without pretending that all of physics reduces to algebraic numbers.

/-- 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

/-- 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

/-- 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 expression certifies its own evaluated value. -/
theorem piFree_eval (e : LedgerExpr) : PiFree e.eval := ⟨e, rfl⟩

What this page does not claim

This module does not derive the value of the golden ratio or any physical constant. The grammar does not prove that π is transcendental; it only excludes it by construction. No claim is made about how certificates are used in practice beyond their algebraic closure property.

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: