OAI/NumberTheory/TwoPoint/Bounds/PositivePrimeCostComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual integer-origin transfer of one positive deletion cost. The event is represented by its literal prime-residue circuit, and the comparison uses the same CRT law as the graph estimates.

  1. theorem OAI.TwoPointCorrelations.BravermanDepth22Input.eventually_positive_prime_cost_comparison line 15