Mathematics · proofs · software

Paper IX · Lean source

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

review/fresh_baseline/ExternalStatement.lean19 lines

Original source pathpreserved/PRSC_IX_Consolidated_Manuscript/review/fresh_baseline/ExternalStatement.lean

Skip source text

1 module
2 public import ConjectureExamples
3 open KomorebiPaperIX
4 open NishibuchiCompletion GlobalEulerBoundary
5 set_option autoImplicit false
6 example (p m j : ℕ) [Fact p.Prime]
7     (hmpos:0<m) (hj:j<m*p) (h:m∣p-1 ∨ m=2) :
8     (∀ n, ((generalizedEuler (m*p) (Nat.mul_ne_zero hmpos.ne' (Fact.out:p.Prime).ne_zero)
9       j (m*p*n):ℚ):ℚ_[p]) ∈ PadicInt.subring p) ∧
10     ∀ r:ℕ, 0<r → ∃ n0:ℕ, 0<n0 ∧ n0≤r ∧ ∀ n:ℕ, n0≤n →
11       precision p (r:ℤ)
12         (generalizedEuler (m*p) (Nat.mul_ne_zero hmpos.ne' (Fact.out:p.Prime).ne_zero) j
13           (m*p*n+Nat.lcm 2 (p-1)*p^r)-
14          generalizedEuler (m*p) (Nat.mul_ne_zero hmpos.ne' (Fact.out:p.Prime).ne_zero) j (m*p*n)) :=
15   conjecture_3_9 p m j hmpos hj h
16 #print KomorebiPaperIX.NishibuchiCompletion.conjecture_3_9
17 #print KomorebiPaperIX.DyadicFourCongruences.normalized_bound
18 #print axioms KomorebiPaperIX.NishibuchiCompletion.conjecture_3_9
19 #print axioms KomorebiPaperIX.DyadicFourCongruences.normalized_bound

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: 899a2824c4013ba1c96740f73f719e3497c396b93563dcf91bdb6c03bbcb60e0

Original source on GitHub

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