@@ -375,6 +375,52 @@ but dangerous for creative/research work.
375375- A language with 44 locked design decisions should get more decisions, not workarounds
376376- Invert the budget: 70% on the project's unique strength, 30% on everything else
377377
378+ **Divergent Invariant Preservation (CRITICAL):**
379+
380+ "Amplify uniqueness" means **deepen**, not **broaden**. Divergent mode
381+ must respect the project's architectural constraints even while pushing
382+ its strengths. The invariants are the riverbanks — diverge within them,
383+ not across them.
384+
385+ Before doing ANY work in divergent mode, read:
386+ 1. The AI manifest (0-AI-MANIFEST.a2ml) for critical invariants
387+ 2. CLAUDE.md for project-specific rules
388+ 3. The language/architecture policy
389+
390+ **What divergent mode DOES:**
391+ - A project with 699 Idris2 proofs gets *deeper* Idris2 proofs
392+ - A project with a novel type system gets *richer* type theory
393+ - A project with a unique algorithm gets *better* performance analysis
394+
395+ **What divergent mode DOES NOT do:**
396+ - Add proofs in Lean4/Coq/Agda to an Idris2-only project
397+ - Add a second language "because it's interesting"
398+ - Broaden the tech stack "to explore alternatives"
399+ - Introduce patterns from other projects that don't fit this one's model
400+
401+ **The broadening trap:** A bot told to "amplify uniqueness" in a formal
402+ verification repo might think "formal verification is cool, let me add
403+ Lean4 proofs too!" This is catastrophically wrong — it dilutes the
404+ project, adds maintenance burden, and violates the single-language
405+ invariant. The correct divergent action is to make the *existing* Idris2
406+ proofs deeper, more complete, or more elegant.
407+
408+ **Test:** Before adding anything in divergent mode, ask:
409+ "Does this deepen the existing strength, or does it add a parallel
410+ strength?" If parallel → stop. Note it as a cross-project insight.
411+ Only deepen.
412+
413+ **Example:**
414+ - `proven` repo (699 Idris2 files, zero believe_me):
415+ - CORRECT divergent: prove harder theorems, fill proof gaps, improve
416+ proof ergonomics, add dependent-type techniques not yet used
417+ - WRONG divergent: add Lean4 translations, add Coq versions, "port
418+ the proofs to Agda for comparison"
419+ - Ephapax compiler (linear types, Rust):
420+ - CORRECT divergent: deepen the linearity checker, prove more properties,
421+ add region inference refinements
422+ - WRONG divergent: add a Haskell backend, "try rewriting in OCaml"
423+
378424**How to choose:**
379425- If the user says "get this up to spec" / "fix" / "convert" / "complete" → convergent
380426- If the user says "develop" / "explore" / "push" / "what makes this special" → divergent
@@ -905,3 +951,14 @@ Same session, after user asked "are we at risk of never arriving?":
905951 found, (d) difficulty-impact classification of remaining work,
906952 (e) recommended focus for next session. This forces honest accounting
907953 of what the meander chose NOT to do.
954+
955+ ** v5 refinement (2026-03-23, divergent safety):**
956+ 24 . ** Divergent Invariant Preservation** — "amplify uniqueness" means
957+ deepen, not broaden. Before any divergent work, read the AI manifest
958+ and CLAUDE.md for invariants. Diverge within the riverbanks, not
959+ across them. Test: "Does this deepen the existing strength, or add
960+ a parallel strength?" If parallel → stop. The broadening trap
961+ (adding Lean4 proofs to an Idris2-only repo, adding a Haskell
962+ backend to a Rust compiler) is the divergent equivalent of
963+ convergent's over-polishing — it feels productive but violates
964+ the project's architectural identity.
0 commit comments