Paper IX · Lean source

DyadicFourSharpeningAudit.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/DyadicFourSharpeningAudit.lean19 lines

Original source path

preserved/PRSC_IX_Consolidated_Manuscript/historical/development_audit_drivers/strengthening/DyadicFourSharpeningAudit.lean

1 module
2 public import DyadicFourSharpening
3 @[expose] public section
4 set_option autoImplicit false
5 open KomorebiPaperIX
6 #print axioms KomorebiPaperIX.DyadicFourSharpening.factorial_even
7 #print axioms KomorebiPaperIX.DyadicFourSharpening.unnormalized_difference_factorial
8 #print axioms KomorebiPaperIX.DyadicFourSharpening.factorial_difference_bound
9 #print axioms KomorebiPaperIX.DyadicFourSharpening.factorial_difference_precision
10 #print axioms KomorebiPaperIX.DyadicFourSharpening.normalized_period
11 #print axioms KomorebiPaperIX.DyadicFourSharpening.half_period
12 #print axioms KomorebiPaperIX.DyadicFourSharpening.half_period_precision
13 #print axioms KomorebiPaperIX.DyadicFourSharpening.half_period_degree
14 #print axioms KomorebiPaperIX.DyadicFourSharpening.all_rows_even
15 
16 example : GlobalEulerBoundary.precision 2 (6 : ℤ)
17     (NishibuchiCompletion.generalizedEuler 4 (by decide) 3 (4 * 5 + 2 ^ 6) -
18      NishibuchiCompletion.generalizedEuler 4 (by decide) 3 (4 * 5)) :=
19   DyadicFourSharpening.half_period_degree 3 6 5 (by decide) (by decide) (by decide) (by decide)

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: 1442928e49574147042ce99b98ac5d6c3107d14e09333391571a0067cc6abdcb

Original source on GitHub

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