Machine Native Reasoning: wider continuation

Download original file

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

Read the typeset paper

1 \chapter{Proof and verification guide}\label{app:verification}
2 
3 \section*{Three levels of evidence}
4 A written proof establishes a conditional mathematical argument. An exact reference computation exercises specified finite inputs and checks an implementation against a declared oracle. A Lean certificate checks a formal declaration in a particular environment. The correspondence between the English statement and that declaration is an additional mathematical obligation.
5 
6 The selected core contains twenty-seven numbered theorem, proposition, and corollary statements. Its archived Machine Theory correspondence accepts twenty-three of them in specified scopes. The four remaining selected targets are Theorem~\ref{r:common}, Proposition~\ref{r:positive-packets}, Corollary~\ref{r:occupancy}, and Theorem~\ref{r:ending}. The expanded ending argument does not change that status.
7 
8 The new composition, control-transport, and migration statements have written proofs and exact finite reference checks. They have not been compiled as new Lean declarations. The proof-field chapter restates selected results from Proof-Path Theory, whose original definitions have an archived formal concordance. That source evidence is retained separately and is not counted as additional coverage of the twenty-seven-result core.
9 
10 \section*{Scope of the archived core correspondence}
11 The retained source record reports two completed builds from empty local object directories, including one from a separately extracted source snapshot. Each build compiled sixty-four production modules, replayed sixty-three substantive modules through Lean's own kernel, and checked the declared negative controls and axiom policy. The source inventory contains 1,003 authored theorem declarations supporting the twenty-three selected source results. Supporting declarations and manuscript results are different counts.
12 
13 The stated foundational axiom set is \texttt{propext}, \texttt{Classical.choice}, and \texttt{Quot.sound}. The upstream compiler and dependency cache are part of the trust boundary. The archive records their identities but does not establish an independently implemented kernel or a new rebuild of all upstream mathematics. No fresh Lean compilation is claimed for the present continuation.
14 
15 \section*{Exact computational checks}
16 The reproducibility companion retains the reference programs, input domains, outcomes, and hashes. The following rows use different units and should not be added into a single theorem or evidence count.
17 
18 \small
19 \begin{longtable}{@{}p{.27\linewidth}p{.22\linewidth}p{.43\linewidth}@{}}
20 \toprule Suite & Recorded scope & What is compared\\\midrule\endhead
21 Reviewed-core regressions & 205,477 assertions in 27 groups & The two original exact suites, retained unchanged and rerun.\\[3pt]
22 Safe continuation & 8,306 finite games & Fixed-point regions against explicit positional-policy enumeration, with ending-rank witnesses.\\[3pt]
23 Joint stochastic/legal interface & Four scenarios, horizons zero through four & Complete projected state paths, labels, action/report histories, positive-history posteriors, and action intersections.\\[3pt]
24 Controlled quotient transport & 5,604 exact quotient cases & Predecessor identities, both fixed-point sequences, ending ranks, and lifted positional witnesses.\\[3pt]
25 Conservative support envelopes & 3,000 constructed cases & One-sided containment of ending and running regions under adversarial overapproximation.\\[3pt]
26 Record migration & 44,168 canonical record pairs & Fibre criteria, supplementary encodings, and smaller exhaustive domains for explicit decoders, observations, and operation transport.\\[3pt]
27 Proof fields & 42,560 protected requests & Closure and feasibility against enumeration of all seeded closed models in the stated small domains.\\\bottomrule
28 \end{longtable}
29 \normalsize
30 
31 The joint-interface checker retains every intermediate state. Comparing only a final state together with an action/report word would not establish full label-history equality. The control checks also distinguish an empty action catalogue from an action with an empty successor set. The latter is rejected, rather than accepted by a vacuous universal condition.
32 
33 Seeded larger games are exact computations on sampled finite fixtures. They are not exhaustive coverage of all games of those sizes. All probability calculations in the joint-history checks use rational arithmetic. Plotting converts declared exact quantities into display coordinates only.
34 
35 \section*{Remaining formal obligations}
36 The next selected target is the sure-ending and safe-running equivalence. A source-facing port must include finite stabilization, first-entry ranks, deadlock, necessity for history-dependent strategies, and the observable command boundary. The common observable quotient must include switching candidate dynamics. The packet result must retain the cone and zero-mass hypotheses. The correction-memory result must retain the full declared evidence algebra and the exact cardinality statement.
37 
38 No broader claim follows merely from completing those four mappings. The joint controlled-history theorem, the support-game interface, and representation migration have their own future correspondence obligations. Independent mathematical review, native-platform execution, and external validation of learned or physical models are also separate from the checks described here.

Back to source controls

Back to Machine Native Reasoning: wider continuation