You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
* feat(strat): Stage-2 REQ-4 — the classifier ops half (Rust) + the differential battery (M2b)
Mirror the Lean kernel classifier from REQ-3 (#325, Thermite.Strat.Cls.admitted)
in Rust, beside thermite-spec's existing validator, and hold the two byte-equal
over a generated clause space.
- thermite-spec/src/classifier.rs: a line-for-line transliteration of the Lean
Cls classifier over the sort-typed surface — Sort2/Mach/Tm/Rel/Atom/Frm,
fin_carrier (R1), idx_grammar (R2 BMS), nnf, sort_graph (E1∪E2), and
admitted = fin_carrier && idx_grammar && acyclic(sort_graph(nnf)). The one
intentional divergence is acyclic: a polynomial transitive-closure computing the
SAME boolean as the Lean exponential Roy–Warshall reach (they agree by
acyclic_iff_no_cycle). classify returns Admitted | Rejected(frozen RejectReason:
seq-quantifier / index-grammar / the named cycle) | Unknown; the four §3.2
micro-examples are unit-tested to the Lean outcomes. A shared S-expression wire
format round-trips every Frm.
- thermite-tv/src/gen.rs: gen_strat_formulas extends the SplitMix64 generator with
well-sorted binder productions (Q5: corpus-mimicking + uniform-random arms),
deterministic, covering every verdict class.
- lean/Thermite/Strat/Cls/Wire.lean: the Lean half — a wire-format parser to the
kernel Cls.Frm + a root main running the kernel Cls.admitted per stdin line
(lake env lean --run); added as a scripts/lean-axiom-probe.sh build target.
- forge/src/strat_tv.rs + `forge strat-tv`: the differential harness — gen ->
classify (Rust) -> lake env lean --run (kernel) -> compare. A disagreement is a
verification-failure exit; the unknown-on-admitted tripwire is counted, logged,
escalated (classifier-suspect), never silently retried; lake-absent is an honest
skip. forge/tests/strat_differential.rs (lake-gated, runs in the lean CI job)
asserts Rust == Lean admitted on N=200 formulas with zero disagreements + zero
tripwire at the pinned and a rotated seed (AC-4).
- Register REQ-S2-4 in the registry with typed evidence; regenerate the status view.
Self-verified: cargo test --workspace (179 groups, 0 fail), clippy -D warnings, fmt
--check; lake build + scripts/lean-axiom-probe.sh green (classifier_correct
axiom-clean); tooling/reqs check + req-status + doc-drift clean.
REQ-4 / AC-4 (.design/stage2-stratified-cage.md); issue #326; gate G2.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
* chore(doc-drift): re-pin design docs for Stage-2 REQ-4 (#326)
The REQ-4 classifier-ops change touched four doc-drift-governed files; re-pin each
governing design doc's content-sha256 to the new digest (the legacy commit pin stays
at its stable-main ancestor — content-sha256 is the active check):
- .design/forge/cli.md — forge/src/cli.rs grew `forge strat-tv` + the
ForgeError::StratDifferential variant.
- .design/scaffold/workspace.md — thermite-spec/src/lib.rs `pub mod classifier;`
+ forge/src/main.rs `mod strat_tv;` (additive).
- .design/tooling/req-registry.md — registry.toml/status.md grew REQ-S2-4 + the
regenerated status view (447 reqs, --check clean).
- .design/verified/contract-tv.md — thermite-tv/src/gen.rs grew gen_strat_formulas
(a new generator; the contract-TV REQs unchanged).
doc-drift.py + make doc-drift clean.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
Copy file name to clipboardExpand all lines: .design/forge/cli.md
+2-2Lines changed: 2 additions & 2 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -3,8 +3,8 @@
3
3
<!--
4
4
tier: 3-component
5
5
status: shipped
6
-
audited-sha: 5ae0816c042debb01c70eb9b89c775837f0c0f24 (re-pinned 2026-06-18 for umbrella REQ-2c / AC-4, the rotating-seed scheduled-CI watchdog: the only change to this doc's governed file (cli.rs) is the additive `--seed <u64>` flag on `forge tv` — parsed into `Command::Tv.seed`, threaded to `run_tv`→`run_generated` for the off-corpus space only (the corpus phase keeps the pinned seed); a missing/non-numeric value is a Usage error (REQ-8 flag discipline, test `parses_tv_seed_flag`). Every other subcommand + flag parse is unchanged. prior: §6 metrics dashboard `--metrics` value)
audited-sha: 5ae0816c042debb01c70eb9b89c775837f0c0f24 (content-sha256 re-pinned 2026-06-20 for stage-2 REQ-4 / AC-4 (#326), the classifier differential battery: the change to this doc's governed file (cli.rs) is the additive `forge strat-tv [--generated N] [--seed <u64>] [--json]` subcommand (`Command::StratTv` → `run_strat_tv`) plus the new `ForgeError::StratDifferential` harness-error variant; every other subcommand + flag parse is unchanged. The legacy commit pin stays at the 5ae0816c stable-main ancestor; only the active content-sha256 digest moves. prior: 2026-06-18 umbrella REQ-2c / AC-4 rotating-seed `--seed` flag on `forge tv`; §6 metrics dashboard `--metrics` value)
Copy file name to clipboardExpand all lines: .design/reqs/registry.toml
+46Lines changed: 46 additions & 0 deletions
Original file line number
Diff line number
Diff line change
@@ -7017,6 +7017,52 @@ kind = "command"
7017
7017
target = "bash scripts/lean-axiom-probe.sh"
7018
7018
note = "AC-3 (ci): Thermite.Strat.Fragment added as a build target (transitively pulls Nnf/Graph) so a sorry/broken proof under Strat/ fails the gate; Thermite.Strat.Cls.classifier_correct added to the axiom-gated THEOREMS list so its axioms must stay subset of {propext, Classical.choice, Quot.sound}"
7019
7019
7020
+
[[requirement]]
7021
+
id = "REQ-S2-4"
7022
+
title = "Stage-2 classifier ops half (Rust) + the differential battery — thermite-spec classifier + forge strat-tv"
7023
+
owner = ".design/stage2-stratified-cage.md"
7024
+
status = "shipped"
7025
+
scope = "verified"
7026
+
summary = "The admission-classifier OPS half + the M2b differential battery (stage2-stratified-cage.md REQ-4 / AC-4; child of thermite2-program.md REQ-10; gate G2; spec of record the stage-2 metatheory sketch GH#2 §1-§3,§5). Mirrors the REQ-3 Lean KERNEL classifier (#325, merged 80e59203) in Rust, beside thermite-spec's existing validator, over the SORT-TYPED Thermite.Strat.Cls surface (Sort2 mach/seq/opaque + the Read/Len/Cast/IdxOp/Mul/spec-fn term vocabulary + sorted binders) — NOT REQ-1's minimal semantic-spine Frm. (1) thermite-spec/src/classifier.rs: a line-for-line transliteration of the Lean defs — Sort2/Mach/Tm/Rel/Atom/Frm, fin_sort/fin_carrier (R1), same_width/has_bound_var/idx_ok_tm/idx_grammar_at (R2 BMS index grammar), nnf/nnf_neg, edges_tm/edges_atom/edges_frm + sort_graph (E1 alternation ∪ E2 function-flow, on NNF), and admitted = fin_carrier && idx_grammar && acyclic(sort_graph(nnf)). The ONE intentional divergence: acyclic is a polynomial transitive-closure (Graph::acyclic) computing the SAME boolean as the Lean exponential Roy-Warshall reach (they agree by acyclic_iff_no_cycle), so the differential is fast. classify returns Verdict {Admitted | Rejected(RejectReason) | Unknown}; the FROZEN rejection vocabulary RejectReason = SeqQuantifier (R1, the only non-finite Sort2) | IndexGrammar (R2) | SortGraphCycle{cycle} (R3, the named cycle). The four §3.2 micro-examples (a[a[i]] self-loop, the width-preserving cast cycle, the kv alternation cycle, sortedness) are unit-tested to the SAME admit/reject outcomes the Lean Fragment.lean decide-checks. A shared compact S-expression WIRE format (to_wire/parse_frm) round-trips every Frm. (2) thermite-tv/src/gen.rs: gen_strat_formulas(seed,n) extends the SplitMix64 generator with well-sorted binder productions — the Q5 default two arms (a corpus-mimicking arm spanning every admit/reject class + a uniform-random bounded recursive-descent arm), every var an in-scope de Bruijn index carrying its binder sort; deterministic (same seed -> same stream), covering every verdict class. (3) lean/Thermite/Strat/Cls/Wire.lean: the Lean half — a partial recursive-descent parser from the wire format back to the kernel Cls.Frm + a root main that runs the KERNEL Cls.admitted (the exact REQ-3 admitted, not a re-impl) on each stdin line, printing one verdict line; an IO tool (no theorem), wired into scripts/lean-axiom-probe.sh as a build target (so a compile break fails the Lean CI job and its dep Strat.Fragment is built). (4) forge/src/strat_tv.rs + the forge strat-tv subcommand: the differential harness — generate N formulas, classify each with BOTH the Rust classifier AND lake env lean --run on the Lean admitted (wire on stdin), compare verdict-for-verdict. A DISAGREEMENT (Rust admit != Lean admit, both definite) is a verification-failure exit (the hard CI failure audit check [8] raises, NOT a ForgeError). The unknown-on-admitted TRIPWIRE (a formula the Rust classifier could not vouch for — Verdict::Unknown, or a Lean parse-error — while the kernel admitted it) is the classifier-suspect signal: counted, logged, escalated (also fails the gate), never silently retried; structurally 0 since classify is total. lake-absent is an honest Skipped (exit 0, never a false pass). AC-4 met: forge/tests/strat_differential.rs (lake-gated, runs live in the lean CI job via cargo nextest run -p forge) asserts the Rust verdict == Lean admitted on N=200 generated formulas with ZERO disagreements + ZERO tripwire, at the pinned seed and a rotated seed; locally verified across 5 seeds (600 formulas) with zero disagreements and a ~50/50 admit/reject balance. cargo test/clippy -D warnings/fmt clean; lake build green."
7027
+
remaining_scope = "The Rust ops-half classifier + the differential battery ONLY. The encoder + T1-S (REQ-5 / #327, the bridge between the Cls classifier surface and the REQ-1 semantic spine), the audit-script [8]/[1'] integration (REQ-9 / #331 — this increment ships the runnable battery + the lake-gated forge test that runs in the lean CI job, NOT the scripts/audit.sh check-[8] wiring), and the rest of the stage-2 tree are SEPARATE downstream requirements."
note = "(1) the Rust admission classifier mirroring Lean Cls.admitted: Sort2/Mach/Tm/Rel/Atom/Frm + fin_carrier (R1) + idx_grammar (R2) + nnf + sort_graph (E1∪E2) + Graph::acyclic (polynomial, result-identical to the Lean Roy-Warshall reach) + classify/admitted + the frozen RejectReason vocabulary + the wire to_wire/parse_frm; the four §3.2 micro-examples unit-tested to the Lean outcomes"
7035
+
7036
+
[[requirement.evidence]]
7037
+
kind = "symbol"
7038
+
target = "thermite_spec::classifier::admitted"
7039
+
note = "the bare boolean mirror of Lean Thermite.Strat.Cls.admitted — the value the differential battery holds byte-equal to lake env lean --run on the kernel admitted"
7040
+
7041
+
[[requirement.evidence]]
7042
+
kind = "file"
7043
+
target = "thermite-tv/src/gen.rs"
7044
+
note = "(2) gen_strat_formulas — the SplitMix64 generator extended with well-sorted binder productions (Q5: corpus-mimicking + uniform-random arms), deterministic, covering every verdict class (admit + each frozen rejection reason)"
7045
+
7046
+
[[requirement.evidence]]
7047
+
kind = "file"
7048
+
target = "lean/Thermite/Strat/Cls/Wire.lean"
7049
+
note = "(3) the Lean half: a wire-format recursive-descent parser to the kernel Cls.Frm + a root main running the kernel Cls.admitted per stdin line; an IO tool, a scripts/lean-axiom-probe.sh build target"
7050
+
7051
+
[[requirement.evidence]]
7052
+
kind = "file"
7053
+
target = "forge/src/strat_tv.rs"
7054
+
note = "(4) the differential harness: gen -> classify (Rust) -> lake env lean --run (kernel) -> compare; disagreement = verification-failure exit, the unknown-on-admitted tripwire (classifier-suspect, escalated), lake-absent = honest Skipped; the forge strat-tv subcommand drives it"
7055
+
7056
+
[[requirement.evidence]]
7057
+
kind = "test"
7058
+
target = "forge/tests/strat_differential.rs"
7059
+
note = "AC-4 (ci): the lake-gated live battery — Rust verdict == Lean admitted on N=200 generated formulas with zero disagreements + zero tripwire, at the pinned seed and a rotated seed; runs in the lean CI job (cargo nextest run -p forge with the spine built)"
7060
+
7061
+
[[requirement.evidence]]
7062
+
kind = "command"
7063
+
target = "cargo run -p forge -- strat-tv --generated 200"
7064
+
note = "the runnable differential driver (the rotating-seed / audit check [8] entry point; add --seed <u64> to rotate): zero disagreements AND zero tripwire -> exit 0; a disagreement or a tripwire -> verification-failure exit; lake-absent -> honest skip (exit 0)"
7065
+
7020
7066
[[requirement]]
7021
7067
id = "REQ-SKILL-V2-FORGE-TIER"
7022
7068
title = "THERMITE.skill.md v2 — the agent-facing Stage-1 forge-tier section"
| REQ-S2-1 | shipped | `.design/stage2-stratified-cage.md` | | verified | Stage-2 Strat spine foundation — Strat/{Syntax,Carrier,Denote}.lean + PinFiniteEscape | file: `lean/Thermite/Strat/Syntax.lean` - (1) the de Bruijn Tm/Atom/Frm language + lift/subst inheriting the SPIKE-1 §1/§3 conventions verbatim (cutoff bumps under all/ex); the stratification keeps carrier vars in eq atoms only<br>file: `lean/Thermite/Strat/Carrier.lean` - (2) CarrierAssign — the hand-rolled finiteness witness (deq+enum+complete as DATA, no Mathlib Fintype) + the Env/cons/insert de Bruijn environment algebra<br>file: `lean/Thermite/Strat/Denote.lean` - (3) sdenote (Bool via List.all/any folds, QFree-oracle-parametric) + the v1 deferral; no Mathlib on the import path<br>symbol: `sdenote_all_iff` - (3) the (R1) upgrade: the all fold = true iff the genuine forall, CONSUMING CarrierAssign.complete — the sole semantic consumer of the finiteness witness<br>symbol: `CarrierAssign` - (2) the opaque-sort bundle with the hand-rolled finiteness witness (deq/enum/complete carried as data), the SPIKE-1 §6 verdict's production input — no Mathlib Fintype<br>symbol: `canonicalQOracle` - (3) the v1 deferral at QFree atoms: the oracle reads the embedded Expr's truth off Thermite.denote (consumed, not re-proven); sdenote_qf_canonical is the bridge<br>test: `lean/Thermite/PinFiniteEscape.lean` - (4) the (R1) pin battery: finiteEscape_pinned / incompleteEnum_escapes (an incomplete-enum fold lies about the forall) + sdenote_all_iff_instance — decide-checked on a concrete 2-element carrier<br>command: `bash scripts/lean-axiom-probe.sh` - AC-1 (ci): the CI Lean job builds Thermite.Strat.Denote + Thermite.PinFiniteEscape (added as build targets), so a sorry or broken proof under Strat/ fails the gate; the probe also confirms the spine theorems stay axiom-clean | |
294
294
| REQ-S2-2 | shipped | `.design/stage2-stratified-cage.md` | | verified | Stage-2 SubstKit binder kit — Strat/SubstKit.lean + PinBrokenLift | file: `lean/Thermite/Strat/SubstKit.lean` - the ~25-lemma binder kit: the load-bearing sdenote_push_lift/sdenote_subst (note §4 shapes verbatim, q as fixed context) + term/atom/env companions + the syntactic lift/subst inverse + the binder-introduction corollaries; comment cites the note sha256 9acf3685; in-file #print axioms = [propext, Quot.sound]<br>symbol: `sdenote_push_lift` - load-bearing lemma A: weakening is denotation-invariant — sdenote q (liftFrm c φ) (insert c v ρ) = sdenote q φ ρ; note §4 verbatim shape, axiom-clean<br>symbol: `sdenote_subst` - load-bearing lemma B: the substitution lemma — sdenote q (substFrm j s φ) ρ = sdenote q φ (insert j (tdenote s ρ) ρ); note §4 verbatim shape, axiom-clean<br>symbol: `substFrm_liftFrm` - the syntactic lift/subst inverse (substTm_liftTm → substAtom_liftAtom → substFrm_liftFrm): substituting at the cutoff a formula was lifted past is the identity — the de Bruijn statement of freshness underwriting REQ-5's fresh-name discipline<br>test: `lean/Thermite/PinBrokenLift.lean` - the broken-lift micro-pin: liftBadFrm omits the cutoff bump under all/ex; brokenLift_breaks_push_lift refutes sdenote_push_lift for it (decide, 2-element carrier); correctLift_satisfies_push_lift pins the divergence to the off-by-one alone<br>command: `bash scripts/lean-axiom-probe.sh` - AC-2 (ci): Thermite.Strat.SubstKit + Thermite.PinBrokenLift added as CI build targets, so a sorry or broken proof in the kit (or the pin) fails the Lean gate; lake build green, the spine theorems stay axiom-clean | |
295
295
| REQ-S2-3 | shipped | `.design/stage2-stratified-cage.md` | | verified | Stage-2 classifier kernel half — Strat/{Nnf,Graph,Fragment}.lean + T3-C classifier_correct | file: `lean/Thermite/Strat/Nnf.lean` - (1) the classifier surface syntax (Sort2 + rich Tm/Atom/Frm with sorted binders, faithful to metatheory §1.2) + the structural denotation fdenote + nnf/prenex with nnf_sound (unconditional) / prenex_sound (dom != [])<br>file: `lean/Thermite/Strat/Graph.lean` - (2) sortGraph (E1 alternation + E2 function-flow, on NNF) + the Roy-Warshall acyclic check + acyclic_iff_no_cycle (structural vertex-peel induction, no pigeonhole, Mathlib-free) + sortGraph_complete (Wf: node set closed for edges)<br>file: `lean/Thermite/Strat/Fragment.lean` - (3) finCarrier (R1) + idxGrammar (R2) + admitted + the declarative Frag + the four §3.2 decide-checked micro-examples<br>symbol: `classifier_correct` - T3-C (AC-3): admitted phi = true <-> Frag phi, axiom-clean (#print axioms = {propext, Quot.sound}); substance is acyclic_iff_no_cycle consuming sortGraph_complete<br>symbol: `acyclic_iff_no_cycle` - the graph-theoretic soundness theorem: the Roy-Warshall DFS acyclic coincides with the absence of a transitive-closure (TC/Chain) cycle, by structural Warshall induction — the core-Lean-only realisation of the sketch's acyclic-vs-Path lemma<br>symbol: `nnf_sound` - the load-bearing NNF denotation-preservation lemma (§3.1 'NNF is load-bearing: ¬∀ = ∃¬'), unconditional; with nnfNeg_sound the mutual pair<br>test: `lean/Thermite/Strat/Fragment.lean` - AC-3 examples: ex_selfLoop_rejected / ex_castCycle_rejected (+ ex_castCycle_idxGrammar_ok) / ex_kvCycle_rejected / ex_sortedness_admitted — decide-checked (kernel, not native_decide) with the expected admit/reject outcomes<br>command: `bash scripts/lean-axiom-probe.sh` - AC-3 (ci): Thermite.Strat.Fragment added as a build target (transitively pulls Nnf/Graph) so a sorry/broken proof under Strat/ fails the gate; Thermite.Strat.Cls.classifier_correct added to the axiom-gated THEOREMS list so its axioms must stay subset of {propext, Classical.choice, Quot.sound} | Kernel (Lean) half ONLY. The Rust classifier mirroring admitted in thermite-spec + the SplitMix64 differential battery (REQ-4 / AC-4, #326), and the [1'] axiom-probe extension to the OTHER stratified soundness theorems (strat_ref_sound/strat_lowering_faithful/restrat_conservative; REQ-9 / #331), are separate requirements. |
296
+
| REQ-S2-4 | shipped | `.design/stage2-stratified-cage.md` | | verified | Stage-2 classifier ops half (Rust) + the differential battery — thermite-spec classifier + forge strat-tv | file: `thermite-spec/src/classifier.rs` - (1) the Rust admission classifier mirroring Lean Cls.admitted: Sort2/Mach/Tm/Rel/Atom/Frm + fin_carrier (R1) + idx_grammar (R2) + nnf + sort_graph (E1∪E2) + Graph::acyclic (polynomial, result-identical to the Lean Roy-Warshall reach) + classify/admitted + the frozen RejectReason vocabulary + the wire to_wire/parse_frm; the four §3.2 micro-examples unit-tested to the Lean outcomes<br>symbol: `thermite_spec::classifier::admitted` - the bare boolean mirror of Lean Thermite.Strat.Cls.admitted — the value the differential battery holds byte-equal to lake env lean --run on the kernel admitted<br>file: `thermite-tv/src/gen.rs` - (2) gen_strat_formulas — the SplitMix64 generator extended with well-sorted binder productions (Q5: corpus-mimicking + uniform-random arms), deterministic, covering every verdict class (admit + each frozen rejection reason)<br>file: `lean/Thermite/Strat/Cls/Wire.lean` - (3) the Lean half: a wire-format recursive-descent parser to the kernel Cls.Frm + a root main running the kernel Cls.admitted per stdin line; an IO tool, a scripts/lean-axiom-probe.sh build target<br>file: `forge/src/strat_tv.rs` - (4) the differential harness: gen -> classify (Rust) -> lake env lean --run (kernel) -> compare; disagreement = verification-failure exit, the unknown-on-admitted tripwire (classifier-suspect, escalated), lake-absent = honest Skipped; the forge strat-tv subcommand drives it<br>test: `forge/tests/strat_differential.rs` - AC-4 (ci): the lake-gated live battery — Rust verdict == Lean admitted on N=200 generated formulas with zero disagreements + zero tripwire, at the pinned seed and a rotated seed; runs in the lean CI job (cargo nextest run -p forge with the spine built)<br>command: `cargo run -p forge -- strat-tv --generated 200` - the runnable differential driver (the rotating-seed / audit check [8] entry point; add --seed <u64> to rotate): zero disagreements AND zero tripwire -> exit 0; a disagreement or a tripwire -> verification-failure exit; lake-absent -> honest skip (exit 0) | The Rust ops-half classifier + the differential battery ONLY. The encoder + T1-S (REQ-5 / #327, the bridge between the Cls classifier surface and the REQ-1 semantic spine), the audit-script [8]/[1'] integration (REQ-9 / #331 — this increment ships the runnable battery + the lake-gated forge test that runs in the lean CI job, NOT the scripts/audit.sh check-[8] wiring), and the rest of the stage-2 tree are SEPARATE downstream requirements. |
Copy file name to clipboardExpand all lines: .design/scaffold/workspace.md
+2-2Lines changed: 2 additions & 2 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -2,8 +2,8 @@
2
2
<!--
3
3
tier: 3-component
4
4
status: draft
5
-
audited-sha: 5ae0816c042debb01c70eb9b89c775837f0c0f24 (re-pinned 2026-06-17 for umbrella REQ-7 / AC-12, the §6 metrics dashboard: the only change to this doc's governed file (main.rs) is one additive module declaration (`mod metrics;`, the new §6 dashboard projection); the workspace/crate structure is otherwise unchanged. prior: stage-1 REQ-10/AC-14 G1 gate seven-verdict test module)
audited-sha: 5ae0816c042debb01c70eb9b89c775837f0c0f24 (content-sha256 re-pinned 2026-06-20 for stage-2 REQ-4 / AC-4 (#326), the classifier ops half: the changes to this doc's governed lib roots are additive — `pub mod classifier;` + the classifier re-exports in thermite-spec/src/lib.rs (the new Rust admission classifier), and `mod strat_tv;` in forge/src/main.rs (the differential battery module); the workspace/crate structure is otherwise unchanged. The legacy commit pin stays at the 5ae0816c stable-main ancestor; only the active content-sha256 digest moves. prior: 2026-06-17 umbrella REQ-7 / AC-12 §6 metrics dashboard `mod metrics;`; stage-1 REQ-10/AC-14 G1 gate seven-verdict test module)
0 commit comments