TreeComparison.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Quantitative paired comparison for the actual rational diagrams

This assembles the graph cycle, all six local quartet estimates, exact product-fiber coordinates, and horizontal density domination. The error is explicit; no tree-comparison theorem is taken as an input.

theorem OAI.Ostmann.pairedRationalTree_comparison line 17