Encyclopedia Delta Delta Kernel Sound

ARTICLE 4 claims 4 theorems

Delta Kernel Sound

A proof checker that accounts for the strength of its own assumptions, and certifies which conclusions need none.

Verify this page

The kernel's self-audit

Delta kernel sound is the part of the Recognition Science framework where the proof checker certifies itself. The checker accepts derivations and returns a ledger, a discrete record of which logical principles each derivation actually used. The soundness theorem, proved in the machine-checked library of formal theorems, states that every derivation the checker accepts is true in the framework's canonical model, and that the ledger is an honest upper bound on the metatheoretic strength the truth of the conclusion requires.

The central theorem, sound_cond, is conditional: it supplies each of three metatheoretic principles, excluded middle, the limited principle of omniscience, and Markov's principle, only when the ledger posted the matching flag. Two corollaries fall out by instantiating the gates. The first, sound_forced, covers a derivation the kernel accepts with an empty ledger: it is true with none of the three principles, and the proof term never touches classical choice. The second, sound_classical, covers any accepted derivation, supplying all three principles from the ambient classical metatheory. This is the one place classical choice enters, recorded by design.

The induction tier flag is orthogonal to soundness. Full induction is sound in the canonical model regardless, because the model genuinely satisfies the induction schema. The flag exists to measure which theorems used it, not to gate their truth. That is why soundness does not branch on it. A third theorem, sound_isForced, accepts every full-induction proof whose ledger posts no omniscience principle, characterizing the forced fragment as Heyting Arithmetic: intuitionistic predicate logic, the Peano axioms, and full induction.

In plain language, the framework's checker does not hide its assumptions. A derivation that needs no classical principles is certified without them, and a derivation that does need them says so in its ledger. The kernel's own soundness proof is the same kind of object it checks, and its forced fragment is certified without omniscience.

