docs: enforcement-intent governance model — ask once, compile forever

DESIGN.md

@@ -81,6 +81,7 @@ hollow alias (minimality ≠ grounding) · state-space conflation (an `Option`/`
 
 - `v2.std.determinism` — §5 determinism mechanism P1 landed (#5941; operator shape-signed, FLAG A/C locked): [determinism mechanism design](docs/plans/determinism-mechanism-design.md)
 - model §1's axioms (A1–A3) explicitly in `.dag` and have a lens **enforce the syllogism** — every claim a consequence-chain back to an axiom, no orphan and no cycle (the §4 acyclicity test turned on the argument itself; the §7 recursion, with this document as the first target). (operator's next project) → candidate articulation for review: [intent-linearity draft](docs/plans/intent-linearity-design-draft.md)
+- **enforcement intent — ask once, compile forever.** The operator's recurring standing directives (enforce complexity repo-wide; lenses must be live; lenses must self-apply; scope must not silently narrow; model must not carry dual representations) are redundant governance work (§2) re-paid each conversation — the operator performing the missing meta-lens by hand. Model each as a durable `StandingIntent` row and gate the relationship (intent ⇄ `LensContract` ⇄ coverage receipt) fail-closed: a mechanism *claiming enforcement* is complete only when it satisfies the `StandingIntent` — named live consumer, declared scope not narrowed, red control, self-application or explicit exemption — else Unknown/Refused, never silently green. One new authority (`StandingIntent`); everything else extends existing machinery — the registry (`LensRegistryEntryV0` → `LensContract`), reusing `ConstructionJustification` / `subject_roster` and consuming `intent_linearity` / `self_applying_lenses` for the fractal (§7) layer (the same property applied to the code, the lens, the subject producer, the registry, and the acceptance template). Default enforcement scope = whole corpus; under-scope is a failing receipt unless explicitly justified. → [enforcement-intent design](docs/plans/enforcement-intent-design.md)
 - can a lens mechanically diagnose the *leaf-side* of decomposition (§2)? (operator-parked)
 - the model↔realization fork is systemic, and where unfinished it fails open: every primitive is modeled as a coproduct and realized as a native `Value`, reconciled by per-site bridges, so coverage is accidental and non-compositional. `match` bridges `Int→Zero/Succ` but `Value::eq` has no `Int↔Variant` arm, so `nat_add(85, 32) == 117` silently compared `false` at its `_ => false` chokepoint — a §5 fail-open, not the §2/§7 redundancy the 🟡 dissolve-on markers track. **Landed:** the *numeric tower* fork now fails closed — `eval_binop`'s `BinOp::Eq`/`Ne` raises `InterpError::CrossRepresentationEquality` when a `false` result is *explained* by a native `Int`/`Float` vs `Nat`-coproduct straddle (recursive: catches `nat_add == nat_add` and `[nat_add(1,1)] == [2]`), with `Value::eq` left infallible so it stays the single `CanonKey` map-key authority. The discriminating witness is `cross_representation_equality_test` (forks → typed error; reconciled/native → `true`; genuine diffs `1 == 2`/`Succ{..} == Zero` → `false`, not error). **Remaining:** (a) the same straddle for `Bool True|False` over `Value::Bool` (no `==` site in the corpus today) and `Optional/Witness` over `Value::Null` — the latter resists a blanket guard because `Value::Null` is the overloaded `None`/`Absent`/miss sentinel and `present == None` (131 sites) is a *legitimate* `false`, so it needs grounding, not an error arm; (b) the root fix (§1/§2/§7) — ground each primitive into its realization. **Numeric tower: GROUNDED** (#5428, 2026-06-21) — Nat construction-side grounded (`Zero → Int(0)`, `Succ{prev:Int(k)} → Int(k+1)`); native form == modeled form; `eval_binop` `CrossRepresentationEquality` guard is dead-in-corpus for numerics, kept as fail-closed backstop until the `Value::Null` split lands (guard removal bundled with that work, fenced out of this window). **Remaining:** `Value::Null` split — Optional/Witness/miss into own carriers (~131 sites; the deeper root, its own runway). (operator: `==` fail-closed, 2026-06-20)
 - the remaining deleted-`docs/` references in `.dag` comments — provenance / `bind:` pointers into the bankrupted `docs/` tree (e.g. `docs/planning/*`, `design-*.md`) — fold into the dep-graph reform, not a blind repoint. (The named-corpus ledger marks — `Practice N`, and `INVARIANTS` / `THESIS` / `MODELING` / `RELEASE_TODO` / … citations — were swept: dropped, or re-homed to DESIGN.md §-anchors.)

ROADMAP.md

@@ -107,7 +107,7 @@ Receipts + adjacent levers: [fractal Gantt](docs/plans/ci-floor-fractal-gantt.md
 
 ## 3. The floor — audit what we have (does it actually do what it claims?)
 
-Both pillars ride the CI floor: tree-wide marker-driven witness discovery · compile-clean gate · generated-artifact drift gates (this document is one) · `regen --verify` (#5873) · doc-graph reachability · emit-determinism (#5941) · the interim self-host comparison (#6009). Those stand. The floor's *expansion* lanes (testgen, wiring-liveness, complexity gates, lens meta-walls) are shelved — a new wall must displace a measured cost on a pillar path to un-shelve.
+Both pillars ride the CI floor: tree-wide marker-driven witness discovery · compile-clean gate · generated-artifact drift gates (this document is one) · `regen --verify` (#5873) · doc-graph reachability · emit-determinism (#5941) · the interim self-host comparison (#6009). Those stand. The floor's *expansion* lanes (testgen, wiring-liveness, complexity gates, lens meta-walls) are shelved — a new wall must displace a measured cost on a pillar path to un-shelve (the **enforcement-intent gate** below is the first such un-shelve, 2026-07-02: displaced cost = the operator's repeated manual *what-is-enforced-by-what-lens-over-what-corpus* join, plus CI-killing quadratics and repeated dual-representation/anemia rediscovery).
 
 **Audit directive (operator, 2026-07-01): thoroughly audit what we have and what it actually does.** For each load-bearing mechanism, prove **by execution** that it does what it claims, with a **discriminating perturb** that goes RED when the behavior is wrong — a typecheck or a grep is not a consumer (DESIGN §5), and a wired gate can still be vacuous. A mechanism claim without a red-control is *unverified*, whatever its docs say. The reset's own mapping found the pattern live: the committed converge shell is spec-without-execution (§2), the fixpoint gate self-declares interim (2-of-92 files), cargo-green is an ignored test. Highest-stakes mechanisms first:
 
@@ -118,6 +118,7 @@ Both pillars ride the CI floor: tree-wide marker-driven witness discovery · com
 - [ ] **cache honesty re-receipt** — re-run the warm==cold purity oracle against CURRENT main (616/616 was pre-reset), and close the sccache exit-0-no-binary class (below); a cache that lies is worse than no cache.
 - [ ] **artifact-freshness gate** *(operator ask: "we need a freshness gate, if we don't already have one")* — we half-do: the per-PR drift gate proves committed==emitted for the PR's OWN tree, but drift still LANDED on main (`.gitignore` stale vs its authority since #6097; found and healed by #6110/#6111) because admission never re-validates against CURRENT main — green-on-branch is not green-on-main. The closing mechanism is the §2 merge-admission freshness block (HELD); this item is its receipt pair: (a) reproduce the landed-drift path as a RED witness, (b) confirm the freshness block refuses it once un-HELD.
 - [ ] **one tree, one verdict** — 2026-07-01 live finding: `dsl_compile_clean_gate` was GREEN while the discovery-corpus resolve of the same tree was RED (`extdeps.shell` module collision, silent last-root-wins shadowing; de-fork + loud-collision wall shipped as the hotfix). Two resolve paths gave two verdicts on one corpus — enumerate every place a module index is built, and make their collision/ordering semantics ONE authority so a gate cannot be green on a tree the floor cannot resolve.
+- [ ] **enforcement intent + model-quality walls** *(operator-directed 2026-07-02; §3 un-shelve — displaced cost: repeated manual "what is enforced, by what lens, over what corpus" joins; CI-killing quadratics; repeated dual-representation/anemia rediscovery)* — model the operator's recurring standing directives as durable `StandingIntent` rows and gate the relationship (intent ⇄ `LensContract` ⇄ `CoverageReceipt`) fail-closed, so a mechanism *claiming* enforcement is complete only when the gate proves the claim **from receipts, not self-declared contract claims**. One new authority (`StandingIntent`); everything else extends existing machinery (`LensRegistryEntryV0` → `LensContract`; reuse `ConstructionJustification` / `subject_roster`; consume `intent_linearity` / `self_applying_lenses`). Anti-overcomplication: no lens may claim *repo-wide* / *blocking* / *complete* / *self-applying* unless the gate can prove it. Rollout: rows live; gate Blocking on contract consistency; object rules AuditOnly until receipts land. Children, A→C before object rules D/E: **A** StandingIntent carrier + LensContract extension (`ConsumerKind`/`ConsumerRequirement` NOT hardwired to `FloorGate`; `EnforcementMode` order `Advisory < AuditOnly < Blocking` modeled) · **B** enforcement_intent_gate contract-consistency reds (over `CoverageReceipt`s) · **C** complexity.repo-wide first proof (3 legs red today, no `decl_facts` dep) · **D** complexity R1 accumulator-in-copied-port object rule (HOLDS behind #6155) · **E** anemia/consolidation first model-quality consumers (suggest a consolidation target, not just warn). [design](docs/plans/enforcement-intent-design.md)
 
 **Open floor holes:**