Delta Kernel Ledger Union Is Forced

The union rule

In formal mathematics, a proof often rests on assumptions. Some of those assumptions are ordinary axioms; others are classical principles like the law of excluded middle, which says every statement is either true or false. Recognition Science tracks these assumptions in a ledger, a discrete record of which principles a derivation consumed. The record is a small table of Boolean flags, one for each named principle, and it answers a simple question: did the derivation use any classical principle, or was it forced, meaning assumption-free?

The declaration union_isForced is a theorem about what happens when two ledgers are combined. Combining ledgers means taking the union of their assumption sets: if either proof used a principle, the combined proof used it too. The theorem states that the combined ledger is forced if and only if both original ledgers were forced. In symbols, (a.union b).isForced = (a.isForced && b.isForced). This is a structural fact about the ledger model, proved by checking all possible combinations of flags. It is not a claim about any particular mathematical statement; it is a claim about how the framework's own accounting behaves.

The theorem matters because it makes the ledger a compositional tool. A large proof can be built from smaller pieces, and the assumption status of the whole is exactly the conjunction of the parts. If every component derivation is forced, the assembled derivation is forced. If any component used a classical principle, the assembly is marked conditional. This mirrors how a careful proof assistant tracks dependencies, but here the tracking is itself part of the framework's kernel, the machine-checked core of its formal library.

The theorem does not claim that any particular derivation is forced. It does not say that the law of excluded middle, the limited principle of omniscience, or Markov's principle are derivable or refutable. It only governs the bookkeeping of the ledger. The theorem also does not address the tier flag, which records whether induction was used on a quantified formula; that flag is reported separately and does not affect the forced status. The union rule is a precise, narrow statement about how assumption sets combine, and it earns its place by making the framework's accounting reliable.

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

/-- Merge two ledgers (a derivation consumes the posits of all its parts). -/
def union (a b : Ledger) : Ledger :=
  ⟨a.em || b.em, a.lpo || b.lpo, a.mp || b.mp, a.indFull || b.indFull⟩

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

What this page does not claim

No particular derivation is proved forced by this theorem. The theorem does not establish or refute excluded middle, LPO, or Markov's principle. The tier flag for full induction is not part of the forced status.

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: