backlog(B-0131..B-0138): formalization roadmap — 8 rows (Aaron 2026-05-01 'do all of those, start with 1')

docs/BACKLOG.md

@@ -96,6 +96,10 @@ are closed (status: closed in frontmatter)._
 - [ ] **[B-0121](backlog/P2/B-0121-otto-kenji-peer-call-cross-harness-claude-cli-aaron-2026-04-30.md)** Otto + Kenji as externally-callable peers via claude-cli — cross-harness symmetry (Aaron 2026-04-30)
 - [ ] **[B-0124](backlog/P2/B-0124-claudeai-csap-conversation-distill-uber-arch-2026-05-01.md)** Distill the Claude.ai CSAP-pushback conversation into uber-architecture (deferred multi-week)
 - [ ] **[B-0127](backlog/P2/B-0127-sibling-repo-leak-scrub-process-when-it-matters-aaron-2026-05-01.md)** Sibling-repo leak scrub-process — when scrubbing matters; future-defensive design
+- [ ] **[B-0131](backlog/P2/B-0131-formalize-zset-retraction-algebra-in-lean-aaron-2026-05-01.md)** Formalize Z-set retraction algebra in Lean (TRACTABLE START — formalization roadmap)
+- [ ] **[B-0132](backlog/P2/B-0132-crdt-composition-for-bft-propagation-aaron-2026-05-01.md)** CRDT-composition for BFT propagation — substrate events as composed CRDTs
+- [ ] **[B-0133](backlog/P2/B-0133-sequent-calculus-for-claim-retraction-attribution-aaron-2026-05-01.md)** Sequent calculus / labeled deductive systems for claim/retraction/attribution
+- [ ] **[B-0134](backlog/P2/B-0134-type-theoretic-orthogonality-discipline-encoding-aaron-2026-05-01.md)** Type-theoretic encoding of orthogonality discipline (extension vs creation as decidable judgment)
 
 ## P3 — convenience / deferred
 
