Delta Kernel Ledger

The delta kernel ledger

The ledger, a discrete record of events, appears throughout Recognition Science as a way to track what a derivation consumes. The delta kernel ledger is that idea made precise for logic itself. It is a structure with four Boolean fields: three record whether a proof used a named classical principle, and the fourth records whether the proof used induction on a formula containing quantifiers. Each field answers one question about the derivation: did it rely on the full excluded middle, the limited principle of omniscience, Markov's principle, or full induction? The ledger is a record of Booleans, so combining two ledgers with a union operation and checking whether a ledger is empty are simple, decidable structural facts.

The kernel's verdicts come in two grades. A derivation is FORCED when its ledger is empty, meaning no classical posit was consumed. It is CONDITIONAL when the ledger holds at least one posit. The central theorem about this structure is that a union of two ledgers is forced exactly when both ledgers are forced: the empty ledger remains empty only if each part was already empty. This is a machine-checked theorem in the framework's library of formal theorems. The same library proves that a ledger built from any single posit, such as excluded middle or Markov's principle, is never forced, while the empty ledger itself is always forced.

The tier flag for full induction is deliberately separate from the posit alphabet. Whether full induction is itself a forced step or a graded strength is treated as a measured question, not a pre-judged one. The ledger therefore reports the tier alongside the verdict, distinguishing FORCED at quantifier-free induction from FORCED at full induction. Reading this tier flag in the kernel's own soundness derivation is the pre-registered self-grounding experiment. The structure establishes, in plain language, that the framework can audit its own reasoning: every derivation carries a receipt for the assumptions it used, and a derivation that used none is marked as forced.

/-- The posit-and-tier ledger. Fields `em`, `lpo`, `mp` are POSITS (named
classical/omniscience principles consumed). Field `indFull` is a TIER marker:
the derivation used induction on a formula with quantifiers. Extending the
posit alphabet = adding a field. -/
structure Ledger where
  /-- Full excluded middle schema `φ ∨ ¬φ`. -/
  em : Bool
  /-- Limited principle of omniscience (arithmetical form):
  pointwise decidability of `φ` yields `(∃x φ) ∨ (∀x ¬φ)`. -/
  lpo : Bool
  /-- Markov's principle for quantifier-free matrices:
  `¬¬(∃x φ) → ∃x φ`. -/
  mp : Bool
  /-- TIER (not a posit): induction was used on a non-quantifier-free
  formula. `FORCED @ FULL-IND` vs `FORCED @ QF-IND`. -/
  indFull : Bool

/-- FORCED is a monoid homomorphism from `(union, empty)` to `(&&, true)`:
a merged judgment is forced iff both parts are. The De Morgan core of the
tamper-evidence proof. -/
theorem union_isForced (a b : Ledger) :
    (a.union b).isForced = (a.isForced && b.isForced) := by
  cases a with
  | mk e1 l1 m1 i1 =>
    cases b with
    | mk e2 l2 m2 i2 =>
      simp only [union, isForced]
      cases e1 <;> cases l1 <;> cases m1 <;> cases e2 <;> cases l2 <;> cases m2 <;> rfl

@[simp] theorem empty_isForced : empty.isForced = true := rfl

@[simp] theorem ofEM_isForced : ofEM.isForced = false := rfl

@[simp] theorem ofMP_isForced : ofMP.isForced = false := rfl

What this page does not claim

No claim that the delta kernel ledger is a physical ledger of recognition events. No claim that full induction is forced; the structure treats it as a measured question. No claim that the ledger itself forces any mathematical result.

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/Ledger.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: