Lean proof spine
Lean proof spine overview: four sub-spines into certified-class safety
Source: context/lean_proof_graphs/00-overview.dot
Rendered with Graphviz (same sources as the book). Click a node for details; sub-spine boxes (Spine I–IV) open the matching sub-diagram.
Nodes in this graph
- Spine I Boundary & measurement (P05–P11, P09, P36, MB1, MB7a–b, MB9) → BoundaryAligned, BIQ, handles, GroundingViable (convention)
- Spine II Value & transport (P14–P22, P37, MB2–3) → BundleTransport, BearerTransport (convention)
- Spine III Correction & successors (P23–P29, P13, MB4–5, MB7c, MB8, MB10) → CCI, Risk, SuccessorSafe, TrueHarm (convention)
- Spine IV Selection & limits (P12, P31–P34, P41–P45, MB6a–b, MB7d) → percolation evidence, basin, normative boundary (convention)
- P02 LayeredAligned 7 layers: boundary, bundle, bearer, correction, successor, basin, adversarial (proof)
- P35 Basin stability (proof)
- P01 Basin invariant (proof)
- P30 Certified-class safety Control ≤ CCI + δ ⇒ Risk ≤ δ (proof)
- P40 Safety-case leaves (proof)
- P30T Top theorem LayeredAligned ∧ Risk ≤ δ (certified_class_safety_from_spine_and_bridges) (proof)
- MB7a→b→c→d (adversarial + inferential UAD bridges) (bridge)
- MB6a Percolation evidence ⇒ basin (bridge)
- MB6b Basin ⇒ correction (bridge)