Finite enclosures for weighted scalar coefficients

The bounded replay used by activation and power pullbacks evaluates all nested coefficients over partial rational intervals. FloatLib proves the endpoint operations and enclosures. Structural lifting preserves their real meaning at every coefficient depth. A successful collection contains no failed leaf.

Each candidate carries a proof that it encloses the real coefficient expression before the codec rounds it. This does not by itself prove the final codec's rounding law, identify that expression with every caller's derivative, or verify a native GPU implementation.

The proof fields are erased from execution. Only the internal replay entrypoints are exported; tensors, model composition and differentiation traversal remain in their own modules.

@[noinline]

def TorchLean.Numeric.Internal.enclosedSlope? {α : Type} [ops : QuotientArithmetic α] (x : α) (seed : Option α) (isTanh : Bool) : Option α

Refine finite coefficient enclosures until the original codec rounds every pair equally.

A coarse exponential bound first checks for unavoidable underflow of the complete coefficient tree. Otherwise the degree/precision choice follows FloatLib's enclosure refinement policy, applied to the widest coefficient. Both searches are bounded and may be inconclusive. A missing finite encoding is not a certificate; primal-only equality of a dual number never accepts differing derivative bounds.

@[noinline]

def TorchLean.Numeric.Internal.enclosedPowerSlope? {α : Type} [ops : QuotientArithmetic α] (x exponent seed : α) : Option α

Refine the complete weighted power coefficient tree for a fixed outer exponent direction.

An exponent constant in every encoded direction uses the polynomial rule, including supported nonpositive bases. An exponent varying in inner directions uses the joint positive-base rule with zero outer exponent direction. Every lower and upper coefficient must round alike through the codec. The search is bounded; unsupported bases, failed finite conversion, or inconclusive bounds return none. The interval proofs concern idealPower and idealPowerTangent, not the codec or a native backend. Logarithms and exponentials use rounded binary-grid arithmetic. The exponential argument must fit a work budget derived from the original coefficient sizes before its enclosure is evaluated.

@[noinline]

def TorchLean.Numeric.Internal.enclosedPowerTangent? {α : Type} [ops : QuotientArithmetic α] (x y dx dy : α) : Option α

Enclose a joint power tangent from the original positive base, exponent, and both directions.

The exponential, logarithm, and complete product/quotient expression use the existing coefficient tree. Finite conversion and a positive base primal are required. Every coefficient's rounded endpoints must agree; bounded work or an unsupported domain returns none, not a certificate. This retains all varying-exponent mixed coefficients without treating them as constants.