Delta Kernel Godel Test Add Comm Full Tier

Pricing a proof route

Commutativity of addition, the statement that x + y = y + x for all natural numbers, is one of the first theorems in arithmetic whose textbook proof needs induction twice. The Recognition Science framework contains a small formal system, a ledger (a discrete record of every inference step a derivation uses) that prices proof routes. Its question is whether the ledger merely decorates a derivation or actually measures something about how the derivation was built.

The experiment takes one fixed theorem and derives it along two genuinely different routes. Route 1 is careful: every induction formula stays quantifier-free, meaning each statement being proved by induction has no "for all" inside it. Route 2 takes the textbook shortcut: it inducts on x with the quantified formula "for all y, x + y = y + x", which lets the induction step instantiate its hypothesis at any y it likes. The framework's executable checker verifies both derivations and records a verdict for each.

The declaration addCommFull_tier establishes the verdict for Route 2. It proves, by direct computation, that the checker accepts the derivation and posts a tier flag marking that this route used full induction. A companion declaration, addComm_forced, proves the same for Route 1: accepted, but with an empty ledger, no tier flag. The pair together, in pricing_discriminates, shows the ledger distinguishes the two routes. The tier flag measures proof-route strength, never truth: both routes export, through a soundness theorem, to the same host theorem that addition commutes, with an axiom closure free of choice.

In Recognition Science, this is the pricing half of a larger program. The framework models the cost of recognition as forced, and this experiment applies that idea to its own kernel: a convenient proof route pays a recorded price, a careful one does not. The declaration does not claim the full arithmetization of the kernel, which remains open and pre-registered as future work. It does not claim that the convenient route is invalid, only that it is more expensive in the ledger's terms.

/-- ROUTE 2 VERDICT (pre-registered): the convenient route proves the SAME
formula but the ledger posts the TIER flag: `FORCED @ FULL-IND`. The
kernel priced the shortcut. -/
theorem addCommFull_tier :
    check [] addCommFull = some (.all (.all commFormula), .ofIndFull) := by
  decide

/-- ROUTE 1 VERDICT (pre-registered): the careful route is accepted with
the EMPTY ledger. `FORCED @ QF-IND`, the strongest verdict the kernel
issues, for full commutativity of addition. -/
theorem addComm_forced :
    check [] addComm = some (.all (.all commFormula), .empty) := by
  decide

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

What this page does not claim

The full arithmetization of the kernel is not established; it remains open and pre-registered as future work. The convenient route is not claimed to be invalid; it is only priced as more expensive in the ledger's terms. The tier flag does not measure the truth of the theorem, only the strength of the proof route.

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: