Delta Kernel Sound Sound Classical

The classical soundness theorem

A proof checker is a computer program that decides whether a proposed derivation is valid. The Recognition Science framework's checker, called the δ-kernel, goes one step further: it returns, alongside each accepted derivation, a ledger, a discrete record of which metatheoretic principles the derivation actually used. The central soundness theorem, sound_cond, states that if the checker accepts a derivation, then the conclusion is true in the canonical model, provided the ledger's posted principles are available. This is a conditional guarantee: the checker certifies the derivation, and the ledger tells you what outside assumptions the certification depends on.

The declaration sound_classical is one of two corollaries that fall out by instantiating the gates of sound_cond. It states that any derivation the checker accepts is true, with all three metatheoretic principles supplied from the ambient classical logic. Those principles are excluded middle (every proposition is true or false), the limited principle of omniscience (an arithmetical choice principle), and Markov's principle (a form of double-negation elimination). The theorem is proved by supplying these three principles through the gates, so the proof term for sound_classical uses Classical.choice, the axiom of choice, by design. This is the "run the whole thing over classical metatheory" reading, and it is the one place where choice legitimately enters, recorded exactly as the ledger would demand.

The theorem does not claim that every derivation is constructive. The companion corollary sound_forced makes the opposite, stronger claim: a derivation accepted with an empty ledger is true with none of the three principles, and its proof term never touches Classical.choice. The distinction matters. sound_classical is the permissive guarantee, useful for running the whole framework over classical mathematics. sound_forced is the austere guarantee, certifying that the forced fragment, the part of the framework that requires no omniscience, is sound without any choice. The two theorems together give the framework's forcing spectrum: a derivation's ledger records exactly how much classical strength its truth requires, and sound_classical is the top of that spectrum, the blanket assurance that nothing accepted is false, even if it needed classical logic to be proved.

The practical consequence is that the framework's users can trust any derivation the checker accepts, without inspecting the derivation tree. The ledger tells them what the derivation depends on, and sound_classical tells them that if they are willing to work in classical mathematics, every accepted derivation is true. The theorem does not say which derivations are constructively valid; that is the job of the ledger and sound_forced. It does not say that the framework's axioms are true in the real world; it says that the kernel's derivations are true in the canonical model, given the classical metatheory. And it does not say that the framework's physical claims, such as the forcing chain that derives the golden ratio or three spatial dimensions, are empirically confirmed; that is a separate question about the model's interpretation, not about the kernel's soundness.

/-- CLASSICAL soundness: ANY accepted derivation is true, supplying the three
principles from the ambient classical metatheory. This is the "run the kernel
over classical metatheory" reading, and it is the ONE place `Classical.choice`
legitimately enters, recorded, by design, exactly as the ledger would demand of
a maximally posit-heavy derivation. -/
theorem sound_classical {Γ : Ctx} {d : Deriv} {φ : DFormula} {O : Ledger}
    (h : check Γ d = some (φ, O)) (ρ : Env) (hΓ : CtxSat ρ Γ) :
    DFormula.sat ρ φ := by
  refine sound_cond d Γ φ O h ?_ ρ hΓ
  refine ⟨fun _ P => Classical.em P, fun _ P _ => ?_, fun _ P _ hnn => ?_⟩
  · exact (Classical.em (∃ n, P n)).elim Or.inl
      (fun hne => Or.inr (fun n hn => hne ⟨n, hn⟩))
  · exact Classical.byContradiction (fun hne => hnn hne)

/-- CLASSICAL soundness: ANY accepted derivation is true, supplying the three
principles from the ambient classical metatheory. This is the "run the kernel
over classical metatheory" reading, and it is the ONE place `Classical.choice`
legitimately enters, recorded, by design, exactly as the ledger would demand of
a maximally posit-heavy derivation. -/
theorem sound_classical {Γ : Ctx} {d : Deriv} {φ : DFormula} {O : Ledger}
    (h : check Γ d = some (φ, O)) (ρ : Env) (hΓ : CtxSat ρ Γ) :
    DFormula.sat ρ φ := by
  refine sound_cond d Γ φ O h ?_ ρ hΓ
  refine ⟨fun _ P => Classical.em P, fun _ P _ => ?_, fun _ P _ hnn => ?_⟩
  · exact (Classical.em (∃ n, P n)).elim Or.inl
      (fun hne => Or.inr (fun n hn => hne ⟨n, hn⟩))
  · exact Classical.byContradiction (fun hne => hnn hne)

/-- FORCED soundness: a derivation the kernel accepts with the EMPTY ledger is
true in the canonical model, with NONE of the three metatheoretic principles.
The gates are discharged vacuously (`Gated.empty`), so the proof term never
touches EM/LPO/MP or `Classical.choice`. `#print axioms sound_forced` is the
kernel's own σ0 / DELTA_FORCED self-audit. -/
theorem sound_forced {d : Deriv} {φ : DFormula} (h : Forced [] d φ) :
    ∀ ρ : Env, DFormula.sat ρ φ := by
  intro ρ
  refine sound_cond d [] φ Ledger.empty h Gated.empty ρ ?_
  intro ψ hψ
  cases hψ

What this page does not claim

The theorem does not claim that every accepted derivation is constructive or choice-free. The theorem does not claim that the framework's axioms are true in the real world, only that derivations are true in the canonical model given classical metatheory. The theorem does not claim that the framework's physical derivations are empirically confirmed.

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/Sound.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: