Claim #36 — Verification of <byteorder::BigEndian as byteorder::ByteOrder>::read_i48 (with Aeneas be86ab0f1989d04944292b345b24c435be3ad10a)

This covers 20 selected writer methods, eight unsigned and eight signed readers, four native-target unsigned identity conversions, and two handwritten Default methods, not all public APIs. Fixed 16/32/64/128-bit reads, variable-width writers, other bulk and in-place conversions, I/O extensions, other targets and release extraction remain unproved. The float result establishes bit serialization only: floating arithmetic, comparisons, rounding, numeric accuracy, NaN arithmetic and signaling behavior are not modeled. Kani public-writer buffer lengths are fixed at 6 and 10; arbitrary valid slice lengths are quantified separately by the Lean theorems. The signed from_slice defaults contain unsafe slice reinterpretation and are not covered; the floating conversions and opposite-endian/other-target paths are also unproved. The byteorder-lite eight-method result is not assumed transferable across versions. Panic messages and unwinding side effects are not specified. The separate variable-width writer comparison is limited to normal-success inputs and the 32-byte allocation shape. It does not establish failing inputs, arbitrary lengths/allocations, or independent memory safety. It adds no Aeneas API claims.