Affine environments for rational boxes

This module supplies the semantic bridge from a rational box to the correlated affine environment built by toAffineEnv. It belongs to interval evaluation, not global optimization: every real point represented by the box has a valid noise assignment for the generated affine forms.

theorem LeanCert.Engine.exists_noise_toAffineEnv (box : List Core.IntervalRat) (rho : ℕ → ℝ) (hrho : ∀ (i : ℕ) (hi : i < box.length), rho i ∈ box[i]) (hzero : ∀ i ≥ box.length, rho i = 0) : ∃ (eps : Affine.AffineForm.NoiseAssignment), Affine.AffineForm.validNoise eps ∧ envMemAffine rho (toAffineEnv box) eps

Every real point of a rational box has the standard affine-noise representation used by toAffineEnv.