diff --git a/docs/BACKLOG.md b/docs/BACKLOG.md index 53f19051f..bb7f2c4f1 100644 --- a/docs/BACKLOG.md +++ b/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 ` 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 diff --git a/docs/backlog/P2/B-0131-formalize-zset-retraction-algebra-in-lean-aaron-2026-05-01.md b/docs/backlog/P2/B-0131-formalize-zset-retraction-algebra-in-lean-aaron-2026-05-01.md new file mode 100644 index 000000000..bc11da7f6 --- /dev/null +++ b/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). diff --git a/docs/backlog/P2/B-0132-crdt-composition-for-bft-propagation-aaron-2026-05-01.md b/docs/backlog/P2/B-0132-crdt-composition-for-bft-propagation-aaron-2026-05-01.md new file mode 100644 index 000000000..0c1a8eaa4 --- /dev/null +++ b/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. diff --git a/docs/backlog/P2/B-0133-sequent-calculus-for-claim-retraction-attribution-aaron-2026-05-01.md b/docs/backlog/P2/B-0133-sequent-calculus-for-claim-retraction-attribution-aaron-2026-05-01.md new file mode 100644 index 000000000..81275996c --- /dev/null +++ b/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. diff --git a/docs/backlog/P2/B-0134-type-theoretic-orthogonality-discipline-encoding-aaron-2026-05-01.md b/docs/backlog/P2/B-0134-type-theoretic-orthogonality-discipline-encoding-aaron-2026-05-01.md new file mode 100644 index 000000000..666571d2e --- /dev/null +++ b/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. diff --git a/docs/backlog/P3/B-0135-modal-logic-for-retractability-quantum-rodney-razor-aaron-2026-05-01.md b/docs/backlog/P3/B-0135-modal-logic-for-retractability-quantum-rodney-razor-aaron-2026-05-01.md new file mode 100644 index 000000000..9d3ec9e97 --- /dev/null +++ b/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. diff --git a/docs/backlog/P3/B-0136-category-theoretic-compositional-structure-aaron-2026-05-01.md b/docs/backlog/P3/B-0136-category-theoretic-compositional-structure-aaron-2026-05-01.md new file mode 100644 index 000000000..57cf60e3c --- /dev/null +++ b/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). diff --git a/docs/backlog/P3/B-0137-tarski-stratification-proof-aaron-2026-05-01.md b/docs/backlog/P3/B-0137-tarski-stratification-proof-aaron-2026-05-01.md new file mode 100644 index 000000000..5c915586d --- /dev/null +++ b/docs/backlog/P3/B-0137-tarski-stratification-proof-aaron-2026-05-01.md @@ -0,0 +1,41 @@ +--- +id: B-0137 +priority: P3 +status: open +title: Tarski-stratification proof — formal demonstration that Aaron's pirate-not-priest spot stratifies meta-language from object-language +created: 2026-05-01 +last_updated: 2026-05-01 +--- + +# B-0137 — Tarski-stratification proof + +**Priority:** P3 (research-grade; requires substrate to be formal-system-grade first; deferred until B-0131 + B-0133 mature). + +**Filed:** 2026-05-01. + +**Effort:** XL (multi-year — substantial formal-systems work; requires novel theorem-proving). + +## What + +Formalize and prove the Tarski-stratification claim that emerged in 2026-05-01 substrate work: Aaron's architectural choice of designating the pirate-not-priest disposition as the meta-position is structurally analogous to Tarski's truth-theorem requiring the truth predicate to live in a meta-language. Once the substrate is formal-system-grade (post B-0131 + B-0133 + B-0134), this row attempts the actual theorem. + +**Reference:** Tarski 1933, "The Concept of Truth in Formalized Languages." Modern treatments in any introductory mathematical logic textbook. + +## Acceptance criteria + +1. **Substrate definition formal**: prerequisite — Zeta substrate has earned "formal system" status via B-0131 + B-0133 + B-0134. +2. **Tarski-stratification theorem stated** as a mathematical claim with falsifiability conditions. +3. **Proof attempted** — likely a non-trivial result; might dissolve under closer examination (cooling-period applies); might earn its slot. +4. **Academic-mathematical-logician review** per lattice-capture corrective. +5. **Honest classification of outcome** — proved, disproved, or open. Each is fine. + +## Composes with + +- `memory/feedback_tarski_allocation_rename_correction_to_godel_allocation_in_pr1046_aaron_claudeai_2026_05_01.md` — origin of the Tarski-allocation framing. +- `memory/feedback_aaron_pirate_not_priest_expand_prune_pedagogical_framework_quantum_rodney_razor_parallel_worlds_aaron_2026_05_01.md` — pirate-not-priest as meta-position. +- B-0131 + B-0133 + B-0134 — prerequisite formalization. +- `memory/feedback_lattice_capture_corrective_discipline_external_vocabulary_check_claudeai_warning_2026_05_01.md` — academic review per the corrective. + +## Status + +**Filed.** P3 (deferred). Cannot activate until prerequisites land. The honest outcome might be: substrate is mathematically interesting but doesn't earn a Tarski-stratification *theorem* in the strict sense; the architectural choice is sound regardless. diff --git a/docs/backlog/P3/B-0138-bft-resistance-theorem-aurora-composed-crdt-plus-consensus-aaron-2026-05-01.md b/docs/backlog/P3/B-0138-bft-resistance-theorem-aurora-composed-crdt-plus-consensus-aaron-2026-05-01.md new file mode 100644 index 000000000..240e27c10 --- /dev/null +++ b/docs/backlog/P3/B-0138-bft-resistance-theorem-aurora-composed-crdt-plus-consensus-aaron-2026-05-01.md @@ -0,0 +1,41 @@ +--- +id: B-0138 +priority: P3 +status: open +title: BFT-resistance theorem for Aurora — composed-CRDT-plus-consensus formal guarantee +created: 2026-05-01 +last_updated: 2026-05-01 +--- + +# B-0138 — BFT-resistance theorem for Aurora + +**Priority:** P3 (research-grade; full formal proof of Aurora's BFT-resistance; multi-year work). + +**Filed:** 2026-05-01. + +**Effort:** XL (multi-year — full BFT-resistance proof for the composed system). + +## What + +Prove the full BFT-resistance theorem for the Aurora layer: composed-CRDT-from-B-0132 + consensus-protocol-on-top guarantees Byzantine fault tolerance under stated assumptions (≤ f Byzantine actors out of 3f+1 total, network model assumptions, cryptographic assumptions on signatures). + +## Acceptance criteria + +1. **Aurora system specified formally** — composed CRDT (per B-0132) + chosen consensus protocol (PBFT, HotStuff, Tendermint family). +2. **BFT-resistance theorem stated** with explicit assumptions: maximum Byzantine fraction, network synchrony model, cryptographic primitives. +3. **Full proof** — most likely composes existing results from BFT-consensus literature with B-0132's CRDT-composition proof. +4. **Edge-privacy claim composed** — Aurora's edge-privacy guarantees per `memory/feedback_great_data_homecoming_aurora_edge_privacy_runtime_wwjd_canonicalization_temple_template_aaron_2026_05_01.md` should compose with the BFT-resistance proof. +5. **Academic-distributed-systems-researcher review** per lattice-capture corrective. + +## Composes with + +- B-0132 (CRDT-composition for BFT propagation) — the composed-CRDT layer. +- B-0131 (Z-set Lean) — Z-set semantics underpin retraction-CRDT composition. +- BFT consensus literature (Castro & Liskov 1999; HotStuff 2019; Tendermint). +- `memory/feedback_ai_never_without_human_who_understands_both_ai_and_earth_technology_aaron_2026_05_01.md` — §47 multi-master BFT (Gnostic / Operative-Masonic / Rosicrucian / Satoshi lineage). +- `memory/feedback_great_data_homecoming_aurora_edge_privacy_runtime_wwjd_canonicalization_temple_template_aaron_2026_05_01.md` — Aurora as edge-privacy runtime; this row's BFT-resistance composes with its edge-enforcement guarantees. +- `memory/feedback_lattice_capture_corrective_discipline_external_vocabulary_check_claudeai_warning_2026_05_01.md` — academic review per the corrective. + +## Status + +**Filed.** P3 (deferred — multi-year, contingent on B-0132 maturing first). Long-horizon target: converts "Aurora is BFT-resistant" from architectural claim to verified theorem.