other

Lean proof spine

Exports to later spines: BoundaryAligned, BIQ ceiling, measurement limits, MB7a–b, access-robust input to MB7d, GroundingViable (MB9)

OUT is an export / summary node in the dependency graph — it names what a sub-spine contributes rather than a standalone theorem. Follow the incoming edges in the graph, or open the sub-spine diagrams below.