Proof contract for configured posit quire decoding

Quire-backed algorithms use the same ExactDecoder capability as the other configured formats. This bridge identifies that generic operation with the quire's complete public decoder; the equality is definitional and adds no second decoding path.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.Quire.Conversion.exactDecoder_run {format : Formats.Posit.Format} (value : Formats.Posit.Quire.Model format) : ExactDecoder.run value = decode value

The installed quire source capability is its public complete decoder.