Delta Kernel Ledger Of Mp Ne Empty

The posit ledger

A ledger, in the Recognition Science framework, is a discrete record of which optional logical principles a derivation used. The record has four Boolean fields: three for named classical principles, and one for whether the derivation applied induction to a formula with quantifiers. The empty ledger records that no such principle was consumed.

The declaration ofMP_ne_empty is a theorem in the framework's machine-checked library of formal theorems. It states that the ledger recording use of Markov's principle, a classical principle that allows deriving existence from double negation, is not equal to the empty ledger. The proof is by direct computation: the two records differ in their third field. The same theorem holds for the ledgers recording excluded middle and the limited principle of omniscience.

In Recognition Science, this theorem is part of a larger accounting system. The framework's kernel classifies derivations as FORCED when they consume no posits, and CONDITIONAL otherwise. The theorem supports the structural fact that a nonempty ledger is genuinely different from an empty one, a distinction that keeps the bookkeeping honest. It also underpins the decidability of ledger operations: union and emptiness checks are computable facts, not matters of interpretation.

What the theorem does not claim is just as important. It does not assert that Markov's principle is true, false, or needed for any particular result. It does not say that a derivation using Markov's principle is invalid. It only records a difference between two bookkeeping states. The theorem is a fact about the ledger structure, not about the mathematics that the ledger describes.

theorem ofMP_ne_empty : ofMP ≠ empty := by decide

What this page does not claim

Markov's principle is true or false in the framework. A derivation using Markov's principle is invalid. The theorem applies to any ledger other than the specific ofMP record.

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: