Encyclopedia Delta Delta Kernel Sigma Forced Iff Posit Free

ARTICLE 3 claims 3 theorems

Delta Kernel Sigma Forced Iff Posit Free

A proof's honesty can be checked by a simple tree-walk, without trusting the checker that produced it.

Verify this page

The audit

A derivation is a tree of steps leading to a conclusion. In the Recognition Science framework, each step can carry a marker, a posit, that records a point where the argument assumed something rather than proving it. The declaration forced_iff_positFree states a precise equivalence: a derivation that the checker accepts is forced, meaning it rests on no posits, exactly when a simple scan of the tree finds no posit symbols at all.

The power of this result is that the scan is purely syntactic. It walks the tree and looks for the three posit constructors, ignoring contexts, conclusions, and any semantic meaning. This is like grepping a text file for a forbidden word. The theorem proves that this grep-level check agrees perfectly with the checker's own internal ledger, the record of assumptions it threads through the derivation. On every accepted derivation, the checker's ledger equals the syntactic scan, so the ledger is tamper-evident: no arrangement of the rules can hide a posit from the scan, and no arrangement of posits can forge a forced verdict.

The theorem also covers the induction tier. A separate scan checks whether the tree contains an induction node on a quantified formula, the full-induction tier. A forced verdict implies the tree is posit-free and stays within the quantifier-free induction tier. Both properties are pure occurrence facts about the derivation data, auditable by anyone with a tree-walk, with no knowledge of the checker's implementation.

What the theorem does not claim is that the derivation is sound in any deeper sense. It does not say the conclusion is true, only that the derivation is free of posit symbols. It does not say the checker is infallible; it says the checker's ledger is reproducible by a syntactic scan. It does not say that a posit-free derivation is the only kind of honest argument, only that within this framework, a forced verdict is exactly a posit-free tree. The theorem is a statement about the syntax of derivations, not about the semantics of the formulas they prove.

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]
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 claim that a posit-free derivation is sound in any deeper semantic sense. The theorem does not claim that the checker is infallible, only that its ledger is reproducible by a syntactic scan. The theorem does not claim that a posit-free derivation is the only kind of honest argument.

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