Mathematics · proofs · software

Machine-Native Reasoning · Recorded formal evidence

Selected results and their formal scope

Read side by side

The accepted release 1.0.0 records all 27 selected results of Reviewed Core v0.2, with no pending selected result. Each entry below connects the written statement, its full written proof, the source-facing discussion of assumptions, and the exact retained Lean declarations.

Accepted release record · Source-to-Lean map · All chapters · Find statements and proofs

Formal correspondence

Read the original authored correspondence chapter

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.

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 3.2. Its formal interface keeps the admitted-evidence restriction explicit. The current target set alone need not retain the distinctions needed for later correction.

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.

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.

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.

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.

What the accepted record covers

The two recorded cold gates each checked 79 production modules, 78 substantive replays through the same Lean kernel, 188 rejection controls, and 3,018 transitive axiom records. The actual axiom union is Classical.choice, Quot.sound, propext. These are retained execution receipts; this HTML edition performs no new Lean execution or mathematical review.

Read the verification report and trusted-base limits · Read the accepted progress ledger

Keep the editions separate

The formal counterparts apply to their declared mathematical contracts. They do not establish learned representations, empirical performance, a deployed system, or external permission to act. A source-map entry alone is not an acceptance receipt.

27 selected results

Numbers follow the authored core, including gaps occupied by counterexamples. Original source-page and line references in the map belong to source/core_v0.2.tex; the HTML statement links open the refreshed reader. Declaration links resolve namespace-qualified names in retained source bytes and are navigation aids.

  1. 1.1 — A record determines a target exactly on its fibres
  2. 1.2 — Evidence-initialized behavioral state
  3. 2.1 — Exact accounting of the discarded excursion
  4. 2.3 — Forward transport of a reusable method
  5. 2.4 — A common observable quotient
  6. 2.5 — When complete packets are genuine probability components
  7. 3.1 — Minimal exact memory for a correction contract
  8. 3.2 — The size of partition correction memory
  9. 3.4 — When a report preserves every Bayesian correction
  10. 3.5 — Least refinement closed under prediction and correction
  11. 3.6 — One quotient for reports, posteriors, and feedback
  12. 3.8 — A whole-history bound with an explicit conditioning cost
  13. 4.1 — A decision bound for one actual approximation chain
  14. 4.2 — A common artifact for fixed recipients
  15. 5.1 — Exact joint feasibility for explicit controllers
  16. 5.3 — A candidate attaining both lower bounds is optimal
  17. 5.4 — The same compressed belief supports the same inquiry
  18. 5.6 — Uniform model error controls a changed policy
  19. 6.1 — What finite counterexamples establish
  20. 6.2 — Ordered semantic compression preserves the teacher trace
  21. 6.4 — A sound prefix exclusion
  22. 7.1 — Selective reuse with complete dependencies
  23. 7.3 — Which gains survive every admitted price?
  24. 7.4 — A conditional error budget for a lineage
  25. 8.1 — Target-relative joint reconstruction
  26. 8.2 — A quotient that preserves legal operations
  27. 8.3 — Safe continuation that retains an ending strategy

Proposition 1.1: A record determines a target exactly on its fibres

Written statement · Written proof · Unchanged source statement

Source label r:factor. Read the domains, quantifiers, and required hypotheses in the statement and the retained formal interfaces.

Assumptions and source correspondence

Formal declarations (2)

Theorem 1.2: Evidence-initialized behavioral state

Written statement · Written proof · Unchanged source statement

Source label r:behavior. Read the domains, quantifiers, and required hypotheses in the statement and the retained formal interfaces.

Assumptions and source correspondence

Formal declarations (4)

Proposition 2.1: Exact accounting of the discarded excursion

Written statement · Written proof · Unchanged source statement

Source label r:packet. Read the domains, quantifiers, and required hypotheses in the statement and the retained formal interfaces.

Assumptions and source correspondence

Formal declarations (5)

Theorem 2.3: Forward transport of a reusable method

Written statement · Written proof · Unchanged source statement

Source label r:transport. Read the domains, quantifiers, and required hypotheses in the statement and the retained formal interfaces.

Assumptions and source correspondence

Formal declarations (4)

Theorem 2.4: A common observable quotient

Written statement · Written proof · Unchanged source statement

Source label r:common. Read the domains, quantifiers, and required hypotheses in the statement and the retained formal interfaces.

Recorded map qualification. Valid only with completed current-source final17/fresh17 gates and production comparison. The finite catalogue, distinguished reference, every initial vector and every word are retained. Current release report supplies actual admission.

Assumptions and source correspondence · Proof guide

Formal declarations (6)

Proposition 2.5: When complete packets are genuine probability components

Written statement · Written proof · Unchanged source statement

Source label r:positive-packets. Read the domains, quantifiers, and required hypotheses in the statement and the retained formal interfaces.

Assumptions and source correspondence · Proof guide

Formal declarations (5)

Theorem 3.1: Minimal exact memory for a correction contract

Written statement · Written proof · Unchanged source statement

Source label r:memory. Read the domains, quantifiers, and required hypotheses in the statement and the retained formal interfaces.

Assumptions and source correspondence

Formal declarations (5)

Corollary 3.2: The size of partition correction memory

Written statement · Written proof · Unchanged source statement

Source label r:occupancy. Read the domains, quantifiers, and required hypotheses in the statement and the retained formal interfaces.

Assumptions and source correspondence · Proof guide

Formal declarations (12)

Theorem 3.4: When a report preserves every Bayesian correction

Written statement · Written proof · Unchanged source statement

Source label r:bayes. Read the domains, quantifiers, and required hypotheses in the statement and the retained formal interfaces.

Assumptions and source correspondence · Proof guide

