Skip to content

Commit d294af1

Browse files
committed
chore: update project files
1 parent be33120 commit d294af1

7 files changed

Lines changed: 166 additions & 109 deletions

File tree

30.2 KB
Binary file not shown.

paper/main.aux

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,7 @@
3636
\citation{polya1927}
3737
\@writefile{toc}{\contentsline {section}{\numberline {6}Extended Certification on $[1.0, 3.0]$}{4}{section.6}\protected@file@percent }
3838
\newlabel{sec:extended}{{6}{4}{Extended Certification on $[1.0, 3.0]$}{section.6}{}}
39-
\newlabel{lem:wtail}{{9}{4}{Uniform tail bound}{theorem.9}{}}
39+
\newlabel{lem:wtail}{{9}{4}{Uniform tail bound on {$[1,3]$}}{theorem.9}{}}
4040
\newlabel{thm:extended}{{10}{4}{}{theorem.10}{}}
4141
\@writefile{toc}{\contentsline {section}{\numberline {7}Tail Bound for $u \geq 3.0$}{4}{section.7}\protected@file@percent }
4242
\newlabel{sec:tailbound}{{7}{4}{Tail Bound for $u \geq 3.0$}{section.7}{}}
@@ -138,6 +138,7 @@
138138
\@writefile{toc}{\contentsline {paragraph}{(iv) AEE assessment.}{14}{section*.19}\protected@file@percent }
139139
\@writefile{toc}{\contentsline {section}{\numberline {B}Proof Certificate Table}{14}{appendix.B}\protected@file@percent }
140140
\newlabel{sec:cert}{{B}{14}{Proof Certificate Table}{appendix.B}{}}
141+
\@writefile{toc}{\contentsline {paragraph}{Proof-critical fields in \texttt {results/verify\_ia\_1\_to\_3.json}.}{15}{section*.20}\protected@file@percent }
141142
\@writefile{toc}{\contentsline {section}{\numberline {C}P\'{o}lya Source Analysis}{15}{appendix.C}\protected@file@percent }
142143
\newlabel{sec:polya_audit}{{C}{15}{P\'{o}lya Source Analysis}{appendix.C}{}}
143144
\@writefile{toc}{\contentsline {section}{\numberline {D}Submission Checklist}{15}{appendix.D}\protected@file@percent }
@@ -147,13 +148,13 @@
147148
\@writefile{toc}{\contentsline {subsection}{\numberline {E.1}Notation and scaling}{16}{subsection.E.1}\protected@file@percent }
148149
\@writefile{toc}{\contentsline {subsection}{\numberline {E.2}Expansion of $\Delta Q$}{16}{subsection.E.2}\protected@file@percent }
149150
\newlabel{lem:deltaQ}{{17}{16}{}{theorem.17}{}}
150-
\@writefile{toc}{\contentsline {subsection}{\numberline {E.3}Explicit derivative formulas and certified bounds}{16}{subsection.E.3}\protected@file@percent }
151-
\newlabel{lem:derivbounds}{{18}{16}{Certified derivative-ratio bounds}{theorem.18}{}}
151+
\@writefile{toc}{\contentsline {subsection}{\numberline {E.3}Explicit derivative formulas and certified bounds}{17}{subsection.E.3}\protected@file@percent }
152+
\newlabel{lem:derivbounds}{{18}{17}{Certified derivative-ratio bounds on {$[1,3]$}}{theorem.18}{}}
152153
\newlabel{cor:Rbounds}{{19}{17}{}{theorem.19}{}}
153154
\@writefile{toc}{\contentsline {subsection}{\numberline {E.4}Bounding $|W_{\mathrm {tail}}|$}{17}{subsection.E.4}\protected@file@percent }
154155
\newlabel{lem:Wtail_bound}{{20}{17}{}{theorem.20}{}}
155-
\@writefile{toc}{\contentsline {subsection}{\numberline {E.5}Interval-arithmetic certificate for $B(u)$ and the sign of $W$}{17}{subsection.E.5}\protected@file@percent }
156-
\newlabel{lem:Bsign}{{21}{17}{Interval-arithmetic certificate}{theorem.21}{}}
156+
\@writefile{toc}{\contentsline {subsection}{\numberline {E.5}Interval-arithmetic certificate for $B(u)$ and the sign of $W$}{18}{subsection.E.5}\protected@file@percent }
157+
\newlabel{lem:Bsign}{{21}{18}{Interval-arithmetic certificate}{theorem.21}{}}
157158
\newlabel{lem:epsstar}{{22}{18}{$\varepsilon ^*$ is strictly decreasing}{theorem.22}{}}
158159
\@writefile{toc}{\contentsline {subsection}{\numberline {E.6}Complete proof of Lemma~\ref {lem:wtail}}{18}{subsection.E.6}\protected@file@percent }
159160
\gdef \@abspage@last{18}

paper/main.log

Lines changed: 71 additions & 64 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
This is pdfTeX, Version 3.141592653-2.6-1.40.28 (MiKTeX 25.12 Portable) (preloaded format=pdflatex 2026.5.13) 3 JUN 2026 09:08
1+
This is pdfTeX, Version 3.141592653-2.6-1.40.28 (MiKTeX 25.12 Portable) (preloaded format=pdflatex 2026.5.13) 3 JUN 2026 09:37
22
entering extended mode
33
restricted \write18 enabled.
44
%&-line parsing enabled.
@@ -623,125 +623,125 @@ Package hyperref Warning: Token not allowed in a PDF string (Unicode):
623623
[3]
624624

625625
Package hyperref Warning: Token not allowed in a PDF string (Unicode):
626-
(hyperref) removing `math shift' on input line 308.
626+
(hyperref) removing `math shift' on input line 311.
627627

628628

629629
Package hyperref Warning: Token not allowed in a PDF string (Unicode):
630-
(hyperref) removing `\geq' on input line 308.
630+
(hyperref) removing `\geq' on input line 311.
631631

632632

633633
Package hyperref Warning: Token not allowed in a PDF string (Unicode):
634-
(hyperref) removing `math shift' on input line 308.
634+
(hyperref) removing `math shift' on input line 311.
635635

636636
[4] [5]
637-
Underfull \hbox (badness 10000) in paragraph at lines 444--444
637+
Underfull \hbox (badness 10000) in paragraph at lines 453--453
638638
\T1/lmr/m/n/10 (+20) log-concavity
639639
[]
640640

641641

642-
Underfull \hbox (badness 10000) in paragraph at lines 446--446
642+
Underfull \hbox (badness 10000) in paragraph at lines 455--455
643643
[]\T1/lmr/m/n/10 (+20) Strong log-
644644
[]
645645

646646

647-
Underfull \hbox (badness 1264) in paragraph at lines 449--449
647+
Underfull \hbox (badness 1264) in paragraph at lines 458--458
648648
[]\T1/lmr/bx/n/10 (+20) Not found
649649
[]
650650

651651

652-
Underfull \hbox (badness 10000) in paragraph at lines 449--449
652+
Underfull \hbox (badness 10000) in paragraph at lines 458--458
653653
\T1/lmr/bx/n/10 (+20) in P�lya
654654
[]
655655

656656

657-
Underfull \hbox (badness 1946) in paragraph at lines 451--452
657+
Underfull \hbox (badness 1946) in paragraph at lines 460--461
658658
[]\T1/lmr/m/n/10 (+20) IF $[] \OML/lmm/m/it/10 Fe[]dt$ \T1/lmr/m/n/10 (+20) has
659659
real ze-ros,
660660
[]
661661

662662

663-
Underfull \hbox (badness 10000) in paragraph at lines 453--453
663+
Underfull \hbox (badness 10000) in paragraph at lines 462--462
664664
[]\T1/lmr/m/n/10 (+20) Confirmed
665665
[]
666666

667667

668-
Underfull \hbox (badness 10000) in paragraph at lines 454--454
668+
Underfull \hbox (badness 10000) in paragraph at lines 463--463
669669
[]\T1/lmr/m/n/10 (+20) Satz II: Mellin--
670670
[]
671671

672672

673-
Underfull \hbox (badness 10000) in paragraph at lines 457--458
673+
Underfull \hbox (badness 10000) in paragraph at lines 466--467
674674
[]\T1/lmr/m/n/10 (+20) Confirmed
675675
[]
676676

677-
LaTeX Font Info: Trying to load font information for TS1+lmr on input line 4
678-
99.
677+
LaTeX Font Info: Trying to load font information for TS1+lmr on input line 5
678+
08.
679679

680680
(C:\Users\trist\scoop\apps\miktex\current\texmfs\install\tex/latex/lm\ts1lmr.fd
681681
File: ts1lmr.fd 2015/05/01 v1.6.1 Font defs for Latin Modern
682682
) [6] [7{C:/Users/trist/scoop/apps/miktex/current/texmfs/install/fonts/enc/dvip
683683
s/lm/lm-ts1.enc}] [8]
684-
Overfull \hbox (27.74112pt too wide) in paragraph at lines 662--681
684+
Overfull \hbox (105.32443pt too wide) in paragraph at lines 671--690
685685
[]
686686
[]
687687

688688
[9] [10]
689-
Overfull \hbox (25.73573pt too wide) in paragraph at lines 754--755
689+
Overfull \hbox (25.73573pt too wide) in paragraph at lines 765--766
690690
[]\T1/lmtt/m/n/10 proof/verify_logconcavity_arb.py|
691691
[]
692692

693693

694-
Underfull \hbox (badness 10000) in paragraph at lines 755--755
694+
Underfull \hbox (badness 10000) in paragraph at lines 766--766
695695
[]\T1/lmtt/m/n/10 python
696696
[]
697697

698698

699-
Overfull \hbox (25.73573pt too wide) in paragraph at lines 755--755
699+
Overfull \hbox (25.73573pt too wide) in paragraph at lines 766--766
700700
\T1/lmtt/m/n/10 proof/verify_logconcavity_arb.py||
701701
[]
702702

703703

704-
Overfull \hbox (51.98566pt too wide) in paragraph at lines 758--759
704+
Overfull \hbox (51.98566pt too wide) in paragraph at lines 769--770
705705
[]\T1/lmtt/m/n/10 proof/verify_logconcavity_rigorous.py|
706706
[]
707707

708708

709-
Underfull \hbox (badness 10000) in paragraph at lines 759--759
709+
Underfull \hbox (badness 10000) in paragraph at lines 770--770
710710
[]\T1/lmtt/m/n/10 python
711711
[]
712712

713713

714-
Overfull \hbox (51.98566pt too wide) in paragraph at lines 759--759
714+
Overfull \hbox (51.98566pt too wide) in paragraph at lines 770--770
715715
\T1/lmtt/m/n/10 proof/verify_logconcavity_rigorous.py||
716716
[]
717717

718718

719-
Underfull \hbox (badness 10000) in paragraph at lines 763--763
719+
Underfull \hbox (badness 10000) in paragraph at lines 774--774
720720
[]\T1/lmtt/m/n/10 python
721721
[]
722722

723723

724-
Underfull \hbox (badness 10000) in paragraph at lines 766--767
724+
Underfull \hbox (badness 10000) in paragraph at lines 777--778
725725
[]\T1/lmtt/m/n/10 verify.py $\OMS/lmsy/m/n/10 !$
726726
[]
727727

728728

729-
Overfull \hbox (56.97314pt too wide) in paragraph at lines 766--767
729+
Overfull \hbox (56.97314pt too wide) in paragraph at lines 777--778
730730
\T1/lmtt/m/n/10 verification/proof_certificate_v2.json|
731731
[]
732732

733733

734-
Underfull \hbox (badness 10000) in paragraph at lines 770--771
734+
Underfull \hbox (badness 10000) in paragraph at lines 781--782
735735
[]\T1/lmtt/m/n/10 falsify.py python
736736
[]
737737

738738

739-
Overfull \hbox (75.5333pt too wide) in paragraph at lines 786--800
739+
Overfull \hbox (75.5333pt too wide) in paragraph at lines 797--811
740740
[]
741741
[]
742742

743743
[11]
744-
Overfull \hbox (4.86513pt too wide) in paragraph at lines 838--841
744+
Overfull \hbox (4.86513pt too wide) in paragraph at lines 849--852
745745
[]\T1/lmr/m/n/10.95 (-20) The in-ter-val arith-metic cer-tifi-cates are not for
746746
-mal-ized in Lean. Ax-ioms \T1/lmtt/m/n/10.95 ia_verification_0_to_1
747747
[]
@@ -753,113 +753,119 @@ Underfull \hbox (badness 1721) in paragraph at lines 75--85
753753
[]
754754

755755
[13])
756-
Underfull \hbox (badness 10000) in paragraph at lines 887--888
756+
Underfull \hbox (badness 10000) in paragraph at lines 898--899
757757
[]\T1/lmtt/m/n/10 Basic.lean\T1/lmr/m/n/10 (+20) :
758758
[]
759759

760760

761-
Underfull \hbox (badness 10000) in paragraph at lines 888--889
761+
Underfull \hbox (badness 10000) in paragraph at lines 899--900
762762
[]\T1/lmtt/m/n/10 Basic.lean\T1/lmr/m/n/10 (+20) :
763763
[]
764764

765765

766-
Overfull \hbox (62.90239pt too wide) in paragraph at lines 890--891
767-
[]\T1/lmtt/m/n/10 verify_logconcavity_rigorous.py|
766+
Overfull \hbox (36.65247pt too wide) in paragraph at lines 901--902
767+
[]\T1/lmtt/m/n/10 verify_logconcavity_arb.py|
768768
[]
769769

770770

771-
Overfull \hbox (36.65247pt too wide) in paragraph at lines 891--892
772-
[]\T1/lmtt/m/n/10 verify_logconcavity_arb.py|
771+
Overfull \hbox (62.90239pt too wide) in paragraph at lines 902--903
772+
[]\T1/lmtt/m/n/10 verify_logconcavity_rigorous.py|
773773
[]
774774

775775

776-
Overfull \hbox (26.1525pt too wide) in paragraph at lines 893--894
776+
Overfull \hbox (26.1525pt too wide) in paragraph at lines 904--905
777777
[]\T1/lmtt/m/n/10 verify_algebraic_core.py|
778778
[]
779779

780780

781-
Underfull \hbox (badness 10000) in paragraph at lines 897--898
781+
Underfull \hbox (badness 10000) in paragraph at lines 908--909
782782
[]\T1/lmr/m/n/10 (+20) No peer-reviewed
783783
[]
784784

785785

786-
Overfull \hbox (6.31557pt too wide) in paragraph at lines 883--901
786+
Overfull \hbox (70.56224pt too wide) in paragraph at lines 894--912
787787
[]
788788
[]
789789

790+
LaTeX Font Info: Font shape `T1/lmtt/bx/n' in size <10.95> not available
791+
(Font) Font shape `T1/lmtt/b/n' tried instead on input line 919.
790792
[14]
791-
Underfull \hbox (badness 1859) in paragraph at lines 942--942
793+
Underfull \hbox (badness 1859) in paragraph at lines 970--970
792794
[]\T1/lmr/m/n/10 (+20) Conc: $[] \OML/lmm/m/it/10 f\OT1/lmr/m/n/10 (+20) (\OML/
793795
lmm/m/it/10 t[]\OT1/lmr/m/n/10 (+20) )\OML/lmm/m/it/10 e[]dt$ \T1/lmr/m/n/10 (+
794796
20) has
795797
[]
796798

799+
[15]
797800

798801
Package hyperref Warning: Token not allowed in a PDF string (Unicode):
799-
(hyperref) removing `math shift' on input line 975.
802+
(hyperref) removing `math shift' on input line 1003.
800803

801804

802805
Package hyperref Warning: Token not allowed in a PDF string (Unicode):
803-
(hyperref) removing `math shift' on input line 975.
806+
(hyperref) removing `math shift' on input line 1003.
804807

805-
[15]
806808

807809
Package hyperref Warning: Token not allowed in a PDF string (Unicode):
808-
(hyperref) removing `math shift' on input line 1007.
810+
(hyperref) removing `math shift' on input line 1035.
809811

810812

811813
Package hyperref Warning: Token not allowed in a PDF string (Unicode):
812-
(hyperref) removing `\Delta' on input line 1007.
814+
(hyperref) removing `\Delta' on input line 1035.
813815

814816

815817
Package hyperref Warning: Token not allowed in a PDF string (Unicode):
816-
(hyperref) removing `math shift' on input line 1007.
818+
(hyperref) removing `math shift' on input line 1035.
817819

818820
[16]
819821

820822
Package hyperref Warning: Token not allowed in a PDF string (Unicode):
821-
(hyperref) removing `math shift' on input line 1080.
823+
(hyperref) removing `math shift' on input line 1121.
822824

823825

824826
Package hyperref Warning: Token not allowed in a PDF string (Unicode):
825-
(hyperref) removing `subscript' on input line 1080.
827+
(hyperref) removing `subscript' on input line 1121.
826828

827829

828830
Package hyperref Warning: Token not allowed in a PDF string (Unicode):
829-
(hyperref) removing `math shift' on input line 1080.
831+
(hyperref) removing `math shift' on input line 1121.
830832

831833

832834
Package hyperref Warning: Token not allowed in a PDF string (Unicode):
833-
(hyperref) removing `math shift' on input line 1104.
835+
(hyperref) removing `math shift' on input line 1145.
834836

835837

836838
Package hyperref Warning: Token not allowed in a PDF string (Unicode):
837-
(hyperref) removing `math shift' on input line 1104.
839+
(hyperref) removing `math shift' on input line 1145.
838840

839841

840842
Package hyperref Warning: Token not allowed in a PDF string (Unicode):
841-
(hyperref) removing `math shift' on input line 1104.
843+
(hyperref) removing `math shift' on input line 1145.
842844

843845

844846
Package hyperref Warning: Token not allowed in a PDF string (Unicode):
845-
(hyperref) removing `math shift' on input line 1104.
847+
(hyperref) removing `math shift' on input line 1145.
846848

847849
[17] [18] (main.aux)
848850
***********
849851
LaTeX2e <2025-11-01>
850852
L3 programming layer <2025-12-24>
851853
***********
854+
855+
856+
LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right.
857+
852858
Package rerunfilecheck Info: File `main.out' has not changed.
853859
(rerunfilecheck) Checksum: 3BC3EB9E1CA15FB8414D40A85B2938EE;5704.
854860
)
855861
Here is how much of TeX's memory you used:
856-
12840 strings out of 467871
857-
203399 string characters out of 5413034
858-
655519 words of memory out of 5000000
859-
41128 multiletter control sequences out of 15000+600000
860-
712398 words of font info for 242 fonts, out of 8000000 for 9000
862+
12849 strings out of 467871
863+
203529 string characters out of 5413034
864+
655537 words of memory out of 5000000
865+
41131 multiletter control sequences out of 15000+600000
866+
712976 words of font info for 245 fonts, out of 8000000 for 9000
861867
1141 hyphenation exceptions out of 8191
862-
75i,12n,79p,1003b,725s stack positions out of 10000i,1000n,20000p,200000b,200000s
868+
75i,12n,79p,1003b,774s stack positions out of 10000i,1000n,20000p,200000b,200000s
863869
<C:/Users/trist/scoop/apps/miktex/current/texmfs/install/fonts/type1/public/l
864870
m/lmbx10.pfb><C:/Users/trist/scoop/apps/miktex/current/texmfs/install/fonts/typ
865871
e1/public/lm/lmbx12.pfb><C:/Users/trist/scoop/apps/miktex/current/texmfs/instal
@@ -883,13 +889,14 @@ c/lm/lmri10.pfb><C:/Users/trist/scoop/apps/miktex/current/texmfs/install/fonts/
883889
type1/public/lm/lmsy10.pfb><C:/Users/trist/scoop/apps/miktex/current/texmfs/ins
884890
tall/fonts/type1/public/lm/lmsy7.pfb><C:/Users/trist/scoop/apps/miktex/current/
885891
texmfs/install/fonts/type1/public/lm/lmsy8.pfb><C:/Users/trist/scoop/apps/mikte
886-
x/current/texmfs/install/fonts/type1/public/lm/lmtt10.pfb><C:/Users/trist/scoop
887-
/apps/miktex/current/texmfs/install/fonts/type1/public/amsfonts/symbols/msam10.
888-
pfb><C:/Users/trist/scoop/apps/miktex/current/texmfs/install/fonts/type1/public
889-
/amsfonts/symbols/msbm10.pfb>
890-
Output written on main.pdf (18 pages, 539706 bytes).
892+
x/current/texmfs/install/fonts/type1/public/lm/lmtk10.pfb><C:/Users/trist/scoop
893+
/apps/miktex/current/texmfs/install/fonts/type1/public/lm/lmtt10.pfb><C:/Users/
894+
trist/scoop/apps/miktex/current/texmfs/install/fonts/type1/public/amsfonts/symb
895+
ols/msam10.pfb><C:/Users/trist/scoop/apps/miktex/current/texmfs/install/fonts/t
896+
ype1/public/amsfonts/symbols/msbm10.pfb>
897+
Output written on main.pdf (18 pages, 570604 bytes).
891898
PDF statistics:
892-
570 PDF objects out of 1000 (max. 8388607)
893-
135 named destinations out of 1000 (max. 500000)
894-
44289 words of extra memory for PDF output out of 51595 (max. 10000000)
899+
580 PDF objects out of 1000 (max. 8388607)
900+
136 named destinations out of 1000 (max. 500000)
901+
44801 words of extra memory for PDF output out of 51595 (max. 10000000)
895902

paper/main.pdf

30.2 KB
Binary file not shown.

0 commit comments

Comments
 (0)