Mathematics · proofs · software

Paper IX · Lean source

RationalAudit.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/RationalAudit.lean10 lines

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

Skip source text

1 module
2 public import DyadicPacketRational
3 
4 #print axioms KomorebiPaperIX.DyadicPacketRational.packet
5 #print axioms KomorebiPaperIX.DyadicPacketRational.packet_zero
6 #print axioms KomorebiPaperIX.DyadicPacketRational.packet_sub
7 #print axioms KomorebiPaperIX.DyadicPacketRational.exact_displacement
8 #print axioms KomorebiPaperIX.DyadicPacketRational.norm_displacement
9 #print axioms KomorebiPaperIX.DyadicPacketRational.norm_sub
10 #print axioms KomorebiPaperIX.DyadicPacketRational.norm_le_one

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: 51b359010b9851123607225cf09c2cd94d230a0cfdca18bb7453cb67073c7627

Original source on GitHub

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