Encyclopedia Delta Delta Kernel Check Conditional

ARTICLE 4 claims 4 theorems

Delta Kernel Check Conditional

A machine-checked proof can carry a receipt: the exact assumptions it consumed, named one by one.

Verify this page

The conditional verdict

A proof checker is a referee. It looks at a proposed derivation, a tree of inference steps, and decides whether the steps are legal. The Recognition Science framework's checker, called check, goes one step further. It returns not just a verdict but a ledger: a discrete record of exactly which non-logical assumptions the derivation used. The declaration Conditional names the situation where the tree passes inspection and the ledger is not empty. It is the honest middle case between a fully forced proof and a rejected one.

In the framework's own terms, a derivation is data, not a type. It is a fully annotated natural-deduction tree for intuitionistic Heyting arithmetic, built over a signature of distinctions. The checker is a total function that takes a context and a derivation and returns either nothing, meaning the tree is ill-formed, or a pair: the formula proved and the set of posits consumed. The posits, the only rules that post to the ledger, are three classical principles: excluded middle, the limited principle of omniscience, and Markov's principle, with Markov restricted to quantifier-free matrices so it stays honestly weaker than excluded middle.

What Conditional establishes is precise. It says that a given derivation, in a given context, checks successfully and that the ledger of posits is exactly a specified set. It does not say the formula is true unconditionally. It does not say the posits are needed, only that they were used. A derivation that uses excluded middle to prove a formula gets a ledger entry for it; a derivation that avoids it gets an empty ledger and earns the stronger label Forced. The distinction matters because the framework treats forced results, those with no posit entries, as its kernel-native certificate of unconditional derivation.

The declaration also makes a structural promise about the checker itself. The checker is total, meaning it always returns an answer. It is structural, meaning every rule's conclusion is computable from its annotations and sub-conclusions, with no unification and no search. And it is Prop-free: the object logic never touches the host's propositions. A sorry, an incomplete proof that closes a goal without a sub-tree, has no counterpart here. An incomplete derivation is simply an ill-formed tree, and the checker rejects it.

In Recognition Science, this is the auditing layer. The framework's large claims, such as the forcing chain that derives the golden ratio and three spatial dimensions, rest on machine-checked proofs. The Conditional declaration is the tool that lets those proofs carry their own receipts, so a reader can see exactly which classical principles, if any, a given result depends on. It does not by itself prove any arithmetic statement. It is the referee's report, not the game.

THEOREM Conditional · IndisputableMonolith/DeltaKernel/Check.lean
Conditional · IndisputableMonolith/DeltaKernel/Check.lean:219 
/-- 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 Forced · IndisputableMonolith/DeltaKernel/Check.lean
Forced · IndisputableMonolith/DeltaKernel/Check.lean:214 
/-- 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 check · IndisputableMonolith/DeltaKernel/Check.lean
check · IndisputableMonolith/DeltaKernel/Check.lean:103 
/-- 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 check · IndisputableMonolith/DeltaKernel/Check.lean
check · IndisputableMonolith/DeltaKernel/Check.lean:103 
/-- 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

Conditional does not prove any arithmetic statement itself. Conditional does not say the posits in the ledger are necessary, only that they were used. The checker's totality does not imply that every formula is decidable.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND