Encyclopedia Delta Delta Kernel Sigma Posit Free Eq Scan Is Forced

ARTICLE 3 claims 3 theorems

Delta Kernel Sigma Posit Free Eq Scan Is Forced

A machine-checked theorem shows that a certain class of proof certificates can be verified by a simple tree-walk, with no knowledge of the checking algorithm.

Verify this page

The syntactic audit

A formal proof is a tree of steps. In the Recognition Science framework, each step may carry a marker, called a posit, a flag that records a special kind of assumption. The framework's checker threads a ledger, a discrete record of such markers, through the tree as it verifies each step. The theorem positFree_eq_scan_isForced states a simple equivalence: a derivation tree contains no posit marker if and only if its scanned ledger is FORCED, meaning the ledger is empty and the proof uses no such assumptions.

The practical content is that a third party can audit a FORCED claim without understanding the checker at all. Instead of running the verification algorithm, one walks the tree and looks for the three posit symbols. If none appear, the ledger is FORCED. This is a purely syntactic occurrence check, like grepping a text file for a forbidden word. The theorem is proved in the framework's machine-checked library of formal theorems, and it is choice-free structural recursion, meaning it does not rely on the axiom of choice.

The theorem does not say that a FORCED proof is correct in any semantic sense. It only says that the ledger, as computed by the checker, agrees with a simple scan of the tree's symbols. It does not claim that the absence of posits makes a derivation valid; validity is a separate matter of the checking rules. It also does not claim that the scan can detect all tampering, only that it can detect the presence or absence of the posit symbols themselves. The agreement theorem scan_eq_check guarantees that on any derivation the checker accepts, the checker's ledger equals the scan, but that is a statement about the checker's behavior, not about the truth of the formula being proved.

For the reader, this means a FORCED certificate is auditable by a simple tree-walk, independent of the kernel implementation. That is a useful property for a framework that wants proofs to be checkable by anyone, not just by the original verifier. It is a step toward tamper-evidence, but it is not a claim about the soundness of the underlying logic or the meaning of the formulas.

THEOREM positFree_eq_scan_isForced · IndisputableMonolith/DeltaKernel/Sigma.lean
positFree_eq_scan_isForced · IndisputableMonolith/DeltaKernel/Sigma.lean:132 
/-- The grep scan for posits agrees with `isForced` of the syntactic ledger:
a tree is posit-free iff its scanned ledger is FORCED. -/
theorem positFree_eq_scan_isForced (d : Deriv) :
    positFree d = (scanLedger d).isForced := by
  induction d with
  | hyp _ => rfl
  | eqRefl _ => rfl
  | eqSubst _ _ _ dEq dT ihE ihT =>
      simp [positFree, scanLedger, Ledger.union_isForced, ihE, ihT]
  | succNeZero _ => rfl
  | succInj d ih => simpa [positFree, scanLedger] using ih
  | addZero _ => rfl
  | addSucc _ _ => rfl
  | mulZero _ => rfl
  | mulSucc _ _ => rfl
  | ind φ d₀ dS ih₀ ihS =>
      cases hqf : φ.isQF <;>
        simp [positFree, scanLedger, hqf, Ledger.union_isForced,
          Ledger.ofIndFull_isForced, ih₀, ihS]
  | implIntro _ d ih => simpa [positFree, scanLedger] using ih
  | implElim d₁ d₂ ih₁ ih₂ =>
      simp [positFree, scanLedger, Ledger.union_isForced, ih₁, ih₂]
  | conjIntro d₁ d₂ ih₁ ih₂ =>
      simp [positFree, scanLedger, Ledger.union_isForced, ih₁, ih₂]
  | conjElim1 d ih => simpa [positFree, scanLedger] using ih
  | conjElim2 d ih => simpa [positFree, scanLedger] using ih
  | disjIntro1 _ d ih => simpa [positFree, scanLedger] using ih
  | disjIntro2 _ d ih => simpa [positFree, scanLedger] using ih
  | disjElim d dL dR ih ihL ihR =>
      simp [positFree, scanLedger, Ledger.union_isForced, ih, ihL, ihR]
  | flsElim _ d ih => simpa [positFree, scanLedger] using ih
  | allIntro d ih => simpa [positFree, scanLedger] using ih
  | allElim _ d ih => simpa [positFree, scanLedger] using ih
  | exIntro _ _ d ih => simpa [positFree, scanLedger] using ih
  | exElim _ d dBody ih ihB =>
      simp [positFree, scanLedger, Ledger.union_isForced, 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_iff_positFree · 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]

What this page does not claim

The theorem does not claim that a FORCED proof is semantically correct. The theorem does not claim that the scan detects all forms of tampering, only the presence of posit symbols. The theorem does not claim that the framework's logic is sound.

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