Latest result
Requested half-root error
AP095 proves the finite error at most 2⁻ⁿ for the unchanged n+8 sample program.
Read AP095 →Definitions first
Conservative notation
Exact expanded definitions and their prerequisite/use links. No new kernel axioms.
Browse definitions →Bigger picture
Irrationality remains open
245 distinct supporting statements, not 245 closed campaign goals. Transcendence follows irrationality.
Open the campaign DAG →All checked supporting results
246 HA/Lean observations represent 245 distinct statements; the E and Vampire P08 demonstrations share one target. The original 33-statement release remains available unchanged.
| Case | Statement | Local proof nodes | Evidence |
|---|---|---|---|
| AP001 | log root argument | 161 | HA + Lean |
| AP002 | exp sample | 186 | HA + Lean |
| AP003 | log root independence | 156 | HA + Lean |
| AP004 | supplied exp sample | 152 | HA + Lean |
| AP005 | exp sample independence | 228 | HA + Lean |
| AP006 | argument modulus | 188 | HA + Lean |
| AP007 | exp two sided continuity | 164 | HA + Lean |
| AP008 | exp two sided horizons | 197 | HA + Lean |
| AP009 | exp sample modulus | 273 | HA + Lean |
| AP010 | positive power comparison | 126 | HA + Lean |
| AP011 | approximation power bounds | 128 | HA + Lean |
| AP012 | exp sample uniform error | 282 | HA + Lean |
| AP013 | exp sample all precision | 297 | HA + Lean |
| AP014 | fixed precision threshold | 130 | HA + Lean |
| AP015 | exp sample dyadic error | 303 | HA + Lean |
| AP016 | atanh odd slice | 113 | HA + Lean |
| AP017 | paired horner | 40 | HA + Lean |
| AP018 | paired power | 27 | HA + Lean |
| AP019 | odd horner quotient | 142 | HA + Lean |
| AP020 | finite odd log series | 169 | HA + Lean |
| AP021 | finite exp series | 160 | HA + Lean |
| AP022 | factorial atanh prefix | 124 | HA + Lean |
| AP023 | factorial exp sample | 190 | HA + Lean |
| AP024 | atomic computation decisions | 153 | HA + Lean |
| AP025 | approximation component decisions | 146 | HA + Lean |
| AP026 | finite table decisions | 133 | HA + Lean |
| AP027 | prescribed sample decision | 174 | HA + Lean |
| AP028 | approximation record exists | 206 | HA + Lean |
| AP029 | approximation record decision | 178 | HA + Lean |
| AP030 | approximation record independence | 229 | HA + Lean |
| AP031 | approximation record error | 305 | HA + Lean |
| AP032 | log exp witness | 439 | HA + Lean |
| AP033 | log exp budget | 46 | HA + Lean |
| AP034 | log exp dyadic witness | 452 | HA + Lean |
| AP035 | exp recurrence normalization | 36 | HA + Lean |
| AP036 | exp recurrence series | 130 | HA + Lean |
| AP037 | convolution shift | 131 | HA + Lean |
| AP038 | exp convolution recurrence | 147 | HA + Lean |
| AP039 | exp convolution prefix | 163 | HA + Lean |
| AP040 | convolution prefix order | 46 | HA + Lean |
| AP041 | convolution sum sandwich | 191 | HA + Lean |
| AP042 | exp product error | 243 | HA + Lean |
| AP043 | exp supplied product | 278 | HA + Lean |
| AP044 | exp half square | 303 | HA + Lean |
| AP045 | half square error transfer | 28 | HA + Lean |
| AP046 | half log precision | 37 | HA + Lean |
| AP047 | half log square | 535 | HA + Lean |
| AP048 | square error linear | 31 | HA + Lean |
| AP049 | half log root comparison | 38 | HA + Lean |
| AP050 | half log root witness | 560 | HA + Lean |
| AP051 | exp large argument ratio | 23 | HA + Lean |
| AP052 | exp large argument tail | 123 | HA + Lean |
| AP053 | halving prefix decay | 36 | HA + Lean |
| AP054 | exp large argument decay | 138 | HA + Lean |
| AP055 | exp large argument truncation | 157 | HA + Lean |
| AP056 | exp geometric majorant | 44 | HA + Lean |
| AP057 | exp normalized truncation | 160 | HA + Lean |
| AP058 | exp normalized witness | 184 | HA + Lean |
| AP059 | exp large argument product | 248 | HA + Lean |
| AP060 | exp recurrence independence | 37 | HA + Lean |
| AP061 | exp supplied large product | 255 | HA + Lean |
| AP062 | exp binary budget | 129 | HA + Lean |
| AP063 | exp requested truncation | 171 | HA + Lean |
| AP064 | exp requested product | 266 | HA + Lean |
| AP065 | exp independent horizon | 179 | HA + Lean |
| AP066 | exp uniform witness | 202 | HA + Lean |
| AP067 | exp product witness | 289 | HA + Lean |
| AP068 | exp relative continuity | 137 | HA + Lean |
| AP069 | exp relative cross continuity | 144 | HA + Lean |
| AP070 | exp absolute continuity | 146 | HA + Lean |
| AP071 | exp submultiplicative | 216 | HA + Lean |
| AP072 | exp integer majorant | 267 | HA + Lean |
| AP073 | exp bounded majorant | 281 | HA + Lean |
| AP074 | exp bounded continuity | 288 | HA + Lean |
| AP075 | exp dyadic continuity | 299 | HA + Lean |
| AP076 | ordered power difference | 36 | HA + Lean |
| AP077 | symmetric power difference | 41 | HA + Lean |
| AP078 | product power | 121 | HA + Lean |
| AP079 | rational power difference | 136 | HA + Lean |
| AP080 | requested power precision | 138 | HA + Lean |
| AP081 | exp joint error | 323 | HA + Lean |
| AP082 | log exp refinement | 229 | HA + Lean |
| AP083 | log exp cutoff refinement | 238 | HA + Lean |
| AP084 | log exp uniform two | 511 | HA + Lean |
| AP085 | fixed log exp convergence | 513 | HA + Lean |
| AP086 | fixed log exp witness | 522 | HA + Lean |
| AP087 | half log exp refinement | 231 | HA + Lean |
| AP088 | half log exp cutoff | 240 | HA + Lean |
| AP089 | half log root uniform | 583 | HA + Lean |
| AP090 | fixed half log root | 585 | HA + Lean |
| AP091 | fixed half log root witness | 586 | HA + Lean |
| AP092 | fixed half log fine root | 595 | HA + Lean |
| AP093 | log root half argument | 69 | HA + Lean |
| AP094 | exp log root half transport | 214 | HA + Lean |
| AP095 | requested half transport | 231 | HA + Lean |
| CV001 | convolution vanishing | 28 | HA + Lean |
| CV002 | logexp recurrence | 31 | HA + Lean |
| CV003 | natural convolution | 126 | HA + Lean |
| CV004 | series power trace | 121 | HA + Lean |
| CV005 | series power vanishing | 131 | HA + Lean |
| CV006 | sum linearity | 109 | HA + Lean |
| CV007 | euler product | 123 | HA + Lean |
| CV008 | natural fubini | 126 | HA + Lean |
| CV009 | sum splitting | 120 | HA + Lean |
| CV010 | convolution commutative | 133 | HA + Lean |
| CV011 | sum zero tail | 123 | HA + Lean |
| CV012 | triple grid | 110 | HA + Lean |
| CV013 | triple row sum | 139 | HA + Lean |
| CV014 | convolution associative | 168 | HA + Lean |
| CV015 | convolution linearity | 123 | HA + Lean |
| CV016 | convolution unit | 142 | HA + Lean |
| CV017 | series power euler | 193 | HA + Lean |
| CV018 | series linear combination | 125 | HA + Lean |
| CV019 | weighted series trace | 110 | HA + Lean |
| CV020 | shifted euler prefix | 107 | HA + Lean |
| CV021 | finite composition euler | 208 | HA + Lean |
| CV022 | exponential weights | 108 | HA + Lean |
| CV023 | weighted series scaling | 116 | HA + Lean |
| CV024 | denominator euler | 224 | HA + Lean |
| CV025 | atanh coefficients | 108 | HA + Lean |
| CV026 | atanh euler | 111 | HA + Lean |
| CV027 | periodic convolution | 137 | HA + Lean |
| CV028 | composition recurrence | 245 | HA + Lean |
| CV029 | composition coefficients | 252 | HA + Lean |
| CV030 | weight factorials | 130 | HA + Lean |
| CV031 | normalized composition | 272 | HA + Lean |
| CV032 | horner trace | 107 | HA + Lean |
| CV033 | geometric horner | 126 | HA + Lean |
| CV034 | composition evaluation | 284 | HA + Lean |
| CV035 | horner linearity | 111 | HA + Lean |
| CV036 | horner zero tail | 122 | HA + Lean |
| CV037 | horner weighted sum | 115 | HA + Lean |
| CV038 | geometric weights | 123 | HA + Lean |
| CV039 | constructed horner sum | 137 | HA + Lean |
| CV040 | horner monomials | 142 | HA + Lean |
| CV041 | convolution weights | 135 | HA + Lean |
| CV042 | weighted convolution | 148 | HA + Lean |
| CV043 | shifted scaled sum | 125 | HA + Lean |
| CV044 | cauchy grid | 110 | HA + Lean |
| CV045 | cauchy row sum | 136 | HA + Lean |
| CV046 | cauchy column sum | 133 | HA + Lean |
| CV047 | cauchy grid sums | 149 | HA + Lean |
| CV048 | convolution total | 162 | HA + Lean |
| CV049 | horner product | 218 | HA + Lean |
| CV050 | convolution locality | 117 | HA + Lean |
| CV051 | power width transport | 141 | HA + Lean |
| CV052 | composition width transport | 151 | HA + Lean |
| CV053 | convolution upper support | 127 | HA + Lean |
| CV054 | power upper support | 141 | HA + Lean |
| CV055 | horner prefix transport | 109 | HA + Lean |
| CV056 | supported horner product | 229 | HA + Lean |
| CV057 | supported horner values | 233 | HA + Lean |
| CV058 | finite power evaluation | 253 | HA + Lean |
| CV059 | row horner values | 115 | HA + Lean |
| CV060 | weighted accumulation evaluation | 137 | HA + Lean |
| CV061 | full composition evaluation | 276 | HA + Lean |
| CV062 | horner splitting | 124 | HA + Lean |
| CV063 | horner base comparison | 125 | HA + Lean |
| CV064 | horner tail majorant | 132 | HA + Lean |
| CV065 | bounded horner | 125 | HA + Lean |
| CV066 | atanh majorant | 136 | HA + Lean |
| CV067 | factorial majorant | 125 | HA + Lean |
| CV068 | ratio sum bound | 112 | HA + Lean |
| CV069 | power weighted prefix | 121 | HA + Lean |
| CV070 | scaled exp terms | 144 | HA + Lean |
| CV071 | scaled exp bound | 163 | HA + Lean |
| CV072 | monomial recurrence | 119 | HA + Lean |
| CV073 | weighted monomial recurrence | 122 | HA + Lean |
| CV074 | composition majorant | 325 | HA + Lean |
| CV075 | rational tail majorant | 144 | HA + Lean |
| CV076 | composition tail bound | 336 | HA + Lean |
| CV077 | supplied composition bound | 317 | HA + Lean |
| CV078 | consumed row transport | 30 | HA + Lean |
| CV079 | successor composition transport | 55 | HA + Lean |
| CV080 | same table composition | 426 | HA + Lean |
| CV081 | supplied composition evaluation | 263 | HA + Lean |
| CV082 | supplied horner splitting | 38 | HA + Lean |
| CV083 | geometric tail sandwich | 14 | HA + Lean |
| CV084 | supplied geometric error | 134 | HA + Lean |
| CV085 | constructed composition error | 435 | HA + Lean |
| CV086 | ternary atanh bound | 46 | HA + Lean |
| CV087 | scaled exp tail | 121 | HA + Lean |
| CV088 | scaled exp tail decay | 136 | HA + Lean |
| CV089 | ternary prefix bound | 40 | HA + Lean |
| CV090 | atanh truncation | 142 | HA + Lean |
| CV091 | atanh rational truncation | 146 | HA + Lean |
| CV092 | atanh scale independence | 37 | HA + Lean |
| CV093 | independent atanh truncation | 155 | HA + Lean |
| CV094 | exp term difference | 40 | HA + Lean |
| CV095 | sum linear bound | 26 | HA + Lean |
| CV096 | exp sum continuity | 147 | HA + Lean |
| CV097 | exp rescaling | 114 | HA + Lean |
| CV098 | exp cross continuity | 156 | HA + Lean |
| CV099 | exp rational continuity | 159 | HA + Lean |
| CV100 | exp truncation | 155 | HA + Lean |
| CV101 | exp two error bound | 189 | HA + Lean |
| CV102 | exp rational two error | 193 | HA + Lean |
| IR016 | ir016 | 182 | HA + Lean |
| NG001 | natural gap | 3 | HA + Lean |
| P04-C00 | p04 c00 | 5 | HA + Lean |
| P04-C01 | p04 c01 | 4 | HA + Lean |
| P04-C02 | p04 c02 | 18 | HA + Lean |
| P04-C03 | p04 c03 | 50 | HA + Lean |
| P04-C04 | p04 c04 | 402 | HA + Lean |
| P04-C05 | p04 c05 | 456 | HA + Lean |
| P04-C06 | p04 c06 | 733 | HA + Lean |
| P04-C07 | p04 c07 | 536 | HA + Lean |
| P04-C08 | p04 c08 | 942 | HA + Lean |
| P04-C09 | p04 c09 | 427 | HA + Lean |
| P04-C10 | p04 c10 | 452 | HA + Lean |
| P04-C11 | p04 c11 | 1477 | HA + Lean |
| P04-C12 | p04 c12 | 39 | HA + Lean |
| P04-soundness | p04 soundness | 1 | HA + Lean |
| P08-eprover | p08 e | 1 | HA + Lean |
| P08-vampire | p08 v | 1 | HA + Lean |
| P10 | p10 | 1486 | HA + Lean |
| QF001 | quadratic product trace | 224 | HA + Lean |
| QF002 | quadratic trace exists | 108 | HA + Lean |
| QF003 | quadratic product exists | 272 | HA + Lean |
| QF004 | canonical quadratic trace | 108 | HA + Lean |
| QF005 | bounded quadratic product | 297 | HA + Lean |
| QH001 | quadratic height | 13 | HA + Lean |
| QH002 | quadratic trace height | 41 | HA + Lean |
| QN001 | quadratic nonzero | 221 | HA + Lean |
| RF001 | rf001 | 1 | HA + Lean |
| RF002 | rf002 | 1 | HA + Lean |
| RF003 | rf003 typed | 1 | HA + Lean |
| RF004 | rf004 | 1 | HA + Lean |
| RF005 | rf005 | 1 | HA + Lean |
| RF006 | rf006 | 1 | HA + Lean |
| RN001 | rational norm transport | 29 | HA + Lean |
| RN002 | rational norm product | 46 | HA + Lean |
| SI001 | signed product nonzero | 34 | HA + Lean |
| SN001 | signed norm | 206 | HA + Lean |
| SN002 | norm separation | 210 | HA + Lean |
| SN003 | norm product | 37 | HA + Lean |
| SQ001 | floor sqrt | 31 | HA + Lean |
| SQ002 | floor sqrt comparison | 16 | HA + Lean |
| SQ003 | scaled sqrt2 | 42 | HA + Lean |
| SQ004 | dyadic sqrt2 | 139 | HA + Lean |
| SQ005 | floor sqrt scaling | 24 | HA + Lean |
| SQ006 | dyadic sqrt2 refinement | 131 | HA + Lean |
| SQ007 | dyadic sqrt2 intervals | 134 | HA + Lean |
| SQ008 | dyadic sqrt2 modulus | 136 | HA + Lean |
| SQ009 | dyadic sqrt2 square error | 53 | HA + Lean |
| SQ010 | dyadic sqrt2 reciprocal | 149 | HA + Lean |
Reproducibility and honest status
Full structured inventory · Pinned source evidence index · Delivery hashes · Historical 33-statement checkpoint.
HA and Lean receipts are observations, not checked-use admission tokens. Kernel bodies remain the proof authority. Agent engineering costs are not represented as zero, and external solver hits are not asserted to be translated proofs.