Mathematics · proofs · software

Paper IX · Lean source

AxiomAudit.lean

Selected results recorded Coverage and evidence

Compiler/replay evidence is reported for a subset or bounded block. No whole-work coverage is implied.

This viewer reads the retained source; it does not run Lean or assign new claim mappings.

historical/development_audit_drivers/strengthening/AxiomAudit.lean29 lines

Original source pathpreserved/PRSC_IX_Consolidated_Manuscript/historical/development_audit_drivers/strengthening/AxiomAudit.lean

Skip source text

1 import DyadicSharpTower
2 
3 #print axioms KomorebiPaperIX.DyadicSharpTower.cothNormalized
4 #print axioms KomorebiPaperIX.DyadicSharpTower.expAt_derivative
5 #print axioms KomorebiPaperIX.DyadicSharpTower.sinh_derivative
6 #print axioms KomorebiPaperIX.DyadicSharpTower.cosh_derivative
7 #print axioms KomorebiPaperIX.DyadicSharpTower.hyperbolic_identity
8 #print axioms KomorebiPaperIX.DyadicSharpTower.coth_times_sinh
9 #print axioms KomorebiPaperIX.DyadicSharpTower.inverse_eq_coth_derivative
10 #print axioms KomorebiPaperIX.DyadicSharpTower.beta_bernoulli
11 #print axioms KomorebiPaperIX.DyadicSharpTower.kappa
12 #print axioms KomorebiPaperIX.DyadicSharpTower.kappa_bernoulli
13 #print axioms KomorebiPaperIX.DyadicSharpTower.odd_factor_valuation
14 #print axioms KomorebiPaperIX.DyadicSharpTower.bernoulli_dyadic_valuation
15 #print axioms KomorebiPaperIX.DyadicSharpTower.bernoulli_even_nonzero
16 #print axioms KomorebiPaperIX.DyadicSharpTower.kappa_valuation
17 #print axioms KomorebiPaperIX.DyadicSharpTower.kappa_nonzero
18 #print axioms KomorebiPaperIX.DyadicSharpTower.kappaPadic
19 #print axioms KomorebiPaperIX.DyadicSharpTower.kappaPadic_coe
20 #print axioms KomorebiPaperIX.DyadicSharpTower.kappaPadic_norm
21 #print axioms KomorebiPaperIX.DyadicSharpTower.kappaPadic_divisible
22 #print axioms KomorebiPaperIX.DyadicSharpTower.summand_kappa
23 #print axioms KomorebiPaperIX.DyadicSharpTower.summandPadic_kappa
24 #print axioms KomorebiPaperIX.DyadicSharpTower.dyadic_supercongruence_sharp
25 #print axioms KomorebiPaperIX.DyadicSharpTower.first_omitted_error
26 #print axioms KomorebiPaperIX.DyadicSharpTower.first_omitted_error_valuation
27 #print axioms KomorebiPaperIX.DyadicSharpTower.summand_valuation
28 #print axioms KomorebiPaperIX.DyadicSharpTower.summandPadic_divisible
29 #print axioms KomorebiPaperIX.DyadicSharpTower.dyadic_supercongruence_row_weight

Back to source controls

Original file and source record

This copy matches the recorded source file. Its publication here does not change the work’s review status.

SHA-256: 29b4710c5b5a2cbc02a1705b5599b38d7b6a910ec03af5c744867c76dad6457e

Original source on GitHub

Back to Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation