Claim #3 — Verification of <core::fmt::Error as From<base16ct::Error>>::from (with Aeneas be86ab0f1989d04944292b345b24c435be3ad10a)

The registered Aeneas mappings cover only decoded_len, encoded_len and From<Error> for core::fmt::Error; general Display formatting is not proved. General-length hexadecimal encoding, decoding, character validation, destination writes, allocation and encode_str's unchecked UTF-8 conversion are not verified. encoded_len behavior above usize::MAX / 2 is outside the proved precondition. Other targets, feature configurations and release overflow behavior were not checked. The separate Display supplement covers only default formatting and this fixed writer, not arbitrary format flags/writers, partial-prefix error policies, other targets or feature configurations. It adds no Aeneas mapping. Encoded-length overflow remains outside the existing precondition. These five codec checks cover only source/destination lengths2/3 for decode and1/4 for encode, with independent1-byte roundtrip decode destinations. They do not prove arbitrary lengths/capacities, general failure-side prefix contents, encode_str UTF8 conversion, allocation or encoded_len overflow. Ordinary Kani supplements add no Aeneas mappings. The Error-default results cover exactly both valid fieldless base16ct Error variants under default x86_64 configuration. They do not verify arbitrary Error implementations, formatting, other configurations/targets or independent std-source/compiler correctness. Deprecated cause/description remain public operations tested directly. The existing decoded_len/encoded_len/foreign-self From mapping, Display1910 and bounded codec1484 evidence remain unchanged; encoded_len above usizeMAX/2 remains unproved. The HexDisplay constructor/projection result establishes logical byte-slice content and length preservation only. It does not establish formatting/encoding/decoding, physical address or pointer identity, arbitrary aliasing/heap behavior, lifetime soundness or general Rust memory safety. Existing Display1910, codec1484 and Error58 protocols retain their separate conditions and compiler boundaries; none is strengthened into an arbitrary backend or formatting theorem by this data-operation result. Primary3 and all existing preconditions remain unchanged.