Encyclopedia Delta Delta Kernel Sigma Forced Syntactic Audit

ARTICLE 3 claims 3 theorems

Delta Kernel Sigma Forced Syntactic Audit

A theorem in the Recognition Science library shows that a certain kind of proof certificate can be checked by simply scanning its symbols, with no need to run the checker itself.

Verify this page

The syntactic audit

A ledger, a discrete record of events, in the Recognition Science framework tracks which derivation rules a proof uses. The framework's machine-checked library of formal theorems defines a checker that walks a derivation tree and records, among other things, whether the proof invokes any of three special posit constructors or a full induction rule. The declaration forced_syntactic_audit proves that whenever the checker returns a verdict of forced, meaning the ledger is empty, the derivation tree itself contains no posit symbol and no full-induction node. This is a purely syntactic fact: it can be verified by a tree-walk that ignores contexts, conclusions, and any semantic meaning, much like grepping a text file for a forbidden word.

The theorem is a corollary of a stronger agreement result in the same module. The checker's ledger on any accepted derivation equals the result of a separate syntactic scan of the tree, a fact proved in scan_eq_check. From that equality, the audit theorem follows in two short steps: if the ledger is empty, the scan reports no posits and no full induction. The library states this as forced_iff_positFree, an equivalence between a forced verdict and the absence of posit symbols, and usesFullInd_eq_scan_indFull, which ties the induction tier to a grep-level check. Together they mean that a third party can audit a claim of the form "this proof uses no oracle symbols" by reading the derivation data alone, independent of the checker's implementation.

The practical consequence is tamper evidence. The ledger cannot be forged by rearranging the derivation rules: no sequence of rule applications can synthesize a posit flag that the syntactic scan would miss, and no arrangement of posits can hide one from the scan. The framework's documentation describes this as the oracle-symbol refactor, realized without changing the derivation language, because the posits are already syntactic symbols in the tree. The theorem forced_syntactic_audit itself is the certificate: a forced verdict, which the framework associates with a clean derivation, is exactly the kind of claim that can be verified by a simple tree-walk.

What the theorem does not claim is broader. It does not say that every derivation the checker accepts is forced; it only says that if a derivation is forced, then its tree is posit-free and uses no full induction. It does not establish that the syntactic scan is faster than the checker, only that it is independent of the checker's internals. And it does not connect the ledger to any physical or empirical claim; the ledger is a formal object inside the framework's proof system, not a statement about the world. The theorem is a result about the framework's own derivation language, not about mathematics or physics outside it.

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
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_iff_positFree · usesFullInd_eq_scan_indFull · IndisputableMonolith/DeltaKernel/Sigma.lean
forced_iff_positFree · IndisputableMonolith/DeltaKernel/Sigma.lean:577 
/-- A checked derivation is FORCED iff its tree contains NO posit symbol.
Left to right is the tamper-evidence direction: a σ0 certificate implies the
grep-level audit passes. Right to left says the checker never invents posits. -/
theorem forced_iff_positFree {Γ : Ctx} {d : Deriv} {φ : DFormula} {O : Ledger}
    (h : check Γ d = some (φ, O)) :
    O.isForced = true ↔ positFree d = true := by
  rw [scan_eq_check h, positFree_eq_scan_isForced]
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

What this page does not claim

The theorem does not claim that every accepted derivation is forced. It does not claim that the syntactic scan is computationally faster than the checker. It does not connect the ledger to any physical or empirical claim outside the framework.

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