Delta Kernel Check Ctx

The context list

In formal logic, a context is the list of assumptions under which a proof proceeds. The Recognition Science declaration Ctx establishes exactly this: it defines a context as a list of formulas, where the i-th entry is the hypothesis referenced by the de Bruijn index i. This is a definitional abbreviation, not a theorem; it chooses a representation for the framework's proof-checking kernel.

The kernel itself is a function that audits a fully annotated natural-deduction tree. It returns either the proved formula together with the exact set of posits consumed, or rejects the tree as ill-formed. The declaration Ctx supplies the ambient list against which hypothesis rules are checked, so the kernel can verify that every assumption cited actually appears in the context.

In Recognition Science, this context list is part of the ledger-auditing machinery: it lets the kernel record which assumptions a derivation rests on, and which classical principles (excluded middle, limited principle of omniscience, Markov's principle) were posted as posits. The declaration itself makes no claim about what can be proved; it only fixes the data structure in which assumptions are stored.

/-- Contexts: hypothesis `i` is the `i`-th formula (de Bruijn into the list). -/
abbrev Ctx := List DFormula

What this page does not claim

Ctx does not prove any formula or establish any logical principle. Ctx does not specify which rules are allowed; it only defines the structure of assumptions.

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