docs(machine-readable): surface PRs #79-#82 proof work to bot-coordination state

The Lean+Coq proof repair/extension (PRs #79-#82, merged) was invisible to the
estate's bot-coordination layer. Surface it through the append-designed,
session-end channels — no curated content overwritten:

- debt.a2ml: carry-forward follow-ups as next-session Phase-0 input
  (Coq binop parity, Lean array typing, cap_subsumes_trans; Coq preservation
  rewrite, Lean float binops, echo-types L3 integration blueprint).
- coverage.a2ml: record docs/proofs/verification/ as a visited component.
- methodology.a2ml: populate divergent-invariants (provers are Lean 4 + Coq,
  not Idris2; admit/sorry stay zero; the Coq.Reals axioms are permitted, not
  escape hatches) and known-constraints (CI-gated + toolchain-pinned;
  complementary Lean/Coq subsets; PROOF-NEEDS #2 ill-posed pending a
  maintainer decision).
- STATE.a2ml: add type-safety-proofs to [frontier]; add proof-gates and
  last-proof-shepherd to [ci]. Existing lines preserved.

https://claude.ai/code/session_013wg3Mtq2QFhYi4XVw1Z6z7

Author: claude

.machine_readable/6a2/STATE.a2ml

@@ -5,7 +5,7 @@
 [metadata]
 project = "wokelang"
 version = "0.1.0"
-last-updated = "2026-06-12"
+last-updated = "2026-06-15"
 status = "active"
 
 [project-context]
@@ -27,11 +27,14 @@ proof-assistant = "Isabelle (preferred)"
 echo-types-source = "hyperpolymath/echo-types (constructive Agda formalization of fiber-based structured loss)"
 goal = "the language sorts the hard consent/affine-safety reasoning so users never have to"
 typechecker-note = "TypeChecker::new seeds a ~64-binding builtin prelude (incl. Result/echo constructors)"
+type-safety-proofs = "docs/proofs/verification/ — WokeLang.lean (Lean 4.30.0) + WokeLang.v (Coq 8.18.0): both compile sorry/admit/axiom-free (Coq only the unavoidable Coq.Reals classical+funext axioms from modelling float as the reals) and are CI-gated (lean-proofs.yml, coq-proofs.yml). Proven for the expression core: canonical_forms, progress, preservation, type_safety (multi-step), consent_{monotonicity,preservation}. Strict subset of the surface language; Lean/Coq cover complementary fragments. Repaired from bit-rot + extended 2026-06-14/15 (PRs #79-#82, merged). Full audit: docs/proofs/verification/AUDIT.md"
 
 [ci]
 workflows = "20 GitHub Actions; thin-wrapper reusables from hyperpolymath/standards"
 gates = "rust-ci, dogfood-gate, e2e (Rust+OCaml), governance, security, codeql, scorecard, secret-scanner, hypatia-scan, clusterfuzzlite, mirror, instant-sync"
+proof-gates = "lean-proofs.yml + coq-proofs.yml (added 2026-06-14): machine-check the Lean/Coq developments on every push. Before this NO CI ran a prover, so the 'verified/sorry-free' claim had silently rotted."
 last-shepherd = "2026-06-12 PR #77: fixed 3 Rust tests, empty wokelang.opam, removed banned ReScript VSCode client (governance); issue #78 tracks AffineScript reimpl"
+last-proof-shepherd = "2026-06-14/15 PRs #79-#82 (merged): repaired bit-rotted WokeLang.lean + WokeLang.v; extended the Lean type-safety core; fixed Coq cap_subsumes reflexivity; added the two prover CI gates; wrote docs/proofs/verification/AUDIT.md"
 
 [spec]
 location = "spec/ — grammar.ebnf, axiomatic-semantics.md, system-specs.md, SPEC.core.scm"

.machine_readable/bot_directives/coverage.a2ml

@@ -9,7 +9,7 @@
 
 [metadata]
 version = "1.0.0"
-last-updated = "2026-03-24"
+last-updated = "2026-06-15"
 
 # ============================================================================
 # COVERAGE STATE
@@ -35,6 +35,12 @@ coverage-percent = 0
 # fixes = 3
 # notes = "boot-guardian built, shutdown-marshal built"
 
+[coverage.visited.proofs-verification]
+date = "2026-06-15"
+ring = 1
+fixes = 4
+notes = "docs/proofs/verification/. Repaired bit-rotted WokeLang.lean (Lean 4.30.0) + WokeLang.v (Coq 8.18.0) to compile sorry/admit/axiom-free; extended the Lean type-safety core (or, sub/mul/div/mod with zero-divisor panic, lt/gt/le/ge, capability preorder); fixed Coq cap_subsumes reflexivity (proved cap_subsumes_refl); added lean-proofs + coq-proofs CI gates (no prover had ever run in CI); wrote AUDIT.md. PRs #79-#82, all merged. Carry-forward recorded in debt.a2ml."
+
 # ============================================================================
 # SKIPPED COMPONENTS WITH MUSTS
 # ============================================================================

.machine_readable/bot_directives/debt.a2ml

@@ -9,7 +9,7 @@
 
 [metadata]
 version = "1.0.0"
-last-updated = "2026-03-24"
+last-updated = "2026-06-15"
 
 # ============================================================================
 # DEBT ITEMS
@@ -34,6 +34,30 @@ last-updated = "2026-03-24"
 # impact = "medium"
 # discovered = "2026-03-23"
 
+# --- Formal-proof carry-forward from PRs #79-#82 (2026-06-14/15). See
+# --- docs/proofs/verification/AUDIT.md §"Recommended next proof steps". ---
+
+[[debt.should]]
+component = "docs/proofs/verification/WokeLang.v (Coq)"
+issue = "Binops behind the Lean file: only add/eq/and have rules. Bring Coq up to parity with the extended Lean set — sub/mul/div/mod (div/mod panic to error on zero divisor), comparisons lt/gt/le/ge, and or."
+effort = "medium"
+impact = "medium"
+discovered = "2026-06-14"
+
+[[debt.should]]
+component = "docs/proofs/verification/WokeLang.lean (Lean)"
+issue = "Array typing/evaluation not modelled (tArray + an array congruence/value rule). The Coq file already has this (T_Array/T_Lit_Array + S_Array_step/S_Array_val + well-founded expr_size induction) and is a ready template."
+effort = "medium"
+impact = "medium"
+discovered = "2026-06-14"
+
+[[debt.should]]
+component = "docs/proofs/verification/WokeLang.v (Coq)"
+issue = "cap_subsumes_trans not yet proven (cap_subsumes_refl is). The relation IS transitive; a robust proof needs explicit per-kind case analysis, not the brittle 6x6x6 automation."
+effort = "medium"
+impact = "low"
+discovered = "2026-06-14"
+
 # ============================================================================
 # COULD — would fix eventually
 # ============================================================================
@@ -47,3 +71,24 @@ last-updated = "2026-03-24"
 # effort = "easy"
 # impact = "low"
 # discovered = "2026-03-23"
+
+[[debt.could]]
+component = "docs/proofs/verification/WokeLang.v (Coq)"
+issue = "preservation is a large brute-force `try solve [...]` pile ending in a literal 'Nuclear option' — it compiles and is axiom-honest but is fragile/unreviewable. Rewrite per-case in the style of the Lean preservation."
+effort = "hard"
+impact = "low"
+discovered = "2026-06-14"
+
+[[debt.could]]
+component = "docs/proofs/verification/WokeLang.lean (Lean)"
+issue = "Float arithmetic variants (sub/mul/div on float, mirroring add on float) not modelled."
+effort = "easy"
+impact = "low"
+discovered = "2026-06-14"
+
+[[debt.could]]
+component = "docs/proofs/verification/ (echo-types integration)"
+issue = "Echo-types L3 integration blueprint not started: a Lean port of EchoLinear + EchoResidue as WokeLang/Echo.lean (a Mode-indexed decoration on top of the base type system, leaving progress/preservation intact), modelled on Ephapax's formal/Echo.v Coq port. Connects to the STATE [frontier] echo-types goal."
+effort = "hard"
+impact = "medium"
+discovered = "2026-06-14"

.machine_readable/bot_directives/methodology.a2ml

@@ -9,7 +9,7 @@
 
 [metadata]
 version = "1.0.0"
-last-updated = "2026-03-24"
+last-updated = "2026-06-15"
 spec = "https://github.com/hyperpolymath/standards/blob/main/agentic-a2ml/docs/ADR-002-methodology-layer.adoc"
 
 # ============================================================================
@@ -70,11 +70,13 @@ deepen-not-broaden = true
 #   If parallel → stop. Note as cross-project insight.
 
 [methodology.divergent-invariants]
+# Real invariants for wokelang's formal-verification strength (populated
+# 2026-06-15 from PRs #79-#82). The generic template examples below are
+# DELIBERATELY NOT used — wokelang's provers are Lean 4 + Coq, not Idris2.
 rules = [
-  # Customise per project. Examples:
-  # "Idris2 only for formal verification — no Lean4, Coq, Agda",
-  # "believe_me count must remain zero",
-  # "FFI architecture: Idris2 → RefC → Zig → C ABI (no shortcuts)",
+  "Verification provers for docs/proofs/verification/ are Lean 4 and Coq — deepen these two; do NOT switch to Idris2/Isabelle or add a third prover for the type-safety track (the STATE [frontier] echo-types narrative is a separate, additive layer, not a prover swap)",
+  "sorry / admit / Admitted count in WokeLang.lean and WokeLang.v must remain zero; the ONLY permitted axioms are Coq.Reals' ClassicalDedekindReals.sig_forall_dec + functional_extensionality (unavoidable from modelling float as the reals R) — these are NOT escape hatches, and an Axiom-scanner must not flag them",
+  "The proofs are a deliberate strict SUBSET of the surface language (the expression core) — broaden along the existing Step/HasType + progress/preservation pattern; do not claim full-language verification",
 ]
 
 # Optional: language invariant for the core strength
@@ -88,10 +90,12 @@ rules = [
 # Updated at session end with newly discovered constraints.
 
 [methodology.known-constraints]
+# Discovered 2026-06-14/15 (PRs #79-#82). See docs/proofs/verification/AUDIT.md.
 constraints = [
-  # Customise per project. Examples:
-  # "End-to-end build has never been verified",
-  # "libproject.so does not exist yet — all bindings call stubs",
+  "Formal proofs live in docs/proofs/verification/: WokeLang.lean (Lean 4, pinned v4.30.0 via lean-toolchain) + WokeLang.v (Coq 8.18.0, ubuntu-24.04), both now CI-gated (lean-proofs.yml, coq-proofs.yml)",
+  "Both proof files had silently bit-rotted because no CI ever ran a prover; the toolchain pins are load-bearing and WokeLang.v is version-sensitive — do not bump Coq blindly",
+  "Lean and Coq cover COMPLEMENTARY subsets: Coq is ahead on arrays (T_Array + well-founded expr_size induction); Lean is ahead on binops (sub/mul/div/mod, lt/gt/le/ge, or). Neither is full-language",
+  "PROOF-NEEDS #2 (eval matches the Lean spec) is NOT a well-posed single theorem: core/eval.ml models a different language (units-of-measure, to_bool coercions, no Result) than the Lean/Coq Step relation. Needs a maintainer decision — (a) treat WokeLang.lean as normative and converge implementations, or (b) build a second model faithful to core/eval.ml — before attempting it",
 ]
 
 # ============================================================================