Claim #14 — Verification of <ascii::AsciiChar as ascii::ToAsciiChar>::to_ascii_char (with Aeneas be86ab0f1989d04944292b345b24c435be3ad10a)

Fifty-one API mappings are Lean-proved; the other explicitly described scalar/case results are separate Kani body checks. The unsafe identity results cover only ToAsciiChar for AsciiChar, AsAsciiStr/AsMutAsciiStr for an existing AsciiStr, and IntoAsciiString for the original default-allocator Vec<AsciiChar>. Inputs must already be valid Rust values of those exact types. Those identity proofs do not cover unchecked scalar conversions; the separate five Kani scalar contracts cover only the documented 0..127 safety domain. They do not cover unchecked byte slices, str, Vec<u8> or other implementations, and do not independently establish general pointer, lifetime or allocator safety. The Lean mathematical code-fold is not a proof of the separate case-conversion APIs; those original bodies instead have the separately recorded full-domain Kani checks. General input validation, the remaining AsciiStr/AsciiString APIs, allocation, serde and arbitrary unsafe conversions remain unproved. The official Vec model stores only element sequences and a length bound. It does not represent capacity, Rust isizeMAX allocation limits, allocator availability, OS failure or OOM. Thus the push result and failure partition are properties of that model; no exact physical allocation/panic behavior or capacity preservation is claimed. Case conversion and printable-picture behavior have separate Kani evidence, not Lean proofs. Invalid enum representations are outside the input domain. The original is_digit_strange_radixes test fails on the pinned modern Rust because char::is_digit panics at radix 0/1; the crate is_digit API is covered separately for all radix values; the failed test comparison invokes std char::is_digit at radix 0/1. Remaining original tests pass with only that test excluded. The five checked scalar conversion bodies and the stated case/character bodies have separate Kani evidence, rather than additional Lean claims. The original AsciiChar::new constructor is checked only on ASCII inputs by the generator; its non-ASCII panic domain remains unproved. All-feature/no-default configurations and other targets were not proved. The four typed-vector claims exclude Vec<u8>, other Vec element/allocator types and all other From/IntoAsciiString implementations. Vector length and element contents are represented, while capacity, allocation addresses and physical allocation behavior are not. These results establish no guarantee for the distinct Vec<u8> implementations or other element types. The generic from_ascii delegation does not independently prove any arbitrary ToAsciiChar implementation validates or terminates. The generic Error description constant does not validate its stored index or owner. The new scalar Kani dependency copies contain archive-identical runtime src9 and Cargo.toml, but omit archive-root tests.rs; crate tests were not run for these supplemental checks. Full package restoration and general unsafe-call safety outside the documented domain are not claimed. The Error2/Default1 checks use default x86_64 Kani and the original runtime src9/Cargo.toml, with root tests.rs absent and not run. They do not establish pointer address identity, general alias/lifetime semantics, other configurations/targets or const evaluation. The manual static-reference Default is distinct from derived AsciiString Default and from AsciiString::new.