{"path":"research/lean-deliberus-analogies.md","content":"# Lean ↔ Deliberus: Deep Analogies and Transferable Patterns\n\n**Date**: March 28, 2026 (Session 4)\n**Context**: Exploring the \"Lean for all knowledge and decision-making\" analogy in depth — going beyond the surface-level \"proposer + verifier\" pattern already documented in [technical-direction.md](../technical-direction.md) to find concrete architectural and social patterns from the Lean proof assistant that could make Deliberus better.\n\n**Companion research**: [lean4-proof-assistant-deep-dive.md](lean4-proof-assistant-deep-dive.md) (architecture), [lean-social-system-research.md](lean-social-system-research.md) (community dynamics)\n\n---\n\n## The Surface Analogy vs. The Deep Analogy\n\nThe **surface analogy** (already in [technical-direction.md §Lean4 Transferable Lessons](../technical-direction.md)):\n- Proof trees ≈ argument trees\n- Premise selection ≈ searching existing claims for duplicates\n- Kernel architecture: small trusted checker, creative proposer layer\n- NOT transferable: deductive certainty, mathematical domain specificity\n\nThe **deep analogy** explored here: Lean's success is not primarily about its type system — it's about the **social system built around formal verification**. Trustless collaboration through machine-checked proofs, progressive formalization via blueprints, accumulated knowledge creating automation, governance by norms rather than rules. Each of these has a direct analogue in collaborative deliberation.\n\n---\n\n## 1. `sorry`-Driven Argument Blueprints (The Big One)\n\n### What `sorry` Does in Lean\n\n`sorry` is a built-in axiom in Lean that can prove *any* proposition. It makes the system unsound — but it lets you **sketch the structure of a proof before filling in every detail.** The compiler tracks `sorry` transitively: if theorem B depends on theorem A, and A uses `sorry`, both are flagged as incomplete. You get a clear audit trail of what's truly proven versus what's just sketched.\n\nTerence Tao's PFR project (Nov 2023) demonstrated the social power: a 33-page proof was formalized in *three weeks* by 25 strangers. Each contributor picked a `sorry`-marked node from the dependency graph, filled it in, and submitted a PR. They didn't need to understand the whole proof — just their node and its immediate dependencies. Tao explicitly noted: \"One key advantage of working with a project based around a proof assistant language such as Lean is that it makes large-scale mathematical collaboration possible without necessarily having a pre-established level of trust amongst the collaborators.\"\n\n### What This Means for Deliberus\n\nThe Deliberus pipeline (see [extraction-pipeline-design.md](extraction-pipeline-design.md)) currently describes *extraction* — getting claims out of text. And the evaluation model describes *scoring* — measuring how well-supported claims are. But there's a gap: **how do people collaboratively BUILD and STRENGTHEN the argument graph over time?**\n\nThe `sorry` pattern fills this gap. Imagine:\n\n1. **A user sketches an argument structure**: \"Factory farming should be banned [because: animal suffering `sorry`, climate impact `sorry`, ethical framework `sorry`].\" The three `sorry` nodes are explicit markers: \"I believe these things matter but haven't justified them yet.\"\n\n2. **The system tracks dependencies transitively**: The conclusion \"factory farming should be banned\" is flagged as resting on three unexamined foundations. Every downstream argument that depends on this conclusion inherits the `sorry` status. You can SEE which parts of a large deliberation rest on unexamined premises.\n\n3. **The dependency graph becomes a contribution interface**: Like Tao's PFR blueprint, each `sorry` node is an *invitation*. Someone who knows climate science fills in the climate `sorry`. Someone with ethics expertise fills in the ethical framework `sorry`. They don't need to understand the whole argument — just their node.\n\n4. **Incompleteness is visible, not hidden**: The platform shows exactly what's well-supported and what's placeholder. This is the opposite of how social media works (every hot take presents itself as fully justified). Making the holes visible IS the epistemic contribution.\n\n### Connection to Progressive Disclosure\n\nThis connects directly to the **progressive disclosure** principle (see [vision.md §The Deeper Thesis](../vision.md)): a casual user sees the argument structure with color-coded health indicators (green = well-supported, blue = ready for evidence, orange = far from resolved). An expert drills into the `sorry` nodes and fills them in.\n\n### Connection to \"No Copout Axioms\"\n\nWhen someone marks a value premise as `sorry`, the system is explicitly saying \"this is an unexamined foundation.\" The Socratic function — \"you marked this as foundational; can you articulate what's underneath?\" (see [vision.md §The \"No Copout Axioms\" Conviction](../vision.md)) — becomes a natural interaction pattern: *help me fill in this `sorry`*.\n\n### The Blueprint System (Patrick Massot)\n\nLean's **Blueprint** tool (317 GitHub stars, used by 40+ formalization projects) makes this even more concrete:\n\n1. **Write LaTeX**: Authors write a conventional mathematical proof broken into labeled lemmas\n2. **Link to Lean code**: Each lemma links to its formalization (or is marked \"not yet formalized\")\n3. **Auto-generate dependency graph**: Visual graph showing how lemmas depend on each other\n4. **Color-coded status**:\n   - **Green**: Fully formalized (both statement and proof in Lean)\n   - **Blue**: Statement formalized, proof ready to be written (all prerequisites done)\n   - **White with green border**: Statement formalized, but some prerequisites missing\n   - **Orange**: Far from being formalizable (many dependencies unmet)\n5. **Progressive formalization**: The graph evolves from mostly white/orange to green as contributors work in parallel\n\n**Deliberus equivalent**: An \"argument blueprint\" where claims have statuses:\n- **Green**: Well-supported (evidence + community vetting)\n- **Blue**: Claim stated, ready for evidence (dependencies met)\n- **White/green border**: Claim stated but some supporting premises still `sorry`\n- **Orange**: Far from resolvable (deep dependencies unmet)\n\nThe blueprint dependency graph IS the contribution interface. Users scan for blue nodes and fill them in.\n\n### How This Changes the Cold-Start Problem\n\nThe single-player utility story (see [single-player-utility.md](single-player-utility.md)) is \"paste a URL → get argument analysis.\" That's consumption. The `sorry` pattern creates a **contribution** primitive that's as low-friction as consumption: \"sketch an argument with holes.\" You don't need to have a complete, rigorous argument to contribute. You just need to see the shape of one.\n\nThis is how Lean solved its own cold-start problem. Mathlib grew because contributing was tractable — you could fill in one lemma without understanding the whole library. Deliberus's argument graph can grow the same way: each `sorry` is a bite-sized contribution opportunity.\n\n### Free-Form Text and Voice as the Ground-Level `sorry` Generator\n\n**Key UX insight (Session 4)**: The `sorry` model maps perfectly to the founding UX vision of a large, friendly text box (or voice transcription) as the ground-level input. A user types freely or speaks naturally:\n\n> \"I think factory farming should be banned because of animal suffering and also climate change, and honestly I think there's a basic ethical issue too\"\n\nThe system's extraction pipeline (see [extraction-pipeline-design.md](extraction-pipeline-design.md)) processes this free-form input and produces:\n\n```\nNORMATIVE CLAIM: \"Factory farming should be banned\"\n  ├── PREMISE (sorry): \"Factory farming causes animal suffering\" [needs evidence]\n  ├── PREMISE (sorry): \"Factory farming accelerates climate change\" [needs evidence]\n  └── VALUE PREMISE (sorry): \"There is a basic ethical obligation regarding animal welfare\" [needs decomposition]\n```\n\nThe user sees the extracted structure: \"Is this what you meant?\" They confirm, edit, or refine. The `sorry` markers are generated automatically — the user never needs to think in terms of formal argument structure. They just talk. The system does the structuring AND marks what's unexamined.\n\nThis is the resolution of Thread 1 (Structure-Adoption Paradox, see [conceptual-threads.md §Thread 1](../conceptual-threads.md)) taken to its logical conclusion: the LLM absorbs the structuring burden, AND the `sorry` mechanism makes incompleteness a feature rather than a barrier. The user experiences **zero friction** while the system maintains **full structural rigor** underneath — with explicit markers for where that rigor has gaps.\n\nThe voice-to-argument pipeline described in [mobile-argument-ux.md](mobile-argument-ux.md) §2.5 and §3 is exactly this: speak for 30-90 seconds → LLM extracts conclusion + premises → user confirms → structured argument with `sorry` markers enters the graph. Every premise the user didn't elaborate on gets a `sorry`. Every value they asserted without justification gets a `sorry (value premise, currently undecomposed)`.\n\n**The contribution barrier drops to zero** because:\n- You don't need to know what argument structure is\n- You don't need to have complete evidence\n- You don't need to be rigorous about your reasoning\n- You just need to care about something enough to say it\n\nThe rigor comes from the system's structuring AND from other contributors filling in the `sorry` nodes. This is the \"hybrid AGI\" (see [conceptual-threads.md §Thread 2](../conceptual-threads.md)) in action: humans contribute messy intuitions, the system structures them, and the collective fills in the gaps.\n\n---\n\n<a id=\"flywheel\"></a>\n\n## 2. The `@[simp]` Flywheel: Accumulated Knowledge That Automates Reasoning\n\n### How It Works in Lean\n\nIn Lean, the `simp` tactic applies a growing set of rewrite rules. Every time someone proves a lemma and tags it `@[simp]`, the system gets slightly smarter — future proofs that would have required manual work can now be automated. The community carefully curates what gets tagged, because a bad `@[simp]` lemma changes the behavior of *every future proof*.\n\nLean's automation has two modes:\n1. **Algorithmic knowledge** (`omega`, `decide`, `norm_num`): Fixed mathematical algorithms — decision procedures that are provably complete for their domain. They don't grow with the library.\n2. **Accumulated knowledge** (`simp`, `aesop`, `exact?`): These grow with every contribution. Each `@[simp]` lemma, each `@[aesop]` rule, each new library lemma makes these tactics more powerful. This is **crowdsourced automation**.\n\nThe `exact?` tactic is especially illuminating: given a proof goal, it searches the *entire* Mathlib library for a lemma that directly solves it. The more lemmas exist, the more likely `exact?` finds one. Every contributor who proves a lemma and adds it to Mathlib makes `exact?` more powerful for everyone.\n\n### Deliberus Application\n\nFor Deliberus, this translates to: **every well-vetted argument should make the platform better at automatically connecting future arguments to existing ones.**\n\nConcretely: when someone claims \"UBI would cost $X,\" the system should automatically surface \"this relates to established claim E1 in the UBI deliberation, which has a net-vs-gross cost qualification (E3)\" (see [extraction-virtual-run.md](extraction-virtual-run.md)). The more the community deliberates, the more the system can do this — the same flywheel that makes Lean's `simp` more powerful with each contribution.\n\n**The curation aspect is critical**: not every verified claim should be in the auto-reasoning set. The community decides what's \"canonical\" enough to be automatically invoked (like Mathlib's `@[simp]` review). This creates a *curated, growing, communal knowledge base* — which is exactly the \"civilizational deliberation graph\" described in [vision.md §The Destination](../vision.md), but with a concrete mechanism for how it grows.\n\n**Two corresponding layers for Deliberus**:\n\n| Layer | Lean Equivalent | Deliberus Application |\n|-------|----------------|----------------------|\n| **Algorithmic** | `omega`, `decide` | Logic checkers, consistency validators, NLI entailment checks, deductive closure — fixed algorithms that check argument structure |\n| **Accumulated** | `simp`, `exact?` | Community-vetted claims that the system auto-references. \"This claim follows from established claims X, Y, Z\" — searched automatically. The `exact?` moment: \"this claim is exactly what was proven in discussion #4523\" |\n\n**The flywheel effect**: More community contributions → more accumulated knowledge → more the system can auto-connect → lower friction for new contributors → more contributions. This is the same positive feedback loop that made Mathlib grow from a hobby project to 1.9 million lines.\n\n---\n\n## 3. The Definition Problem Is Recursive\n\n### The Deepest Philosophical Connection\n\nKevin Buzzard's key observation: \"If you miss or garble an axiom then your code will still compile, it just won't mean what it is supposed to mean.\"\n\nIn Lean, the kernel can check proofs but **NOT** whether definitions capture the intended mathematical concept. Definitions require *human judgment and social process* — Zulip discussions, multi-tier review, and the explicit review question: \"are the definitions introduced the best way to formalize the concept (very difficult!)?\"\n\nThis maps exactly to Deliberus's contested concepts problem (see [conceptual-threads.md §Thread 4](../conceptual-threads.md), Emanuel's discourse-layer insight in [voice-memo-emanuel-sofia.md](voice-memo-emanuel-sofia.md)). The system can check argument *structure*, but whether the *terms* are defined correctly is the hardest problem — and it's the problem that requires *deliberation*.\n\n### The Recursive Beauty\n\n**The tool for deliberation needs deliberation to define its own terms.** What counts as a \"well-formed argument\"? What are the rules of rational argumentation? These are themselves questions that should be deliberated upon. In Lean, the kernel is designed by logicians and is small enough (~5,000 lines of C++) to be audited. In Deliberus, the \"argument validity kernel\" — the set of rules by which the system judges argument structure — should similarly be:\n\n- **Small**: A minimal set of structural rules (does the argument have the claimed logical form? are premises relevant to conclusion? are terms consistently defined?)\n- **Explicit**: Every rule is visible and inspectable by any user\n- **Deliberatable**: The community can argue about the rules themselves — using the platform to reason about its own foundations\n\nThis is the \"rationality standards built into the software\" from [vision.md §The Solution](../vision.md), given a concrete architectural form. And Lean's lesson is that the kernel's trustworthiness comes from its *smallness*. Don't try to encode all of rational argumentation into the kernel — encode the minimum, and let everything else be human judgment mediated by the system.\n\n### What the Deliberus Kernel Can and Cannot Check\n\n| Can check (kernel) | Requires human judgment |\n|---|---|\n| Argument has the claimed logical form | Whether premises are TRUE |\n| Premises are relevant to conclusion | Whether values are IMPORTANT |\n| Terms are used consistently within one argument | Whether definitions CAPTURE the intended concept |\n| No circular reasoning | Whether analogies are apt |\n| Deductive steps follow | Whether inductive evidence is sufficient |\n\nThis maps to the fact/value boundary (see [conceptual-threads.md §Thread 3](../conceptual-threads.md)): the kernel handles structure; humans handle meaning.\n\n**A 2026 sharpening of this boundary, and a limit it imposes.** The analogy got stronger and narrower at the same time. Stronger: AlphaProof reached IMO-silver-level formal reasoning and then, in 2026, nine open Erdős problems and 44 unproven OEIS conjectures — **with** Lean rather than by outgrowing it, on the explicit ground that the kernel certifies correctness so search can be rewarded by a verifier instead of by model judgment. Its stated failure mode is ours in another register: *\"error cascade is invisible in informal proofs — small hallucinations produce wrong mathematics that still reads fluently.\"*\n\nNarrower: Lean's kernel pays **twice**, and only one of those payments is available here. It checks, and it supplies free, infinite, ground-truth reward, which is what made large-scale reinforcement learning possible in mathematics. Deliberation has no such oracle, because what a Deliberus kernel could certify is validity-of-form, never truth-of-content — which is exactly what the table above already says. So **we can borrow the checkability argument and must not expect the training flywheel**, and Deliberus should not model its trajectory on AlphaProof's. Full analysis: [structure-versus-scale.md](structure-versus-scale.md).\n\n---\n\n## 4. Deprecation Over Deletion: How Understanding Evolves\n\n### The Lean Pattern\n\nWhen Mathlib finds a better definition, the old one isn't deleted — it's linked to the new one with a deprecation period. Old and new coexist for months, with automated warnings pointing users to the improved version. The \"Growing Mathlib\" paper (Baanen et al., 2025) documents this as a core maintenance practice.\n\n### Why This Matters More for Deliberation Than for Math\n\nFor deliberation, this is MORE important than for mathematics. When understanding evolves — when a better formulation of \"fairness\" emerges in the UBI debate (see [extraction-virtual-run.md §Contested Concepts](extraction-virtual-run.md)) — the old formulation should remain linked, visible, navigable. The *history of how understanding evolved* is itself a form of knowledge.\n\nThe \"aha moment\" described in [extraction-virtual-run.md §Key Findings](extraction-virtual-run.md) — \"oh, we were using the same word differently — THAT'S why we disagree\" — is only possible if you can see the definitional evolution.\n\n**Concrete application for Deliberus**:\n- When a better formulation of a claim is found, the old one isn't deleted — it's linked to the new formulation with a \"superseded by\" relationship\n- Users can still navigate old formulations and understand why the community moved to the new one\n- The evolution trail IS content — \"we used to think 'fairness' meant X; then we realized it meant three different things (D2, D3 from the UBI extraction); now each sense has its own node\"\n- This connects to Graphiti's temporal metadata — Deliberus needs temporal versioning of claims, definitions, and argument structures\n\n---\n\n## 5. Trustless Collaboration Through Structural Verification\n\n### The Lean Insight\n\nLean's deepest social innovation: strangers can contribute to a shared proof without trusting each other, because the compiler verifies correctness. Tao's PFR project had 25 contributors, most of whom had never met, approving each other's PRs based on automated verification alone.\n\n### The Deliberus Challenge\n\nFor Deliberus, the verification is weaker — arguments are richer than proofs, and \"correctness\" is not binary. But the principle transfers in modified form:\n\n**Structural verification**: The system can check that a contribution *fits* — that a claimed premise actually supports its conclusion (via NLI), that terms are used consistently, that the argument type classification is correct. This is enough to enable trustless contribution to the structural skeleton. The *content* still needs human judgment, but the *structure* can be machine-checked.\n\n**The trust spectrum**:\n- **Fully machine-checkable**: Deductive validity, term consistency, circular reasoning detection\n- **Machine-assisted, human-confirmed**: NLI entailment probability, argument type classification, relevance scoring\n- **Fully human-judged**: Truth of premises, importance of values, aptness of analogies, quality of evidence\n\nThis creates a participation model where different contributions require different levels of trust — similar to Lean's distinction between kernel-checked proofs and reviewer-assessed definitions.\n\n---\n\n## 6. The Three Skills Model\n\n### Lean's Observation\n\nAlex Kontorovich (Rutgers) identifies \"three distinct skills\" in Lean formalization:\n1. **Knowing the mathematics** — to write the blueprint\n2. **Coordinating the formalization** — to organize contributors\n3. **Refactoring into Mathlib-quality code** — to integrate results into the shared library\n\nThese are different skills that different people may excel at.\n\n### Deliberus Equivalent\n\n1. **Contributing arguments** — domain expertise, caring about a topic enough to articulate your reasoning\n2. **Organizing deliberations** — structuring the debate, identifying contested concepts, suggesting decompositions\n3. **Curating the canonical graph** — deciding what's canonical, managing concept evolution, maintaining quality standards\n\nThese correspond roughly to Shneiderman's Reader → Contributor → Collaborator → Leader progression (see [academic-foundations.md §8](../academic-foundations.md)), but with Lean-specific insight about what each tier actually does.\n\n---\n\n## 7. Incremental Re-Validation (The Lake Pattern)\n\n### The Lean Problem\n\nMathlib is 1.9 million lines. Without incremental builds, every change would require recompiling everything. Lake (Lean's build system) tracks dependencies at the file level and recompiles only what's necessary. The community is very conscious of import hierarchies — adding an unnecessary import can cause huge compilation cascades.\n\n### The Deliberus Application\n\nWhen a claim in the Deliberus graph changes — new evidence, revised definition, superseded formulation — the system can't re-validate the entire graph. It needs dependency tracking and incremental re-validation:\n\n- When claim X is updated, re-check only arguments that directly depend on X\n- Track which conclusions are affected by the change and flag them for re-evaluation\n- Minimize the \"compilation cascade\" — a change to a foundational definition shouldn't require re-evaluating every argument in the graph, but it should flag all affected downstream arguments\n\nThis is a practical architecture insight for the graph engine described in [extraction-pipeline-design.md §Graph Schema](extraction-pipeline-design.md).\n\n---\n\n## Master Mapping Table\n\n| Lean Pattern | Deliberus Application | Primary Reference |\n|---|---|---|\n| `sorry` placeholders | Sketch arguments with explicit holes; contribute by filling them | §1 above |\n| Blueprint dependency graph | Visual map of argument health — what's supported, what needs work | §1 above |\n| Free-form text/voice → `sorry` | Users talk freely, system extracts structure with `sorry` markers | §1 (Free-Form Text section) |\n| `@[simp]` knowledge flywheel | Each vetted claim makes the system better at connecting future arguments | §2 above |\n| `exact?` library search | \"This claim already exists in discussion #X\" — auto-surfacing | §2 above |\n| Small trusted kernel (~5K lines) | Minimal, auditable rules of argument structure | §3 above |\n| Definition deliberation via Zulip | The platform deliberates about its own concepts (recursive) | §3 above |\n| Deprecation over deletion | Track how understanding evolves, don't erase history | §4 above |\n| Transitive `sorry` tracking | See which conclusions rest on unexamined foundations | §1 above |\n| Trustless collaboration via compiler | Structural verification enables contribution without prior trust | §5 above |\n| Three skills (math, coordination, integration) | Contributing arguments, organizing deliberations, curating the canonical graph | §6 above |\n| Lake incremental builds | Re-validate only affected arguments when a claim changes | §7 above |\n| Proof terms as ground truth | Formal argument graphs as the ground truth artifact | [technical-direction.md](../technical-direction.md) |\n| Type class inference chains | Automatic classification of claim types and relationships | [technical-direction.md](../technical-direction.md) |\n| Mathlib as escape velocity | Community-built library of vetted arguments as critical mass | [single-player-utility.md](single-player-utility.md) |\n| Formalisation coefficient | Effort ratio: formal argument structure vs. informal statement | §1 above |\n| The \"LLMs lie\" problem (Buzzard) | Why structured argumentation with community vetting is needed | [vision.md §The Problem](../vision.md) |\n\n---\n\n## The Deepest Lesson\n\n**The social system IS the verification system.** Mathlib's governance — Zulip discussions, multi-tier review, collective vision maintenance, deprecation processes — is as much a part of the \"proof assistant\" as the type checker. The social norms ARE the quality control. Lean's 5,000-line kernel draws a hard boundary between what the machine guarantees and what the community governs.\n\nDeliberus should design its social processes with the same intentionality that Lean designs its type system. The machine checks structure; the community judges meaning. The machine tracks incompleteness; the community fills in the gaps. The machine accumulates canonical knowledge; the community curates what's canonical.\n\nNeither alone is Deliberus. The synthesis is the system.\n\n## 8. The Convergence Thesis: Lean's Deepest Gift (Mar 31, 2026)\n\nThe Lean analogy has one more layer — perhaps the most important. In Lean, the axioms (type theory) are trusted, shared, and universal. Every proof in Mathlib verifies against the same foundations. The question for Deliberus: what are OUR axioms?\n\nThe founder's conviction (session 8): **human values converge when decomposed far enough.** The \"No Copout Axioms\" principle, taken to its ultimate depth, doesn't just say you CAN keep decomposing — it says that when you DO, different worldviews arrive at the same bedrock: consciousness matters, suffering is real, shared humanity is foundational. The disagreements that consume us live in the middle layers (definitions, cultural framing, empirical beliefs), not at the bottom.\n\nIf this is true, the Lean analogy becomes structural, not metaphorical:\n\n| Lean | Deliberus |\n|------|-----------|\n| Axioms: type theory (trusted, universal) | Axioms: human values (convergent at depth) |\n| Kernel: ~5,000 lines of C++ | Value bedrock: consciousness, suffering, shared humanity |\n| Agents verify proofs against axioms | Agents verify reasoning against converged values |\n\nThis means AI alignment through Deliberus isn't \"checking against what humans decided\" (culturally relative) — it's verifying reasoning against the **natural convergence of human values at depth** (potentially universal). Alignment through shared foundations, not imposed constraints.\n\n**External validation — Tao's verification thesis** (March 29, 2026): Terence Tao — who used Lean for the PFR project that inspired §1 above — published \"Mathematical Methods and Human Thought in the Age of AI\" ([arXiv:2603.26524](https://arxiv.org/abs/2603.26524)). His core argument: verification is the bottleneck, formal infrastructure (Lean) provides structural guarantees, but meaning and value remain irreducibly human. His \"red team\" framework (AI for verification, humans for meaning) IS the Deliberus workflow. And his warning about \"AI collapse\" (AI trained on AI outputs degrades without genuine human content) validates why a human-maintained argument graph matters — it's immune to recursive degradation. See [ai-safety-and-tao-augmentation-research.md §5.3](ai-safety-and-tao-augmentation-research.md).\n\n**The row that says *agents verify reasoning against converged values* stayed a single table cell for four and a half months.** Collected 2026-08-17 into a strategy: the distinction between an agent *fact-checking against* the graph and an agent *verifying an inference through* it decides whether agent consumption is a commodity or the one thing this architecture is uniquely shaped to do. See [agents-as-a-consumer-class.md](agents-as-a-consumer-class.md) § 2.\n\nFull exploration: [session8-landing-page-and-civilizational-vision.md §8](session8-landing-page-and-civilizational-vision.md). See also [vision.md §The \"No Copout Axioms\" Conviction — The Convergence Thesis](../vision.md).\n\n---\n\n## Cross-References\n\n- **Companion research**: [lean4-proof-assistant-deep-dive.md](lean4-proof-assistant-deep-dive.md) (Lean architecture, kernel, tactics, Mathlib, AI integration), [lean-social-system-research.md](lean-social-system-research.md) (sorry, blueprints, simp, governance, community dynamics)\n- **Upstream docs**: [vision.md](../vision.md) §Core Dialectic, §No Copout Axioms, §The Destination | [conceptual-threads.md](../conceptual-threads.md) §Thread 1 (sorry solves the Structure-Adoption Paradox), §Thread 2 (hybrid intelligence), §Thread 4 (simp flywheel for dedup), §Thread 7 (trustless collaboration for gaming resistance) | [technical-direction.md](../technical-direction.md) §Lean4 Transferable Lessons\n- **Downstream implications**: [extraction-pipeline-design.md](extraction-pipeline-design.md) (sorry markers generated during extraction), [mobile-argument-ux.md](mobile-argument-ux.md) (voice → sorry), [single-player-utility.md](single-player-utility.md) (sorry lowers cold-start barrier)\n"}