Encyclopedia Delta Delta Kernel Sigma Uses Full Ind Eq Scan Ind Full

ARTICLE 3 claims 3 theorems

Delta Kernel Sigma Uses Full Ind Eq Scan Ind Full

A machine-checked theorem lets anyone verify a proof's highest induction tier by a simple tree-walk, with no knowledge of the checking algorithm.

Verify this page

A Grep-Level Check

In Recognition Science, a derivation is a tree of inference steps, and each step carries a ledger entry recording what kind of rule was used. The declaration usesFullInd_eq_scan_indFull proves that one particular ledger flag, the one marking an induction step on a quantified formula, is exactly equivalent to a purely syntactic property of the tree: whether it contains such an induction node at all. This is a theorem in the machine-checked library of formal theorems, and it means the flag is not a hidden judgment by the checker but a visible fact about the derivation's shape.

The practical consequence is that auditing a proof's induction tier becomes a grep-level scan. A third party can walk the tree, look for the induction node on a quantified formula, and set the flag accordingly, without ever consulting the checker, the context, or any semantic notion. This is the same way one might grep a proof term for a particular axiom. The theorem scan_eq_check extends this: on every derivation the checker accepts, the checker's threaded ledger equals the syntactic scan, so the ledger is tamper-evident. A forced verdict, meaning an empty ledger, is equivalent to the tree containing no posit symbols and no full-induction node, both checkable by tree-walk.

What this theorem does not claim is broader. It does not say that full induction is unnecessary or that quantified induction is weak; it only identifies the syntactic marker for that tier. It does not prove that any particular derivation is correct, only that the ledger flag matches a tree property on accepted derivations. And it does not address whether the induction rule itself is sound, only that its use is auditable. The theorem is about bookkeeping, not about the power of the rules.

THEOREM usesFullInd_eq_scan_indFull · IndisputableMonolith/DeltaKernel/Sigma.lean
usesFullInd_eq_scan_indFull · IndisputableMonolith/DeltaKernel/Sigma.lean:172 
/-- The grep scan for the induction tier agrees with the `indFull` flag of the
syntactic ledger. -/
theorem usesFullInd_eq_scan_indFull (d : Deriv) :
    usesFullInd d = (scanLedger d).indFull := by
  induction d with
  | hyp _ => rfl
  | eqRefl _ => rfl
  | eqSubst _ _ _ dEq dT ihE ihT =>
      simp [usesFullInd, scanLedger, Ledger.union, ihE, ihT]
  | succNeZero _ => rfl
  | succInj d ih => simpa [usesFullInd, scanLedger] using ih
  | addZero _ => rfl
  | addSucc _ _ => rfl
  | mulZero _ => rfl
  | mulSucc _ _ => rfl
  | ind φ d₀ dS ih₀ ihS =>
      cases hqf : φ.isQF <;>
        simp [usesFullInd, scanLedger, hqf, Ledger.union, Ledger.ofIndFull,
          ih₀, ihS]
  | implIntro _ d ih => simpa [usesFullInd, scanLedger] using ih
  | implElim d₁ d₂ ih₁ ih₂ =>
      simp [usesFullInd, scanLedger, Ledger.union, ih₁, ih₂]
  | conjIntro d₁ d₂ ih₁ ih₂ =>
      simp [usesFullInd, scanLedger, Ledger.union, ih₁, ih₂]
  | conjElim1 d ih => simpa [usesFullInd, scanLedger] using ih
  | conjElim2 d ih => simpa [usesFullInd, scanLedger] using ih
  | disjIntro1 _ d ih => simpa [usesFullInd, scanLedger] using ih
  | disjIntro2 _ d ih => simpa [usesFullInd, scanLedger] using ih
  | disjElim d dL dR ih ihL ihR =>
      simp [usesFullInd, scanLedger, Ledger.union, ih, ihL, ihR]
  | flsElim _ d ih => simpa [usesFullInd, scanLedger] using ih
  | allIntro d ih => simpa [usesFullInd, scanLedger] using ih
  | allElim _ d ih => simpa [usesFullInd, scanLedger] using ih
  | exIntro _ _ d ih => simpa [usesFullInd, scanLedger] using ih
  | exElim _ d dBody ih ihB =>
      simp [usesFullInd, scanLedger, Ledger.union, ih, ihB]
  | emPosit _ => rfl
  | lpoPosit _ => rfl
  | mpPosit _ => rfl
