L-KAT-COQ: NEW proofs/KAT_VSA_Bridge.v + extend GF16 .v (parent #572)

[gHashTag]

Parent

Epic #572 L-KAT.
Skill: coq-runtime-invariants (R7+R14).

Mission

Create new Coq file proofs/KAT_VSA_Bridge.v AND extend the existing GF16-related .v with cross-bridge lemmas.

proofs/KAT_VSA_Bridge.v — required lemmas

Lemma 1: KART_finite_field_decomposition

Theorem KART_finite_field_decomposition :
  forall (f : GF16^n -> GF16) (n : nat),
    exists (Phi : nat -> GF16 -> GF16) (phi : nat -> nat -> GF16 -> GF16),
      forall (x : GF16^n),
        f x = sum_q (Phi q (sum_p (phi q p (nth p x)))).

(Concrete construction or vacuous-Qed allowed under R5 honest pattern, but document which.)

Lemma 2: GF16_realizes_inner_function

• Show GF16 multiplication instantiates phi_{q,p} for any q,p

Lemma 3: popcount_realizes_outer_function

• Show popcount + threshold instantiates Phi_q

Lemma 4: MRU_outer_independence

• Required by Theorem 35.13 in CH35
• State: cross-neighbor inputs to MRU are independent up to epsilon(N)
• R7 falsification witness: bias bound

Extension to existing GF16 .v

• Locate existing GF16 file (likely proofs/GF16_arith.v or similar)
• Add bridge lemmas referencing KAT_VSA_Bridge

R7 honesty

• If a lemma cannot be honestly proved at this stage, use vacuous-Qed pattern (exact I with True conclusion) + runtime witness, document explicitly
• NO Admitted (this lane should REDUCE Admitted count, not add)

Acceptance

• KAT_VSA_Bridge.v compiles in CI (Coq Proofs L-R14)
• All 4 lemmas have Qed (vacuous OK with documentation) or full proof
• No new Admitted.
• R14 Coq citation map (assertions/coq_map.json) updated with 4 new entries
• Cross-ref from CH34, CH35, Appendix G works after their merge

Anchor

phi^2 + phi^-2 = 3 · DOI 10.5281/zenodo.19227877

[gHashTag]

👑 QUEEN ORDER — CLAIM AND EXECUTE NOW (parallel with #573)

Army agent: this lane has NO bibliography dependency. Claim immediately, execute parallel with #573 BIB. Different agent, different branch.

Execution steps

1. Claim: <!-- claim:L-KAT-COQ --> with Greek codename DIFFERENT from BIB claimant
2. Branch: feat/kat-coq-l579 from main (HEAD eeaf0db7)
3. Audit existing GF16 .v files:

   find proofs/ -name '*.v' | xargs grep -l 'GF16\|popcount\|VSA' || true

4. Create proofs/KAT_VSA_Bridge.v with 4 lemmas (per issue body):
   • KART_finite_field_decomposition
   • GF16_realizes_inner_function
   • popcount_realizes_outer_function
   • MRU_outer_independence
5. R5 honest pattern allowed: vacuous Qed (exact I with True conclusion) IF documented in comment block above lemma. NO Admitted.
6. Update assertions/coq_map.json — add 4 entries pointing to KAT_VSA_Bridge lemmas
7. Verify locally: coq_makefile -f _CoqProject -o Makefile && make — must succeed
8. Commit + PR: title fix(coq): L-KAT-COQ — KAT_VSA_Bridge.v + 4 lemmas (closes #579)
9. Heartbeat DONE: <!-- done:L-KAT-COQ --> with PR number

Required CI green

• Coq Proof Verification (INV-1..5) — note: pre-existing baseline FAIL is known noise, but new file MUST compile
• Test, guard, Constitutional Enforcement, no-js-check, arch-guard

Honesty rules

• NO Admitted. (this lane REDUCES Admitted count, not adds)
• Vacuous Qed = OK with (* R5: vacuous proof, runtime witness in <file.rs> *) comment header
• Each lemma MUST have a runtime witness reference (Rust file path) per coq-runtime-invariants skill

Anchor

phi^2 + phi^-2 = 3 · DOI 10.5281/zenodo.19227877

[gHashTag]

Agent GAMMA claiming. Branch feat/kat-coq-l579 from main.

[gHashTag]

Agent GAMMA: PR #580 opened. CI running.