Packing equivalence for configured posits

Configured posits may live in a byte, native word, fixed pair of limbs, or a wide carrier. The public model is independent of that choice, so packing and decoding must be lossless for every storage plan.

These mutual-inverse theorems discharge that obligation once by case analysis on the plan. Codec instances and arithmetic capabilities reuse them instead of maintaining width-specific conversion proofs that could drift apart.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Configured.Code.toModel_ofModel {format : Format} {plan : StoragePlan format} (value : Model format) : (ofModel value).toModel = value

Decoding a freshly packed posit model returns that exact model.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Configured.Code.ofModel_toModel {format : Format} {plan : StoragePlan format} (code : Code plan) : ofModel code.toModel = code

Repacking a decoded posit code returns the original packed code.