Paper IX · Lean source
PadicTowerLimitContract.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/contracts/PadicTowerLimitContract.lean20 lines
Original source path
preserved/PRSC_IX_Consolidated_Manuscript/polynomial_towers/contracts/PadicTowerLimitContract.leanSkip declarations and read code
1 module
2 public import PadicTowerLimit
3
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 open Filter Topology
8 namespace Komorebi.PadicTowerLimitContract
9
10 /-- Compatibility alone supplies the actual p-adic limit; convergence and the
11 retention of all residues are conclusions. -/
12 theorem explicit_vector_limit {ι : Type*} (p L : ℕ) [Fact (Nat.Prime p)]
13 (z : ℕ → ι → ℤ)
14 (hstep : ∀ n i, (p : ℤ)^(L+n) ∣ z (n+1) i - z n i) :
15 ∃ a : ι → ℤ_[p],
16 Tendsto (fun n i => (z n i : ℤ_[p])) atTop (𝓝 a) ∧
17 ∀ n i, (p : ℤ_[p])^(L+n) ∣ a i - (z n i : ℤ_[p]) := by
18 exact PadicTowerLimit.compatible_vector_tower_limit p L z hstep
19
20 end Komorebi.PadicTowerLimitContract
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: 6d81199904dec30c4e6d0ce263e7a69ae9a2bae7ffa70b4ab86ef5a6ad5a5c1e
Back to Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation