Arithmetic for nested quotient rules

Checked operations retain range-loss information until the complete quotient has been evaluated. The cold path evaluates the original finite coefficient trees over Rat, then rounds each coefficient through FloatLib to the requested format. The same algebra can carry partial enclosures for compound expressions without duplicating its product and quotient rules. Quotient replay alone cannot recover information lost before its inputs were formed.

inductive TorchLean.Numeric.Coefficients (α : Type) : ℕ → Type

Coefficients in n commuting square-zero variables, with a chosen scalar carrier.

• scalar {α : Type} : α → Coefficients α 0
• dual {α : Type} {n : ℕ} : Coefficients α n → Coefficients α n → Coefficients α (n + 1)

@[instance_reducible]

instance TorchLean.Numeric.instBEqCoefficients {α✝ : Type} {a✝ : ℕ} [BEq α✝] : BEq (Coefficients α✝ a✝)

def TorchLean.Numeric.instBEqCoefficients.beq {α✝ : Type} {a✝ : ℕ} [BEq α✝] : Coefficients α✝ a✝ → Coefficients α✝ a✝ → Bool

@[reducible, inline]

abbrev TorchLean.Numeric.QuotientCoefficients (n : ℕ) (α : Type := ℚ) : Type

Finite rational coefficients by default; enclosure replay can choose another leaf carrier.

def TorchLean.Numeric.QuotientCoefficients.primal {α : Type} {n : ℕ} : QuotientCoefficients n α → α

Constant coefficient, obtained by setting all square-zero variables to zero.

def TorchLean.Numeric.QuotientCoefficients.add {α : Type} [Add α] {n : ℕ} : QuotientCoefficients n α → QuotientCoefficients n α → QuotientCoefficients n α

Add corresponding coefficients using the chosen leaf arithmetic.

def TorchLean.Numeric.QuotientCoefficients.sub {α : Type} [Sub α] {n : ℕ} : QuotientCoefficients n α → QuotientCoefficients n α → QuotientCoefficients n α

Subtract corresponding coefficients using the chosen leaf arithmetic.

def TorchLean.Numeric.QuotientCoefficients.mul {α : Type} [Add α] [Mul α] {n : ℕ} : QuotientCoefficients n α → QuotientCoefficients n α → QuotientCoefficients n α

Multiply coefficient trees using the product rule at each square-zero extension.

def TorchLean.Numeric.QuotientCoefficients.div {α : Type} [Add α] [Sub α] [Mul α] [Div α] {n : ℕ} : QuotientCoefficients n α → QuotientCoefficients n α → QuotientCoefficients n α

Divide coefficient trees. Rational callers check the primal denominator first; partial enclosure arithmetic propagates a failed or zero-crossing divisor at each leaf.

def TorchLean.Numeric.QuotientCoefficients.map {α β : Type} (f : α → β) {n : ℕ} : QuotientCoefficients n α → QuotientCoefficients n β

Change the leaf representation without changing the differentiation directions.

def TorchLean.Numeric.QuotientCoefficients.mapM {α β : Type} {m : Type → Type} [Monad m] (f : α → m β) {n : ℕ} : QuotientCoefficients n α → m (QuotientCoefficients n β)

Convert every coefficient, propagating a failed conversion.

def TorchLean.Numeric.QuotientCoefficients.ofScalar {α : Type} [Zero α] (n : ℕ) : α → QuotientCoefficients n α

A constant has zero coefficients in every differentiation direction.

def TorchLean.Numeric.QuotientCoefficients.exp {α : Type} [Add α] [Mul α] (evaluate : α → α) {n : ℕ} : QuotientCoefficients n α → QuotientCoefficients n α

Lift scalar exponential evaluation through the existing coefficient product rule.

class TorchLean.Numeric.QuotientArithmetic (α : Type) : Type

Operations used inside one complete quotient, together with finite coefficient conversion.

Internal byte flags record nonfinite or subnormal results, including a nonzero product or quotient rounded to zero. Zero means no range loss; recursive carriers combine flags with bitwise OR. The checked-operation entrypoints expose the same Boolean result without converting at each internal node. Unsupported carriers use the ordinary operations and do not supply a conversion.

• supported : Bool
• depth : ℕ
• addWithFlags : α → α → α × UInt8
• subWithFlags : α → α → α × UInt8
• mulWithFlags : α → α → α × UInt8
• divWithFlags : α → α → α × UInt8
• encode : α → Option (QuotientCoefficients (depth α))
• decode : QuotientCoefficients (depth α) → Option α
• copyPrimal : α → α → α

  Copy the scalar primal's native sign of zero after replaying derivative coefficients.

@[instance_reducible, instance 100]

instance TorchLean.Numeric.instQuotientArithmeticOfAddOfSubOfMulOfDiv {α : Type} [Add α] [Sub α] [Mul α] [Div α] : QuotientArithmetic α

@[inline]

def TorchLean.Numeric.QuotientArithmetic.divChecked {α : Type} [ops : QuotientArithmetic α] (x y : α) : α × Bool

@[noinline]

def TorchLean.Numeric.QuotientArithmetic.replay? {α : Type} {depth : ℕ} (encode : α → Option (QuotientCoefficients depth)) (decode : QuotientCoefficients depth → Option α) (x y : α) : Option α

