L-KAT-12: Theorem 12.7 KART-GF(16) isomorphism (ch_12 + Coq stub + Rust witness) — parent #572

[gHashTag]

Lane: L-KAT-12 · Theorem 12.7 KART-GF(16) isomorphism
Parent epic: #572
Anchor: φ² + φ⁻² = 3 · DOI 10.5281/zenodo.19227877

Scope

• docs/phd/chapters/ch_12.tex — Theorem 12.7 (KART–GF(16) isomorphism), Lee/GVSU style
• proofs/kart_gf16_isomorphism.v — Coq stub Admitted (R1, R5-honest)
• tests/kart_gf16_witness.rs — Rust brute-force exhaustive witness for n ∈ {2, 4}

Acceptance gates (R5-honest)

• Theorem typeset under R12 Lee/GVSU style with \theorem/\proof/\qed
• Coq stub compiles, marked Admitted, cited in assertions/coq_citation_map.json (LC lane)
• Rust witness passes cargo test --release kart_gf16_witness for n ∈ {2, 4}
• No false promotion of Admitted → Proven; no prune_threshold = 2.65 regressions

PR: #591