Delta Kernel Godel Test Add Comm Syntactic Audit

The syntactic audit

Commutativity of addition, the fact that x + y = y + x for any two natural numbers, is among the first theorems a student proves. The standard textbook proof uses mathematical induction twice. A careful version keeps every induction formula free of quantifiers, meaning each formula states a fact about specific numbers. A convenient version uses a stronger induction principle, allowing the induction hypothesis to be a general statement about all numbers at once.

The Recognition Science framework's machine-checked library of formal theorems contains a declaration, addComm_syntactic_audit, that inspects the careful derivation. It establishes two syntactic facts by computation: the derivation's induction formulas are quantifier-free, and it does not use the full induction rule. This is a statement about the proof's shape, not about the truth of commutativity itself, which is already established by a separate soundness theorem.

The audit is part of a pre-registered test asking whether the framework's ledger, a discrete record of proof steps, prices derivations or merely decorates them. The test derives commutativity along two routes. The careful route is predicted to cost nothing on the ledger, while the convenient route is predicted to post a tier flag for using full induction. The declaration addCommFull_syntactic_audit confirms the second prediction: the convenient derivation does use full induction. A companion theorem, pricing_discriminates, shows the two routes receive different ledger entries.

Both routes export through a soundness theorem to the same host theorem, n + m = m + n, with a choice-free axiom closure. The tier flag measures proof-route strength, never truth. The audit thus shows the framework can distinguish between two proofs of the same theorem based on the logical power they invoke, a distinction invisible in the final result.

What the audit does not claim is broader. It does not prove commutativity of addition; that is the job of add_comm_certified. It does not claim the full arithmetization of the framework's kernel is complete; that remains open and pre-registered as future work. It does not claim the convenient route is invalid, only that it is priced differently.

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

theorem addCommFull_syntactic_audit :
    positFree addCommFull = true ∧ usesFullInd addCommFull = true := 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
CAREFUL route (`FORCED @ QF-IND`). -/
theorem add_comm_certified (n m : Nat) : n + m = m + n :=
  sound_forced addComm_forced (fun _ => 0) n m

What this page does not claim

It does not prove commutativity of addition. It does not claim the full arithmetization of the kernel is complete. It does not claim the convenient route is invalid.

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: