RELEASE_SCOPE.md
Certified Inference
RELEASE_SCOPE.md
1 # First-release finish line
2
3 Author: Komorebi P. Release: Certified Inference Core 1.0.0.
4
5 The finished contract is finite-dimensional inference for one observation update,
6 with exact rational factor-coded model data, positive noise floor, fixed complete
7 self-adjoint rational packet families, positive rational posterior tolerance, and
8 positive rational output-radius tolerance. A supplied output-packet seed and scan
9 cover the finite label set. The mathematical program returns a represented gain,
10 a checked posterior Wasserstein tolerance, and parameter intervals of its Joseph
11 Gaussian. Singular priors and rectangular observation operators are supported.
12
13 The canonical entry point is Komorebi.CachedPosterior.runCached. Its iterative
14 updates and cached quantities are exact rational. Final verification and parameter
15 output use outward-rounded dyadic operations. The retained v11 solver is a separate
16 branch with genuinely rounded full-gain updates and its own termination theorem.
17
18 Completed release obligations:
19
20 1. An actual solver, sound successful returns, and guaranteed success for positive
21 tolerances under the declared hypotheses.
22 2. Cached residual/energy invariants and equality with the original greedy gains.
23 3. Computable iteration fuel, verification precision, and output precision.
24 4. A narrow, inspectable input/output and arithmetic boundary.
25 5. Bounded full-cost reference measurements, including exported certificate checks.
26 6. A clean active-source rebuild and complete axiom audit, with preserved failures.
27 7. A bounded primary-source literature comparison and conservative attribution.
28
29 The Python producer and exporter are useful reference tools. Their parser and
30 implementation are not universally refined to the Lean program. An exported
31 instance certifies the explicit rational data in that Lean source. This is why
32 Python success is labeled provisional. Resource caps can return RESOURCE_LIMIT;
33 mathematical finite termination does not promise completion on bounded hardware.
34
35 Output intervals enclose the mean/covariance of the certified approximation. They
36 do not certify a separate Gaussian formed from the interval centers, and delta is
37 not an exact-posterior coordinate error bound. No sampler is part of this release.
38
39 Remaining capabilities belong to explicitly separate extensions: rounded selective
40 updates and approximate selection, hierarchy-changing refinement, large-scale
41 implementations, sequential filtering, uncertain inputs, parser refinement, hardware
42 floating point and sampling. Literature priority and practical superiority remain
43 unestablished. Their absence does not leave the declared theorem conditional.
44
45 The new rounded-selective route was assessed rather than silently claimed closed.
46 A checked counterexample shows independently rounding gain and cached residual
47 centers breaks the cache invariant. The independent final verifier still rejects
48 that false internal convergence signal. A future rounded cache must carry and
49 propagate error bounds, not reuse the exact-cache invariant without proof.