Encyclopedia Delta Delta Kernel Sound Sound Is Forced

ARTICLE 4 claims 4 theorems

Delta Kernel Sound Sound Is Forced

A machine-checked proof system certifies its own strongest guarantee: derivations that avoid omniscience principles are true without them.

Verify this page

The kernel's self-audit

A proof checker is a machine that decides whether a formal derivation is valid. The Recognition Science framework builds one, and its declaration sound_isForced certifies the checker itself. The theorem states: if the checker accepts a derivation from no assumptions, and the derivation's ledger records no use of three classical omniscience principles, then the conclusion is true in the framework's canonical model. The ledger is a discrete record of which logical principles a proof actually used. The three principles are excluded middle, the limited principle of omniscience, and Markov's principle, each a way of asserting existence without constructing an example.

The guarantee is conditional and precise. The full soundness theorem sound_cond says that any accepted derivation is true, provided the ledger's recorded principles are supplied. The sound_isForced corollary instantiates that condition: when the ledger posts none of the three principles, the proof term never touches them or Classical.choice. The proof is constructive, meaning it does not rely on the law of excluded middle in the metatheory. This is the kernel's own self-audit, a proof about proofs, and it is machine-checked in the framework's library of formal theorems.

The theorem does not claim that every accepted derivation is constructive. The companion corollary sound_classical supplies all three principles from the ambient classical metatheory, so any derivation, however it uses omniscience, is still true in the model. The induction tier flag is orthogonal: full induction is sound regardless, and the flag exists to measure usage, not to gate truth. The theorem also does not claim the framework's physical conclusions, such as the golden ratio or three spatial dimensions, are constructively proved. It certifies the logical kernel, not the empirical content of the theories built on it.

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ψ
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_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ψ
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)

What this page does not claim

The theorem does not claim that every accepted derivation is constructive. The theorem does not claim the framework's physical conclusions are constructively proved. The theorem does not claim the induction tier flag affects soundness.

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