Formal declarations (5)

Theorem 3.5: Least refinement closed under prediction and correction

Written statement · Written proof · Unchanged source statement

Source label r:joint-refinement. Read the domains, quantifiers, and required hypotheses in the statement and the retained formal interfaces.

Assumptions and source correspondence · Proof guide

Formal declarations (8)

Theorem 3.6: One quotient for reports, posteriors, and feedback

Written statement · Written proof · Unchanged source statement

Source label r:instrument. Read the domains, quantifiers, and required hypotheses in the statement and the retained formal interfaces.

Assumptions and source correspondence

Formal declarations (8)

Proposition 3.8: A whole-history bound with an explicit conditioning cost

Written statement · Written proof · Unchanged source statement

Source label r:history-bound. Read the domains, quantifiers, and required hypotheses in the statement and the retained formal interfaces.

Assumptions and source correspondence · Proof guide

Formal declarations (5)

Theorem 4.1: A decision bound for one actual approximation chain

Written statement · Written proof · Unchanged source statement

Source label r:risk. Read the domains, quantifiers, and required hypotheses in the statement and the retained formal interfaces.

Recorded map qualification. Bounded metric response error plus total variation on the same finite world set; actual finite minimizers, capped regret, strict-gap uniqueness and risk threshold. Direct conditional-history and stored-record composition included as supporting results.

Assumptions and source correspondence · Proof guide

Formal declarations (5)

Theorem 4.2: A common artifact for fixed recipients

Written statement · Written proof · Unchanged source statement

Source label r:recipient. Read the domains, quantifiers, and required hypotheses in the statement and the retained formal interfaces.

Assumptions and source correspondence · Proof guide

Formal declarations (5)

Theorem 5.1: Exact joint feasibility for explicit controllers

Written statement · Written proof · Unchanged source statement

Source label r:inquiry. Read the domains, quantifiers, and required hypotheses in the statement and the retained formal interfaces.

Assumptions and source correspondence · Proof guide

Formal declarations (12)

Theorem 5.3: A candidate attaining both lower bounds is optimal

Written statement · Written proof · Unchanged source statement

Source label r:lowerbound. Read the domains, quantifiers, and required hypotheses in the statement and the retained formal interfaces.

Assumptions and source correspondence · Proof guide

Formal declarations (6)

Theorem 5.4: The same compressed belief supports the same inquiry

Written statement · Written proof · Unchanged source statement

Source label r:belief-planning. Read the domains, quantifiers, and required hypotheses in the statement and the retained formal interfaces.

Assumptions and source correspondence · Proof guide

Formal declarations (11)

Proposition 5.6: Uniform model error controls a changed policy

Written statement · Written proof · Unchanged source statement

Source label r:policy-error. Read the domains, quantifiers, and required hypotheses in the statement and the retained formal interfaces.

Assumptions and source correspondence · Proof guide

Formal declarations (5)

Proposition 6.1: What finite counterexamples establish

Written statement · Written proof · Unchanged source statement

Source label r:cegis. Read the domains, quantifiers, and required hypotheses in the statement and the retained formal interfaces.

Assumptions and source correspondence · Proof guide

Formal declarations (8)

Theorem 6.2: Ordered semantic compression preserves the teacher trace

Written statement · Written proof · Unchanged source statement

Source label r:ordered. Read the domains, quantifiers, and required hypotheses in the statement and the retained formal interfaces.

Assumptions and source correspondence · Proof guide

Formal declarations (4)

Proposition 6.4: A sound prefix exclusion

Written statement · Written proof · Unchanged source statement

Source label r:prefix. Read the domains, quantifiers, and required hypotheses in the statement and the retained formal interfaces.

Assumptions and source correspondence · Proof guide

Formal declarations (5)

Theorem 7.1: Selective reuse with complete dependencies

Written statement · Written proof · Unchanged source statement

Source label r:dependencies. Read the domains, quantifiers, and required hypotheses in the statement and the retained formal interfaces.

Assumptions and source correspondence · Proof guide

Formal declarations (4)

Proposition 7.3: Which gains survive every admitted price?

Written statement · Written proof · Unchanged source statement

Source label r:prices. Read the domains, quantifiers, and required hypotheses in the statement and the retained formal interfaces.

Assumptions and source correspondence · Proof guide

Formal declarations (7)

Proposition 7.4: A conditional error budget for a lineage

Written statement · Written proof · Unchanged source statement

Source label r:lineage. Read the domains, quantifiers, and required hypotheses in the statement and the retained formal interfaces.

Assumptions and source correspondence · Proof guide

Formal declarations (7)

Proposition 8.1: Target-relative joint reconstruction

Written statement · Written proof · Unchanged source statement

Source label r:reconstruction. Read the domains, quantifiers, and required hypotheses in the statement and the retained formal interfaces.

Assumptions and source correspondence · Proof guide

Formal declarations (6)

Theorem 8.2: A quotient that preserves legal operations

Written statement · Written proof · Unchanged source statement

Source label r:governance. Read the domains, quantifiers, and required hypotheses in the statement and the retained formal interfaces.

Assumptions and source correspondence · Proof guide

Formal declarations (9)

Theorem 8.3: Safe continuation that retains an ending strategy

Written statement · Written proof · Unchanged source statement

Source label r:ending. Read the domains, quantifiers, and required hypotheses in the statement and the retained formal interfaces.

Recorded map qualification. Admission requires completed current-source final16/fresh16 gates and production comparison. Full-history strategies, deadlock, observable command, first-arrival safety and first-entry rank are explicit. The source hold-at-goal assumption is unnecessary for first-arrival semantics.

Assumptions and source correspondence

Formal declarations (11)