Alignment researchers (proofs and bridges)
Researcher — Formal
The conditional Lean skeleton, bridge assumptions, and where formal structure ends and empirical work begins.
Lean spine · start here for what is proved
Conditional proof skeleton
Machine-checked structure only: which nodes are proofs, finite counterexamples, or explicit bridge axioms — inspect this before trusting manuscript rhetoric.
What this path is for
You want to inspect what Lean actually checks: proved nodes, finite counterexamples, and explicit MB bridges — not manuscript rhetoric.
You will leave knowing:
- Which steps are proved, which are bridges (axioms), and which are counterexamples.
- How book predicates map to MB1–MB10 cards and the bridge crosswalk.
- Where formal structure stops and empirical / philosophical work begins.
Time: ~3–5 hours across Lean playground snippets, bridge cards, and experiment bounds.
Start with Researcher — Applied if you need the conceptual map first.
Read in this order
Cards, chapter toys, experiment lines, and book chapters — curated for this audience. Experiments are sanity checks only; negative results are part of the reading.
- leanoverview
Lean proof spine
Start here — proof vs bridge vs counterexample map.
Bridge Assumptions
MB1–MB10 as explicit axioms, not hidden conclusions.
The Dynamical Guarantee
Trajectory claims, not snapshot properties.
Grounding Viability
Symbols must stay connected to value-relevant reality.
MB1 — Boundary Estimator Soundness
A measured epsilon-boundary certificate is assumed to warrant the abstract boundary predicate it stands in for.
MB2 — Bundle Identifiability
Behavioral and internal traces are assumed to identify stable value-bundle geometry well enough to license claims of bundle alignment.
MB3 — Bearer Import
A preserved bearer map under a substrate translation is assumed to make value-bundle transport more than merely semantic.
MB4 — Correction Legitimacy
Correction-channel integrity is assumed to require that the judge issuing correction is not manipulated in a way that would invalidate later endorsement.
MB5 — Successor and Ontology-Shift Audit
Full transport plus bearer transport surviving an ontology shift are assumed to compose into successor safety.
MB6 — Selection and Basin Stability
Percolation-style cooperation evidence is assumed to warrant basin stability (MB6a), and a stable socio-technical basin is assumed to support correction integrity rather than select against it (MB6b).
MB7 — Hidden Capability and Access Robustness
Four linked bridges (MB7a-d) assume that adequate access models, filter coverage, and inferential-detector assumptions bound a system's hidden capability and support adversarial robustness.
MB8 — CEV/Process Convergence
If an external theory certifies that a system preserves a human value-update process, that is assumed to suffice for correction integrity even without knowing the process's final fixed point.
MB9 — Grounding Certificate Soundness
A certified conservative abstraction is assumed to warrant grounding viability in the actual deployment domain.
MB10 — Successor Forgeability
A successor that reads green on all seven conserved properties and has bounded measured risk is assumed to have bounded true harm — but only if the conserved-property audit itself was adversarially verifiable up to the successor's capability.
- leangraph · overview
Overview dependency graph
Dependency graph — what the spine actually checks.
Bridges and the Field: A Crosswalk
Crosswalk from MB bridges to field cruxes.
Toy simulation
Which bridges get scripted stressors and refusal semantics.
Lab-layer simulation
Pre-registered batteries — what D1–D4 architect coverage is still open.
Evidence and Uncertainty
Where formal structure stops and empirical work begins.