THEOREM scan_eq_check · IndisputableMonolith/DeltaKernel/Sigma.lean
scan_eq_check · IndisputableMonolith/DeltaKernel/Sigma.lean:214 · truncated 
/-- AGREEMENT: on every derivation the checker accepts, the checker's
threaded ledger is EXACTLY the syntactic σ-scan of the tree. So the σ-grade
of a checked judgment is an oracle-symbol occurrence fact about the
derivation data, not an artifact of the checking algorithm: the ledger is
tamper-evident. -/
theorem scan_eq_check {d : Deriv} :
    ∀ {Γ : Ctx} {φ : DFormula} {O : Ledger},
      check Γ d = some (φ, O) → O = scanLedger d := by
  induction d with
  | hyp i =>
      intro Γ φ O hchk
      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
          exact hchk.2.symm
  | eqRefl t =>
      intro Γ φ O hchk
      simp only [check, Option.some.injEq, Prod.mk.injEq] at hchk
      exact hchk.2.symm
  | eqSubst hole t s dEq dT ihEq ihT =>
      intro Γ φ O hchk
      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
              · split at hchk
                · simp only [Option.some.injEq, Prod.mk.injEq] at hchk
                  obtain ⟨_, hO⟩ := hchk
                  rw [ihEq hdE, ihT hdT] at hO
                  exact hO.symm
                · nomatch hchk
              · nomatch hchk
  | succNeZero t =>
      intro Γ φ O hchk
      simp only [check, Option.some.injEq, Prod.mk.injEq] at hchk
      exact hchk.2.symm
  | succInj d ih =>
      intro Γ φ O hchk
      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 ⟨_, hO⟩ := hchk
                      rw [ih hd] at hO
                      exact hO.symm
                  | 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
      simp only [check, Option.some.injEq, Prod.mk.injEq] at hchk
      exact hchk.2.symm
  | addSucc t s =>
      intro Γ φ O hchk
      simp only [check, Option.some.injEq, Prod.mk.injEq] at hchk
      exact hchk.2.symm
  | mulZero t =>
      intro Γ φ O hchk
      simp only [check, Option.some.injEq, Prod.mk.injEq] at hchk
      exact hchk.2.symm
  | mulSucc t s =>
      intro Γ φ O hchk
      simp only [check, Option.some.injEq, Prod.mk.injEq] at hchk
      exact hchk.2.symm
  | ind hole d₀ dS ih₀ ihS =>
      intro Γ φ O hchk
      simp only [check] at hchk
      cases hd0 : check Γ d₀ with
      | none => simp [hd0] at hchk
      | some cp0 =>
          obtain ⟨c₀, 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
              · split at hchk
                · simp only [Option.some.injEq, Prod.mk.injEq] at hchk
                  obtain ⟨_, hO⟩ := hchk
                  rw [ih₀ hd0, ihS hdS] at hO
                  exact hO.symm
                · nomatch hchk
              · nomatch hchk
  | implIntro hole d ih =>
      intro Γ φ O hchk
      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 ⟨_, hO⟩ := hchk
          rw [ih hd] at hO
          exact hO.symm
  | implElim d₁ d₂ ih₁ ih₂ =>
      intro Γ φ O hchk
      simp only [check] at hchk
      cases hd1 : check Γ d₁ with
      | none => simp [hd1] at hchk
      | some cp1 =>
          obtain ⟨c₁, o₁⟩ := cp1
          cases hd2 : check Γ d₂ with
          | none => simp [hd1, hd2] at hchk
          | some cp2 =>
              obtain ⟨c₂, o₂⟩ := cp2
              cases c₁ with
              | impl a b =>
                  simp only [hd1, hd2] at hchk
                  split at hchk
                  · simp only [Option.some.injEq, Prod.mk.injEq] at hchk
                    obtain ⟨_, hO⟩ := hchk
                    rw [ih₁ hd1, ih₂ hd2] at hO
                    exact hO.symm
                  · 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 d₁ d₂ ih₁ ih₂ =>
      intro Γ φ O hchk
      simp only [check] at hchk
      cases hd1 : check Γ d₁ with
      | none => simp [hd1] at hchk
      | some cp1 =>
          obtain ⟨c₁, o₁⟩ := cp1
          cases hd2 : check Γ d₂ with
          | none => simp [hd1, hd2] at hchk
          | some cp2 =>
              obtain ⟨c₂, o₂⟩ := cp2
              simp only [hd1, hd2, Option.some.injEq, Prod.mk.injEq] at hchk
              obtain ⟨_, hO⟩ := hchk
              rw [ih₁ hd1, ih₂ hd2] at hO
              exact hO.symm
  | conjElim1 d ih =>
      intro Γ φ O hchk
      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 ⟨_, hO⟩ := hchk
              rw [ih hd] at hO
              exact hO.symm
          | 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
      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 ⟨_, hO⟩ := hchk
              rw [ih hd] at hO
              exact hO.symm
          | 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 ψ d ih =>
      intro Γ φ O hchk
      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 ⟨_, hO⟩ := hchk
          rw [ih hd] at hO
          exact hO.symm
  | disjIntro2 ψ d ih =>
      intro Γ φ O hchk
      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 ⟨_, hO⟩ := hchk
          rw [ih hd] at hO
          exact hO.symm
  | disjElim d dL dR ih ihL ihR =>
      intro Γ φ O hchk
      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 ⟨χ₁, o₁⟩ := cpL
                  cases hdR : check (b :: Γ) dR with
                  | none => simp [hdL, hdR] at hchk
                  | some cpR =>
                      obtain ⟨χ₂, o₂⟩ := cpR
                      simp only [hdL, hdR] at hchk
                      split at hchk
                      · simp only [Option.some.injEq, Prod.mk.injEq] at hchk
                        obtain ⟨_, hO⟩ := hchk
                        rw [ih hd, ihL hdL, ihR hdR] at hO
                        exact hO.symm
                      · nomatch hchk
          | eq _ _ => simp [hd] at hchk
          | fls => simp [hd] at hchk
          | conj _ _ => simp [hd] at hchk
          | impl _ _ => simp [hd] at hchk
          | all _ => simp [hd] at hchk
          | ex _ => simp [hd] at hchk
  | flsElim ψ d ih =>
      intro Γ φ O hchk
      simp only [check] at hchk
      cases hd : check Γ d with
      | none => simp [hd] at hchk
      | some cp =>
          obtain ⟨c, o⟩ := cp
          cases c with
          | fls =>
              simp only [hd, Option.some.injEq, Prod.mk.injEq] at hchk
              obtain ⟨_, hO⟩ := hchk
              rw [ih hd] at hO
              exact hO.symm
          | eq _ _ => 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
  | allIntro d ih =>
      intro Γ φ O hchk
      simp only [check] at hchk
      cases hd : check (Γ.map (DFormula.lift 1 0)) 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 ⟨_, hO⟩ := hchk
          rw [ih hd] at hO
          exact hO.symm
  | allElim t d ih =>
      intro Γ φ O hchk
      simp only [check] at hchk
      cases hd : check Γ d with
      | none => simp [hd] at hchk
      | some cp =>
          obtain ⟨c, o⟩ := cp
          cases c with
          | all a =>
              simp only [hd, Option.some.injEq, Prod.mk.injEq] at hchk
              obtain ⟨_, hO⟩ := hchk
              rw [ih hd] at hO
              exact hO.symm
          | eq _ _ => simp [hd] at hchk
          | fls => simp [hd] at hchk
          | conj _ _ => simp [hd] at hchk
          | disj _ _ => simp [hd] at hchk
          | impl _ _ => simp [hd] at hchk
          | ex _ => simp [hd] at hchk
  | exIntro ψ t d ih =>
      intro Γ φ O hchk
      simp only [check] at hchk
      cases hd : check Γ d with
      | none => simp [hd] at hchk
      | some cp =>
          obtain ⟨c, o⟩ := cp
          simp only [hd] at hchk
          split at hchk
          · simp only [Option.some.injEq, Prod.mk.injEq] at hchk
            obtain ⟨_, hO⟩ := hchk
            rw [ih hd] at hO
            exact hO.symm
          · nomatch hchk
  | exElim ψ d dBody ih ihBody =>
      intro Γ φ O hchk
      simp only [check] at hchk
      cases hd : check Γ d with
      | none => simp [hd] at hchk
      | some cp =>
          obtain ⟨c, o⟩ := cp
          cases c with
          | ex a =>
              simp only [hd] at hchk
              cases hdB : check (a :: Γ.map (DFormula.lift 1 0)) dBody with
              | none => simp [hdB] at hchk
              | some cpB =>
                  obtain ⟨χ, o₂⟩ := cpB
                  simp only [hdB] at hchk
                  split at hchk
                  · simp only [Option.some.injEq, Prod.mk.injEq] at hchk
                    obtain ⟨_, hO⟩ := hchk
                    rw [ih hd, ihBody hdB] at hO
                    exact hO.symm

-- … truncated for the page; open the module for the rest.
THEOREM forced_syntactic_audit · IndisputableMonolith/DeltaKernel/Sigma.lean
forced_syntactic_audit · IndisputableMonolith/DeltaKernel/Sigma.lean:585 
/-- A FORCED verdict (empty ledger) implies the tree is posit-free AND stayed
in the QF induction tier: the `σ0 @ QF-IND` certificate is a pure syntactic
occurrence fact, auditable by tree-walk with no knowledge of the checker. -/
theorem forced_syntactic_audit {Γ : Ctx} {d : Deriv} {φ : DFormula}
    (h : Forced Γ d φ) :
    positFree d = true ∧ usesFullInd d = false := by
  have hscan : Ledger.empty = scanLedger d := scan_eq_check h
  constructor
  · rw [positFree_eq_scan_isForced, ← hscan]; rfl
  · rw [usesFullInd_eq_scan_indFull, ← hscan]; rfl

What this page does not claim

The theorem does not prove that full induction is necessary or that quantified induction is weak. It does not certify that any particular derivation is correct, only that the ledger flag matches a tree property on accepted derivations. It does not address the soundness of the induction rule itself.

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/Sigma.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