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. This is scoped to one quotient: it cannot recover information lost before its inputs were formed.

inductive TorchLean.Numeric.QuotientCoefficients : ℕ → Type

Coefficients in the algebra generated by n commuting square-zero variables.

• scalar : ℚ → QuotientCoefficients 0
• dual {n : ℕ} : QuotientCoefficients n → QuotientCoefficients n → QuotientCoefficients (n + 1)

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

def TorchLean.Numeric.QuotientCoefficients.add {n : ℕ} : QuotientCoefficients n → QuotientCoefficients n → QuotientCoefficients n

def TorchLean.Numeric.QuotientCoefficients.sub {n : ℕ} : QuotientCoefficients n → QuotientCoefficients n → QuotientCoefficients n

def TorchLean.Numeric.QuotientCoefficients.mul {n : ℕ} : QuotientCoefficients n → QuotientCoefficients n → QuotientCoefficients n

def TorchLean.Numeric.QuotientCoefficients.div {n : ℕ} : QuotientCoefficients n → QuotientCoefficients n → QuotientCoefficients n

The caller checks that the denominator's primal is nonzero before entering this recursion.

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.addChecked {α : Type} [ops : QuotientArithmetic α] (x y : α) : α × Bool

@[inline]

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

@[inline]

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

@[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.

def TorchLean.Numeric.QuotientArithmetic.finiteRat? (bits : UInt64) : Option ℚ

def TorchLean.Numeric.QuotientArithmetic.roundFloat (value : ℚ) : Float

def TorchLean.Numeric.QuotientArithmetic.roundFloat32 (value : ℚ) : Float32

@[noinline]

def TorchLean.Numeric.QuotientArithmetic.zero64 : Float

@[noinline]

def TorchLean.Numeric.QuotientArithmetic.minNormal64 : Float

@[noinline]

def TorchLean.Numeric.QuotientArithmetic.negMinNormal64 : Float

@[noinline]

def TorchLean.Numeric.QuotientArithmetic.zero32 : Float32

@[noinline]

def TorchLean.Numeric.QuotientArithmetic.minNormal32 : Float32

@[noinline]

def TorchLean.Numeric.QuotientArithmetic.negMinNormal32 : Float32

@[inline]

def TorchLean.Numeric.QuotientArithmetic.zeroFlag64 (x : Float) : UInt8

@[inline]

def TorchLean.Numeric.QuotientArithmetic.nonfiniteFlag64 (x : Float) : UInt8

@[inline]

def TorchLean.Numeric.QuotientArithmetic.rangeFlags64Using (zero : Float → UInt8) (x : Float) : UInt8

@[inline]

def TorchLean.Numeric.QuotientArithmetic.rangeFlags64 (x : Float) : UInt8

@[inline]

def TorchLean.Numeric.QuotientArithmetic.exposed64 (x : Float) : Bool

@[noinline, specialize #[0]]

def TorchLean.Numeric.QuotientArithmetic.addSub64Flags (zero : Float → UInt8) (z : Float) : UInt8

@[noinline, specialize #[0]]

def TorchLean.Numeric.QuotientArithmetic.product64Flags (zero : Float → UInt8) (x y z : Float) : 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 #[0]]

def TorchLean.Numeric.QuotientArithmetic.quotient64Flags (zero : Float → UInt8) (x z : Float) : 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.add64WithFlags (x y : Float) : Float × UInt8

@[inline]

def TorchLean.Numeric.QuotientArithmetic.sub64WithFlags (x y : Float) : Float × UInt8

@[inline]

def TorchLean.Numeric.QuotientArithmetic.mul64WithFlags (x y : Float) : Float × UInt8

@[inline]

def TorchLean.Numeric.QuotientArithmetic.div64WithFlags (x y : Float) : Float × UInt8

@[inline]

def TorchLean.Numeric.QuotientArithmetic.zeroFlag32 (x : Float32) : UInt8

@[inline]

def TorchLean.Numeric.QuotientArithmetic.nonfiniteFlag32 (x : Float32) : UInt8

@[inline]

def TorchLean.Numeric.QuotientArithmetic.rangeFlags32Using (zero : Float32 → UInt8) (x : Float32) : UInt8

@[inline]

def TorchLean.Numeric.QuotientArithmetic.rangeFlags32 (x : Float32) : UInt8

@[inline]

def TorchLean.Numeric.QuotientArithmetic.exposed32 (x : Float32) : Bool

@[noinline, specialize #[0]]

def TorchLean.Numeric.QuotientArithmetic.addSub32Flags (zero : Float32 → UInt8) (z : Float32) : UInt8

@[noinline, specialize #[0]]

def TorchLean.Numeric.QuotientArithmetic.product32Flags (zero : Float32 → UInt8) (x y z : Float32) : 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 #[0]]

def TorchLean.Numeric.QuotientArithmetic.quotient32Flags (zero : Float32 → UInt8) (x z : Float32) : 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.add32WithFlags (x y : Float32) : Float32 × UInt8

@[inline]

def TorchLean.Numeric.QuotientArithmetic.sub32WithFlags (x y : Float32) : Float32 × UInt8

@[inline]

def TorchLean.Numeric.QuotientArithmetic.mul32WithFlags (x y : Float32) : Float32 × UInt8

@[inline]

def TorchLean.Numeric.QuotientArithmetic.div32WithFlags (x y : Float32) : Float32 × 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 (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan) × FloatLib.Floats.Formats.BinaryInterchange.Model.IEEEStatus) : 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 IEEE values use FloatLib's nearest-even operations and exact finite decoder.

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.