ASSUMPTION_REVIEW_BLOCK02.md
Machine Native Reasoning
ASSUMPTION_REVIEW_BLOCK02.md
1 # Block 02 — source-to-formal assumption review
2
3 **10 October 2026 · Reviewed Core 0.2 · Two added results**
4
5 ## Admission 3.4, `r:bayes`
6
7 - Finite model, observation and report alphabets are explicit. Global equivalences require a nonempty model type and a nonempty raw-observation type. A probability prior itself rules out an empty model set. Nonempty observations are needed for the arbitrary reconstruction row of an impossible report.
8 - Observation likelihoods and reporting rows are nonnegative and normalized. The channel cannot inspect the hidden model. The exact joint likelihood is constructed from these two objects.
9 - All-prior preservation means equality on every positive-probability **pair**, not merely matching a marginal law or one realized observation.
10 - One full-support prior means exact posterior agreement for that prior at all such pairs. It does not mean one sample or a prior supported on only a subset. The point-mass/erasure example refutes that weakening.
11 - The reverse stochastic kernel factors the actual coupled experiment modelwise. It is not an unrelated simulator of matching marginals.
12 - Every impossible pair is handled by nonnegativity and zero mass. No cancellation uses a zero denominator or zero prior coordinate. The utility `update` is a total algebraic expression, but the semantic equivalence is guarded by positive mass.
13 - The arbitrary normalized row on an impossible report remains only a reconstruction row. The probability interface gives no posterior on that report.
14 - The formalization proves both directions and explicitly constructs a reconstruction. It introduces no statistical estimation, finite-sample extrapolation, or learned likelihood assumption.
15
16 ## Admission 3.5, `r:joint-refinement`
17
18 - X is finite. Actions and likelihood indices can be arbitrary types in the abstract statement, strengthening the finite-index manuscript case without changing its instance. Kernel entries remain exact real values. Supplied `Law X A Unit` gives normalized nonnegative transition columns.
19 - The mandatory partition has at least two blocks, represented by two nonequivalent states. Every likelihood is strictly positive at every state. These are the manuscript's premises, not consequences of the refinement.
20 - Bayesian necessity is derived from two-point priors. It does not define admissibility to contain fibre constancy as an unproved extra condition.
21 - Separate Bayesian updates are permitted as operations in their own right and must commute for every prior with one fixed positive coarse likelihood per observation. This is stronger than one chosen transition/report schedule. Optional normalization over a complete report alphabet is unnecessary for the individual-update theorem and not inferred.
22 - The initial partition preserves all likelihood values and mandatory distinctions. Every subsequent split uses complete successor probabilities into every current block. `step_rel_iff` establishes the exact displayed block-sum semantics.
23 - Strict refinement implies strict block-count increase. The stated bound is the number of states minus the initial block count, not a looser bound substituted without disclosure.
24 - The stopping index is selected from a proved bounded existence statement; the result establishes stability, normalization of the coarse transition, separate Bayesian closure, coarseness and uniqueness.
25 - The coarseness proof covers every admissible refinement, not just partitions visited by the implemented iteration.
26 - The construction relies on classical finite quotients and `Nat.find` for mathematical existence. It is not an extracted efficient algorithm, a claim to acquire the input tables, or a certificate of finite-precision arithmetic.
27 - One-block and omitted-likelihood examples expose separate hypotheses. The four-state example connects the exact iteration to the operational admissibility predicate.
28
29 ## Retained six results
30
31 The six predecessor source modules are byte-identical and recompiled from source in each current cumulative run. Their earlier source-assumption review is preserved as `docs/ASSUMPTION_REVIEW.md`. This block reviews their use at the new interface and reruns their formal verification. It does not relabel them as two additional discoveries or import the assurance of unrelated Lean projects.
32
33 ## Proof and execution boundaries
34
35 API examples restate central types independently of their declaration statements. They help catch a weakened export, but do not replace mathematical interpretation of the model. The axiom audit checks actual elaborated dependencies. Local `leanchecker` replay uses Lean's same kernel and the pinned imported objects. Neither it nor checksum matching provides independent implementation, origin authentication, model truth, or a host-language refinement theorem.