Delta Kernel Godel Test Add Comm Full Syntactic Audit

The pricing audit

Commutativity of addition, the fact that x + y = y + x for any two natural numbers, is usually the first theorem a student proves by induction. The textbook proof is short, but it hides a choice: the induction hypothesis can be stated narrowly, for one fixed number at a time, or broadly, as a claim about every number at once. The distinction matters to anyone who wants to know what a proof actually costs, and it is the subject of this audit.

The framework under examination is a ledger, a discrete record of proof steps, each checked by a small executable kernel. The audit takes one theorem, commutativity, and derives it along two routes. The careful route keeps every induction formula quantifier-free, proving a helper lemma first. The convenient route uses the textbook shortcut: it states the induction hypothesis with a quantifier, which lets the proof instantiate it at any number it likes. This is exactly the extra power that full induction buys.

The declaration addCommFull_syntactic_audit establishes, by direct computation, that the convenient route's proof term has two properties at once. First, its induction formulas contain no positive quantifiers, so the proof is not hiding a stronger axiom in its statement. Second, it does use the full induction rule, so the proof is genuinely taking the shortcut. The same audit on the careful route returns the opposite second answer: no full induction. The two routes are therefore distinguishable by a purely syntactic scan, without running the kernel.

This matters because the ledger's purpose is to price derivations, not just to record them. A tier flag attached to a proof, here marking the use of full induction, measures the strength of the proof route, not the truth of the conclusion. Both routes export through a soundness theorem to the same host theorem about natural numbers, with a choice-free axiom closure. The convenient route is not more true; it is merely more powerful in how it gets there.

What the audit does not claim is just as important. It does not prove that the full arithmetization of the ledger, encoding derivations inside the natural numbers and proving the kernel's own soundness, is complete. That remains open and is pre-registered as future work. The audit is the pricing half of a larger program, a test of whether the ledger can distinguish proof routes at all. It answers that test in the affirmative, for this one theorem, by a method that any reader can re-check by hand.

theorem addCommFull_syntactic_audit :
    positFree addCommFull = true ∧ usesFullInd addCommFull = true := by
  decide

theorem addCommFull_syntactic_audit :
    positFree addCommFull = true ∧ usesFullInd addCommFull = true := by
  decide

theorem addCommFull_syntactic_audit :
    positFree addCommFull = true ∧ usesFullInd addCommFull = true := by
  decide

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

What this page does not claim

The full arithmetization of the kernel, encoding Deriv inside the natural numbers, is not proved here. The audit does not show that the convenient route is more true than the careful route. No claim is made that the ledger can price every possible proof route, only this one pair.

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: