Mathematics · proofs · software

Paper IX · Lean source

BridgeAxiomAudit.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/BridgeAxiomAudit.lean23 lines

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

Skip source text

1 import StepAmplificationExamples
2 import AllResidueStepAmplification
3 #print axioms KomorebiPaperIX.StepAmplification.binomial_step_precision
4 #print axioms KomorebiPaperIX.StepAmplification.offset_displacement
5 #print axioms KomorebiPaperIX.StepAmplification.difference_compose
6 #print axioms KomorebiPaperIX.StepAmplification.repeated_offset
7 #print axioms KomorebiPaperIX.StepAmplification.repeated_precision
8 #print axioms KomorebiPaperIX.DyadicStepAmplification.normalized_bound
9 #print axioms KomorebiPaperIX.DyadicStepAmplification.normalized_precision
10 #print axioms KomorebiPaperIX.DyadicStepAmplification.prime_power_step_bound
11 #print axioms KomorebiPaperIX.DyadicStepAmplification.unnormalized_factorial_bound
12 #print axioms KomorebiPaperIX.DyadicStepAmplification.unnormalized_factorial_precision
13 #print axioms KomorebiPaperIX.StepAmplificationExamples.actual_second_coefficient
14 #print axioms KomorebiPaperIX.StepAmplificationExamples.actual_first_difference
15 #print axioms KomorebiPaperIX.StepAmplificationExamples.actual_first_difference_valuation
16 #print axioms KomorebiPaperIX.StepAmplificationExamples.no_uniform_extra_digit
17 #print axioms KomorebiPaperIX.AllResidueStepAmplification.unnormalized_bound
18 #print axioms KomorebiPaperIX.AllResidueStepAmplification.unnormalized_precision
19 #print axioms KomorebiPaperIX.AllResidueStepAmplification.normalized_precision
20 #print KomorebiPaperIX.DyadicStepAmplification.normalized_precision
21 #print KomorebiPaperIX.DyadicStepAmplification.unnormalized_factorial_precision
22 #print KomorebiPaperIX.AllResidueStepAmplification.unnormalized_precision
23 #print KomorebiPaperIX.AllResidueStepAmplification.normalized_precision

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: aea809f86739834d279cbc02ead1991d828d127ec7f84c08c36340693872e963

Original source on GitHub

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