[Feature]: C3 — real Idris2 contract spec + strict Elixir runtime validation boundary (drop the fictional ABI claims)

[hyperpolymath]

Part of #274 (pipeline epic). Resolves the C3 checklist line ("Verified-ABI payload boundary — or drop the Idris-inside claim") with the owner-selected middle path: build a minimal real Idris2 contract now, enforce at runtime in Elixir, and stop claiming what doesn't exist.

The problem

feedback-o-tron has zero .idr files (all removed 2026-03-29 as empty scaffolding), a no-op Zig FFI, and README badges claiming "Idris-inside". The diagram's "Clean Validated Payload → Idris2 Verified ABI" stage was fictional.

What this builds

1. src/abi/FeedbackOTron/Contract.idr — a small, genuinely compiling, %default total Idris2 model of the clean-payload contract: Form/Field/Answers, validate : Form -> Answers -> Either (List Violation) ValidPayload with ValidPayload's constructor unexported (unconstructable except via validate), plus provable completeness lemma(s). No believe_me, no postulate. Checked in CI (proofs.yml, idris2 --check).
2. FeedbackATron.Synthesis.FormValidator — the runtime enforcement mirroring the Idris contract field-by-field (required-missing / unknown-field / invalid-option), applied in Submitter before any dispatch when template_data is present; violations fail closed.
3. Honesty repairs — README badges, TOPOLOGY.md, STATE.a2ml, ABI-FFI-README.md all reconciled: Idris2 = verified contract spec (real), Elixir = runtime boundary, Zig FFI = stub and labeled as such.

Explicitly deferred

Full FFI enforcement — the Idris-derived validator actually on the dispatch path via Zig NIF — is tracked as a follow-up issue in feedback-o-tron (linked from the PR). Connects to the boj proof tracks (#197, #200).

Delivery

Same draft-PR set as the C1+C2 issue, branch claude/feedback-o-tron-boj-integration-4iuxyt.