Mathematics · proofs · software

Paper IX · Lean source

PadicTowerLimitAudit.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.

polynomial_towers/development/limit/PadicTowerLimitAudit.lean33 lines

Original source pathpreserved/PRSC_IX_Consolidated_Manuscript/polynomial_towers/development/limit/PadicTowerLimitAudit.lean

Skip source text

1 module
2 public import PadicTowerLimit
3 
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 open Filter Topology
8 
9 example (p L : ℕ) [Fact p.Prime] (z : ℕ → ℤ)
10     (hstep : ∀ n, (p : ℤ) ^ (L + n) ∣ z (n + 1) - z n) :
11     ∃ a : ℤ_[p],
12       Tendsto (fun n => (z n : ℤ_[p])) atTop (𝓝 a) ∧
13       ∀ n, (p : ℤ_[p]) ^ (L + n) ∣ a - (z n : ℤ_[p]) :=
14   Komorebi.PadicTowerLimit.compatible_int_tower_limit p L z hstep
15 
16 example {ι : Type*} (p L : ℕ) [Fact p.Prime] (z : ℕ → ι → ℤ)
17     (hstep : ∀ n i, (p : ℤ) ^ (L + n) ∣ z (n + 1) i - z n i) :
18     ∃ a : ι → ℤ_[p],
19       Tendsto (fun n i => (z n i : ℤ_[p])) atTop (𝓝 a) ∧
20       ∀ n i, (p : ℤ_[p]) ^ (L + n) ∣ a i - (z n i : ℤ_[p]) :=
21   Komorebi.PadicTowerLimit.compatible_vector_tower_limit p L z hstep
22 
23 example (p L : ℕ) [Fact p.Prime] (z : ℕ → ℤ)
24     (hz : ∀ n, (p : ℤ) ^ (L + n) ∣ z n) :
25     Tendsto (fun n => (z n : ℤ_[p])) atTop (𝓝 0) :=
26   Komorebi.PadicTowerLimit.divisible_int_tendsto_zero p L z hz
27 
28 #print axioms Komorebi.PadicTowerLimit.tower_pair_dvd
29 #print axioms Komorebi.PadicTowerLimit.compatible_int_tower_cauchy
30 #print axioms Komorebi.PadicTowerLimit.compatible_int_tower_limit
31 #print axioms Komorebi.PadicTowerLimit.compatible_vector_tower_limit
32 #print axioms Komorebi.PadicTowerLimit.divisible_int_tendsto_zero
33 #print axioms Komorebi.PadicTowerLimit.compatible_int_tower_unique_limit

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: 1a0a43524c2bc67335339de596dd91f8e652fe1510c02adbaddf2eefa33a1305

Original source on GitHub

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