Registering certified interval enclosures

Tag a ConstantBounds c definition or a theorem E.Sound f with @[interval_extension] to associate the named real constant or function with its executable bounds. Importing the provider's module imports the registration. Local and scoped attributes follow Lean's usual visibility rules.

Functions have a fixed number of real arguments; parameters of other types can be fixed in a named wrapper. Registration checks the contract and does not introduce axioms or numerical facts.

opaque FloatLib.Numerics.Interval.Tactic.intervalExtensionRegistry : Lean.SimpleScopedEnvExtension (Lean.Name × Lean.Name) (Lean.NameMap Lean.Name)

Registered certificate names indexed by the real function they enclose.

def FloatLib.Numerics.Interval.Tactic.extensionCertificate (name : Lean.Name) : Lean.MetaM (Q(Extension) × Lean.Expr × ℕ × Lean.Expr)

Recover the enclosure, named real function, and containment proof from a registration.

def FloatLib.Numerics.Interval.Tactic.intervalExtensionAttr : Lean.ParserDescr

Register proved constant bounds or a containment theorem for a user-defined operation.

partial def FloatLib.Numerics.Interval.Tactic.registeredApplication? (e : Q(ℝ)) (visited : Array Lean.Name := #[]) : Lean.MetaM (Option (Lean.Name × Array Q(ℝ)))

Recognize registered applications through definitional aliases.