Delta Kernel Godel Test

The Gödel test

The ledger, a discrete record of recognition events, prices every derivation it checks. The Gödel test asks a pointed question: does that price measure the route a proof takes, or merely decorate a finished result? The test takes one fixed theorem, the commutativity of addition, and derives it along two genuinely different routes. The theorem itself is the same; the routes differ in how much logical power they use.

The classical target is the first theorem of arithmetic whose textbook proof reaches for induction twice. The careful route keeps every induction formula quantifier-free, proving a helper statement about successors first. The convenient route uses the textbook shortcut: induction on one variable with the quantified formula for all values of the other. That shortcut lets the induction step instantiate its hypothesis at any value it likes, which is exactly the convenience full induction buys.

In Recognition Science, the framework's machine-checked library of formal theorems runs both routes through its executable checker. The pricing discriminates: the careful route posts an empty ledger, while the convenient route posts a tier flag marking that it used full induction. Syntactic scans confirm the difference is grep-auditable. Both routes then export through soundness to the same host theorem with a choice-free axiom closure. The tier flag measures proof-route strength, never truth.

The result is a proof of concept: the ledger does not merely decorate, it prices. A reader can now see that the framework's cost mechanism distinguishes between a careful derivation and a convenient one, even when both land on the same theorem. This is the pricing half of the Gödel program; the full arithmetization of the kernel's own soundness remains open and pre-registered as future work.

theorem pricing_discriminates :
    (check [] addComm = some (.all (.all commFormula), .empty)) ∧
    (check [] addCommFull = some (.all (.all commFormula), .ofIndFull)) :=
  ⟨addComm_forced, addCommFull_tier⟩

/-- Commutativity of `Nat` addition, certified through the δ-kernel's
CAREFUL route (`FORCED @ QF-IND`). -/
theorem add_comm_certified (n m : Nat) : n + m = m + n :=
  sound_forced addComm_forced (fun _ => 0) n m

/-- Commutativity of `Nat` addition, certified through the δ-kernel's
CONVENIENT route (`FORCED @ FULL-IND`). Still choice-free: the tier flag
measures proof-route strength, not metatheoretic consumption. -/
theorem add_comm_full_certified (n m : Nat) : n + m = m + n := by
  have h := sound_cond addCommFull [] (.all (.all commFormula)) Ledger.ofIndFull
    addCommFull_tier Gated.ofIndFull (fun _ => 0) (fun ψ hψ => by cases hψ)
  exact h n m

theorem addComm_syntactic_audit :
    positFree addComm = true ∧ usesFullInd addComm = false := by
  decide

What this page does not claim

The full Gödel program is not established; only the pricing half is verified. The tier flag does not affect the truth of the commutativity theorem. No claim is made about the framework's kernel being able to prove its own soundness.

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/DeltaKernel/GodelTest.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: