[codex] Place Practice-10 derived-operation invariant

INVARIANTS.md

@@ -99,6 +99,16 @@ A type that models an external spec primitive is declared as a **bare alias** 
 
 **Receipt:** v4 decision D2 modeled external language primitives as alias-identity declarations (`type RustI32 = Int32`). Each passed structural review precisely because it was minimal. The operator reversed D2 (2026-05-17): the aliases asserted unproven identities and modeled nothing. Dissolution: fact-bundle modeling — every external primitive carries the facts its own spec states; deduplication onto `std/` happens only on proven coincidence.
 
+### Problem shape: Hand-rolled derived operation
+
+**Do not hand-roll a derived operation.** If a function's behavior is determined entirely by the shape of a modeled type, it is re-deriving something the compiler already derives. The deficiency is in the model, not the code — model the missing fact; do not hand-roll the operation.
+
+A function walks a modeled structure, projects a property from a variant shape, threads a standard carrier by hand, or templates an emitter from local strings. The behavior is fixed by the model's shape, so the code is a second authority for a fact the model should carry or derive.
+
+**Solution shape:** Add or consume the substrate primitive that derives the operation — a catamorphism, traversal, structural fact, grammar model, or other declared carrier — and delete the hand-rolled local function. When the primitive is missing, record a tracked dissolution gate with the owning substrate task and dissolve on arrival; untracked hand-rolled derived operations block merge.
+
+**Receipt:** Practice 10 in `docs/modeling-discipline.md` names the derived-operations registry and the dissolution findings (`walker`, `traverse`, `predicate`, `carrier`, `emit/template`, `nominalization`, and coproduct dissolution). It is the review rubric for deciding whether a local helper is real logic or a duplicated derivation.
+
 ### Procedure: substrate-fact introduction (decision procedure for new modeling)
 
 **When to run this:** any time you're about to introduce a new substrate type, sum-type variant, field, or named lane. Run BEFORE authoring; if any check surfaces a gap, redirect rather than escalate.
@@ -144,6 +154,7 @@ Fundamental primitives (physics, computation, mathematics) declare as substrate
 - **Bounded Substrate Seed** — Rust-native seed items must remain narrow; undeclared seed growth is ungrounded
 - **Design Commitments Must Name The Substrate Target** — unnamed substrate = ungrounded claim
 - **Heuristics Indicate Lost Structure** — heuristic output traces to a dropped upstream fact, not to a declared source
+- **Do not hand-roll a derived operation** — if behavior is fixed by modeled shape, model the missing fact or consume the derived operation
 - **Documentation Describes Live State** — aspirational docs describe a reality the codebase doesn't embody
 - **Substrate-Fact Introduction Procedure** (above) — operational decision procedure for adding new substrate types/variants/fields
 

MODELING.md

@@ -120,6 +120,10 @@ Types decompose into smaller types that each assert one fact.
 
 > Fact modeling is the **inputs facet** of the derived homomorphism: the facts a type asserts are what the compiler derives the cross-target map *from* (see [docs/modeling-discipline.md](docs/modeling-discipline.md) "The three facets").
 
+Do not hand-roll a derived operation. If a function's behavior is determined entirely by the shape of a modeled type, it is re-deriving something the compiler already derives. The deficiency is in the model, not the code — model the missing fact; do not hand-roll the operation.
+
+Practice 10 in [docs/modeling-discipline.md](docs/modeling-discipline.md#10-dont-hand-roll-a-derived-operation) is the operational checklist for this rule: identify the derived operation, then either consume the declared substrate primitive, model the missing fact, or record a tracked dissolution gate when the primitive is not yet present.
+
 ### M2: No duplicate type authorities
 
 Every type is defined in exactly one place.

docs/modeling-discipline.md

@@ -58,7 +58,7 @@ Mapping:
 - Practice 7 (Projection over enumeration) — implements **P1: Modeling Faithfulness**
 - Practice 8 (Fact-bundle modeling) — implements **P1: Modeling Faithfulness**
 - Practice 9 (No-prose discipline) — implements **P2: Boundary Discipline**
-- Practice 10 (Don't hand-roll a derived operation) — implements **P1: Modeling Faithfulness** (and the proposed *Do not hand-roll a derived operation* invariant — pending operator ratification, rework-tracker PR #3240 task A1)
+- Practice 10 (Don't hand-roll a derived operation) — implements **P1: Modeling Faithfulness** and the *Do not hand-roll a derived operation* invariant.
 
 A reviewer should name specifically whether the diff satisfies each
 relevant practice, where it could be violated, and whether the existing
@@ -588,10 +588,8 @@ the code. The fix is never to polish the hand-rolled construct — it is to
 model the missing fact, or name the missing substrate primitive, and let
 the operation be derived.
 
-**The invariant this implements** (proposed — pending operator
-ratification, rework-tracker PR #3240 task A1; on ratification it lands
-in [INVARIANTS.md](../INVARIANTS.md) / [MODELING.md](../MODELING.md), and
-this Practice cites it directly):
+**The invariant this implements** (see [INVARIANTS.md](../INVARIANTS.md)
+P1 and [MODELING.md](../MODELING.md) M1):
 
 > **Do not hand-roll a derived operation.** If a function's behavior is
 > determined entirely by the shape of a modeled type, it is re-deriving
@@ -715,11 +713,11 @@ it is what stops a reviewer from wrongly demanding the impossible:
   recursion or `match` is genuinely irregular (the call graph is not the
   data graph), or the construct already uses the derived operation.
 
-The retroactive v4 dissolution audit (rework-tracker PR #3240 task C1)
-applies this legend per-file, per-finding — a symbol-marked inventory,
-not prose. The symbol records a finding's *disposition*; the matching
-in-file `.dag` tag lands with the fix, per migration PR — it is not
-retro-applied across all v4 files at once.
+The retroactive v4 dissolution audit applies this legend per-file,
+per-finding — a symbol-marked inventory, not prose. The symbol records a
+finding's *disposition*; the matching in-file `.dag` tag lands with the
+fix, per migration PR — it is not retro-applied across all v4 files at
+once.
 
 **Decidability — checker-flaggable vs reviewer-judgment.** Every
 dissolution finding is **blocking** — there is no advisory tier and no
@@ -742,12 +740,11 @@ would:
 | coproduct dissolution | already enforced — per-coproduct 🟢/🟡/🔴 tag + `DECISIONS.md` ledger (Practices 4 / 9) | already enforced |
 
 The *enforcement mechanism* — the checker-script build path and the
-eventual dissolution lens — is design work, specified in the planned
-`docs/design-dissolution-lens.md` (rework-tracker PR #3240 task B1). This
-Practice carries only the classification, which is discipline a reviewer
-applies by hand. Worked examples — the #3225 dissolution inventory — land
-in [modeling/grounding-worked-examples.md](modeling/grounding-worked-examples.md)
-(PR #3240 task B2).
+eventual dissolution lens — is design work, specified in
+`docs/design-dissolution-lens.md`. This Practice carries only the
+classification, which is discipline a reviewer applies by hand. Worked
+examples from the #3225 dissolution inventory live in
+[modeling/grounding-worked-examples.md](modeling/grounding-worked-examples.md).
 
 **What to check.** For any function in the diff: is its behavior fixed by
 the *shape* of a modeled type rather than by logic unique to this call