Machine Native Reasoning

Download original file

This is the original TeX manuscript source. Use the paper’s PDF for typeset equations.

Read the typeset paper

1 \chapter{Formal correspondence}
2 The selected finite reasoning core has formal counterparts for all twenty-seven source results. The correspondence covers the chain developed in the eight mathematical chapters: accessible evidence, representation and probability, correction memory, decisions and explanations, bounded inquiry, search, revision, and maintained obligations.
3 
4 For evidence consisting exactly of unions of partition cells, the final result identifies correction memory with occupancy records over attained cell--target pairs and proves the exact cardinality and fixed-width binary bound in Corollary~\ref{r:occupancy}. Its formal interface keeps the admitted-evidence restriction explicit. The current target set alone need not retain the distinctions needed for later correction.
5 
6 A source correspondence is more specific than a shared theorem name. The companion retains the original statement, its source label, the Lean declaration, and the explicit hypotheses under which the declaration represents the written claim. Source-facing checks apply the formal interfaces to those hypotheses. Negative fixtures test the omission of conditions that matter.
7 
8 The mathematical statements and proofs in the main chapters are unchanged from the authenticated reviewed core. The formal declarations are maintained separately, so the reader remains legible without requiring knowledge of Lean syntax. The release proof guide explains the principal constructions; the clause correspondence file and result ledger give the detailed map.
9 
10 The accepted release records completed cold Lean builds, transitive axiom checks, same-kernel replay, source-facing checks, rejection controls, and verification from separately extracted source. The record identifies the exact source and dependencies checked by those gates. The compiler, recorded dependencies, and standard logical axioms remain within the trusted base. The reader's own fresh reproduction also reruns the original exact finite checks, which supplement rather than replace the proofs.
11 
12 This correspondence concerns the selected finite reasoning chain. It does not certify every specialist chapter in the wider monograph, learned representations, empirical performance, a deployed system, or external authority to act. Earlier source-suite receipts retain their original provenance. The larger monograph has a separate source-recovery and publication record.

Back to source controls

Back to Machine Native Reasoning