mixle.experimental.certified_bounds module¶
P11 (experimental) – certified model properties by abstract interpretation over the tree.
G1 propagates distributions through the model tree; the verification sibling propagates sets (here, intervals). Closed-form leaves have exact range arithmetic, and the combinators are few and typed, so a property of a composed model can be turned from a measured receipt into a proven one: a certified bound holds for EVERY point in an input box, not just the sampled ones.
This module certifies two properties for Gaussian leaves and their mixtures:
certified_density_bounds()– sound lower/upper bounds on the density over an input box (the mixture bound is the weighted interval sum of its components);certify_density_monotonic()– whether the density is provably monotone (one sign of the derivative) over the box; a mixture is certified monotone only when all components agree.
Soundness (the certified interval really contains every value) and tightness (it is not absurdly loose) are checked against dense grid evaluation in the test, per the card’s validation plan.
Exploratory mixle.experimental code (P11 card).
- class DensityBoundReceipt(lower, upper, interval, component_means, component_variances, normalized_weights, rule='gaussian-weighted-interval-sum/v1')[source]
Bases:
objectCertified interval together with the assumptions used by the proof.
- certified_density_bounds(model, lo, hi)[source]
Certify a density interval and record every validated proof assumption.
- certify_density_monotonic(model, lo, hi)[source]
Certify the density is monotone over the box: ‘increasing’, ‘decreasing’, or ‘not certified’.
A Gaussian density rises toward its mode and falls after it, so it is monotone on any box that does not straddle the mode. A mixture is certified monotone only when every component is monotone in the same direction (a sound, not complete, rule).
- grid_density_range(model, lo, hi, n=2001)[source]
Empirical [min, max] of the density on a dense grid (the validation reference).