Containment for registered operations

Parallel tables of executable enclosures and real functions are connected by containment proofs. Only the executable table participates in the Boolean check. The semantic table and its proofs enter the soundness theorem, preserving the same trust boundary as the built-in backend.

noncomputable def FloatLib.Numerics.Interval.extensionValues (functions : List (List ℝ → ℝ)) (index : ℕ) : List ℝ → ℝ

Interpret a registered operation index; unavailable entries have an unused default value.

def FloatLib.Numerics.Interval.ExtensionsSound (extensions : List Extension) (functions : List (List ℝ → ℝ)) : Prop

The enclosure and semantic tables agree at every available index.

theorem FloatLib.Numerics.Interval.extensionsSound_nil : ExtensionsSound [] []

Empty extension tables have no successful calls.

theorem FloatLib.Numerics.Interval.ExtensionsSound.cons {extensions : List Extension} {functions : List (List ℝ → ℝ)} (h : ExtensionsSound extensions functions) {E : Extension} {f : RealFunction E.arity} (hf : E.Sound f) : ExtensionsSound (E :: extensions) (f.apply :: functions)

Add one proved enclosure and its real function to matching extension tables.

theorem FloatLib.Numerics.Interval.Backend.withExtensions_sound {α : Type u_1} {B : Backend α} {baseFunctions : ℕ → List ℝ → ℝ} (hB : B.Sound baseFunctions) (config : Config) {extensions : List Extension} {functions : List (List ℝ → ℝ)} (hE : ExtensionsSound extensions functions) : (B.withExtensions config extensions).Sound (extensionValues functions)

Registered proofs and outward rounding extend any sound endpoint backend.