Explicit-entropy stochastic quantization

A stochastic quantizer is represented as an ordinary relational specification whose context contains the incoming entropy and whose result contains the updated entropy. No hidden random source is available to the kernel, so executions can be replayed and proofs can state exactly which entropy transition was used.

Probability laws remain family-specific: some kernels consume a random bit, others a fixed-width word or a splittable generator. Those distributional guarantees are separate from the shared state-transition interface defined here.

def FloatLib.Numerics.Quantization.Stochastic.ofRelation {Context : Type u} {Entropy : Type v} {Exact : Type w} {Result : Type x} (relation : Context → Entropy → Exact → Result → Entropy → Prop) : Spec (Context × Entropy) Exact (Operation.EntropyResult Entropy Result)

Lift an explicit entropy-transition relation into the common quantization interface.

def FloatLib.Numerics.Quantization.Stochastic.ofKernel {Context : Type u} {Entropy : Type v} {Exact : Type w} {Result : Type x} (run : Operation.EntropyKernel Context Entropy Exact Result) : Spec (Context × Entropy) Exact (Operation.EntropyResult Entropy Result)

View a concrete entropy-threading kernel as a singleton stochastic specification.

theorem FloatLib.Numerics.Quantization.Stochastic.implements_ofKernel {Context : Type u} {Entropy : Type v} {Exact : Type w} {Result : Type x} (run : Operation.EntropyKernel Context Entropy Exact Result) : (ofKernel run).Implements fun (state : Context × Entropy) (input : Exact) => run state.fst state.snd input

A concrete entropy kernel implements the singleton specification generated from itself.

theorem FloatLib.Numerics.Quantization.Stochastic.implements_ofRelation_iff {Context : Type u} {Entropy : Type v} {Exact : Type w} {Result : Type x} (relation : Context → Entropy → Exact → Result → Entropy → Prop) (run : Operation.EntropyKernel Context Entropy Exact Result) : ((ofRelation relation).Implements fun (state : Context × Entropy) (input : Exact) => run state.fst state.snd input) ↔ Operation.RefinesEntropy run relation

Conformance to an entropy relation is exactly the pointwise transition property.