Mathematics · proofs · software

Paper IX · Lean source

DyadicControlsAudit.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/isometry/DyadicControlsAudit.lean9 lines

Original source pathpreserved/PRSC_IX_Consolidated_Manuscript/historical/development_audit_drivers/isometry/DyadicControlsAudit.lean

Skip source text

1 module
2 public import DyadicIsometryControls
3 
4 #print axioms KomorebiPaperIX.DyadicIsometryControls.address_zero_at_one
5 #print axioms KomorebiPaperIX.DyadicIsometryControls.address_zero_at_two
6 #print axioms KomorebiPaperIX.DyadicIsometryControls.address_zero_not_additive
7 #print axioms KomorebiPaperIX.DyadicIsometryControls.address_zero_inverse_at_thirty_four
8 #print axioms KomorebiPaperIX.DyadicIsometryControls.original_address_zero_ne_zero
9 #print axioms KomorebiPaperIX.DyadicIsometryControls.original_address_zero_not_surjective

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

Original source on GitHub

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