Replay only finite input trees with an invertible denominator.

Only coefficient conversion crosses this cold boundary, leaving the checked arithmetic operations available for specialization in the caller.

class TorchLean.Numeric.QuotientArithmetic.NativeFormat (α : Type) : Type

Native constants and rational rounding, selected by the scalar type.

• zero : α
• minNormal : α
• negMinNormal : α
• round : ℚ → α

  Round a rational once to the native scalar type.

@[instance_reducible, noinline]

instance TorchLean.Numeric.QuotientArithmetic.instNativeFormatFloat : NativeFormat Float

@[instance_reducible, noinline]

instance TorchLean.Numeric.QuotientArithmetic.instNativeFormatFloat32 : NativeFormat Float32

@[inline]

def TorchLean.Numeric.QuotientArithmetic.Native.zeroFlag {α : Type} [NativeFormat α] [BEq α] (x : α) : UInt8

@[inline]

def TorchLean.Numeric.QuotientArithmetic.Native.nonfiniteFlag {α : Type} [BEq α] [Sub α] (x : α) : UInt8

@[inline]

def TorchLean.Numeric.QuotientArithmetic.Native.rangeFlags {α : Type} [NativeFormat α] [BEq α] [LT α] [DecidableLT α] [Sub α] (zero : α → UInt8) (x : α) : UInt8

@[noinline, specialize #[]]

def TorchLean.Numeric.QuotientArithmetic.Native.addSubFlags {α : Type} [NativeFormat α] [BEq α] [LT α] [DecidableLT α] [Sub α] (zero : α → UInt8) (z : α) : UInt8

@[noinline, specialize #[]]

def TorchLean.Numeric.QuotientArithmetic.Native.productFlags {α : Type} [NativeFormat α] [BEq α] [LT α] [DecidableLT α] [Sub α] (zero : α → UInt8) (x y z : α) : UInt8

Range flags for the actual native product z = x * y, using native zero equality. The open subnormal interval includes zero; nonzero inputs detect a product rounded to zero. This formula requires the actual product, not an independently supplied third value.

@[noinline, specialize #[]]

def TorchLean.Numeric.QuotientArithmetic.Native.quotientFlags {α : Type} [NativeFormat α] [BEq α] [LT α] [DecidableLT α] [Sub α] (zero : α → UInt8) (x z : α) : UInt8

Range flags for the actual native quotient z = x / y, using native zero equality. A zero denominator already makes the result nonfinite. A zero or subnormal result with a nonzero numerator requires replay. This formula assumes z is the actual division result.

@[inline]

def TorchLean.Numeric.QuotientArithmetic.Native.addWithFlags {α : Type} [NativeFormat α] [BEq α] [LT α] [DecidableLT α] [Sub α] [Add α] (x y : α) : α × UInt8

@[inline]

def TorchLean.Numeric.QuotientArithmetic.Native.subWithFlags {α : Type} [NativeFormat α] [BEq α] [LT α] [DecidableLT α] [Sub α] (x y : α) : α × UInt8

@[inline]

def TorchLean.Numeric.QuotientArithmetic.Native.mulWithFlags {α : Type} [NativeFormat α] [BEq α] [LT α] [DecidableLT α] [Sub α] [Mul α] (x y : α) : α × UInt8

@[inline]

def TorchLean.Numeric.QuotientArithmetic.Native.divWithFlags {α : Type} [NativeFormat α] [BEq α] [LT α] [DecidableLT α] [Sub α] [Div α] (x y : α) : α × UInt8

@[instance_reducible, inline]

instance TorchLean.Numeric.QuotientArithmetic.instFloat : QuotientArithmetic Float

@[instance_reducible, inline]

instance TorchLean.Numeric.QuotientArithmetic.instFloat32 : QuotientArithmetic Float32

def TorchLean.Numeric.QuotientArithmetic.configuredFlags {format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat} {plan : FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [FloatLib.Floats.ExecFloat.ModelCodec plan (FloatLib.Floats.Formats.BinaryInterchange.Model format) code] (outcome : FloatLib.Floats.ExecFloat.Binary.IEEEOutcome) : UInt8

FloatLib exception status plus the stricter range predicate needed by a nested quotient.

IEEE underflow requires inexactness. An exact subnormal intermediate must also trigger replay, since subsequent multiplication or division can lose coefficients. Ordinary inexact rounding alone does not trigger replay.

@[instance_reducible]

instance TorchLean.Numeric.QuotientArithmetic.configured {format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat} {plan : FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [FloatLib.Floats.ExecFloat.ModelCodec plan (FloatLib.Floats.Formats.BinaryInterchange.Model format) code] : QuotientArithmetic (FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan))

Configured values with IEEE exceptional encoding use FloatLib's nearest-even operations and exact finite decoder, including custom exponent biases. Status is computed on the descriptor model and repacked through the codec, independently of the selected arithmetic backend.

The complete derivative tree is replayed by the recursive Dual instance. Every coefficient is rounded independently to the original descriptor and storage plan, including formats wider than binary64. Finite-only encodings are not enabled: their saturation policy would require a separate derivative contract. True coefficients outside the IEEE range may still round to zero or infinity.