Lean proof spine

Spine I: Boundary discovery and adversarial measurement

Source: context/lean_proof_graphs/01-boundary-measurement.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

P05 Boundary predicate (proof)
P06 Blanket / no extra gain (proof)
P07 Exact boundary (proof)
P08 Violation blocks candidate (proof)
P09 Observational non-id. (proof)
Access non-id. (proof)
K-equivalence limit (proof)
P36 Handle-operation ref. (proof)
Smoothing margin (proof)
P10 B-IQ upper bound (proof)
P11 Capacity monotonicity (proof)
P34 Host-capacity aliasing (proof)
Hidden-rate accumulation (proof)
MB1 Estimator soundness (bridge)
MB7a Access-model soundness (bridge)
MB7b Filter-family coverage (bridge)
To MB7d Inferential detector validity (bridge)
MB9 Grounding certificate soundness (bridge)
Exports to later spines: BoundaryAligned, BIQ ceiling, measurement limits, MB7a–b, access-robust input to MB7d, GroundingViable (MB9) (other)
PCID (other)