Encyclopedia Delta Delta Kernel Check
ARTICLE 4 claims 4 theorems
Delta Kernel Check
A machine-checked library that audits every derivation in Recognition Science, returning the proved formula and the exact assumptions it consumed.
The auditing checker
Delta kernel check is the auditing component of Recognition Science's machine-checked library of formal theorems. It takes a fully annotated derivation tree and either rejects it as ill-formed or returns the proved formula together with the exact set of posits consumed. The checker is total: every input produces an output, and it is structural, meaning it inspects the tree from the leaves upward with no search and no unification.
The object logic is intuitionistic Heyting arithmetic over a distinction signature, with no types and no host propositions. Derivations are data, not terms inhabiting types. The rule inventory covers the standard natural-deduction rules: hypothesis by de Bruijn index, reflexivity and Leibniz substitution, the Peano axioms including induction as an initiality schema, and the full intuitionistic propositional and quantifier rules. Three posit rules, EM, LPO, and MP, are the only rules that post to the ledger, and MP is restricted to quantifier-free matrices to keep it honestly weaker than EM.
The checker's key output is the ledger, a discrete record of which posits a derivation actually used. A derivation that checks with an empty ledger is a FORCED verdict, the kernel-native certificate of a theorem that depends on no assumptions beyond the base logic. A derivation with a non-empty ledger is a CONDITIONAL verdict, naming its posits explicitly. This distinction lets the framework separate what is forced from what is assumed, and it is what makes the audit meaningful: every proof carries its own receipt.
In plain language, the checker establishes that a proof in Recognition Science is not a black box. It is a tree you can inspect, and the checker tells you exactly what that tree proves and exactly what it leaned on. A sorry has no counterpart here: there is no rule that closes a goal without a complete sub-tree, so an incomplete derivation is simply an ill-formed tree and the checker rejects it.
The consequence is practical. When the framework claims a theorem is axiom-clean, that claim is backed by a machine-checked audit that returns an empty ledger. When a result depends on a posit, the ledger names it. The checker turns epistemic honesty from a promise into a computable property.
THEOREM 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
THEOREM 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)
THEOREM Conditional · IndisputableMonolith/DeltaKernel/Check.lean
/-- CONDITIONAL verdict: the tree checks, and the ledger names its posits. -/
def Conditional (Γ : Ctx) (d : Deriv) (φ : DFormula) (O : Ledger) : Prop :=
check Γ d = some (φ, O)
THEOREM 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
What this page does not claim
The checker does not prove that any particular derivation is correct; it only audits trees given to it. The module does not establish that the posit rules are consistent with the base logic. The FULL-IND tier flag does not resolve whether full induction is forced by initiality or is a strength step.
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 specific theorems in the framework have been audited to an empty ledger?
- What is the measured question the FULL-IND tier flag exists to answer?
- How does the ledger distinction between EM, LPO, and MP affect the strength of derived results?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM 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 checker is total: every input produces an output, and it is structural, meaning it inspects the tree from the leaves upward with no search and no unification. check · IndisputableMonolith/DeltaKernel/Check.leanTHEOREM 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 derivation that checks with an empty ledger is a FORCED verdict, the kernel-native certificate of a theorem that depends on no assumptions beyond the base logic. Forced · IndisputableMonolith/DeltaKernel/Check.leanTHEOREM Conditional · IndisputableMonolith/DeltaKernel/Check.lean
/-- CONDITIONAL verdict: the tree checks, and the ledger names its posits. -/ def Conditional (Γ : Ctx) (d : Deriv) (φ : DFormula) (O : Ledger) : Prop := check Γ d = some (φ, O)A derivation with a non-empty ledger is a CONDITIONAL verdict, naming its posits explicitly. Conditional · IndisputableMonolith/DeltaKernel/Check.leanTHEOREM 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 noneA sorry has no counterpart here: there is no rule that closes a goal without a complete sub-tree, so an incomplete derivation is simply an ill-formed tree and the checker rejects it. check · IndisputableMonolith/DeltaKernel/Check.lean