Formal companion scope notes
The formal companion contains 254 proof modules and 255 compilation targets, including its root. The inventory records 4,454 named declarations and 2,887 named theorems: 2,556 supporting results and 331 example results. These counts describe formal declarations, separately from the 87 numbered manuscript propositions.
Fresh verification passed 697 stages: 255 compilation targets, one exact example execution, one full axiom audit, 254 module kernel replays, 183 isolated rejection controls and three Python checks. The 694 Lean stages admit only propext, Classical.choice and Quot.sound. Pinned upstream libraries were not exhaustively rebuilt or replayed.
All 87 numbered proposition cores have complete reviewed formal mappings. No proposition core remains partial or unformalized. Surrounding explanatory prose and additional unnumbered claims are not thereby separately formalized. The final scope notes state the principal assumptions and boundaries.
P11, P23, P24. Ideal risk and grammar
Conditional expectations decompose ideal risk. Summable grammar evidence controls tails. Prior refinement preserves whole record evidence when the corresponding likelihood mixtures and split prior masses agree.
P31, P35, P37. Stochastic identification
Passive laws can miss interventions. Independent reset trials give simultaneous bounds. Observable completion retains experiment coverage, spectral separation, state bounds and filtering margins.
P46 to P51. Curved domains and matrix witnesses
Rotation witnesses require a curved cone. Positive matrix embeddings certify probability laws. Polygon error, sequential coverage and conditional learning retain domain, initial state and experiment assumptions.
P52 to P58. Continuous instruments and moments
Integrable positive densities define consistent laws. Finite Gram witnesses, supplied polynomial degree and covered invertible cores enable reconstruction. Exact bins and positive averages retain policy and resolution assumptions.
P59 to P65. Realization and approximation
Common domains and policies give full record budgets. Template matching and ellipsoid proposals require separate verification. Positive polynomial approximation keeps Lipschitz bias, coefficient error and correction costs distinct.
P66 to P70. Dependent observation evidence
Actual conditional means give residual bounds with exact countable budgets and interval widths. Covered actions require positive recorded propensities. Causal comparisons and lower evidence retain separate assumptions.
P71 to P74. Robustness and repair
Oriented margins control the full cone. Boundary images can have zero unrestricted noise tolerance. Reset repair retains its prediction cost. Proposal error requires the declared singular gap and residual bounds.
P75 to P80. Finite curved certificates
Both rational charts and complete Bernstein trees cover the continuum. Strict search, coefficient boxes, selected geometry and repair brackets retain whole family quantifiers. The repaired example keeps its comparison budget.
P81 to P82. Regression and operator sets
A derived Gaussian mixture gives time uniform ridge confidence under predictable design and conditional noise assumptions. Observable moment inversion propagates row confidence into operator sets with the actual inverse factors.
P83 to P87. Covered observable domains
The declared scalar family links curved domains, exact outer intervals and law error. One simultaneous event covers selected rectangles. Marginal and rolling window stability require positive reference minorization.
All 87 numbered proposition cores are mapped and checked. Each theorem retains its stated hypotheses; surrounding prose claims are not separately certified by this count.