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