Encyclopedia Delta Delta Kernel Check Deriv
Delta Kernel Check Deriv
A derivation is a fully written-out proof tree that a machine can audit line by line, and it records exactly which assumptions each step leans on.
The derivation tree
A derivation is a complete, written-out proof in the style of natural deduction, the proof format taught in introductory logic. Every step is present: each hypothesis, each application of a rule, each conclusion. Nothing is left for a reader to fill in. The declaration Deriv in the Recognition Science framework's machine-checked library of formal theorems defines this object as a data structure, a tree whose nodes are proof steps and whose leaves are either assumptions or axioms.
The tree is annotated so that checking it requires no search and no guesswork. Each node carries enough information for a checker to verify the step by computation alone. The rules cover the standard apparatus of intuitionistic arithmetic: reflexivity of equality, substitution of equals for equals, the Peano axioms for zero and successor, recursion equations for addition and multiplication, and induction. Propositional connectives and quantifiers have their usual introduction and elimination rules. The framework's library implements this checker as a total function that either rejects a malformed tree or returns the formula proved together with a ledger, a discrete record of which special assumptions were consumed.
Three special rules, called posits, are the only steps that post to the ledger: excluded middle, the limited principle of omniscience, and Markov's principle. A proof that uses none of them checks with an empty ledger and earns the label forced. A proof that uses them checks with a nonempty ledger and is labeled conditional. This split gives a precise, machine-checked answer to the question of which results depend on which assumptions.
In Recognition Science, the framework models this distinction as the difference between what is forced and what is conditional. The declaration does not claim that any particular formula is provable; it only defines what a proof is. It does not claim that excluded middle or Markov's principle are true or false; it records when a proof uses them. It does not claim that the framework's own theorems are derivable in this system; those theorems live in the host logic of the library, not in the object logic that Deriv describes.
MODEL Deriv · IndisputableMonolith/DeltaKernel/Check.lean
/-- Fully annotated natural-deduction derivations. Annotations are chosen so
that checking requires no unification and no search: every rule's conclusion
is computable from its annotations and its sub-conclusions. -/
inductive Deriv : Type where
/-- Hypothesis: the `i`-th formula of the context. -/
| hyp : Nat → Deriv
/-- `⊢ t = t`. -/
| eqRefl : DTerm → Deriv
/-- Leibniz: from `t = s` and `φ[t/x₀]` conclude `φ[s/x₀]`.
Annotations: the hole formula `φ`, the terms `t`, `s`. -/
| eqSubst : DFormula → DTerm → DTerm → Deriv → Deriv → Deriv
/-- Distinction axiom: `⊢ ¬(S t = 0)`. A fresh distinction is not silence. -/
| succNeZero : DTerm → Deriv
/-- Distinction axiom: from `S t = S s` conclude `t = s` (injectivity). -/
| succInj : Deriv → Deriv
/-- Recursion equation: `⊢ t + 0 = t`. -/
| addZero : DTerm → Deriv
/-- Recursion equation: `⊢ t + S s = S (t + s)`. -/
| addSucc : DTerm → DTerm → Deriv
/-- Recursion equation: `⊢ t · 0 = 0`. -/
| mulZero : DTerm → Deriv
/-- Recursion equation: `⊢ t · S s = t · s + t`. -/
| mulSucc : DTerm → DTerm → Deriv
/-- Induction (initiality of ℕδ): from `φ[0/x₀]` and
`∀x (φ → φ[S x₀/x₀])` conclude `∀x φ`. Annotation: `φ`. -/
| ind : DFormula → Deriv → Deriv → Deriv
/-- From a proof of `ψ` under extra hypothesis `φ`, conclude `φ → ψ`. -/
| implIntro : DFormula → Deriv → Deriv
/-- Modus ponens. -/
| implElim : Deriv → Deriv → Deriv
| conjIntro : Deriv → Deriv → Deriv
| conjElim1 : Deriv → Deriv
| conjElim2 : Deriv → Deriv
/-- From `φ` conclude `φ ∨ ψ` (annotation: `ψ`). -/
| disjIntro1 : DFormula → Deriv → Deriv
/-- From `ψ` conclude `φ ∨ ψ` (annotation: `φ`). -/
| disjIntro2 : DFormula → Deriv → Deriv
/-- Case split: from `φ ∨ ψ`, a proof of `χ` under `φ`, and a proof of
`χ` under `ψ`, conclude `χ`. -/
| disjElim : Deriv → Deriv → Deriv → Deriv
/-- Ex falso: from `⊥` conclude any annotated `φ`. -/
| flsElim : DFormula → Deriv → Deriv
/-- Generalization: from a proof of `φ` in the lifted context conclude
`∀ φ` (the fresh eigenvariable is de Bruijn 0). -/
| allIntro : Deriv → Deriv
/-- Instantiation: from `∀ φ` conclude `φ[t/x₀]` (annotation: `t`). -/
| allElim : DTerm → Deriv → Deriv
/-- Witness: from `φ[t/x₀]` conclude `∃ φ` (annotations: `φ`, `t`). -/
| exIntro : DFormula → DTerm → Deriv → Deriv
/-- Use: from `∃ φ` and a proof of `ψ` (lifted) under `φ` in the lifted
context, conclude `ψ` (annotation: `ψ`, which must not mention the
eigenvariable; enforced by requiring the sub-proof to conclude
`ψ` lifted). -/
| exElim : DFormula → Deriv → Deriv → Deriv
/-- POSIT (EM): `⊢ φ ∨ ¬φ`. Posts `em`. -/
| emPosit : DFormula → Deriv
/-- POSIT (LPO, arithmetical form):
`⊢ (∀x (φ ∨ ¬φ)) → ((∃x φ) ∨ (∀x ¬φ))`. Posts `lpo`. -/
| lpoPosit : DFormula → Deriv
/-- POSIT (MP): `⊢ ¬¬(∃x φ) → ∃x φ` for quantifier-free `φ`. Posts `mp`. -/
| mpPosit : DFormula → Deriv
MODEL check · IndisputableMonolith/DeltaKernel/Check.lean
/-- The kernel: audit a derivation tree in a context. Returns the proved
formula and the exact posit ledger, or `none` if the tree is ill-formed.
Total, structural, and `Prop`-free: the object logic never touches the
host's propositions. -/
def check (Γ : Ctx) : Deriv → Option (DFormula × Ledger)
| .hyp i =>
match Γ[i]? with
| some φ => some (φ, .empty)
| none => none
| .eqRefl t => some (.eq t t, .empty)
| .eqSubst φ t s dEq dT =>
match check Γ dEq, check Γ dT with
| some (cEq, o₁), some (cT, o₂) =>
if cEq = DFormula.eq t s then
if cT = φ.subst 0 t then some (φ.subst 0 s, o₁.union o₂)
else none
else none
| _, _ => none
| .succNeZero t => some (.neg (.eq (.succ t) .zero), .empty)
| .succInj d =>
match check Γ d with
| some (.eq (.succ t) (.succ s), o) => some (.eq t s, o)
| _ => none
| .addZero t => some (.eq (.add t .zero) t, .empty)
| .addSucc t s => some (.eq (.add t (.succ s)) (.succ (.add t s)), .empty)
| .mulZero t => some (.eq (.mul t .zero) .zero, .empty)
| .mulSucc t s => some (.eq (.mul t (.succ s)) (.add (.mul t s) t), .empty)
| .ind φ d₀ dS =>
match check Γ d₀, check Γ dS with
| some (c₀, o₁), some (cS, o₂) =>
if c₀ = φ.subst 0 .zero then
if cS = DFormula.all (.impl φ φ.stepSucc) then
-- Stratification: induction on a quantified formula posts the
-- FULL-IND tier flag; on a QF formula it stays in the QF tier.
-- Whether FULL-IND is "forced by initiality" or a strength step
-- is the measured question the flag exists to answer.
let base := o₁.union o₂
let o := if φ.isQF then base else base.union .ofIndFull
some (.all φ, o)
else none
else none
| _, _ => none
| .implIntro φ d =>
match check (φ :: Γ) d with
| some (ψ, o) => some (.impl φ ψ, o)
| none => none
| .implElim d₁ d₂ =>
match check Γ d₁, check Γ d₂ with
| some (.impl φ ψ, o₁), some (φ', o₂) =>
if φ' = φ then some (ψ, o₁.union o₂) else none
| _, _ => none
| .conjIntro d₁ d₂ =>
match check Γ d₁, check Γ d₂ with
| some (φ, o₁), some (ψ, o₂) => some (.conj φ ψ, o₁.union o₂)
| _, _ => none
| .conjElim1 d =>
match check Γ d with
| some (.conj φ _, o) => some (φ, o)
| _ => none
| .conjElim2 d =>
match check Γ d with
| some (.conj _ ψ, o) => some (ψ, o)
| _ => none
| .disjIntro1 ψ d =>
match check Γ d with
| some (φ, o) => some (.disj φ ψ, o)
| none => none
| .disjIntro2 φ d =>
match check Γ d with
| some (ψ, o) => some (.disj φ ψ, o)
| none => none
| .disjElim d dL dR =>
match check Γ d with
| some (.disj φ ψ, o) =>
match check (φ :: Γ) dL, check (ψ :: Γ) dR with
| some (χ₁, o₁), some (χ₂, o₂) =>
if χ₁ = χ₂ then some (χ₁, (o.union o₁).union o₂) else none
| _, _ => none
| _ => none
| .flsElim φ d =>
match check Γ d with
| some (.fls, o) => some (φ, o)
| _ => none
| .allIntro d =>
match check (Γ.map (DFormula.lift 1 0)) d with
| some (φ, o) => some (.all φ, o)
| none => none
| .allElim t d =>
match check Γ d with
| some (.all φ, o) => some (φ.subst 0 t, o)
| _ => none
| .exIntro φ t d =>
match check Γ d with
| some (c, o) =>
if c = φ.subst 0 t then some (.ex φ, o) else none
| none => none
| .exElim ψ d dBody =>
match check Γ d with
| some (.ex φ, o) =>
match check (φ :: Γ.map (DFormula.lift 1 0)) dBody with
| some (ψ', o₂) =>
if ψ' = ψ.lift 1 0 then some (ψ, o.union o₂) else none
| none => none
| _ => none
| .emPosit φ => some (.disj φ φ.neg, .ofEM)
| .lpoPosit φ =>
some (.impl (.all (.disj φ φ.neg)) (.disj (.ex φ) (.all φ.neg)), .ofLPO)
| .mpPosit φ =>
if φ.isQF then some (.impl (.neg (.neg (.ex φ))) (.ex φ), .ofMP)
else none
MODEL check · IndisputableMonolith/DeltaKernel/Check.lean
/-- The kernel: audit a derivation tree in a context. Returns the proved
formula and the exact posit ledger, or `none` if the tree is ill-formed.
Total, structural, and `Prop`-free: the object logic never touches the
host's propositions. -/
def check (Γ : Ctx) : Deriv → Option (DFormula × Ledger)
| .hyp i =>
match Γ[i]? with
| some φ => some (φ, .empty)
| none => none
| .eqRefl t => some (.eq t t, .empty)
| .eqSubst φ t s dEq dT =>
match check Γ dEq, check Γ dT with
| some (cEq, o₁), some (cT, o₂) =>
if cEq = DFormula.eq t s then
if cT = φ.subst 0 t then some (φ.subst 0 s, o₁.union o₂)
else none
else none
| _, _ => none
| .succNeZero t => some (.neg (.eq (.succ t) .zero), .empty)
| .succInj d =>
match check Γ d with
| some (.eq (.succ t) (.succ s), o) => some (.eq t s, o)
| _ => none
| .addZero t => some (.eq (.add t .zero) t, .empty)
| .addSucc t s => some (.eq (.add t (.succ s)) (.succ (.add t s)), .empty)
| .mulZero t => some (.eq (.mul t .zero) .zero, .empty)
| .mulSucc t s => some (.eq (.mul t (.succ s)) (.add (.mul t s) t), .empty)
| .ind φ d₀ dS =>
match check Γ d₀, check Γ dS with
| some (c₀, o₁), some (cS, o₂) =>
if c₀ = φ.subst 0 .zero then
if cS = DFormula.all (.impl φ φ.stepSucc) then
-- Stratification: induction on a quantified formula posts the
-- FULL-IND tier flag; on a QF formula it stays in the QF tier.
-- Whether FULL-IND is "forced by initiality" or a strength step
-- is the measured question the flag exists to answer.
let base := o₁.union o₂
let o := if φ.isQF then base else base.union .ofIndFull
some (.all φ, o)
else none
else none
| _, _ => none
| .implIntro φ d =>
match check (φ :: Γ) d with
| some (ψ, o) => some (.impl φ ψ, o)
| none => none
| .implElim d₁ d₂ =>
match check Γ d₁, check Γ d₂ with
| some (.impl φ ψ, o₁), some (φ', o₂) =>
if φ' = φ then some (ψ, o₁.union o₂) else none
| _, _ => none
| .conjIntro d₁ d₂ =>
match check Γ d₁, check Γ d₂ with
| some (φ, o₁), some (ψ, o₂) => some (.conj φ ψ, o₁.union o₂)
| _, _ => none
| .conjElim1 d =>
match check Γ d with
| some (.conj φ _, o) => some (φ, o)
| _ => none
| .conjElim2 d =>
match check Γ d with
| some (.conj _ ψ, o) => some (ψ, o)
| _ => none
| .disjIntro1 ψ d =>
match check Γ d with
| some (φ, o) => some (.disj φ ψ, o)
| none => none
| .disjIntro2 φ d =>
match check Γ d with
| some (ψ, o) => some (.disj φ ψ, o)
| none => none
| .disjElim d dL dR =>
match check Γ d with
| some (.disj φ ψ, o) =>
match check (φ :: Γ) dL, check (ψ :: Γ) dR with
| some (χ₁, o₁), some (χ₂, o₂) =>
if χ₁ = χ₂ then some (χ₁, (o.union o₁).union o₂) else none
| _, _ => none
| _ => none
| .flsElim φ d =>
match check Γ d with
| some (.fls, o) => some (φ, o)
| _ => none
| .allIntro d =>
match check (Γ.map (DFormula.lift 1 0)) d with
| some (φ, o) => some (.all φ, o)
| none => none
| .allElim t d =>
match check Γ d with
| some (.all φ, o) => some (φ.subst 0 t, o)
| _ => none
| .exIntro φ t d =>
match check Γ d with
| some (c, o) =>
if c = φ.subst 0 t then some (.ex φ, o) else none
| none => none
| .exElim ψ d dBody =>
match check Γ d with
| some (.ex φ, o) =>
match check (φ :: Γ.map (DFormula.lift 1 0)) dBody with
| some (ψ', o₂) =>
if ψ' = ψ.lift 1 0 then some (ψ, o.union o₂) else none
| none => none
| _ => none
| .emPosit φ => some (.disj φ φ.neg, .ofEM)
| .lpoPosit φ =>
some (.impl (.all (.disj φ φ.neg)) (.disj (.ex φ) (.all φ.neg)), .ofLPO)
| .mpPosit φ =>
if φ.isQF then some (.impl (.neg (.neg (.ex φ))) (.ex φ), .ofMP)
else none
MODEL Forced · IndisputableMonolith/DeltaKernel/Check.lean
/-- FORCED verdict: the tree checks with an empty ledger. This is the
kernel-native σ0 / DELTA_FORCED certificate. -/
def Forced (Γ : Ctx) (d : Deriv) (φ : DFormula) : Prop :=
check Γ d = some (φ, Ledger.empty)
What this page does not claim
No particular formula is proved by the declaration itself. No claim that excluded middle, limited principle of omniscience, or Markov's principle are true or false. No claim that the framework's own theorems are derivable inside this object logic.
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/Check.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:
- Which classical theorems of arithmetic check with an empty ledger, and which require a posit?
- How does the ledger of posits relate to the forcing chain's notion of what is forced?
- What is the measured strength difference between induction on quantifier-free formulas and induction on quantified formulas?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
MODEL Deriv · IndisputableMonolith/DeltaKernel/Check.lean
/-- Fully annotated natural-deduction derivations. Annotations are chosen so that checking requires no unification and no search: every rule's conclusion is computable from its annotations and its sub-conclusions. -/ inductive Deriv : Type where /-- Hypothesis: the `i`-th formula of the context. -/ | hyp : Nat → Deriv /-- `⊢ t = t`. -/ | eqRefl : DTerm → Deriv /-- Leibniz: from `t = s` and `φ[t/x₀]` conclude `φ[s/x₀]`. Annotations: the hole formula `φ`, the terms `t`, `s`. -/ | eqSubst : DFormula → DTerm → DTerm → Deriv → Deriv → Deriv /-- Distinction axiom: `⊢ ¬(S t = 0)`. A fresh distinction is not silence. -/ | succNeZero : DTerm → Deriv /-- Distinction axiom: from `S t = S s` conclude `t = s` (injectivity). -/ | succInj : Deriv → Deriv /-- Recursion equation: `⊢ t + 0 = t`. -/ | addZero : DTerm → Deriv /-- Recursion equation: `⊢ t + S s = S (t + s)`. -/ | addSucc : DTerm → DTerm → Deriv /-- Recursion equation: `⊢ t · 0 = 0`. -/ | mulZero : DTerm → Deriv /-- Recursion equation: `⊢ t · S s = t · s + t`. -/ | mulSucc : DTerm → DTerm → Deriv /-- Induction (initiality of ℕδ): from `φ[0/x₀]` and `∀x (φ → φ[S x₀/x₀])` conclude `∀x φ`. Annotation: `φ`. -/ | ind : DFormula → Deriv → Deriv → Deriv /-- From a proof of `ψ` under extra hypothesis `φ`, conclude `φ → ψ`. -/ | implIntro : DFormula → Deriv → Deriv /-- Modus ponens. -/ | implElim : Deriv → Deriv → Deriv | conjIntro : Deriv → Deriv → Deriv | conjElim1 : Deriv → Deriv | conjElim2 : Deriv → Deriv /-- From `φ` conclude `φ ∨ ψ` (annotation: `ψ`). -/ | disjIntro1 : DFormula → Deriv → Deriv /-- From `ψ` conclude `φ ∨ ψ` (annotation: `φ`). -/ | disjIntro2 : DFormula → Deriv → Deriv /-- Case split: from `φ ∨ ψ`, a proof of `χ` under `φ`, and a proof of `χ` under `ψ`, conclude `χ`. -/ | disjElim : Deriv → Deriv → Deriv → Deriv /-- Ex falso: from `⊥` conclude any annotated `φ`. -/ | flsElim : DFormula → Deriv → Deriv /-- Generalization: from a proof of `φ` in the lifted context conclude `∀ φ` (the fresh eigenvariable is de Bruijn 0). -/ | allIntro : Deriv → Deriv /-- Instantiation: from `∀ φ` conclude `φ[t/x₀]` (annotation: `t`). -/ | allElim : DTerm → Deriv → Deriv /-- Witness: from `φ[t/x₀]` conclude `∃ φ` (annotations: `φ`, `t`). -/ | exIntro : DFormula → DTerm → Deriv → Deriv /-- Use: from `∃ φ` and a proof of `ψ` (lifted) under `φ` in the lifted context, conclude `ψ` (annotation: `ψ`, which must not mention the eigenvariable; enforced by requiring the sub-proof to conclude `ψ` lifted). -/ | exElim : DFormula → Deriv → Deriv → Deriv /-- POSIT (EM): `⊢ φ ∨ ¬φ`. Posts `em`. -/ | emPosit : DFormula → Deriv /-- POSIT (LPO, arithmetical form): `⊢ (∀x (φ ∨ ¬φ)) → ((∃x φ) ∨ (∀x ¬φ))`. Posts `lpo`. -/ | lpoPosit : DFormula → Deriv /-- POSIT (MP): `⊢ ¬¬(∃x φ) → ∃x φ` for quantifier-free `φ`. Posts `mp`. -/ | mpPosit : DFormula → DerivA derivation is a complete, written-out proof in the style of natural deduction, the proof format taught in introductory logic. Deriv · IndisputableMonolith/DeltaKernel/Check.leanMODEL check · IndisputableMonolith/DeltaKernel/Check.lean
/-- The kernel: audit a derivation tree in a context. Returns the proved formula and the exact posit ledger, or `none` if the tree is ill-formed. Total, structural, and `Prop`-free: the object logic never touches the host's propositions. -/ def check (Γ : Ctx) : Deriv → Option (DFormula × Ledger) | .hyp i => match Γ[i]? with | some φ => some (φ, .empty) | none => none | .eqRefl t => some (.eq t t, .empty) | .eqSubst φ t s dEq dT => match check Γ dEq, check Γ dT with | some (cEq, o₁), some (cT, o₂) => if cEq = DFormula.eq t s then if cT = φ.subst 0 t then some (φ.subst 0 s, o₁.union o₂) else none else none | _, _ => none | .succNeZero t => some (.neg (.eq (.succ t) .zero), .empty) | .succInj d => match check Γ d with | some (.eq (.succ t) (.succ s), o) => some (.eq t s, o) | _ => none | .addZero t => some (.eq (.add t .zero) t, .empty) | .addSucc t s => some (.eq (.add t (.succ s)) (.succ (.add t s)), .empty) | .mulZero t => some (.eq (.mul t .zero) .zero, .empty) | .mulSucc t s => some (.eq (.mul t (.succ s)) (.add (.mul t s) t), .empty) | .ind φ d₀ dS => match check Γ d₀, check Γ dS with | some (c₀, o₁), some (cS, o₂) => if c₀ = φ.subst 0 .zero then if cS = DFormula.all (.impl φ φ.stepSucc) then -- Stratification: induction on a quantified formula posts the -- FULL-IND tier flag; on a QF formula it stays in the QF tier. -- Whether FULL-IND is "forced by initiality" or a strength step -- is the measured question the flag exists to answer. let base := o₁.union o₂ let o := if φ.isQF then base else base.union .ofIndFull some (.all φ, o) else none else none | _, _ => none | .implIntro φ d => match check (φ :: Γ) d with | some (ψ, o) => some (.impl φ ψ, o) | none => none | .implElim d₁ d₂ => match check Γ d₁, check Γ d₂ with | some (.impl φ ψ, o₁), some (φ', o₂) => if φ' = φ then some (ψ, o₁.union o₂) else none | _, _ => none | .conjIntro d₁ d₂ => match check Γ d₁, check Γ d₂ with | some (φ, o₁), some (ψ, o₂) => some (.conj φ ψ, o₁.union o₂) | _, _ => none | .conjElim1 d => match check Γ d with | some (.conj φ _, o) => some (φ, o) | _ => none | .conjElim2 d => match check Γ d with | some (.conj _ ψ, o) => some (ψ, o) | _ => none | .disjIntro1 ψ d => match check Γ d with | some (φ, o) => some (.disj φ ψ, o) | none => none | .disjIntro2 φ d => match check Γ d with | some (ψ, o) => some (.disj φ ψ, o) | none => none | .disjElim d dL dR => match check Γ d with | some (.disj φ ψ, o) => match check (φ :: Γ) dL, check (ψ :: Γ) dR with | some (χ₁, o₁), some (χ₂, o₂) => if χ₁ = χ₂ then some (χ₁, (o.union o₁).union o₂) else none | _, _ => none | _ => none | .flsElim φ d => match check Γ d with | some (.fls, o) => some (φ, o) | _ => none | .allIntro d => match check (Γ.map (DFormula.lift 1 0)) d with | some (φ, o) => some (.all φ, o) | none => none | .allElim t d => match check Γ d with | some (.all φ, o) => some (φ.subst 0 t, o) | _ => none | .exIntro φ t d => match check Γ d with | some (c, o) => if c = φ.subst 0 t then some (.ex φ, o) else none | none => none | .exElim ψ d dBody => match check Γ d with | some (.ex φ, o) => match check (φ :: Γ.map (DFormula.lift 1 0)) dBody with | some (ψ', o₂) => if ψ' = ψ.lift 1 0 then some (ψ, o.union o₂) else none | none => none | _ => none | .emPosit φ => some (.disj φ φ.neg, .ofEM) | .lpoPosit φ => some (.impl (.all (.disj φ φ.neg)) (.disj (.ex φ) (.all φ.neg)), .ofLPO) | .mpPosit φ => if φ.isQF then some (.impl (.neg (.neg (.ex φ))) (.ex φ), .ofMP) else noneThe tree is annotated so that checking it requires no search and no guesswork. check · IndisputableMonolith/DeltaKernel/Check.leanMODEL check · IndisputableMonolith/DeltaKernel/Check.lean
/-- The kernel: audit a derivation tree in a context. Returns the proved formula and the exact posit ledger, or `none` if the tree is ill-formed. Total, structural, and `Prop`-free: the object logic never touches the host's propositions. -/ def check (Γ : Ctx) : Deriv → Option (DFormula × Ledger) | .hyp i => match Γ[i]? with | some φ => some (φ, .empty) | none => none | .eqRefl t => some (.eq t t, .empty) | .eqSubst φ t s dEq dT => match check Γ dEq, check Γ dT with | some (cEq, o₁), some (cT, o₂) => if cEq = DFormula.eq t s then if cT = φ.subst 0 t then some (φ.subst 0 s, o₁.union o₂) else none else none | _, _ => none | .succNeZero t => some (.neg (.eq (.succ t) .zero), .empty) | .succInj d => match check Γ d with | some (.eq (.succ t) (.succ s), o) => some (.eq t s, o) | _ => none | .addZero t => some (.eq (.add t .zero) t, .empty) | .addSucc t s => some (.eq (.add t (.succ s)) (.succ (.add t s)), .empty) | .mulZero t => some (.eq (.mul t .zero) .zero, .empty) | .mulSucc t s => some (.eq (.mul t (.succ s)) (.add (.mul t s) t), .empty) | .ind φ d₀ dS => match check Γ d₀, check Γ dS with | some (c₀, o₁), some (cS, o₂) => if c₀ = φ.subst 0 .zero then if cS = DFormula.all (.impl φ φ.stepSucc) then -- Stratification: induction on a quantified formula posts the -- FULL-IND tier flag; on a QF formula it stays in the QF tier. -- Whether FULL-IND is "forced by initiality" or a strength step -- is the measured question the flag exists to answer. let base := o₁.union o₂ let o := if φ.isQF then base else base.union .ofIndFull some (.all φ, o) else none else none | _, _ => none | .implIntro φ d => match check (φ :: Γ) d with | some (ψ, o) => some (.impl φ ψ, o) | none => none | .implElim d₁ d₂ => match check Γ d₁, check Γ d₂ with | some (.impl φ ψ, o₁), some (φ', o₂) => if φ' = φ then some (ψ, o₁.union o₂) else none | _, _ => none | .conjIntro d₁ d₂ => match check Γ d₁, check Γ d₂ with | some (φ, o₁), some (ψ, o₂) => some (.conj φ ψ, o₁.union o₂) | _, _ => none | .conjElim1 d => match check Γ d with | some (.conj φ _, o) => some (φ, o) | _ => none | .conjElim2 d => match check Γ d with | some (.conj _ ψ, o) => some (ψ, o) | _ => none | .disjIntro1 ψ d => match check Γ d with | some (φ, o) => some (.disj φ ψ, o) | none => none | .disjIntro2 φ d => match check Γ d with | some (ψ, o) => some (.disj φ ψ, o) | none => none | .disjElim d dL dR => match check Γ d with | some (.disj φ ψ, o) => match check (φ :: Γ) dL, check (ψ :: Γ) dR with | some (χ₁, o₁), some (χ₂, o₂) => if χ₁ = χ₂ then some (χ₁, (o.union o₁).union o₂) else none | _, _ => none | _ => none | .flsElim φ d => match check Γ d with | some (.fls, o) => some (φ, o) | _ => none | .allIntro d => match check (Γ.map (DFormula.lift 1 0)) d with | some (φ, o) => some (.all φ, o) | none => none | .allElim t d => match check Γ d with | some (.all φ, o) => some (φ.subst 0 t, o) | _ => none | .exIntro φ t d => match check Γ d with | some (c, o) => if c = φ.subst 0 t then some (.ex φ, o) else none | none => none | .exElim ψ d dBody => match check Γ d with | some (.ex φ, o) => match check (φ :: Γ.map (DFormula.lift 1 0)) dBody with | some (ψ', o₂) => if ψ' = ψ.lift 1 0 then some (ψ, o.union o₂) else none | none => none | _ => none | .emPosit φ => some (.disj φ φ.neg, .ofEM) | .lpoPosit φ => some (.impl (.all (.disj φ φ.neg)) (.disj (.ex φ) (.all φ.neg)), .ofLPO) | .mpPosit φ => if φ.isQF then some (.impl (.neg (.neg (.ex φ))) (.ex φ), .ofMP) else noneThree special rules, called posits, are the only steps that post to the ledger. check · IndisputableMonolith/DeltaKernel/Check.leanMODEL Forced · IndisputableMonolith/DeltaKernel/Check.lean
/-- FORCED verdict: the tree checks with an empty ledger. This is the kernel-native σ0 / DELTA_FORCED certificate. -/ def Forced (Γ : Ctx) (d : Deriv) (φ : DFormula) : Prop := check Γ d = some (φ, Ledger.empty)A proof that uses none of them checks with an empty ledger and earns the label forced. Forced · IndisputableMonolith/DeltaKernel/Check.lean