Format-generic executable sine and cosine

Finite arguments are reduced against a configurable fixed-point approximation of pi / 2. Reduced sine and cosine values are evaluated from exact common-denominator Taylor polynomials and rounded once to Model fmt. Reduction checks Config.trigMaxExponent before constructing the scaled argument. sinCosResult and sinCosWithResult expose a budget failure; the value-only operations return the format's invalid result on failure. A full-range configuration can be requested explicitly.

For leading exponents below -(fracWidth + 2), the provider returns the input and one, preserving tiny sine results without converting them to the fixed-point reduction scale. The kernels remain deterministic approximations without a whole-algorithm accuracy or correct-rounding certificate.

structure FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.TrigReductionError : Type

A finite argument exceeds the exponent budget of the selected reduction data.

• inputExponent : ℤ

  Leading binary exponent of the argument's absolute value.

• maxExponent : ℤ

  Largest leading exponent accepted by the configuration.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.instReprTrigReductionError.repr : TrigReductionError → ℕ → Std.Format

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.instReprTrigReductionError : Repr TrigReductionError

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.instDecidableEqTrigReductionError.decEq (x✝ x✝¹ : TrigReductionError) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.instDecidableEqTrigReductionError : DecidableEq TrigReductionError

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.sinCosTaylorSmallWith (fmt : FloatFormat) (config : Config) (value : Numerics.Dyadic) : Model fmt × Model fmt

Evaluate the reduced sine and cosine kernels and round each result once.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.sinCosScaledWithResult (fmt : FloatFormat) (config : Config) (value : Numerics.Dyadic) : Except TrigReductionError (Model fmt × Model fmt)

Reduce a dyadic argument only within the configuration's exponent budget.

Zero and tiny inputs need no reduction. An ok result records successful evaluation of the approximation policy; it does not certify numerical accuracy.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.sinCosScaledWithResult_exponentBudget (fmt : FloatFormat) (config : Config) (value : Numerics.Dyadic) (hnonzero : value.significand ≠ 0) (hlarge : 0 ≤ Int.ofNat value.significand.log2 + value.exponent) (hbudget : config.trigMaxExponent < Int.ofNat value.significand.log2 + value.exponent) : sinCosScaledWithResult fmt config value = Except.error { inputExponent := Int.ofNat value.significand.log2 + value.exponent, maxExponent := config.trigMaxExponent }

An oversized nonzero argument is rejected before fixed-point reduction, for every format.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.sinCosScaledWith (fmt : FloatFormat) (config : Config) (value : Numerics.Dyadic) : Model fmt × Model fmt

Reduce a dyadic argument, returning invalid results when the exponent budget is exceeded.

def FloatLib.Floats.Formats.BinaryInterchange.Model.sinCosWithProviderResult {fmt : FloatFormat} (getConfig : Unit → Transcendentals.Config) (x : Model fmt) : Except Transcendentals.TrigReductionError (Model fmt × Model fmt)

Evaluate sine and cosine, preserving a reduction-budget failure in the result type.

The provider is called only for finite, nonzero inputs outside the tiny-argument branch. Exceptional inputs retain their ordinary encoded results; this error type is not IEEE status.

def FloatLib.Floats.Formats.BinaryInterchange.Model.sinCosWithProvider {fmt : FloatFormat} (getConfig : Unit → Transcendentals.Config) (x : Model fmt) : Model fmt × Model fmt

Evaluate sine and cosine, mapping reduction-budget failures to the format's invalid result.

def FloatLib.Floats.Formats.BinaryInterchange.Model.sinCosWithResult {fmt : FloatFormat} (config : Transcendentals.Config) (x : Model fmt) : Except Transcendentals.TrigReductionError (Model fmt × Model fmt)

Joint sine/cosine approximation with explicit data and a separate reduction-budget error.

def FloatLib.Floats.Formats.BinaryInterchange.Model.sinCosWith {fmt : FloatFormat} (config : Transcendentals.Config) (x : Model fmt) : Model fmt × Model fmt

Joint deterministic sine/cosine evaluation with explicit approximation data.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.sinWith {fmt : FloatFormat} (config : Transcendentals.Config) (x : Model fmt) : Model fmt

Deterministic sine with explicit approximation data.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.cosWith {fmt : FloatFormat} (config : Transcendentals.Config) (x : Model fmt) : Model fmt

Deterministic cosine with explicit approximation data.

def FloatLib.Floats.Formats.BinaryInterchange.Model.piWith (fmt : FloatFormat) (config : Transcendentals.Config) : Model fmt

The configured approximation to pi, rounded once to the destination format.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.sinCos {fmt : FloatFormat} (x : Model fmt) : Model fmt × Model fmt

Joint sine/cosine evaluation using the default configuration.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.sinCosResult {fmt : FloatFormat} (x : Model fmt) : Except Transcendentals.TrigReductionError (Model fmt × Model fmt)

Joint sine/cosine approximation with an explicit failure when default reduction is too small.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.sin {fmt : FloatFormat} (x : Model fmt) : Model fmt

Sine using the default configuration; a reduction-budget failure gives invalidResult.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.cos {fmt : FloatFormat} (x : Model fmt) : Model fmt

Cosine using the default configuration; a reduction-budget failure gives invalidResult.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.pi (fmt : FloatFormat) : Model fmt

Pi using the default configuration for the destination format.