Explicit entropy for numerical operations

Stochastic rounding and randomized numerical algorithms must expose their entropy state in the function type. EntropyResult and EntropyKernel make that state transition explicit without a global random source or a runtime operation dictionary.

An optimized kernel remains an ordinary monomorphic function. Its proof contract records how the input entropy, result, and output entropy are related.

structure FloatLib.Numerics.Operation.EntropyResult (Entropy : Type u) (Result : Type v) : Type (max u v)

A numerical result paired with the entropy state available to the next operation.

• result : Result

  The operation's ordinary result.

• entropy : Entropy

  The explicitly updated entropy state.

@[instance_reducible]

instance FloatLib.Numerics.Operation.instDecidableEqEntropyResult {Entropy✝ : Type u_1} {Result✝ : Type u_2} [DecidableEq Entropy✝] [DecidableEq Result✝] : DecidableEq (EntropyResult Entropy✝ Result✝)

def FloatLib.Numerics.Operation.instDecidableEqEntropyResult.decEq {Entropy✝ : Type u_1} {Result✝ : Type u_2} [DecidableEq Entropy✝] [DecidableEq Result✝] (x✝ x✝¹ : EntropyResult Entropy✝ Result✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Numerics.Operation.instReprEntropyResult {Entropy✝ : Type u_1} {Result✝ : Type u_2} [Repr Entropy✝] [Repr Result✝] : Repr (EntropyResult Entropy✝ Result✝)

def FloatLib.Numerics.Operation.instReprEntropyResult.repr {Entropy✝ : Type u_1} {Result✝ : Type u_2} [Repr Entropy✝] [Repr Result✝] : EntropyResult Entropy✝ Result✝ → Nat → Std.Format

@[reducible, inline]

abbrev FloatLib.Numerics.Operation.EntropyKernel (Context : Type u) (Entropy : Type v) (Exact : Type w) (Result : Type x) : Type (max (max (max (max u v) w) x) v)

Direct function type for a context-dependent operation that consumes and returns entropy.

@[inline]

def FloatLib.Numerics.Operation.EntropyResult.map {Entropy : Type u} {A : Type v} {B : Type w} (f : A → B) (outcome : EntropyResult Entropy A) : EntropyResult Entropy B

Transform only the ordinary result while preserving the updated entropy state.

@[simp]

theorem FloatLib.Numerics.Operation.EntropyResult.map_result {Entropy : Type u} {A : Type v} {B : Type w} (f : A → B) (outcome : EntropyResult Entropy A) : (map f outcome).result = f outcome.result

Mapping an entropy result applies the supplied function to its ordinary result.

@[simp]

theorem FloatLib.Numerics.Operation.EntropyResult.map_entropy {Entropy : Type u} {A : Type v} {B : Type w} (f : A → B) (outcome : EntropyResult Entropy A) : (map f outcome).entropy = outcome.entropy

Mapping an entropy result leaves its updated entropy state unchanged.

def FloatLib.Numerics.Operation.RefinesEntropy {Context : Type u} {Entropy : Type v} {Exact : Type w} {Result : Type x} (run : EntropyKernel Context Entropy Exact Result) (post : Context → Entropy → Exact → Result → Entropy → Prop) : Prop

Relational correctness of an entropy-threading executable operation.

The relation may express deterministic state evolution, a probabilistic interpretation of the consumed bits, or merely that the selected result belongs to a permitted stochastic support.