Mathematics · proofs · software

Paper IX · Lean source

DensePadicIsometryAudit.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/DensePadicIsometryAudit.lean25 lines

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

Skip source text

1 module
2 public import DensePadicIsometry
3 
4 @[expose] public section
5 
6 #print axioms KomorebiPaperIX.DensePadicIsometry.onNaturalRange
7 #print axioms KomorebiPaperIX.DensePadicIsometry.onNaturalRange_nat
8 #print axioms KomorebiPaperIX.DensePadicIsometry.onNaturalRange_isometry
9 #print axioms KomorebiPaperIX.DensePadicIsometry.extension
10 #print axioms KomorebiPaperIX.DensePadicIsometry.extension_continuous
11 #print axioms KomorebiPaperIX.DensePadicIsometry.extension_nat
12 #print axioms KomorebiPaperIX.DensePadicIsometry.extension_isometry
13 #print axioms KomorebiPaperIX.DensePadicIsometry.extension_unique
14 #print axioms KomorebiPaperIX.DensePadicIsometry.extension_surjective
15 #print axioms KomorebiPaperIX.DensePadicIsometry.extensionEquiv
16 #print axioms KomorebiPaperIX.DensePadicIsometry.extensionEquiv_apply
17 #print axioms KomorebiPaperIX.DensePadicIsometry.extensionEquiv_nat
18 #print axioms KomorebiPaperIX.DensePadicIsometry.extensionEquiv_unique_continuous
19 #print axioms KomorebiPaperIX.DensePadicIsometry.extensionEquiv_unique
20 #print axioms KomorebiPaperIX.DensePadicIsometry.existsUnique_extensionEquiv
21 
22 example (p : ℕ) [Fact p.Prime] (f : ℕ → ℤ_[p])
23     (hdist : ∀ m n : ℕ, dist (f m) (f n) = dist (m : ℤ_[p]) (n : ℤ_[p])) :
24     ∃! e : ℤ_[p] ≃ᵢ ℤ_[p], ∀ n : ℕ, e (n : ℤ_[p]) = f n :=
25   KomorebiPaperIX.DensePadicIsometry.existsUnique_extensionEquiv p f hdist

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

Original source on GitHub

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