@@ -141,5 +145,9 @@ are closed (status: closed in frontmatter)._
 - [ ] **[B-0116](backlog/P3/B-0116-gh-jq-safe-wrapper-zsh-quoting-2026-04-30.md)** tools/gh-jq-safe.sh — wrap gh-jq calls to handle zsh quoting (Deepseek 2026-04-30 finding)
 - [ ] **[B-0119](backlog/P3/B-0119-peer-call-existing-scripts-role-ref-cleanup-2026-04-30.md)** Existing peer-call scripts (grok.sh / gemini.sh / codex.sh / amara.sh) — role-ref cleanup per copilot-instructions.md (Codex 2026-04-30 finding on PR #962)
 - [ ] **[B-0123](backlog/P3/B-0123-stacked-pr-create-tooling-gh-fallback-aaron-2026-04-30.md)** Stacked-PR creation tooling — `gh pr create --base <not-main>` fails with cryptic GraphQL error; needs a wrapper or doc (Aaron 2026-04-30)
+- [ ] **[B-0135](backlog/P3/B-0135-modal-logic-for-retractability-quantum-rodney-razor-aaron-2026-05-01.md)** Modal logic for retractability — Quantum-Rodney's-Razor in S4 or dynamic logic
+- [ ] **[B-0136](backlog/P3/B-0136-category-theoretic-compositional-structure-aaron-2026-05-01.md)** Category-theoretic compositional structure — operads + monoidal categories for substrate composition
+- [ ] **[B-0137](backlog/P3/B-0137-tarski-stratification-proof-aaron-2026-05-01.md)** Tarski-stratification proof — formal demonstration that Aaron's pirate-not-priest spot stratifies meta-language from object-language
+- [ ] **[B-0138](backlog/P3/B-0138-bft-resistance-theorem-aurora-composed-crdt-plus-consensus-aaron-2026-05-01.md)** BFT-resistance theorem for Aurora — composed-CRDT-plus-consensus formal guarantee
 
 <!-- END AUTO-GENERATED -->

docs/backlog/P2/B-0131-formalize-zset-retraction-algebra-in-lean-aaron-2026-05-01.md

@@ -0,0 +1,78 @@
+---
+id: B-0131
+priority: P2
+status: open
+title: Formalize Z-set retraction algebra in Lean (TRACTABLE START — formalization roadmap)
+created: 2026-05-01
+last_updated: 2026-05-01
+---
+
+# B-0131 — Formalize Z-set retraction algebra in Lean (TRACTABLE START)
+
+**Priority:** P2 (research-grade; first tractable slice of the formalization roadmap; Aaron 2026-05-01 *"we should do all of those backlog and start with 1 i think if you agree"*).
+
+**Filed:** 2026-05-01.
+
+**Filed by:** Otto under backlog-prioritization authority delegated 2026-05-01. Origin: formalization roadmap Otto laid out in long-form writeup to Aaron 2026-05-01 ~10:00Z, after Claude.ai's substantive critique that Zeta substrate is "not yet, strictly speaking, a formal system." Aaron's response: *"not yet, i'm only a high school graduate, this is where you could really help :)"* — formalization is a path, not a current state.
+
+**Effort:** L (multi-month — extend Budiu et al.'s DBSP denotational semantics, mechanize proofs in Lean 4, integrate with Mathlib).
+
+## What
+
+Extend Mihai Budiu et al.'s DBSP formal definitions (papers 2022 onward) into a Lean 4 mechanization. The F# implementation in `src/Core/` is the working reference; Lean formalization mechanizes the underlying theorems.
+
+Specific scope:
+
+- **Z-set semi-ring algebra**: formalize Z-sets as multisets-with-multiplicity (positive and negative), with operations {+, -, ⋈, π, σ, ρ, distinct}. Already partially formal in DBSP papers; mechanize.
+- **Retraction operator semantics**: prove that retractions form a group (every operation invertible) and compose monotonically with other Z-set operations.
+- **Incremental view maintenance theorem**: mechanize the central DBSP claim that ΔV(t) = D[V(t-1) + ΔI(t)] for any monotone view V.
+- **Composition theorems**: formalize how operators compose (associativity, identity, distributivity where applicable).
+
+## Why P2
+
+- **Research-grade, not blocking**: the F# implementation works; Lean formalization is rigor-grade extension, not bug-fix.
+- **Substantial effort**: multi-month project minimum; needs Lean familiarity to actually execute.
+- **Tractable**: Budiu et al. already did the math; mechanization is translation work, not novel theorem-proving.
+- **High leverage when complete**: formal DBSP foundation is cited-by everything else in the roadmap (B-0132 through B-0138 build on or reference Z-set semantics).
+
+## Acceptance criteria
+
+1. **Lean 4 project structure** under `tools/lean4/` extending the existing setup, with explicit dependence on Mathlib.
+2. **Z-set type definition** with explicit positive/negative multiplicity. `ZSet α : Type` with operations as instances of typeclasses (`AddGroup`, `MulZeroClass`, etc. where applicable).
+3. **Retraction-operator theorems** mechanized: idempotence on retractions, group-inversion property, monotone composition with other operators.
+4. **Incremental view maintenance theorem** stated and proved (the central DBSP claim).
+5. **At least one non-trivial composition theorem** mechanized (e.g., `D[A ⋈ B] = D[A] ⋈ B + A ⋈ D[B] + D[A] ⋈ D[B]` or equivalent for the operator family Zeta uses).
+6. **Documentation** of the formal-to-engineering bridge — for each mechanized theorem, point at the corresponding F# code path that implements it.
+7. **At least one academic-mathematician review** (per lattice-capture corrective discipline B-0130 / `feedback_lattice_capture_*`): send the formalization summary to a working researcher in incremental computation / database theory; ask "did I capture the math correctly?"
+
+## Out of scope
+
+- **Performance proofs**: complexity bounds on the F# implementation are separate work.
+- **Operator-extensions specific to Aurora**: Bayesian-inference operators, soul-file-executor operators are downstream (different roadmap items).
+- **Formalization of carved-sentence semantics**: that's B-0133 (sequent calculus); compose with this row.
+- **Replacing the F# implementation**: Lean formalization is rigor-grade companion, not production runtime.
+
+## Composes with
+
+- **Budiu et al. DBSP papers** (2022 onward) — load-bearing source.
+- **F# implementation** in `src/Core/` — working reference; Lean formalization mechanizes its underlying math.
+- **Mathlib** — Lean 4 standard library; required dependency.
+- **B-0132** (CRDT-composition) — when Z-set semantics are mechanized, the CRDT-composition row can build on them.
+- **B-0133** (sequent calculus for claim/retraction/attribution) — sequent calculus formalization composes with Z-set semantics for the retraction operator specifically.
+- **B-0137** (Tarski-stratification proof) — requires substrate to be formal-system-grade first; Z-set mechanization is a foundation toward that.
+- **B-0130** (mechanized auditor for verify-before-state-claim) — academic-mathematician review per lattice-capture corrective is the operational test.
+- **`memory/feedback_lattice_capture_corrective_discipline_external_vocabulary_check_claudeai_warning_2026_05_01.md`** — the external-vocabulary check applies to this row's review step.
+
+## Status
+
+**Filed.** Awaiting Aaron's activation signal for implementation tick. Otto picks the implementation start (per backlog-prioritization-authority delegation 2026-05-01); first concrete step is to set up Lean 4 project structure under `tools/lean4/zset/` and stub out the type definitions before tackling theorems.
+
+## Verify-before-deferring note
+
+Budiu et al.'s DBSP papers are public (`https://www.feldera.com/research/`); Lean 4 + Mathlib are well-developed; the formalization is well-scoped engineering, not novel-theorem-proving. The "tractable" classification is honest — the math exists; the work is mechanization.
+
+## Pedagogical pointers (for Aaron, if pursuing alongside Otto)
+
+- *Theorem Proving in Lean 4* (Avigad et al., free online) — primary onboarding text.
+- Mathlib documentation — community-maintained, growing.
+- Budiu et al. DBSP papers (start with the original 2022 SIGMOD).

docs/backlog/P2/B-0132-crdt-composition-for-bft-propagation-aaron-2026-05-01.md

@@ -0,0 +1,57 @@
+---
+id: B-0132
+priority: P2
+status: open
+title: CRDT-composition for BFT propagation — substrate events as composed CRDTs
+created: 2026-05-01
+last_updated: 2026-05-01
+---
+
+# B-0132 — CRDT-composition for BFT propagation
+
+**Priority:** P2 (research-grade; second tractable slice of formalization roadmap; converts Aaron's "competing lattices" intuition into research-grade work).
+
+**Filed:** 2026-05-01.
+
+**Effort:** L (multi-month — write substrate propagation as composed CRDTs; prove strong eventual consistency; layer BFT consensus on top for Byzantine resistance).
+
+## What
+
+Map Zeta substrate's propagation events to formally-defined CRDT operators and prove the composition's properties. Builds on Shapiro et al. (INRIA 2011) "A comprehensive study of Convergent and Commutative Replicated Data Types."
+
+Substrate-event → CRDT mapping (initial sketch):
+
+| Substrate event | CRDT type | Notes |
+|---|---|---|
+| Claim creation | G-Set add | Add-only is monotone |
+| Claim revision | LWW-Register or Multi-Value-Register | LWW or branch-and-merge |
+| Claim retraction | OR-Set remove | Observed-Remove preserves causal history |
+| Candidate promotion | State machine on monotone semi-lattice | Rank/level transitions |
+| Consensus formation | PBFT / HotStuff / Tendermint family | Where BFT proper lives |
+
+Aaron's "competing lattices" intuition was reaching for **CRDT-composition theory** (multiple semilattices composing under merge operations) — this row captures the actual mathematical work.
+
+## Why P2
+
+- High-leverage research-grade target. Converts "Aurora is BFT-resistant" from architectural claim to verified theorem.
+- Tractable — Shapiro framework + BFT consensus literature does most of the work; substrate-specific mapping is the contribution.
+- Multi-month effort; not blocking; pace via cooling-period discipline.
+
+## Acceptance criteria
+
+1. **Substrate-event-to-CRDT mapping** documented per-event with explicit conflict-resolution semantics.
+2. **Strong eventual consistency proof** for the composed CRDT (each replica converges to same state given same set of operations).
+3. **BFT layer specification**: which consensus family (PBFT / HotStuff / Tendermint), with proof that BFT-resistance composes correctly with CRDT semantics.
+4. **At least one academic-mathematician review** (lattice-capture corrective per B-0130).
+
+## Composes with
+
+- B-0131 (Z-set Lean formalization) — Z-set semantics underpin retraction CRDT.
+- Shapiro et al. INRIA 2011 — load-bearing source.
+- BFT consensus literature (Castro & Liskov 1999; HotStuff 2019; Tendermint).
+- `feedback_retraction_native_paraconsistent_set_theory_candidate_quantum_bp.md` — Quantum-Rodney's-Razor + retraction-native theory connects here.
+- `docs/research/2026-05-01-e8-vs-crdt-lattice-bft-propagation-candidate-aaron-question-claudeai-pushback.md` — origin of CRDT-composition direction (Otto's refinement of Aaron's E8 hypothesis).
+
+## Status
+
+**Filed.** Awaiting B-0131 progress (Z-set mechanization is foundational) before activation.

docs/backlog/P2/B-0133-sequent-calculus-for-claim-retraction-attribution-aaron-2026-05-01.md

@@ -0,0 +1,41 @@
+---
+id: B-0133
+priority: P2
+status: open
+title: Sequent calculus / labeled deductive systems for claim/retraction/attribution
+created: 2026-05-01
+last_updated: 2026-05-01
+---
+
+# B-0133 — Sequent calculus for claim/retraction/attribution
+
+**Priority:** P2 (research-grade; third tractable slice of formalization roadmap).
+
+**Filed:** 2026-05-01.
+
+**Effort:** L (multi-month — define inference rules; prove cut-elimination or substrate-equivalent; mechanize in Lean alongside B-0131).
+
+## What
+
+Express the substrate's claim/retraction/attribution machinery as a sequent calculus or labeled deductive system. Substrate claims map naturally to sequents; attribution graphs map to *labeled* deductive systems where each formula carries an attribution label (who claimed it, with what evidence).
+
+**Reference:** Troelstra & Schwichtenberg, *Basic Proof Theory* (Cambridge, 2nd ed). Chapters 1-3 cover what's needed.
+
+## Acceptance criteria
+
+1. **Inference rules** defined formally for: claim-creation, claim-revision, claim-retraction, candidate-promotion, consensus-formation.
+2. **Cut-elimination theorem** (or substrate-equivalent) proved — the proof-theoretic version of the razor: derivability without redundant rules.
+3. **Conservativity proof** — extending the substrate doesn't accidentally prove things that weren't already provable.
+4. **Attribution-label semantics** formalized — sequents carry labels indicating attribution-graph position.
+5. **Academic-proof-theorist review** per lattice-capture corrective (B-0130).
+
+## Composes with
+
+- B-0131 (Z-set Lean) — retraction operator semantics.
+- Troelstra & Schwichtenberg — load-bearing source.
+- The razor — cut-elimination is its formal cousin.
+- `feedback_aaron_pirate_not_priest_expand_prune_pedagogical_framework_quantum_rodney_razor_parallel_worlds_aaron_2026_05_01.md` — pirate-not-priest disposition + razor as cut-elimination.
+
+## Status
+
+**Filed.** Pace alongside B-0131; sequent-calculus semantics compose with Z-set semantics for the retraction operator specifically.

docs/backlog/P2/B-0134-type-theoretic-orthogonality-discipline-encoding-aaron-2026-05-01.md

@@ -0,0 +1,40 @@
+---
+id: B-0134
+priority: P2
+status: open
+title: Type-theoretic encoding of orthogonality discipline (extension vs creation as decidable judgment)
+created: 2026-05-01
+last_updated: 2026-05-01
+---
+
+# B-0134 — Type-theoretic encoding of orthogonality discipline
+
+**Priority:** P2 (research-grade; fourth tractable slice of formalization roadmap).
+
+**Filed:** 2026-05-01.
+
+**Effort:** M-L (1-3 months — type-theoretic encoding; potentially mechanize in Lean).
+
+## What
+
+Encode the meta-meta-meta-rule (orthogonality check before creating a new substrate class) as a decidable type-theoretic judgment. Currently orthogonality is judged informally; mechanizing the check would catch class-creation failures at compose-time rather than at PR-review-time.
+
+**Reference:** *Theorem Proving in Lean 4* (Avigad et al.) for the type-theory side; HoTT book for refinement-types side.
+
+## Acceptance criteria
+
+1. **Formal definition** of "extension" vs "new orthogonal class" as a typed predicate on substrate-tree positions.
+2. **Decidability proof or procedure**: given a candidate new class, mechanically determine whether it reduces to existing classes (extension) or is genuinely independent (orthogonal).
+3. **Soundness**: never claim "extension" when the candidate genuinely adds an irreducible base concept.
+4. **Lean mechanization** (or equivalent) integrated with `tools/lean4/`.
+5. **Test fixtures** exercising the catch logic on prior orthogonality decisions (the meta-meta-meta-rule's empirical validation).
+
+## Composes with
+
+- `memory/feedback_class_level_rules_need_orthogonality_check_extend_or_create_aaron_2026_05_01.md` — the rule being mechanized.
+- B-0130 (audit-suite) — this row's mechanization is one specific audit in B-0130's family.
+- B-0131 + B-0133 — type-theoretic encoding composes with sequent calculus and Z-set Lean.
+
+## Status
+
+**Filed.** Pace after B-0131 + B-0133 progress.

docs/backlog/P3/B-0135-modal-logic-for-retractability-quantum-rodney-razor-aaron-2026-05-01.md

@@ -0,0 +1,40 @@
+---
+id: B-0135
+priority: P3
+status: open
+title: Modal logic for retractability — Quantum-Rodney's-Razor in S4 or dynamic logic
+created: 2026-05-01
+last_updated: 2026-05-01
+---
+
+# B-0135 — Modal logic for retractability
+
+**Priority:** P3 (research-grade; deferred — substantive theorem-proving territory; not yet activated).
+
+**Filed:** 2026-05-01.
+
+**Effort:** L (multi-month — modal-logic formalization; Kripke semantics for retraction operators).
+
+## What
+
+Formalize Quantum-Rodney's-Razor (possibility-space pruning preserving retractability) as a specific modal logic. *Many-worlds-pruning* IS the Kripke-semantics-of-modal-logic frame. **S4** (reflexive + transitive accessibility) probably fits the substrate's pruning semantics; **dynamic logic** (with explicit programs that transform worlds) fits retraction-operators.
+
+**Reference:** Blackburn, de Rijke, Venema, *Modal Logic* (Cambridge, 2001).
+
+## Acceptance criteria
+
+1. **Modal logic chosen** with justification (S4, dynamic logic, or hybrid).
+2. **Kripke semantics** for retraction operators formalized.
+3. **Retractability invariants** stated as modal formulas; key ones proved.
+4. **Compose with B-0131 + B-0133** — Z-set retraction operators are the concrete instances; modal logic is the meta-language.
+
+## Composes with
+
+- B-0131 (Z-set Lean) — concrete retraction operators.
+- B-0133 (sequent calculus) — proof-theoretic side complementing modal-logic semantic side.
+- `feedback_aaron_pirate_not_priest_expand_prune_pedagogical_framework_quantum_rodney_razor_parallel_worlds_aaron_2026_05_01.md` — parallel-worlds-pruning metaphysics.
+- `feedback_retraction_native_paraconsistent_set_theory_candidate_quantum_bp.md` — Quantum-Rodney's-Razor + paraconsistent set theory.
+
+## Status
+
+**Filed.** P3 (deferred). Activation contingent on B-0131/B-0133 progress + Aaron's interest signal.

docs/backlog/P3/B-0136-category-theoretic-compositional-structure-aaron-2026-05-01.md

@@ -0,0 +1,41 @@
+---
+id: B-0136
+priority: P3
+status: open
+title: Category-theoretic compositional structure — operads + monoidal categories for substrate composition
+created: 2026-05-01
+last_updated: 2026-05-01
+---
+
+# B-0136 — Category-theoretic compositional structure
+
+**Priority:** P3 (research-grade; cross-cutting; not urgent; pays off when composing substrate-instances across projects).
+
+**Filed:** 2026-05-01.
+
+**Effort:** L (multi-month — categorical formalization).
+
+## What
+
+Identify the substrate's compositional invariants in categorical terms. The substrate has many compositional pieces — claims compose, retractions compose, attribution graphs compose. **Operads** (n-ary operations + their compositions) and **monoidal categories** (parallel composition) are the relevant frameworks.
+
+**References:**
+
+- Bartosz Milewski, *Category Theory for Programmers* (free, online; written for engineers).
+- *Categories for the Working Mathematician* (Mac Lane) — depth.
+- Fong & Spivak, *Seven Sketches in Compositionality* (free) — application-oriented.
+
+## Acceptance criteria
+
+1. **Substrate compositional invariants** named in categorical terms (the razor as a functor; orthogonality as a coproduct property; etc.).
+2. **At least one categorical theorem** about substrate composition stated and proved.
+3. **Cross-project applicability** demonstrated — the categorical framing should compose with the Frontier / Factory / Peers split (per `project_repo_split_provisional_names_frontier_factory_and_peers_2026_04_23.md`).
+
+## Composes with
+
+- B-0131 + B-0133 + B-0134 — categorical framing unifies the formalization-roadmap items.
+- *Project: Frontier / Factory / Peers split* — categorical framing supports cross-instance composition.
+
+## Status
+
+**Filed.** P3 (deferred — not urgent; pays off when other formalization items mature).