Checkpoint 2026-06-05: branch reconciliation (#51/#52) + licence normalisation + provable gate + STATE rewrite

[hyperpolymath]

Durable session checkpoint (survives context compaction). State + owed work as of 2026-06-05.

Branch reconciliation

• ci(codeql): cron weekly→monthly (cut 3, standards#288) #51 (CodeQL cron weekly→monthly) — squash auto-merge ARMED. Verified safe: CodeQL also runs on push+pull_request, so the cron is only a backstop — monthly is not a security regression.
• feat(abi): Tier-2 Idris bindings + retire legacy Foreign + close L10 transitive cycle #52 (abi-tier2: Tier-2 Idris bindings + retire legacy Foreign + close L10 transitive cycle) — squash auto-merge ARMED. Proofs machine-verified 2026-06-05: idris2 0.8.0 (pinned commit 15a3e4e…), --build vclut-core.ipkg exit 0 (12/12 modules), L4 --check exit 0, zero proof-escape — byte-identical to main baseline, no regression. (Pre-existing-on-main nit: 2 implicit-bind shadow warnings in ABI.Layout:232/234.)
• After both merge: delete stale local branches; reconcile to one main.

Licence — CRITICAL (REUSE 6.2.0 audit 2026-06-05; reuse lint: FAIL)

Owner decision so far: MPL-2.0 canonical (code), CC-BY-SA-4.0 (docs).
⚠️ Reconfirm before any bulk flip: the 34 AGPL-3.0-or-later files are a coherent cluster — the trusted boundary crates (parse, attest, recompute-wasm) + the proof corpus (verification/proofs/*, src/core/Decide.idr, WireConformance/WireDecode, proof-corpus.yml, parse-gate.yml). That's exactly the security/verification core, deliberately flipped to AGPL in #46 "per estate policy". Root LICENSE + root Cargo.toml are AGPL; 315 other files are MPL. So this may be intentional (AGPL core / MPL tooling), not an accident. → Decide: (A) MPL everywhere, or (B) keep AGPL core + MPL tooling.
Unambiguous bug regardless of A/B: 3 Cargo.toml declare license = "PMPL-1.0-or-later" (src/interface/{parse,attest,recompute-wasm}) — PMPL is not a valid SPDX id (breaks cargo publish); set to the chosen licence.
Other fixes: add LICENSES/{MPL-2.0,AGPL-3.0-or-later,CC-BY-SA-4.0}.txt; setup.sh:255 + docs/practice/AI-CONVENTIONS.adoc:26 (SPDX inside a string) → wrap REUSE-IgnoreStart/End; SPDX headers on ~44 docs (CC-BY-SA-4.0) + 5 root files. GitHub Licensee currently reports AGPL-3.0 (root LICENSE) — confirm intended.
Provable gate to install (replaces the toothless check): REUSE lint + a k9/Nickel licence-policy contract (closed per-path allow-list, one-SPDX-per-file) + pre-commit + a required CI check.

STATE / machine_readable

• STATE.a2ml last-updated 2026-04-25; route-to-mvp still describes the template's milestones (its own NOTE admits it); no mention of the Phase-5 proof corpus — rewrite.
• De-dupe: .machine_readable/STATE.a2ml is byte-identical to .machine_readable/6a2/STATE.a2ml — single-source it.
• Reconcile contractiles across 4 locations (.machine_readable/*.contractile, .machine_readable/contractiles/, top-level contractiles/, docs/templates/contractiles/).

Proof disclosed-limits (keep documented per VERIFICATION-STANCE)

NaN-payload reconstruction; cross-module Refl non-reduction (schema verdicts pinned Rust-side); L3 subquery scoping; L9/L10 predicate depth; additive↔ceil alignUp sliver; C-ABI Tier-2 fallback not re-checkable.

Ref: https://claude.ai/code/session_01W9Voe3JceP66Bna9FT4jME