THEOREM sound_cond · IndisputableMonolith/DeltaKernel/Sound.lean
sound_cond · IndisputableMonolith/DeltaKernel/Sound.lean:199 · truncated 
theorem sound_cond : ∀ (d : Deriv) (Γ : Ctx) (φ : DFormula) (O : Ledger),
    check Γ d = some (φ, O) → Gated O → ∀ ρ : Env, CtxSat ρ Γ → DFormula.sat ρ φ := by
  intro d
  induction d with
  | hyp i =>
      intro Γ φ O hchk hG ρ hΓ
      simp only [check] at hchk
      cases hg : Γ[i]? with
      | none => simp [hg] at hchk
      | some ψ =>
          simp only [hg, Option.some.injEq, Prod.mk.injEq] at hchk
          obtain ⟨hφ, _⟩ := hchk
          subst hφ
          exact hΓ ψ (mem_of_getElem? hg)
  | eqRefl t =>
      intro Γ φ O hchk hG ρ hΓ
      simp only [check, Option.some.injEq, Prod.mk.injEq] at hchk
      obtain ⟨hc, _⟩ := hchk
      subst hc
      rfl
  | eqSubst hole t s dEq dT ihEq ihT =>
      intro Γ φ O hchk hG ρ hΓ
      simp only [check] at hchk
      cases hdE : check Γ dEq with
      | none => simp [hdE] at hchk
      | some cpE =>
          obtain ⟨cEq, o₁⟩ := cpE
          cases hdT : check Γ dT with
          | none => simp [hdE, hdT] at hchk
          | some cpT =>
              obtain ⟨cT, o₂⟩ := cpT
              simp only [hdE, hdT] at hchk
              split at hchk
              · rename_i h1
                split at hchk
                · rename_i h2
                  simp only [Option.some.injEq, Prod.mk.injEq] at hchk
                  obtain ⟨hc, hO⟩ := hchk
                  subst hc; subst hO
                  have HE := ihEq Γ cEq o₁ hdE (Gated.union_left hG) ρ hΓ
                  have HT := ihT Γ cT o₂ hdT (Gated.union_right hG) ρ hΓ
                  rw [h1] at HE
                  rw [h2] at HT
                  have hts : t.eval ρ = s.eval ρ := HE
                  rw [DFormula.sat_subst0] at HT
                  rw [DFormula.sat_subst0]
                  rw [← hts]
                  exact HT
                · nomatch hchk
              · nomatch hchk
  | succNeZero t =>
      intro Γ φ O hchk hG ρ hΓ
      simp only [check, Option.some.injEq, Prod.mk.injEq] at hchk
      obtain ⟨hc, _⟩ := hchk
      subst hc
      simp only [DFormula.sat, DFormula.neg, DTerm.eval]
      omega
  | succInj d ih =>
      intro Γ φ O hchk hG ρ hΓ
      simp only [check] at hchk
      cases hd : check Γ d with
      | none => simp [hd] at hchk
      | some cp =>
          obtain ⟨c, o⟩ := cp
          cases c with
          | eq a b =>
              cases a with
              | succ ta =>
                  cases b with
                  | succ tb =>
                      simp only [hd, Option.some.injEq, Prod.mk.injEq] at hchk
                      obtain ⟨hc, hO⟩ := hchk
                      subst hc; subst hO
                      have H := ih Γ (DFormula.eq (DTerm.succ ta) (DTerm.succ tb)) o hd hG ρ hΓ
                      simp only [DFormula.sat, DTerm.eval] at H ⊢
                      omega
                  | var _ => simp [hd] at hchk
                  | zero => simp [hd] at hchk
                  | add _ _ => simp [hd] at hchk
                  | mul _ _ => simp [hd] at hchk
              | var _ => simp [hd] at hchk
              | zero => simp [hd] at hchk
              | add _ _ => simp [hd] at hchk
              | mul _ _ => simp [hd] at hchk
          | fls => simp [hd] at hchk
          | conj _ _ => simp [hd] at hchk
          | disj _ _ => simp [hd] at hchk
          | impl _ _ => simp [hd] at hchk
          | all _ => simp [hd] at hchk
          | ex _ => simp [hd] at hchk
  | addZero t =>
      intro Γ φ O hchk hG ρ hΓ
      simp only [check, Option.some.injEq, Prod.mk.injEq] at hchk
      obtain ⟨hc, _⟩ := hchk
      subst hc
      simp only [DFormula.sat, DTerm.eval]
      omega
  | addSucc t s =>
      intro Γ φ O hchk hG ρ hΓ
      simp only [check, Option.some.injEq, Prod.mk.injEq] at hchk
      obtain ⟨hc, _⟩ := hchk
      subst hc
      simp only [DFormula.sat, DTerm.eval]
      omega
  | mulZero t =>
      intro Γ φ O hchk hG ρ hΓ
      simp only [check, Option.some.injEq, Prod.mk.injEq] at hchk
      obtain ⟨hc, _⟩ := hchk
      subst hc
      simp [DFormula.sat, DTerm.eval]
  | mulSucc t s =>
      intro Γ φ O hchk hG ρ hΓ
      simp only [check, Option.some.injEq, Prod.mk.injEq] at hchk
      obtain ⟨hc, _⟩ := hchk
      subst hc
      simp only [DFormula.sat, DTerm.eval]
      exact Nat.mul_succ (t.eval ρ) (s.eval ρ)
  | ind hole d0 dS ih0 ihS =>
      intro Γ φ O hchk hG ρ hΓ
      simp only [check] at hchk
      cases hd0 : check Γ d0 with
      | none => simp [hd0] at hchk
      | some cp0 =>
          obtain ⟨c0, o₁⟩ := cp0
          cases hdS : check Γ dS with
          | none => simp [hd0, hdS] at hchk
          | some cpS =>
              obtain ⟨cS, o₂⟩ := cpS
              simp only [hd0, hdS] at hchk
              split at hchk
              · rename_i hc0
                split at hchk
                · rename_i hcS
                  simp only [Option.some.injEq, Prod.mk.injEq] at hchk
                  obtain ⟨hc, hO⟩ := hchk
                  subst hc
                  have hbase : Gated (o₁.union o₂) := by
                    split at hO
                    · subst hO; exact hG
                    · subst hO; exact Gated.union_left hG
                  have H0 := ih0 Γ c0 o₁ hd0 (Gated.union_left hbase) ρ hΓ
                  have HS := ihS Γ cS o₂ hdS (Gated.union_right hbase) ρ hΓ
                  rw [hc0] at H0
                  rw [hcS] at HS
                  have H0' := (DFormula.sat_subst0 hole DTerm.zero ρ).mp H0
                  simp only [DFormula.sat] at HS
                  simp only [DFormula.sat]
                  intro n
                  induction n with
                  | zero => exact H0'
                  | succ k ihk => exact (DFormula.sat_stepSucc hole k ρ).mp (HS k ihk)
                · nomatch hchk
              · nomatch hchk
  | implIntro hole d ih =>
      intro Γ φ O hchk hG ρ hΓ
      simp only [check] at hchk
      cases hd : check (hole :: Γ) d with
      | none => simp [hd] at hchk
      | some cp =>
          obtain ⟨c, o⟩ := cp
          simp only [hd, Option.some.injEq, Prod.mk.injEq] at hchk
          obtain ⟨hc, hO⟩ := hchk
          subst hc; subst hO
          simp only [DFormula.sat]
          intro hhole
          exact ih (hole :: Γ) c o hd hG ρ (CtxSat.cons hhole hΓ)
  | implElim d1 d2 ih1 ih2 =>
      intro Γ φ O hchk hG ρ hΓ
      simp only [check] at hchk
      cases hd1 : check Γ d1 with
      | none => simp [hd1] at hchk
      | some cp1 =>
          obtain ⟨c1, o₁⟩ := cp1
          cases hd2 : check Γ d2 with
          | none => simp [hd1, hd2] at hchk
          | some cp2 =>
              obtain ⟨c2, o₂⟩ := cp2
              cases c1 with
              | impl a b =>
                  simp only [hd1, hd2] at hchk
                  split at hchk
                  · rename_i hcond
                    simp only [Option.some.injEq, Prod.mk.injEq] at hchk
                    obtain ⟨hb, hO⟩ := hchk
                    subst hb; subst hO
                    have H1 := ih1 Γ (DFormula.impl a b) o₁ hd1 (Gated.union_left hG) ρ hΓ
                    have H2 := ih2 Γ c2 o₂ hd2 (Gated.union_right hG) ρ hΓ
                    rw [hcond] at H2
                    exact H1 H2
                  · nomatch hchk
              | eq _ _ => simp [hd1, hd2] at hchk
              | fls => simp [hd1, hd2] at hchk
              | conj _ _ => simp [hd1, hd2] at hchk
              | disj _ _ => simp [hd1, hd2] at hchk
              | all _ => simp [hd1, hd2] at hchk
              | ex _ => simp [hd1, hd2] at hchk
  | conjIntro d1 d2 ih1 ih2 =>
      intro Γ φ O hchk hG ρ hΓ
      simp only [check] at hchk
      cases hd1 : check Γ d1 with
      | none => simp [hd1] at hchk
      | some cp1 =>
          obtain ⟨c1, o₁⟩ := cp1
          cases hd2 : check Γ d2 with
          | none => simp [hd1, hd2] at hchk
          | some cp2 =>
              obtain ⟨c2, o₂⟩ := cp2
              simp only [hd1, hd2, Option.some.injEq, Prod.mk.injEq] at hchk
              obtain ⟨hc, hO⟩ := hchk
              subst hc; subst hO
              have H1 := ih1 Γ c1 o₁ hd1 (Gated.union_left hG) ρ hΓ
              have H2 := ih2 Γ c2 o₂ hd2 (Gated.union_right hG) ρ hΓ
              exact ⟨H1, H2⟩
  | conjElim1 d ih =>
      intro Γ φ O hchk hG ρ hΓ
      simp only [check] at hchk
      cases hd : check Γ d with
      | none => simp [hd] at hchk
      | some cp =>
          obtain ⟨c, o⟩ := cp
          cases c with
          | conj a b =>
              simp only [hd, Option.some.injEq, Prod.mk.injEq] at hchk
              obtain ⟨hc, hO⟩ := hchk
              subst hc; subst hO
              have H := ih Γ (DFormula.conj a b) o hd hG ρ hΓ
              exact H.1
          | eq _ _ => simp [hd] at hchk
          | fls => simp [hd] at hchk
          | disj _ _ => simp [hd] at hchk
          | impl _ _ => simp [hd] at hchk
          | all _ => simp [hd] at hchk
          | ex _ => simp [hd] at hchk
  | conjElim2 d ih =>
      intro Γ φ O hchk hG ρ hΓ
      simp only [check] at hchk
      cases hd : check Γ d with
      | none => simp [hd] at hchk
      | some cp =>
          obtain ⟨c, o⟩ := cp
          cases c with
          | conj a b =>
              simp only [hd, Option.some.injEq, Prod.mk.injEq] at hchk
              obtain ⟨hc, hO⟩ := hchk
              subst hc; subst hO
              have H := ih Γ (DFormula.conj a b) o hd hG ρ hΓ
              exact H.2
          | eq _ _ => simp [hd] at hchk
          | fls => simp [hd] at hchk
          | disj _ _ => simp [hd] at hchk
          | impl _ _ => simp [hd] at hchk
          | all _ => simp [hd] at hchk
          | ex _ => simp [hd] at hchk
  | disjIntro1 ψf d ih =>
      intro Γ φ O hchk hG ρ hΓ
      simp only [check] at hchk
      cases hd : check Γ d with
      | none => simp [hd] at hchk
      | some cp =>
          obtain ⟨c, o⟩ := cp
          simp only [hd, Option.some.injEq, Prod.mk.injEq] at hchk
          obtain ⟨hc, hO⟩ := hchk
          subst hc; subst hO
          have H := ih Γ c o hd hG ρ hΓ
          exact Or.inl H
  | disjIntro2 φf d ih =>
      intro Γ φ O hchk hG ρ hΓ
      simp only [check] at hchk
      cases hd : check Γ d with
      | none => simp [hd] at hchk
      | some cp =>
          obtain ⟨c, o⟩ := cp
          simp only [hd, Option.some.injEq, Prod.mk.injEq] at hchk
          obtain ⟨hc, hO⟩ := hchk
          subst hc; subst hO
          have H := ih Γ c o hd hG ρ hΓ
          exact Or.inr H
  | disjElim d dL dR ih ihL ihR =>
      intro Γ φ O hchk hG ρ hΓ
      simp only [check] at hchk
      cases hd : check Γ d with
      | none => simp [hd] at hchk
      | some cp =>
          obtain ⟨c, o⟩ := cp
          cases c with
          | disj a b =>
              simp only [hd] at hchk
              cases hdL : check (a :: Γ) dL with
              | none => simp [hdL] at hchk
              | some cpL =>
                  obtain ⟨χ1, o₁⟩ := cpL
                  cases hdR : check (b :: Γ) dR with
                  | none => simp [hdL, hdR] at hchk
                  | some cpR =>
                      obtain ⟨χ2, o₂⟩ := cpR
                      simp only [hdL, hdR] at hchk
                      split at hchk
                      · rename_i hchi
                        simp only [Option.some.injEq, Prod.mk.injEq] at hchk
                        obtain ⟨hc, hO⟩ := hchk
                        subst hc; subst hO
                        have Hd := ih Γ (DFormula.disj a b) o hd
                          (Gated.union_left (Gated.union_left hG)) ρ hΓ
                        simp only [DFormula.sat] at Hd
                        rcases Hd with ha | hb
                        · exact ihL (a :: Γ) χ1 o₁ hdL
                            (Gated.union_right (Gated.union_left hG)) ρ (CtxSat.cons ha hΓ)
                        · have HR := ihR (b :: Γ) χ2 o₂ hdR
                            (Gated.union_right hG) ρ (CtxSat.cons hb hΓ)
                          rw [hchi]
                          exact HR
                      · nomatch hchk
          | eq _ _ => simp [hd] at hchk
          | fls => simp [hd] at hchk
          | conj _

-- … truncated for the page; open the module for the rest.
THEOREM sound_forced · IndisputableMonolith/DeltaKernel/Sound.lean
sound_forced · IndisputableMonolith/DeltaKernel/Sound.lean:663 
/-- 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ψ
THEOREM sound_classical · IndisputableMonolith/DeltaKernel/Sound.lean
sound_classical · IndisputableMonolith/DeltaKernel/Sound.lean:706 
/-- 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)
THEOREM sound_isForced · IndisputableMonolith/DeltaKernel/Sound.lean
sound_isForced · IndisputableMonolith/DeltaKernel/Sound.lean:686 
/-- FORCED-VERDICT soundness: a derivation the kernel accepts with an
`isForced` ledger (no EM/LPO/MP posited, induction TIER unrestricted) is true
in the canonical model, with none of the three metatheoretic principles.
Unlike `sound_forced`, this does not pin `indFull = false`, so it accepts every
full-induction (quantified-formula) proof.

The forced fragment characterized by `isForced` is Heyting Arithmetic:
intuitionistic predicate logic, the Peano axioms, and full induction. The
posits EM/LPO/MP are the classical or omniscience extensions beyond HA.
Pinning `indFull = false` would reject HA proofs that induct on a quantified
formula. This theorem is choice-free (`Gated.of_isForced` discharges the gate
vacuously), so `#print axioms` matches `sound_forced`. -/
theorem sound_isForced {d : Deriv} {φ : DFormula} {O : Ledger}
    (h : check [] d = some (φ, O)) (hf : O.isForced = true) :
    ∀ ρ : Env, DFormula.sat ρ φ := by
  intro ρ
  refine sound_cond d [] φ O h (Gated.of_isForced hf) ρ ?_
  intro ψ hψ
  cases hψ

What this page does not claim

This answer does not claim that the framework's checker is sound in the sense of a conventional mathematical proof assistant. This answer does not claim that the three metatheoretic principles are the only assumptions the framework relies on. This answer does not claim that the canonical model Nδ is a model of all of Recognition Science.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND