Epi.lean — FrcLedger

1import Mathlib23/-!4# 13-epi — the classical constants on the shell: the ledger predicates in Lean (2026-09-18)56Rows of the predicate ledger of *Finite Field Realisation of the Classical Constants π and e* (tree7`13-epi-20260713`).  The wall of `e`: Wilson reflection, the wall identity `!(p−1) ≡ !p`, the terminal residue8`−(!p)⁻¹`, antiperiodicity `!(n+p) ≡ −!n`, the series duals, the fixed-shell tower exact at every grade9(F1–F4, F7); the wall hierarchy of `π`: the legibility window, the half-wall terminus `−2`, the quarter-wall10two-squares invariant given Gauss's congruence, Lucas on the tower `C(2p^r, p^r) ≡ 2`, the first revival `8`,11the tower of `π` exact (G1–G3, G5, G9); the Cayley quarter-turn map and its composition law (C3); the Wallis12pair: strict monotonicity, the width identity and the enclosure `v_n < π < w_n` (E2, with Mathlib's Wallis13product); the impossibility of exact calibration of `e` from the irrationality of `π` (H3); the index condition14of the null experiment (H5); the wall of `π` at second order: the π-Wieferich condition of G4 in its three15forms with the exact identity `q_p(4) = 2q_p(2) + p·q_p(2)²`, Eisenstein's congruence `2q_p(2) ≡ −H_{(p−1)/2}`,16the identification with OEIS A355959 (G10), and G4's second-order clause from Morley's congruence; the Machin chain:17the alternating bound and pairing of the arctangent series, the error `17/((2N+3)5^{2N+3})`, the binary64 readout at18`N = 10`, the hundred digits at `N = 71`, the rational bracket of `π` at `m = 12` read by the core (E3, E4), the Gregory19brackets and the rounding chain (E5).  Classical (tier 2) on Mathlib's hierarchy; the finite content — the derangement20recurrence, antiperiodicity, the tower, orientation transport, the wrap-free window and the value rows on21`𝔽₁₃` and the six wall shells — is proved with no axioms in `FrcCore/Epi.lean`.2223The ring arithmetic of the wall is proved once over an arbitrary field `K` with `p = 0`, `(p−1)! = −1` and24`k! ≠ 0` (`k ≤ p−1`); the sections `prime` and `primepi` instantiate `K := ZMod p`.25-/2627namespace FRC.Epi2829open Finset Nat30/-! ## The Wallis pair (13:E1, E2) -/31section wallis3233variable {K : Type*} [Field K]3435/-- 13:E1 — the Wallis pair on the framed rationals: `v n = 2·16^n/((2n+1)·C(2n,n)²)` (the doubled Wallis36partial product) and `w n = 16^n/(n·C(2n,n)²)` (the joint-return tally). -/37noncomputable def wallisV (n : ℕ) : K := 2 * (16 : K) ^ n / ((2 * (n : K) + 1) * ((centralBinom n : ℕ) : K) ^ 2)3839/-- The Wallis chain on a field: `w n = 16^n / (n · C(2n,n)²)`. -/40noncomputable def wallisW (n : ℕ) : K := (16 : K) ^ n / ((n : K) * ((centralBinom n : ℕ) : K) ^ 2)4142end wallis4344section rencontres45open Equiv4647variable {α : Type*} [Fintype α] [DecidableEq α]4849/-- The fixed-point set of a permutation, as a finset. -/50def fixSet (σ : Perm α) : Finset α := univ.filter (fun a => σ a = a)5152/-- The permutations fixing `F` pointwise number `(card α − |F|)!`: they are the permutations of the complement. -/53theorem card_fixing (F : Finset α) :54    (univ.filter (fun σ : Perm α => ∀ a ∈ F, σ a = a)).card = (Fintype.card α - F.card).factorial := by55  have e : {f : Perm α // ∀ a, ¬ (a ∉ F) → f a = a} ≃ Perm {a // a ∉ F} :=56    (Perm.subtypeEquivSubtypePerm (fun a => a ∉ F)).symm57  rw [← Fintype.card_subtype]58  have h : Fintype.card {σ : Perm α // ∀ a ∈ F, σ a = a} = Fintype.card {f : Perm α // ∀ a, ¬ (a ∉ F) → f a = a} := by59    apply Fintype.card_congr60    exact Equiv.subtypeEquivRight (fun σ => by simp)61  rw [h, Fintype.card_congr e, Fintype.card_perm, Fintype.card_subtype_compl, Fintype.card_coe]6263/-- `x^|Fix σ| = Σ_{F ⊆ Fix σ} (x − 1)^|F|`: the binomial expansion of `((x − 1) + 1)^|Fix σ|`. -/64theorem pow_card_fixSet {R : Type*} [CommRing R] (x : R) (σ : Perm α) :65    x ^ (fixSet σ).card = ∑ F ∈ (fixSet σ).powerset, (x - 1) ^ F.card := by66  have := sum_pow_mul_eq_add_pow (x - 1) 1 (fixSet σ)67  simp only [one_pow, mul_one, sub_add_cancel] at this68  exact this.symm6970/-- 13:C2 — the rencontres identity (the derangement selector, Prop. selector-e): `Σ_{σ ∈ S_n} x^{fix σ} = Σ_{k ≤ n} C(n,k)(n−k)! (x − 1)^k`, `n = card α`, over any71commutative ring, by double counting the pairs `(σ, F)` with `F` a set of fixed points of `σ`. -/72theorem rencontres {R : Type*} [CommRing R] (x : R) :73    ∑ σ : Perm α, x ^ (fixSet σ).card74      = ∑ k ∈ range (Fintype.card α + 1),75          (((Fintype.card α).choose k * (Fintype.card α - k).factorial : ℕ) : R) * (x - 1) ^ k := by76  simp_rw [pow_card_fixSet]77  rw [sum_comm' (t' := (univ : Finset α).powerset)78      (s' := fun F => univ.filter (fun σ : Perm α => ∀ a ∈ F, σ a = a))]79  · simp_rw [sum_const, nsmul_eq_mul, card_fixing]80    rw [sum_powerset_apply_card (fun m => ((Fintype.card α - m).factorial : R) * (x - 1) ^ m)]81    rw [Finset.card_univ]82    refine sum_congr rfl fun k _ => ?_83    rw [nsmul_eq_mul, Nat.cast_mul]; ring84  · intro σ F85    simp only [mem_univ, true_and, mem_powerset, mem_filter, fixSet, subset_iff]86    exact ⟨fun h => ⟨h, fun _ _ => trivial⟩, fun h => h.1⟩8788/-- 13:C2 — the ledger's form of the rencontres identity, `P_n(x) = n! Σ_{k ≤ n} (x−1)^k/k!`: the coefficient `C(n,k)(n−k)!` is `n!/k!`. -/89theorem rencontres_rat (x : ℚ) :90    ∑ σ : Perm α, x ^ (fixSet σ).card91      = (Fintype.card α).factorial * ∑ k ∈ range (Fintype.card α + 1), (x - 1) ^ k / k.factorial := by92  rw [rencontres, mul_sum]93  refine sum_congr rfl fun k hk => ?_94  have hk' : k ≤ Fintype.card α := Nat.lt_succ_iff.mp (mem_range.mp hk)95  have h := Nat.choose_mul_factorial_mul_factorial hk'96  have hkf : (k.factorial : ℚ) ≠ 0 := by positivity97  have h' : ((Fintype.card α).factorial : ℚ) = (((Fintype.card α).choose k * (Fintype.card α - k).factorial : ℕ) : ℚ) * k.factorial := by98    rw [← Nat.cast_mul, ← h]; push_cast; ring99  rw [h']; field_simp100101/-- 13:C2 — `P_n(1) = n!`: the normalised kernel `Z_n = P_n/n!` takes the value one at `x = 1`. -/102theorem rencontres_one : ∑ σ : Perm α, (1 : ℚ) ^ (fixSet σ).card = (Fintype.card α).factorial := by103  simp [Fintype.card_perm]104105/-- 13:C2 — `P_n(0) = !n`: the value at `x = 0` is the number of derangements, so `Z_n(0) = !n/n!` and the unit registration ratio `Z_n(1)/Z_n(0)` is `n!/!n`. -/106theorem rencontres_zero : ∑ σ : Perm α, (0 : ℚ) ^ (fixSet σ).card = numDerangements (Fintype.card α) := by107  rw [← card_derangements_eq_numDerangements α]108  have : ∀ σ : Perm α, (0 : ℚ) ^ (fixSet σ).card = if σ ∈ derangements α then 1 else 0 := by109    intro σ110    by_cases h : σ ∈ derangements α111    · have : fixSet σ = ∅ := by112        rw [fixSet, filter_eq_empty_iff]; intro a _; exact h a113      simp [this, h]114    · have : (fixSet σ).card ≠ 0 := by115        rw [Ne, Finset.card_eq_zero, fixSet, filter_eq_empty_iff]116        intro hall; exact h (fun a => hall (mem_univ a))117      simp [h, zero_pow this]118  simp_rw [this]119  rw [sum_boole, Fintype.card_subtype]120121end rencontres122123section tailAndReadout124open Filter Topology125126/-- The partial sums `expNegOneSum m = Σ_{i<m} (−1)^i/i!` of the alternating series of `e⁻¹`. -/127noncomputable def expNegOneSum (m : ℕ) : ℝ := ∑ i ∈ range m, (-1 : ℝ) ^ i * (1 / (i.factorial : ℝ))128129theorem expNegOneSum_succ (m : ℕ) : expNegOneSum (m + 1) = expNegOneSum m + (-1 : ℝ) ^ m * (1 / (m.factorial : ℝ)) := by130  simp [expNegOneSum, sum_range_succ]131132/-- The alternating series sums to `e⁻¹`. -/133theorem hasSum_expNegOneSum : HasSum (fun i : ℕ => (-1 : ℝ) ^ i * (1 / (i.factorial : ℝ))) (Real.exp (-1)) := by134  have h := NormedSpace.expSeries_div_hasSum_exp (-1 : ℝ)135  rw [← Real.exp_eq_exp_ℝ] at h136  convert h using 1137  ext i; ring138139theorem tendsto_expNegOneSum : Tendsto expNegOneSum atTop (𝓝 (Real.exp (-1))) := hasSum_expNegOneSum.tendsto_sum_nat140141theorem antitone_inv_factorial : Antitone (fun i : ℕ => (1 / (i.factorial : ℝ))) := by142  intro i j hij143  have : (i.factorial : ℝ) ≤ j.factorial := by exact_mod_cast Nat.factorial_le hij144  exact one_div_le_one_div_of_le (by positivity) this145146theorem expNegOneSum_even_le (k : ℕ) : expNegOneSum (2 * k) ≤ Real.exp (-1) :=147  Antitone.alternating_series_le_tendsto tendsto_expNegOneSum antitone_inv_factorial k148149theorem le_expNegOneSum_odd (k : ℕ) : Real.exp (-1) ≤ expNegOneSum (2 * k + 1) :=150  Antitone.tendsto_le_alternating_series tendsto_expNegOneSum antitone_inv_factorial k151152/-- `!n = n! · expNegOneSum(n+1)`: the inclusion–exclusion sum of the derangement number. -/153theorem numDerangements_eq_sum (n : ℕ) : (numDerangements n : ℝ) = n.factorial * expNegOneSum (n + 1) := by154  have h := numDerangements_sum n155  have h' : (numDerangements n : ℝ) = ∑ k ∈ range (n + 1), (-1 : ℝ) ^ k * ((k + 1).ascFactorial (n - k) : ℝ) := by156    exact_mod_cast h157  rw [h', expNegOneSum, mul_sum]158  refine sum_congr rfl fun k hk => ?_159  have hk' : k ≤ n := Nat.lt_succ_iff.mp (mem_range.mp hk)160  have hf : (k.factorial : ℝ) * ((k + 1).ascFactorial (n - k) : ℝ) = n.factorial := by161    rw [← Nat.cast_mul, Nat.factorial_mul_ascFactorial, Nat.add_sub_cancel' hk']162  have hkf : (k.factorial : ℝ) ≠ 0 := by positivity163  field_simp164  linear_combination hf165166/-- `δ_n = (−1)^n (!n − n!/e)`, the signed tail. -/167noncomputable def tailDelta (n : ℕ) : ℝ := (-1 : ℝ) ^ n * (numDerangements n - n.factorial * Real.exp (-1))168169/-- `δ_n = (−1)^{n+1} n! (e⁻¹ − expNegOneSum(n+1))`. -/170theorem tailDelta_eq (n : ℕ) : tailDelta n = (-1 : ℝ) ^ (n + 1) * n.factorial * (Real.exp (-1) - expNegOneSum (n + 1)) := by171  rw [tailDelta, numDerangements_eq_sum, pow_succ]; ring172173/-- 13:D2 — the closed tail bounds `1/(n+2) ≤ δ_n ≤ 1/(n+1)`, from the alternating series of `e⁻¹`. -/174theorem tailDelta_bounds (n : ℕ) : 1 / ((n : ℝ) + 2) ≤ tailDelta n ∧ tailDelta n ≤ 1 / ((n : ℝ) + 1) := by175  rw [tailDelta_eq]176  have hf : (0 : ℝ) < n.factorial := by positivity177  have h1 : ((n + 1).factorial : ℝ) = (n + 1) * n.factorial := by push_cast [Nat.factorial_succ]; ring178  have h2 : ((n + 2).factorial : ℝ) = (n + 2) * (n + 1) * n.factorial := by179    rw [show n + 2 = (n + 1) + 1 from rfl, Nat.factorial_succ, Nat.factorial_succ]; push_cast; ring180  rcases Nat.even_or_odd n with ⟨k, hk⟩ | ⟨k, hk⟩181  · -- n = 2k even: n + 1 = 2k + 1 odd; e⁻¹ ≤ expNegOneSum(n+1), expNegOneSum(n+2) ≤ e⁻¹, e⁻¹ ≤ expNegOneSum(n+3)182    have hA := le_expNegOneSum_odd k            -- e⁻¹ ≤ expNegOneSum (2k+1)183    have hB := expNegOneSum_even_le (k + 1)     -- expNegOneSum (2k+2) ≤ e⁻¹184    have hC := le_expNegOneSum_odd (k + 1)      -- e⁻¹ ≤ expNegOneSum (2k+3)185    have e1 : 2 * k + 1 = n + 1 := by omega186    have e2 : 2 * (k + 1) = n + 2 := by omega187    have e3 : 2 * (k + 1) + 1 = n + 3 := by omega188    rw [e1] at hA; rw [e2] at hB; rw [e3] at hC189    rw [show n + 2 = (n + 1) + 1 from rfl, expNegOneSum_succ] at hB190    rw [show n + 3 = (n + 1) + 1 + 1 from rfl, expNegOneSum_succ, expNegOneSum_succ] at hC191    have hs : (-1 : ℝ) ^ (n + 1) = -1 := by rw [hk]; simp [pow_succ, pow_mul]192    have hs2 : (-1 : ℝ) ^ (n + 1 + 1) = 1 := by rw [hk]; simp [pow_succ, pow_mul]193    rw [hs] at hB hC ⊢194    rw [hs2] at hC195    rw [h1] at hB hC; rw [h2] at hC196    constructor197    · rw [div_le_iff₀ (by positivity)]198      have : Real.exp (-1) - expNegOneSum (n + 1) ≤ -(1 / ((n + 1) * n.factorial)) + 1 / ((n + 2) * (n + 1) * n.factorial) := by linarith199      calc (1 : ℝ) = (n.factorial * (1 / ((n + 1) * n.factorial) - 1 / ((n + 2) * (n + 1) * n.factorial))) * (n + 2) := by200              field_simp; ring201        _ ≤ _ := by nlinarith [this]202    · rw [le_div_iff₀ (by positivity)]203      have : -(1 / ((n + 1) * (n.factorial : ℝ))) ≤ Real.exp (-1) - expNegOneSum (n + 1) := by linarith204      calc (-1 * (n.factorial : ℝ) * (Real.exp (-1) - expNegOneSum (n + 1))) * (n + 1) ≤ (n.factorial * (1 / ((n + 1) * n.factorial))) * (n + 1) := by nlinarith [this]205        _ = 1 := by field_simp206  · -- n = 2k + 1 odd: n + 1 = 2k + 2 even; expNegOneSum(n+1) ≤ e⁻¹ ≤ expNegOneSum(n+2); expNegOneSum(n+3) ≤ e⁻¹207    have hA := expNegOneSum_even_le (k + 1)     -- expNegOneSum (2k+2) ≤ e⁻¹208    have hB := le_expNegOneSum_odd (k + 1)      -- e⁻¹ ≤ expNegOneSum (2k+3)209    have hC := expNegOneSum_even_le (k + 2)     -- expNegOneSum (2k+4) ≤ e⁻¹210    have e1 : 2 * (k + 1) = n + 1 := by omega211    have e2 : 2 * (k + 1) + 1 = n + 2 := by omega212    have e3 : 2 * (k + 2) = n + 3 := by omega213    rw [e1] at hA; rw [e2] at hB; rw [e3] at hC214    rw [show n + 2 = (n + 1) + 1 from rfl, expNegOneSum_succ] at hB215    rw [show n + 3 = (n + 1) + 1 + 1 from rfl, expNegOneSum_succ, expNegOneSum_succ] at hC216    have hs : (-1 : ℝ) ^ (n + 1) = 1 := by rw [hk]; simp [pow_succ, pow_mul]217    have hs2 : (-1 : ℝ) ^ (n + 1 + 1) = -1 := by rw [hk]; simp [pow_succ, pow_mul]218    rw [hs] at hB hC ⊢219    rw [hs2] at hC220    rw [h1] at hB hC; rw [h2] at hC221    constructor222    · rw [div_le_iff₀ (by positivity)]223      have : 1 / ((n + 1) * (n.factorial : ℝ)) - 1 / ((n + 2) * (n + 1) * n.factorial) ≤ Real.exp (-1) - expNegOneSum (n + 1) := by linarith224      calc (1 : ℝ) = (n.factorial * (1 / ((n + 1) * n.factorial) - 1 / ((n + 2) * (n + 1) * n.factorial))) * (n + 2) := by225              field_simp; ring226        _ ≤ _ := by nlinarith [this]227    · rw [le_div_iff₀ (by positivity)]228      have : Real.exp (-1) - expNegOneSum (n + 1) ≤ 1 / ((n + 1) * (n.factorial : ℝ)) := by linarith229      calc (1 * (n.factorial : ℝ) * (Real.exp (-1) - expNegOneSum (n + 1))) * (n + 1) ≤ (n.factorial * (1 / ((n + 1) * n.factorial))) * (n + 1) := by nlinarith [this]230        _ = 1 := by field_simp231232/-- The recursion `δ_n = (1 − δ_{n+1})/(n+1)`. -/233theorem tailDelta_succ (n : ℕ) : tailDelta n = (1 - tailDelta (n + 1)) / ((n : ℝ) + 1) := by234  rw [tailDelta_eq, tailDelta_eq, expNegOneSum_succ (n + 1)]235  have h1 : ((n + 1).factorial : ℝ) = (n + 1) * n.factorial := by push_cast [Nat.factorial_succ]; ring236  rw [h1]237  have hf : (0 : ℝ) < n.factorial := by positivity238  have hs1 : (-1 : ℝ) ^ (n + 1) = -((-1 : ℝ) ^ n) := by rw [pow_succ]; ring239  have hs2 : (-1 : ℝ) ^ (n + 1 + 1) = (-1 : ℝ) ^ n := by rw [pow_succ, pow_succ]; ring240  have hsq : ((-1 : ℝ) ^ n) ^ 2 = 1 := by rw [← pow_mul, mul_comm, pow_mul]; norm_num241  rw [hs1, hs2]242  field_simp243  linear_combination (1 : ℝ) * hsq244245/-- 13:D2 — the tail form: `!n = n!/e + (−1)^n δ_n` with `δ_n ∈ (1/(n+2), 1/(n+1))` strictly, so `!n` is the nearest integer to `n!/e`. -/246theorem tailDelta_strict (n : ℕ) : 1 / ((n : ℝ) + 2) < tailDelta n ∧ tailDelta n < 1 / ((n : ℝ) + 1) := by247  have hb := tailDelta_bounds (n + 1)248  have hb2 := tailDelta_bounds (n + 2)249  have hpos : 0 < tailDelta (n + 2) := lt_of_lt_of_le (by positivity) hb2.1250  have hlt : tailDelta (n + 1) < 1 / ((n : ℝ) + 2) := by251    rw [tailDelta_succ (n + 1)]252    push_cast253    rw [div_lt_div_iff₀ (by positivity) (by positivity)]254    nlinarith [hpos]255  have hpos1 : 0 < tailDelta (n + 1) := lt_of_lt_of_le (by positivity) hb.1256  have hlt' : tailDelta (n + 1) * ((n : ℝ) + 2) < 1 := (lt_div_iff₀ (by positivity)).mp hlt257  rw [tailDelta_succ n]258  constructor259  · rw [div_lt_div_iff₀ (by positivity) (by positivity)]260    nlinarith [hlt']261  · rw [div_lt_div_iff₀ (by positivity) (by positivity)]262    nlinarith [hpos1]263264/-! ### 13:D3 — the superexponential enclosure -/265266/-- The derangement chain `ε_n = n!/!n`. -/267noncomputable def epsChain (n : ℕ) : ℝ := n.factorial / numDerangements n268269theorem exp_neg_one_eq : Real.exp (-1) = (Real.exp 1)⁻¹ := by rw [Real.exp_neg]270271/-- 13:D2 — `!n = n!·e⁻¹ + (−1)^n δ_n`, the tail form itself. -/272theorem numDerangements_eq_tailDelta (n : ℕ) :273    (numDerangements n : ℝ) = n.factorial * Real.exp (-1) + (-1 : ℝ) ^ n * tailDelta n := by274  have hsq : ((-1 : ℝ) ^ n) ^ 2 = 1 := by rw [← pow_mul, mul_comm, pow_mul]; norm_num275  rw [tailDelta]; linear_combination (-(numDerangements n : ℝ) + n.factorial * Real.exp (-1)) * hsq276277theorem tailDelta_pos (n : ℕ) : 0 < tailDelta n := lt_of_lt_of_le (by positivity) (tailDelta_bounds n).1278279/-- `!n > 0` for `n ≥ 2`. -/280theorem numDerangements_pos_real (n : ℕ) (hn : 2 ≤ n) : (0 : ℝ) < numDerangements n := by281  rw [numDerangements_eq_tailDelta]282  have hE : (2 : ℝ) < Real.exp 1 := Real.exp_one_gt_two283  have hE' : Real.exp 1 < 2.7182818286 := Real.exp_one_lt_d9284  have hinv : (1 : ℝ) / 2.7182818286 < Real.exp (-1) := by285    rw [exp_neg_one_eq, ← one_div]; exact one_div_lt_one_div_of_lt (by positivity) hE'286  have hf : (2 : ℝ) ≤ n.factorial := by exact_mod_cast Nat.self_le_factorial n |>.trans' hn287  have hd := tailDelta_bounds n288  have hd1 : tailDelta n ≤ 1 / 3 := hd.2.trans (by289    rw [div_le_div_iff₀ (by positivity) (by positivity)]; have : (2 : ℝ) ≤ n := by exact_mod_cast hn290    linarith)291  have hsgn : -(tailDelta n) ≤ (-1 : ℝ) ^ n * tailDelta n := by292    rcases neg_one_pow_eq_or ℝ n with h | h <;> rw [h] <;> nlinarith [tailDelta_pos n]293  nlinarith [hinv, hf, hd1, hsgn, tailDelta_pos n]294295/-- `ε_n − e = (−1)^{n+1} e δ_n / !n`. -/296theorem epsChain_sub_exp (n : ℕ) (hn : 2 ≤ n) :297    epsChain n - Real.exp 1 = (-1 : ℝ) ^ (n + 1) * Real.exp 1 * tailDelta n / numDerangements n := by298  have hD := numDerangements_pos_real n hn299  have hE : (0 : ℝ) < Real.exp 1 := Real.exp_pos 1300  rw [epsChain, eq_div_iff hD.ne', sub_mul, div_mul_cancel₀ _ hD.ne']301  have h := numDerangements_eq_tailDelta n302  have hsq : ((-1 : ℝ) ^ n) ^ 2 = 1 := by rw [← pow_mul, mul_comm, pow_mul]; norm_num303  have hinv : Real.exp 1 * Real.exp (-1) = 1 := by rw [exp_neg_one_eq, mul_inv_cancel₀ hE.ne']304  rw [pow_succ]305  linear_combination (-(Real.exp 1)) * h + (-(n.factorial : ℝ)) * hinv306307/-- 13:D3 — the sign `sign(ε_n − e) = (−1)^{n+1}`: `ε_{2m} < e < ε_{2m+1}`. -/308theorem epsChain_sign (n : ℕ) (hn : 2 ≤ n) : 0 < (-1 : ℝ) ^ (n + 1) * (epsChain n - Real.exp 1) := by309  rw [epsChain_sub_exp n hn]310  have hsq : ((-1 : ℝ) ^ (n + 1)) ^ 2 = 1 := by rw [← pow_mul, mul_comm, pow_mul]; norm_num311  have : (-1 : ℝ) ^ (n + 1) * ((-1) ^ (n + 1) * Real.exp 1 * tailDelta n / numDerangements n)312      = Real.exp 1 * tailDelta n / numDerangements n := by313    rw [mul_div_assoc', ← mul_assoc, ← mul_assoc, ← sq, hsq, one_mul]314  rw [this]315  exact div_pos (mul_pos (Real.exp_pos 1) (tailDelta_pos n)) (numDerangements_pos_real n hn)316317/-- `ε_n ≤ e + 1` for `n ≥ 2`. -/318theorem epsChain_le (n : ℕ) (hn : 2 ≤ n) : epsChain n ≤ Real.exp 1 + 1 := by319  have hD := numDerangements_pos_real n hn320  rw [epsChain, div_le_iff₀ hD, numDerangements_eq_tailDelta]321  have hE : (2 : ℝ) < Real.exp 1 := Real.exp_one_gt_two322  have hE' : Real.exp 1 < 2.7182818286 := Real.exp_one_lt_d9323  have hinv : Real.exp 1 * Real.exp (-1) = 1 := by rw [exp_neg_one_eq, mul_inv_cancel₀ (Real.exp_pos 1).ne']324  have hd := tailDelta_bounds n325  have hdp := tailDelta_pos n326  have hsgn : -(tailDelta n) ≤ (-1 : ℝ) ^ n * tailDelta n := by327    rcases neg_one_pow_eq_or ℝ n with h | h <;> rw [h] <;> nlinarith328  have hd1 : tailDelta n * ((n : ℝ) + 1) ≤ 1 := (le_div_iff₀ (by positivity)).mp hd.2329  rcases Nat.lt_or_ge n 3 with h3 | h3330  · -- n = 2: !2 = 1 and 2 ≤ e + 1331    have : n = 2 := by omega332    subst this333    have h2 : (numDerangements 2 : ℝ) = 1 := by norm_num [numDerangements_add_two]334    rw [← numDerangements_eq_tailDelta, h2]; norm_num; linarith335  · -- n ≥ 3: n!/e − 1/(n+1) ≥ n!/(e+1) since (n+1)! ≥ 24 > e(e+1)336    have hf : (6 : ℝ) ≤ n.factorial := by337      have := Nat.factorial_le h3; exact_mod_cast (by norm_num : 6 ≤ Nat.factorial 3).trans this338    have hn3 : (3 : ℝ) ≤ n := by exact_mod_cast h3339    have hne : Real.exp (-1) = (Real.exp 1)⁻¹ := exp_neg_one_eq340    have hEinv : (1 : ℝ) / 2.7182818286 < Real.exp (-1) := by341      rw [hne, ← one_div]; exact one_div_lt_one_div_of_lt (by positivity) hE'342    nlinarith [hinv, hsgn, hd1, hf, hn3, hEinv, Real.exp_pos 1, mul_pos (Real.exp_pos 1) hdp]343344/-- 13:D3 — the superexponential enclosure `|ε_n − e| ≤ e(e+1)/(n+1)! < 10.2/(n+1)!` for `n ≥ 2`. -/345theorem epsChain_enclosure (n : ℕ) (hn : 2 ≤ n) :346    |epsChain n - Real.exp 1| ≤ Real.exp 1 * (Real.exp 1 + 1) / ((n + 1).factorial : ℝ) ∧347      Real.exp 1 * (Real.exp 1 + 1) / ((n + 1).factorial : ℝ) < 10.2 / ((n + 1).factorial : ℝ) := by348  have hD := numDerangements_pos_real n hn349  have hE := Real.exp_pos 1350  have hE' : Real.exp 1 < 2.7182818286 := Real.exp_one_lt_d9351  have h1 : ((n + 1).factorial : ℝ) = (n + 1) * n.factorial := by push_cast [Nat.factorial_succ]; ring352  constructor353  · rw [epsChain_sub_exp n hn, abs_div, abs_mul, abs_mul, abs_of_pos hE, abs_of_pos (tailDelta_pos n), abs_of_pos hD]354    have hs : |(-1 : ℝ) ^ (n + 1)| = 1 := by simp355    rw [hs, one_mul, h1, div_le_div_iff₀ hD (by positivity)]356    have hd : tailDelta n * ((n : ℝ) + 1) ≤ 1 := (le_div_iff₀ (by positivity)).mp (tailDelta_bounds n).2357    have hl := epsChain_le n hn358    rw [epsChain, div_le_iff₀ hD] at hl359    nlinarith [mul_nonneg hE.le (tailDelta_pos n).le, mul_le_mul_of_nonneg_left hd hE.le, mul_le_mul_of_nonneg_left hl hE.le, mul_pos hE hD]360  · rw [div_lt_div_iff_of_pos_right (by positivity)]; nlinarith361362/-! ### 13:D4 — the binary64 readout -/363364theorem numDerangements_2 : numDerangements 2 = 1 := by decide365theorem numDerangements_3 : numDerangements 3 = 2 := by decide366theorem numDerangements_4 : numDerangements 4 = 9 := by decide367theorem numDerangements_5 : numDerangements 5 = 44 := by decide368theorem numDerangements_6 : numDerangements 6 = 265 := by decide369theorem numDerangements_7 : numDerangements 7 = 1854 := by decide370theorem numDerangements_8 : numDerangements 8 = 14833 := by decide371theorem numDerangements_9 : numDerangements 9 = 133496 := by decide372theorem numDerangements_10 : numDerangements 10 = 1334961 := by decide373theorem numDerangements_11 : numDerangements 11 = 14684570 := by decide374theorem numDerangements_12 : numDerangements 12 = 176214841 := by decide375theorem numDerangements_13 : numDerangements 13 = 2290792932 := by decide376theorem numDerangements_14 : numDerangements 14 = 32071101049 := by decide377theorem numDerangements_15 : numDerangements 15 = 481066515734 := by decide378theorem numDerangements_16 : numDerangements 16 = 7697064251745 := by decide379theorem numDerangements_17 : numDerangements 17 = 130850092279664 := by decide380theorem numDerangements_18 : numDerangements 18 = 2355301661033953 := by decide381382/-- The binary64 constant nearest `e`: `6121026514868073 / 2^51`. -/383noncomputable def binary64E : ℝ := 6121026514868073 / 2 ^ 51384385/-- 13:D4, 13:I1 — `e` lies within the half-ulp `2⁻⁵²` of the binary64 constant (from Mathlib's twenty-digit bracket of `e`),386`ε_18` lies within the same half-ulp, and no `ε_n` with `2 ≤ n ≤ 17` does: `n = 18` is the minimal readout grade. -/387theorem readout_binary64 :388    |Real.exp 1 - binary64E| < 1 / 2 ^ 52 ∧ |epsChain 18 - binary64E| < 1 / 2 ^ 52 ∧389      ∀ n, 2 ≤ n → n ≤ 17 → 1 / 2 ^ 52 < |epsChain n - binary64E| := by390  refine ⟨?_, ?_, ?_⟩391  · have h := Real.exp_one_near_20392    have h2 : |(363916618873 : ℝ) / 133877442384 - binary64E| < 1 / 2 ^ 52 - 1 / 10 ^ 20 := by393      rw [binary64E, abs_lt]; constructor <;> norm_num394    calc |Real.exp 1 - binary64E| = |(Real.exp 1 - 363916618873 / 133877442384) + (363916618873 / 133877442384 - binary64E)| := by ring_nf395      _ ≤ |Real.exp 1 - 363916618873 / 133877442384| + |(363916618873 : ℝ) / 133877442384 - binary64E| := abs_add_le _ _396      _ < 1 / 2 ^ 52 := by linarith397  · rw [epsChain, binary64E, numDerangements_18, abs_lt]; constructor <;> norm_num [Nat.factorial]398  · intro n h2 h17399    interval_cases n <;> rw [epsChain, binary64E] <;> simp only [numDerangements_2, numDerangements_3, numDerangements_4, numDerangements_5, numDerangements_6, numDerangements_7, numDerangements_8, numDerangements_9, numDerangements_10, numDerangements_11, numDerangements_12, numDerangements_13, numDerangements_14, numDerangements_15, numDerangements_16, numDerangements_17, numDerangements_18] <;> rw [lt_abs] <;> norm_num [Nat.factorial]400401/-- The `k`-bit readout on `[2, 4)`: the grid of spacing `2^{2−k}`, rounding to the nearest point (ties up),402`ρ_k(x) = ⌊x·2^{k−2} + 1/2⌋ / 2^{k−2}`. -/403noncomputable def roundTo (k : ℕ) (x : ℝ) : ℝ := (⌊x * 2 ^ (k - 2) + 1 / 2⌋ : ℝ) / 2 ^ (k - 2)404405/-- The distance `d_k(y)` from `y` to the nearest rounding boundary of the `k`-bit grid: with `t = y·2^{k−2} + 1/2`,406the smaller of `t − ⌊t⌋` and `⌊t⌋ + 1 − t`, scaled back by `2^{2−k}`. -/407noncomputable def cellDist (k : ℕ) (y : ℝ) : ℝ :=408  min (y * 2 ^ (k - 2) + 1 / 2 - ⌊y * 2 ^ (k - 2) + 1 / 2⌋) (⌊y * 2 ^ (k - 2) + 1 / 2⌋ + 1 - (y * 2 ^ (k - 2) + 1 / 2)) /409    2 ^ (k - 2)410411theorem floor_eq_of_abs_sub_lt (s t : ℝ) (h : |s - t| < min (t - ⌊t⌋) (⌊t⌋ + 1 - t)) : ⌊s⌋ = ⌊t⌋ := by412  have h1 := Int.floor_le t413  have h2 := Int.lt_floor_add_one t414  rw [abs_lt] at h415  have ha : -(t - ⌊t⌋) < s - t := lt_of_le_of_lt (neg_le_neg (min_le_left _ _)) h.1416  have hb : s - t < ⌊t⌋ + 1 - t := lt_of_lt_of_le h.2 (min_le_right _ _)417  rw [Int.floor_eq_iff]418  constructor <;> linarith419420/-- The plateau lemma: a point within `d_k(y)` of `y` reads out as `y` does. -/421theorem roundTo_eq_of_lt_cellDist (k : ℕ) (x y : ℝ) (h : |x - y| < cellDist k y) : roundTo k x = roundTo k y := by422  unfold roundTo423  congr 1424  have hp : (0 : ℝ) < 2 ^ (k - 2) := by positivity425  have h' : |x * 2 ^ (k - 2) + 1 / 2 - (y * 2 ^ (k - 2) + 1 / 2)| <426      min (y * 2 ^ (k - 2) + 1 / 2 - ⌊y * 2 ^ (k - 2) + 1 / 2⌋) (⌊y * 2 ^ (k - 2) + 1 / 2⌋ + 1 - (y * 2 ^ (k - 2) + 1 / 2)) := by427    have e : x * 2 ^ (k - 2) + 1 / 2 - (y * 2 ^ (k - 2) + 1 / 2) = (x - y) * 2 ^ (k - 2) := by ring428    rw [e, abs_mul, abs_of_pos hp]429    unfold cellDist at h430    rwa [lt_div_iff₀ hp] at h431  exact_mod_cast floor_eq_of_abs_sub_lt _ _ h'432433theorem floor_sub_abs_le_one (s t : ℝ) (h : |s - t| < 1 / 2) : |(⌊s⌋ : ℝ) - ⌊t⌋| ≤ 1 := by434  rw [abs_lt] at h435  have h1 := Int.floor_le t; have h2 := Int.lt_floor_add_one t436  have h3 := Int.floor_le s; have h4 := Int.lt_floor_add_one s437  have a : ⌊s⌋ ≤ ⌊t⌋ + 1 := by438    have : (⌊s⌋ : ℝ) < ⌊t⌋ + 2 := by linarith439    have : ⌊s⌋ < ⌊t⌋ + 2 := by exact_mod_cast this440    omega441  have b : ⌊t⌋ ≤ ⌊s⌋ + 1 := by442    have : (⌊t⌋ : ℝ) < ⌊s⌋ + 2 := by linarith443    have : ⌊t⌋ < ⌊s⌋ + 2 := by exact_mod_cast this444    omega445  rw [abs_le]; constructor446  · have : (⌊t⌋ : ℝ) - 1 ≤ ⌊s⌋ := by exact_mod_cast (by omega : ⌊t⌋ - 1 ≤ ⌊s⌋)447    linarith448  · have : (⌊s⌋ : ℝ) ≤ ⌊t⌋ + 1 := by exact_mod_cast a449    linarith450451/-- Two points less than half a grid step apart read out within one grid step of each other. -/452theorem roundTo_sub_le (k : ℕ) (x y : ℝ) (h : |x - y| * 2 ^ (k - 2) < 1 / 2) :453    |roundTo k x - roundTo k y| ≤ 1 / 2 ^ (k - 2) := by454  unfold roundTo455  have hp : (0 : ℝ) < 2 ^ (k - 2) := by positivity456  have h' : |x * 2 ^ (k - 2) + 1 / 2 - (y * 2 ^ (k - 2) + 1 / 2)| < 1 / 2 := by457    have e : x * 2 ^ (k - 2) + 1 / 2 - (y * 2 ^ (k - 2) + 1 / 2) = (x - y) * 2 ^ (k - 2) := by ring458    rw [e, abs_mul, abs_of_pos hp]; exact h459  have hf := floor_sub_abs_le_one _ _ h'460  rw [← sub_div, abs_div, abs_of_pos hp, div_le_div_iff_of_pos_right hp]461  exact hf462463/-- 13:D4 — the readout within one grid step: for `n ≥ 2` with `e(e+1)/(n+1)! < 2^{−k}` (the threshold `n₀(k)`),464`ρ_k(ε_n)` is `ρ_k(e)` or its neighbour, `|ρ_k(ε_n) − ρ_k(e)| ≤ 2^{2−k}`. -/465theorem readout_within_ulp (k n : ℕ) (hk : 2 ≤ k) (hn : 2 ≤ n)466    (h : Real.exp 1 * (Real.exp 1 + 1) / ((n + 1).factorial : ℝ) < 1 / 2 ^ k) :467    |roundTo k (epsChain n) - roundTo k (Real.exp 1)| ≤ 1 / 2 ^ (k - 2) := by468  apply roundTo_sub_le469  have h1 := (epsChain_enclosure n hn).1470  have hp : (0 : ℝ) < 2 ^ (k - 2) := by positivity471  have e2 : (2 : ℝ) ^ k = 2 ^ (k - 2) * 4 := by472    rw [show k = (k - 2) + 2 by omega, pow_add]; norm_num473  calc |epsChain n - Real.exp 1| * 2 ^ (k - 2) ≤ Real.exp 1 * (Real.exp 1 + 1) / ((n + 1).factorial : ℝ) * 2 ^ (k - 2) := by gcongr474    _ < 1 / 2 ^ k * 2 ^ (k - 2) := by gcongr475    _ = 1 / 4 := by rw [e2]; field_simp476    _ < 1 / 2 := by norm_num477478/-- 13:D4 — the plateau: for `n ≥ 2` with `e(e+1)/(n+1)! < d_k(e)`, the enclosure lies in the rounding cell of `e` and479`ρ_k(ε_n) = ρ_k(e)`; the readouts below that index are compared exactly (the package's e.R2). -/480theorem readout_plateau (k n : ℕ) (hn : 2 ≤ n)481    (h : Real.exp 1 * (Real.exp 1 + 1) / ((n + 1).factorial : ℝ) < cellDist k (Real.exp 1)) :482    roundTo k (epsChain n) = roundTo k (Real.exp 1) :=483  roundTo_eq_of_lt_cellDist k _ _ (lt_of_le_of_lt (epsChain_enclosure n hn).1 h)484485/-- 13:D4 — the threshold `n₀(k)` alone does not give the plateau: at `k = 6`, `n₀(6) = 5`, `ε₅ = 30/11` reads out as486`44/16` and `e` as `43/16`, although `e(e+1)/6! < 2⁻⁶`. -/487theorem readout_six_bits :488    roundTo 6 (epsChain 5) = 44 / 16 ∧ roundTo 6 (Real.exp 1) = 43 / 16 ∧489      Real.exp 1 * (Real.exp 1 + 1) / ((5 + 1).factorial : ℝ) < 1 / 2 ^ 6 := by490  have hE : 2.7182818283 < Real.exp 1 := Real.exp_one_gt_d9491  have hE' : Real.exp 1 < 2.7182818286 := Real.exp_one_lt_d9492  refine ⟨?_, ?_, ?_⟩493  · rw [roundTo, epsChain, numDerangements_5]494    have : ⌊((5 : ℕ).factorial : ℝ) / (44 : ℕ) * 2 ^ (6 - 2) + 1 / 2⌋ = 44 := by495      rw [Int.floor_eq_iff]; norm_num [Nat.factorial]496    rw [this]; norm_num497  · rw [roundTo]498    have : ⌊Real.exp 1 * 2 ^ (6 - 2) + 1 / 2⌋ = 43 := by499      rw [Int.floor_eq_iff]; constructor <;> norm_num <;> linarith500    rw [this]; norm_num501  · norm_num [Nat.factorial]; nlinarith502503/-! ### 13:D5 — feasibility -/504505/-- 13:D5 — the derangement chain's step counts: `n = 11, 18, 70` are the least `n` with `8/(n+1)! < 2^{−k}` for506`k = 24, 53, 333` (the enclosure bound of D3 with the sharper constant `8`; `8/(m+1)!` falls with `m`). -/507theorem derangement_cost :508    ((8 : ℚ) / (Nat.factorial 12) < 1 / 2 ^ 24 ∧ ∀ m < 11, ¬ ((8 : ℚ) / (Nat.factorial (m + 1)) < 1 / 2 ^ 24)) ∧509    ((8 : ℚ) / (Nat.factorial 19) < 1 / 2 ^ 53 ∧ ∀ m < 18, ¬ ((8 : ℚ) / (Nat.factorial (m + 1)) < 1 / 2 ^ 53)) ∧510    ((8 : ℚ) / (Nat.factorial 71) < 1 / 2 ^ 333 ∧ ∀ m < 70, ¬ ((8 : ℚ) / (Nat.factorial (m + 1)) < 1 / 2 ^ 333)) := by511  have mono : ∀ m n : ℕ, m ≤ n → (8 : ℚ) / (Nat.factorial n) ≤ 8 / (Nat.factorial m) := fun m n h =>512    div_le_div_of_nonneg_left (by norm_num) (by positivity) (by exact_mod_cast Nat.factorial_le h)513  have lt_iff : ∀ (n k : ℕ), ((8 : ℚ) / (Nat.factorial n) < 1 / 2 ^ k ↔ 8 * 2 ^ k < Nat.factorial n) := fun n k => by514    rw [div_lt_div_iff₀ (by positivity) (by positivity), one_mul]; exact_mod_cast Iff.rfl515  refine ⟨⟨?_, fun m hm h => ?_⟩, ⟨?_, fun m hm h => ?_⟩, ⟨?_, fun m hm h => ?_⟩⟩516  · rw [lt_iff]; decide517  · have := mono (m + 1) 11 (by omega); have h11 : ¬ ((8 : ℚ) / (Nat.factorial 11) < 1 / 2 ^ 24) := by518      rw [lt_iff]; decide519    exact h11 (lt_of_le_of_lt this h)520  · rw [lt_iff]; decide521  · have := mono (m + 1) 18 (by omega); have h18 : ¬ ((8 : ℚ) / (Nat.factorial 18) < 1 / 2 ^ 53) := by522      rw [lt_iff]; decide523    exact h18 (lt_of_le_of_lt this h)524  · rw [lt_iff]; decide525  · have := mono (m + 1) 70 (by omega); have h70 : ¬ ((8 : ℚ) / (Nat.factorial 70) < 1 / 2 ^ 333) := by526      rw [lt_iff]; decide527    exact h70 (lt_of_le_of_lt this h)528529/-- `log(1 + 1/n) ≤ 1/n − 1/(4n²)` for `n ≥ 5` (the cubic Taylor bound of Mathlib). -/530theorem log_one_add_inv_le (n : ℕ) (hn : 5 ≤ n) :531    Real.log (1 + 1 / (n : ℝ)) ≤ 1 / n - 1 / (4 * (n : ℝ) ^ 2) := by532  have hn' : (5 : ℝ) ≤ n := by exact_mod_cast hn533  have hx : |(-1 : ℝ) / n| < 1 := by534    rw [abs_div, abs_neg, abs_one, abs_of_pos (by positivity : (0 : ℝ) < n), div_lt_one (by positivity)]; linarith535  have h := Real.abs_log_sub_add_sum_range_le hx 2536  have hsum : (∑ i ∈ Finset.range 2, ((-1 : ℝ) / n) ^ (i + 1) / (i + 1)) = -1 / n + 1 / (2 * (n : ℝ) ^ 2) := by537    simp [Finset.sum_range_succ]; field_simp; ring538  have hlog : (1 : ℝ) - (-1) / n = 1 + 1 / n := by ring539  rw [hsum, hlog] at h540  have habs : |(-1 : ℝ) / n| = 1 / n := by541    rw [abs_div, abs_neg, abs_one, abs_of_pos (by positivity : (0 : ℝ) < n)]542  rw [habs] at h543  have hn0 : (n : ℝ) ≠ 0 := by positivity544  have hn1 : (n : ℝ) - 1 ≠ 0 := by linarith545  have hrem : (1 / (n : ℝ)) ^ (2 + 1) / (1 - 1 / n) ≤ 1 / (4 * (n : ℝ) ^ 2) := by546    have ht0 : (0 : ℝ) < 1 / n := by positivity547    have ht5 : 1 / (n : ℝ) ≤ 1 / 5 := one_div_le_one_div_of_le (by norm_num) hn'548    have e : 1 / (4 * (n : ℝ) ^ 2) = (1 / n) ^ 2 / 4 := by field_simp549    rw [e, div_le_iff₀ (by linarith)]550    nlinarith [mul_pos ht0 ht0, mul_pos (mul_pos ht0 ht0) ht0]551  have h' := (abs_le.mp h).2552  have e2 : 1 / (2 * (n : ℝ) ^ 2) = 2 * (1 / (4 * (n : ℝ) ^ 2)) := by field_simp; ring553  linarith554555/-- 13:D5, 13:E5, 13:I3 — the compound chain is slow: `(1 + 1/n)^n ≤ e · 4n/(4n+1)` for `n ≥ 5`, so the gap `e − (1+1/n)^n`556is at least `e/(4n+1)`: `k` bits cost `n ≍ 2^k` steps. -/557theorem compound_cost (n : ℕ) (hn : 5 ≤ n) :558    (1 + 1 / (n : ℝ)) ^ n ≤ Real.exp 1 * (4 * n) / (4 * n + 1) := by559  have hn' : (5 : ℝ) ≤ n := by exact_mod_cast hn560  have hpos : (0 : ℝ) < 1 + 1 / n := by positivity561  have hl := log_one_add_inv_le n hn562  have h1 : (1 + 1 / (n : ℝ)) ^ n = Real.exp (n * Real.log (1 + 1 / n)) := by563    rw [Real.exp_nat_mul, Real.exp_log hpos]564  have h2 : (n : ℝ) * Real.log (1 + 1 / n) ≤ 1 - 1 / (4 * n) := by565    have := mul_le_mul_of_nonneg_left hl (by positivity : (0 : ℝ) ≤ n)566    calc (n : ℝ) * Real.log (1 + 1 / n) ≤ n * (1 / n - 1 / (4 * (n : ℝ) ^ 2)) := this567      _ = 1 - 1 / (4 * n) := by field_simp568  have h3 : Real.exp (1 - 1 / (4 * (n : ℝ))) = Real.exp 1 * Real.exp (-(1 / (4 * n))) := by569    rw [← Real.exp_add]; ring_nf570  have h4 : Real.exp (-(1 / (4 * (n : ℝ)))) ≤ (4 * n) / (4 * n + 1) := by571    have := Real.add_one_le_exp (1 / (4 * (n : ℝ)))572    rw [Real.exp_neg, inv_le_comm₀ (Real.exp_pos _) (by positivity)]573    calc ((4 * (n : ℝ)) / (4 * n + 1))⁻¹ = 1 / (4 * n) + 1 := by field_simp; ring574      _ ≤ Real.exp (1 / (4 * n)) := this575  calc (1 + 1 / (n : ℝ)) ^ n = Real.exp (n * Real.log (1 + 1 / n)) := h1576    _ ≤ Real.exp (1 - 1 / (4 * n)) := Real.exp_le_exp.mpr h2577    _ = Real.exp 1 * Real.exp (-(1 / (4 * n))) := h3578    _ ≤ Real.exp 1 * ((4 * n) / (4 * n + 1)) := by gcongr579    _ = Real.exp 1 * (4 * n) / (4 * n + 1) := by ring580581/-! ### 13:C5 — the joint-return tally -/582583/-- 13:C5 — the returning `±1` histories of length `2n` in one direction (the sets of `n` up-steps among `2n`) number584`C(2n,n)`, the paired histories in the two directions `16^n`, and the joint returns `C(2n,n)²`. -/585theorem joint_return_tally (n : ℕ) :586    ((Finset.univ : Finset (Finset (Fin (2 * n)))).filter (fun expNegOneSum => expNegOneSum.card = n)).card = Nat.centralBinom n ∧587    Fintype.card (Finset (Fin (2 * n)) × Finset (Fin (2 * n))) = 16 ^ n ∧588    (((Finset.univ : Finset (Finset (Fin (2 * n)))).filter (fun expNegOneSum => expNegOneSum.card = n)) ×ˢ589      ((Finset.univ : Finset (Finset (Fin (2 * n)))).filter (fun expNegOneSum => expNegOneSum.card = n))).card = (Nat.centralBinom n) ^ 2 := by590  have h1 : ((Finset.univ : Finset (Finset (Fin (2 * n)))).filter (fun expNegOneSum => expNegOneSum.card = n)).card = Nat.centralBinom n := by591    rw [← Finset.powerset_univ, ← Finset.powersetCard_eq_filter, Finset.card_powersetCard, Finset.card_univ,592      Fintype.card_fin, Nat.centralBinom_eq_two_mul_choose]593  refine ⟨h1, ?_, ?_⟩594  · rw [Fintype.card_prod, Fintype.card_finset, Fintype.card_fin, ← pow_add, show 2 * n + 2 * n = 4 * n by ring, pow_mul]; norm_num595  · rw [Finset.card_product, h1, sq]596597/-- `C(2n,n) · (n!)² = (2n)!`. -/598theorem centralBinom_mul_factorial_sq (n : ℕ) : Nat.centralBinom n * (n.factorial) ^ 2 = (2 * n).factorial := by599  have h := Nat.choose_mul_factorial_mul_factorial (show n ≤ 2 * n by omega)600  rw [show 2 * n - n = n by omega] at h601  rw [Nat.centralBinom_eq_two_mul_choose, sq, ← mul_assoc]; exact h602603/-- `16^n/(n C_n²) = W_n · (2n+1)/n` for `n ≥ 1`, `W_n` Mathlib's Wallis product. -/604theorem wallis_chain_eq (n : ℕ) (hn : 1 ≤ n) :605    (16 : ℝ) ^ n / (n * (Nat.centralBinom n : ℝ) ^ 2) = Real.Wallis.W n * ((2 * n + 1) / n) := by606  rw [Real.Wallis.W_eq_factorial_ratio]607  have hc : (Nat.centralBinom n : ℝ) * (n.factorial : ℝ) ^ 2 = ((2 * n).factorial : ℝ) := by608    exact_mod_cast centralBinom_mul_factorial_sq n609  have hn' : (0 : ℝ) < n := by exact_mod_cast hn610  have hf : (0 : ℝ) < n.factorial := by positivity611  have hcb : (0 : ℝ) < Nat.centralBinom n := by exact_mod_cast Nat.centralBinom_pos n612  rw [← hc]613  have h16 : (2 : ℝ) ^ (4 * n) = 16 ^ n := by rw [pow_mul]; norm_num614  rw [h16]615  field_simp616617/-- 13:C5 — `π = lim 16^n/(n C_n²)`: the joint-return ratio converges to `π` (Mathlib's Wallis product). -/618theorem tendsto_wallis_chain :619    Filter.Tendsto (fun n : ℕ => (16 : ℝ) ^ n / (n * (Nat.centralBinom n : ℝ) ^ 2)) Filter.atTop (𝓝 Real.pi) := by620  have hW := Real.Wallis.tendsto_W_nhds_pi_div_two621  have hr : Filter.Tendsto (fun n : ℕ => ((2 * n + 1 : ℝ) / n)) Filter.atTop (𝓝 2) := by622    have h0 : Filter.Tendsto (fun n : ℕ => (1 : ℝ) / n) Filter.atTop (𝓝 0) := tendsto_one_div_atTop_nhds_zero_nat623    have : Filter.Tendsto (fun n : ℕ => (2 : ℝ) + 1 / n) Filter.atTop (𝓝 (2 + 0)) := tendsto_const_nhds.add h0624    rw [add_zero] at this625    refine this.congr' ?_626    filter_upwards [Filter.eventually_ge_atTop 1] with n hn627    have hn' : (n : ℝ) ≠ 0 := by positivity628    field_simp629  have hprod := hW.mul hr630  rw [show Real.pi / 2 * 2 = Real.pi by ring] at hprod631  refine hprod.congr' ?_632  filter_upwards [Filter.eventually_ge_atTop 1] with n hn633  exact (wallis_chain_eq n hn).symm634635end tailAndReadout636637/-! ## The Machin chain, the Gregory brackets and the rounding chain (13:E3, E4, E5)638639The arctangent series as a `ℚ`-native chain: the alternating bound and the alternating pairing (two-sided640enclosures at every truncation), Machin's formula `π/4 = 4 arctan(1/5) − arctan(1/239)` (Mathlib), the binary64641readout of `π` at `N = 10`, the hundred digits at `N = 71`, the rational bracket at `m = 12` that the core's642`arcsin_tail_bound` reads (E3), the Gregory brackets of the Leibniz series (the base case), and the factorial-rate643chain by rounding that exists for every real (E5). -/644section machin645open Filter Topology Real646647/-- The partial sums of the arctangent series, `S_x(N) = Σ_{n ≤ N} (−1)^n x^{2n+1}/(2n+1)`. -/648noncomputable def arctanSum (x : ℝ) (N : ℕ) : ℝ := ∑ n ∈ range (N + 1), (-1 : ℝ) ^ n * (x ^ (2 * n + 1) / (2 * n + 1))649650/-- The terms of the arctangent series decrease for `0 ≤ x ≤ 1`. -/651theorem arctanTerm_antitone {x : ℝ} (hx0 : 0 ≤ x) (hx1 : x ≤ 1) :652    Antitone (fun n : ℕ => x ^ (2 * n + 1) / (2 * n + 1)) := by653  intro m n hmn654  apply div_le_div₀ (by positivity) (pow_le_pow_of_le_one hx0 hx1 (by omega)) (by positivity)655  have : (m : ℝ) ≤ n := by exact_mod_cast hmn656  linarith657658/-- The arctangent series sums to `arctan x` for `0 ≤ x < 1` (Mathlib's `Real.hasSum_arctan`). -/659theorem arctanTerm_hasSum {x : ℝ} (hx0 : 0 ≤ x) (hx1 : x < 1) :660    HasSum (fun n : ℕ => (-1 : ℝ) ^ n * (x ^ (2 * n + 1) / (2 * n + 1))) (arctan x) := by661  have h := Real.hasSum_arctan (x := x) (by rw [Real.norm_eq_abs, abs_of_nonneg hx0]; exact hx1)662  convert h using 1663  ext n; push_cast; ring664665/-- The error of the arctangent series for `0 ≤ x < 1` is at most the first omitted term. -/666theorem arctanSum_error {x : ℝ} (hx0 : 0 ≤ x) (hx1 : x < 1) (N : ℕ) :667    |arctan x - arctanSum x N| ≤ x ^ (2 * N + 3) / (2 * N + 3) := by668  set f : ℕ → ℝ := fun n => x ^ (2 * n + 1) / (2 * n + 1) with hf669  have hfa : Antitone f := arctanTerm_antitone hx0 hx1.le670  have hsum : HasSum (fun n : ℕ => (-1 : ℝ) ^ n * f n) (arctan x) := arctanTerm_hasSum hx0 hx1671  have hfs : Summable f := by672    refine Summable.of_nonneg_of_le (fun n => by positivity) (fun n => ?_) (summable_geometric_of_lt_one hx0 hx1)673    simp only [hf]674    calc x ^ (2 * n + 1) / (2 * n + 1) ≤ x ^ (2 * n + 1) / 1 := by675            apply div_le_div_of_nonneg_left (by positivity) (by norm_num) (by linarith [(by positivity : (0:ℝ) ≤ 2 * n)])676      _ ≤ x ^ n := by rw [div_one]; exact pow_le_pow_of_le_one hx0 hx1.le (by omega)677  have h := alternating_series_error_bound f hfa hfs (N + 1)678  rw [hsum.tsum_eq] at h679  simpa [arctanSum, hf, show 2 * (N + 1) + 1 = 2 * N + 3 by ring, show ((2 : ℝ) * (N + 1) + 1) = 2 * N + 3 by ring] using h680681/-- 13:E4 — the alternating pairing of the arctangent series: for `0 ≤ x < 1`, `S_x(2k+1) ≤ arctan x ≤ S_x(2k)`,682a certified two-sided enclosure at every truncation. -/683theorem arctan_pairing {x : ℝ} (hx0 : 0 ≤ x) (hx1 : x < 1) (k : ℕ) :684    arctanSum x (2 * k + 1) ≤ arctan x ∧ arctan x ≤ arctanSum x (2 * k) := by685  have hfa := arctanTerm_antitone hx0 hx1.le686  have hT := (arctanTerm_hasSum hx0 hx1).tendsto_sum_nat687  refine ⟨?_, ?_⟩688  · have h := Antitone.alternating_series_le_tendsto hT hfa (k + 1)689    rw [show 2 * (k + 1) = 2 * k + 1 + 1 by ring] at h690    exact h691  · exact Antitone.tendsto_le_alternating_series hT hfa k692693/-- The Machin chain `M_N = 4(4 S_{1/5}(N) − S_{1/239}(N))`. -/694noncomputable def machin (N : ℕ) : ℝ := 4 * (4 * arctanSum (1 / 5) N - arctanSum (1 / 239) N)695696/-- 13:E4, 13:E5, 13:I3 — the Machin chain's error: `|M_N − π| < 17/((2N+3)·5^{2N+3})` for every `N`, from697Machin's formula `π/4 = 4 arctan(1/5) − arctan(1/239)` and the alternating bound on each arctangent series: the698geometric `ℚ`-rate of `π`. -/699theorem machin_bound (N : ℕ) : |machin N - π| < 17 / ((2 * N + 3) * 5 ^ (2 * N + 3)) := by700  have hM := Real.four_mul_arctan_inv_5_sub_arctan_inv_239701  have h5 := arctanSum_error (x := 1 / 5) (by norm_num) (by norm_num) N702  have h239 := arctanSum_error (x := 1 / 239) (by norm_num) (by norm_num) N703  have hpi : π = 4 * (4 * arctan (1 / 5) - arctan (1 / 239)) := by704    rw [one_div, one_div, hM]; ring705  have e : machin N - π = 4 * (4 * (arctanSum (1 / 5) N - arctan (1 / 5)) - (arctanSum (1 / 239) N - arctan (1 / 239))) := by706    rw [machin, hpi]; ring707  rw [e]708  have hN : (0 : ℝ) < 2 * N + 3 := by positivity709  have h5' : |arctanSum (1 / 5) N - arctan (1 / 5)| ≤ (1 / 5) ^ (2 * N + 3) / (2 * N + 3) := by rw [abs_sub_comm]; exact h5710  have h239' : |arctanSum (1 / 239) N - arctan (1 / 239)| ≤ (1 / 239) ^ (2 * N + 3) / (2 * N + 3) := by rw [abs_sub_comm]; exact h239711  have hsmall : (1 / 239 : ℝ) ^ (2 * N + 3) < (1 / 4) * (1 / 5) ^ (2 * N + 3) := by712    have : (1 / 239 : ℝ) ^ (2 * N + 3) ≤ (1 / 239) ^ 1 * (1 / 5) ^ (2 * N + 2) := by713      rw [show 2 * N + 3 = 1 + (2 * N + 2) by ring, pow_add]714      gcongr; norm_num715    calc (1 / 239 : ℝ) ^ (2 * N + 3) ≤ (1 / 239) ^ 1 * (1 / 5) ^ (2 * N + 2) := this716      _ < (1 / 4) * (1 / 5) ^ (2 * N + 3) := by717          have hp := pow_pos (by norm_num : (0:ℝ) < 1 / 5) (2 * N + 2)718          have e3 : (1 / 5 : ℝ) ^ (2 * N + 3) = (1 / 5) ^ (2 * N + 2) * (1 / 5) := by rw [pow_succ]719          rw [e3]; norm_num; nlinarith [hp]720  calc |4 * (4 * (arctanSum (1 / 5) N - arctan (1 / 5)) - (arctanSum (1 / 239) N - arctan (1 / 239)))|721      ≤ 4 * (4 * |arctanSum (1 / 5) N - arctan (1 / 5)| + |arctanSum (1 / 239) N - arctan (1 / 239)|) := by722        rw [abs_mul, abs_of_pos (by norm_num : (0:ℝ) < 4)]723        gcongr724        calc |4 * (arctanSum (1 / 5) N - arctan (1 / 5)) - (arctanSum (1 / 239) N - arctan (1 / 239))|725            ≤ |4 * (arctanSum (1 / 5) N - arctan (1 / 5))| + |arctanSum (1 / 239) N - arctan (1 / 239)| := abs_sub _ _726          _ = 4 * |arctanSum (1 / 5) N - arctan (1 / 5)| + |arctanSum (1 / 239) N - arctan (1 / 239)| := by727              rw [abs_mul, abs_of_pos (by norm_num : (0:ℝ) < 4)]728    _ ≤ 4 * (4 * ((1 / 5) ^ (2 * N + 3) / (2 * N + 3)) + (1 / 239) ^ (2 * N + 3) / (2 * N + 3)) := by gcongr729    _ < 4 * (4 * ((1 / 5) ^ (2 * N + 3) / (2 * N + 3)) + (1 / 4) * (1 / 5) ^ (2 * N + 3) / (2 * N + 3)) := by730        gcongr731    _ = 17 / ((2 * N + 3) * 5 ^ (2 * N + 3)) := by732        rw [one_div_pow]; field_simp; ring733734/-- 13:E4 — the first hundred decimal digits are fixed by `M_71`: `|M_71 − π| < 10⁻¹⁰⁰`. -/735theorem machin_hundred_digits : |machin 71 - π| < 1 / 10 ^ 100 := by736  refine lt_trans (machin_bound 71) ?_737  norm_num738739/-- The pairing enclosure of the Machin chain, lower end: `4(4 S_{1/5}(2m+1) − S_{1/239}(2m))`. -/740noncomputable def machinLo (m : ℕ) : ℝ := 4 * (4 * arctanSum (1 / 5) (2 * m + 1) - arctanSum (1 / 239) (2 * m))741742/-- The pairing enclosure of the Machin chain, upper end: `4(4 S_{1/5}(2m) − S_{1/239}(2m+1))`. -/743noncomputable def machinHi (m : ℕ) : ℝ := 4 * (4 * arctanSum (1 / 5) (2 * m) - arctanSum (1 / 239) (2 * m + 1))744745/-- 13:E4 — the alternating pairing of the two arctangent series encloses `π` at every truncation:746`machinLo m ≤ π ≤ machinHi m`, a certified two-sided `ℚ`-enclosure. -/747theorem machin_pairing (m : ℕ) : machinLo m ≤ π ∧ π ≤ machinHi m := by748  have hM := Real.four_mul_arctan_inv_5_sub_arctan_inv_239749  have hpi : π = 4 * (4 * arctan (1 / 5) - arctan (1 / 239)) := by750    rw [one_div, one_div, hM]; ring751  have h5 := arctan_pairing (x := 1 / 5) (by norm_num) (by norm_num) m752  have h239 := arctan_pairing (x := 1 / 239) (by norm_num) (by norm_num) m753  rw [machinLo, machinHi, hpi]754  constructor <;> linarith [h5.1, h5.2, h239.1, h239.2]755756/-- 13:E3 — the rational bracket of `π` at `m = 12`, the ends of the pairing enclosure as reduced fractions757(width below `10⁻³⁶`): the bracket on which the core's `arcsin_tail_bound` decides the tail bound of the arcsin758chain for `1 ≤ n ≤ 40`. -/759theorem pi_bracket_24 :760    (56982451095683495439374565467485478486061627198245408555021816811556209980957932490824931053425856737444302864615815079280095539452134822710663747992660383090256176690756 : ℝ) / 18138077522740431478132504469278196026908888402936691374051205499784758924249616118578433027852823624088713136757082253607690672547607224629473421373404562473297119140625 ≤ π ∧761    π ≤ (130195783561461477719700582162729520693370052310728319298679169305810308737653928066126520396560009514814646871106941551053006194003594103465911391825667397563687081581706376 : ℝ) / 41442605047058247458496271511585593410122504578565869919087156374128208580482492892372746919359245529262855323388051816332995956263674891122406052090809680521488189697265625 := by762  have h := machin_pairing 12763  have hLo : machinLo 12 = (56982451095683495439374565467485478486061627198245408555021816811556209980957932490824931053425856737444302864615815079280095539452134822710663747992660383090256176690756 : ℝ) / 18138077522740431478132504469278196026908888402936691374051205499784758924249616118578433027852823624088713136757082253607690672547607224629473421373404562473297119140625 := by764    rw [machinLo, arctanSum, arctanSum]; simp only [Finset.sum_range_succ, Finset.sum_range_zero]; norm_num765  have hHi : machinHi 12 = (130195783561461477719700582162729520693370052310728319298679169305810308737653928066126520396560009514814646871106941551053006194003594103465911391825667397563687081581706376 : ℝ) / 41442605047058247458496271511585593410122504578565869919087156374128208580482492892372746919359245529262855323388051816332995956263674891122406052090809680521488189697265625 := by766    rw [machinHi, arctanSum, arctanSum]; simp only [Finset.sum_range_succ, Finset.sum_range_zero]; norm_num767  rw [hLo] at h; rw [hHi] at h768  exact h769770/-- The binary64 constant nearest `π`: `884279719003555 / 2^48`. -/771noncomputable def binary64Pi : ℝ := 884279719003555 / 2 ^ 48772773/-- 13:E4, 13:I2 — the binary64 readout of `π`: `π` and `M_10` lie within the half-ulp `2⁻⁵²` of the binary64 constant774(Mathlib's twenty-digit bracket of `π`), and no `M_N` with `N ≤ 9` does: `N = 10` is minimal. -/775theorem readout_binary64_pi :776    |π - binary64Pi| < 1 / 2 ^ 52 ∧ |machin 10 - binary64Pi| < 1 / 2 ^ 52 ∧ ∀ N ≤ 9, 1 / 2 ^ 52 < |machin N - binary64Pi| := by777  refine ⟨?_, ?_, ?_⟩778  · have h1 := Real.pi_gt_d20; have h2 := Real.pi_lt_d20779    rw [binary64Pi, abs_lt]; constructor <;> norm_num at h1 h2 ⊢ <;> linarith780  · rw [machin, arctanSum, arctanSum, binary64Pi, abs_lt]; simp only [Finset.sum_range_succ, Finset.sum_range_zero]781    constructor <;> norm_num782  · intro N hN783    interval_cases N <;> rw [machin, arctanSum, arctanSum, binary64Pi, lt_abs] <;> simp only [Finset.sum_range_succ, Finset.sum_range_zero] <;> norm_num784785/-- The Leibniz partial sums `S_m = Σ_{n < m} (−1)^n/(2n+1)`. -/786noncomputable def leibnizSum (m : ℕ) : ℝ := ∑ n ∈ range m, (-1 : ℝ) ^ n * (1 / (2 * n + 1))787788/-- 13:E4, 13:E5 — the Gregory brackets, the base case of the pairing: `S_{2m} ≤ π/4 ≤ S_{2m+1}`, of width789`1/(4m+1)` — the Leibniz chain's `2^k` steps per `k` binary digits. -/790theorem gregory_brackets (m : ℕ) : leibnizSum (2 * m) ≤ π / 4 ∧ π / 4 ≤ leibnizSum (2 * m + 1) ∧791    leibnizSum (2 * m + 1) - leibnizSum (2 * m) = 1 / (4 * m + 1) := by792  have hT : Tendsto leibnizSum atTop (𝓝 (π / 4)) := by793    have h := Real.tendsto_sum_pi_div_four794    refine h.congr' (Eventually.of_forall fun m => ?_)795    simp only [leibnizSum]; refine sum_congr rfl fun i _ => ?_; rw [mul_one_div]796  have hfa : Antitone (fun n : ℕ => (1 : ℝ) / (2 * n + 1)) := by797    intro a b hab; apply one_div_le_one_div_of_le (by positivity)798    have : (a : ℝ) ≤ b := by exact_mod_cast hab799    linarith800  refine ⟨Antitone.alternating_series_le_tendsto hT hfa m, Antitone.tendsto_le_alternating_series hT hfa m, ?_⟩801  rw [leibnizSum, leibnizSum, sum_range_succ]802  have : (-1 : ℝ) ^ (2 * m) = 1 := by rw [pow_mul]; norm_num803  rw [this]; push_cast; ring804805/-- 13:E5 — a factorial-rate chain exists for every real by rounding: `|x − ⌊x·n!⌋/n!| < 1/n!`, so the806feasibility split is by kind of chain, not by rate. -/807theorem rounding_chain (x : ℝ) (n : ℕ) : |x - (⌊x * n.factorial⌋ : ℝ) / n.factorial| < 1 / n.factorial := by808  have hf : (0 : ℝ) < n.factorial := by positivity809  have h1 := Int.floor_le (x * n.factorial)810  have h2 := Int.lt_floor_add_one (x * n.factorial)811  have e : x - (⌊x * n.factorial⌋ : ℝ) / n.factorial = (x * n.factorial - ⌊x * n.factorial⌋) / n.factorial := by812    field_simp813  rw [e, abs_div, abs_of_pos hf, div_lt_div_iff_of_pos_right hf, abs_lt]814  constructor <;> linarith815816end machin817818819/-- Kurepa's left factorial `!n = Σ_{k<n} k!`. -/820def kurepa (n : ℕ) : ℕ := ∑ k ∈ range n, k !821822/-- The alternating factorial sum `A(n) = Σ_{k<n} (−1)^k k!`. -/823def altFact (n : ℕ) : ℤ := ∑ k ∈ range n, (-1 : ℤ) ^ k * (k ! : ℤ)824825/-! ## The wall, over any field of characteristic `p` with Wilson's value826827Everything is proved once over a field `K` in which `p = 0`, `(p−1)! = −1` and `k! ≠ 0` for `k ≤ p − 1`;828the section `prime` instantiates `K := ZMod p` (whose instances under `Fact p.Prime` are not `ring`-friendly). -/829section wall830831variable {K : Type*} [Field K]832833theorem neg_one_pow_mul_self (k : ℕ) : (-1 : K) ^ k * (-1) ^ k = 1 := by834  rw [← pow_add, ← two_mul, pow_mul]; simp835836theorem neg_one_pow_sub_of_pow_eq_one {a k : ℕ} (h : (-1 : K) ^ a = 1) (hk : k ≤ a) :837    (-1 : K) ^ (a - k) = (-1) ^ k := by838  have : (-1 : K) ^ (a - k) * ((-1) ^ k * (-1) ^ k) = (-1) ^ a * (-1) ^ k := by839    rw [← mul_assoc, ← pow_add, Nat.sub_add_cancel hk]840  rwa [neg_one_pow_mul_self, mul_one, h, one_mul] at this841842theorem natCast_pred_sub (p : ℕ) (hp0 : (p : K) = 0) (h1 : 1 ≤ p) (k : ℕ) (hk : k ≤ p - 1) :843    ((p - 1 - k : ℕ) : K) = -((k : K) + 1) := by844  rw [Nat.cast_sub hk, Nat.cast_sub h1, hp0]; ring845846theorem factorial_mul_reflect (p : ℕ) (hp0 : (p : K) = 0) (hw : (((p - 1) ! : ℕ) : K) = -1)847    (h1 : 1 ≤ p) (k : ℕ) (hk : k ≤ p - 1) :848    ((k ! : ℕ) : K) * (((p - 1 - k) ! : ℕ) : K) = -(-1) ^ k := by849  induction k with850  | zero => rw [Nat.factorial_zero, Nat.cast_one, one_mul, Nat.sub_zero, hw, pow_zero]851  | succ k ih =>852    have hk' : k ≤ p - 1 := Nat.le_of_succ_le hk853    have e : p - 1 - k = (p - 1 - (k + 1)) + 1 := by omega854    have := ih hk'855    rw [e, Nat.factorial_succ, ← e, Nat.cast_mul, natCast_pred_sub p hp0 h1 k hk'] at this856    rw [Nat.factorial_succ, Nat.cast_mul, Nat.cast_add, Nat.cast_one]857    linear_combination -this858859theorem wilson_reflection (p : ℕ) (hp0 : (p : K) = 0) (hw : (((p - 1) ! : ℕ) : K) = -1)860    (h1 : 1 ≤ p) (k : ℕ) (hk : k ≤ p - 1) :861    ((k ! : ℕ) : K)⁻¹ = -(-1) ^ k * (((p - 1 - k) ! : ℕ) : K) := by862  apply inv_eq_of_mul_eq_one_right863  linear_combination -(-1 : K) ^ k * factorial_mul_reflect p hp0 hw h1 k hk + neg_one_pow_mul_self (K := K) k864865theorem ascFactorial_reflect (p : ℕ) (hp0 : (p : K) = 0) (hw : (((p - 1) ! : ℕ) : K) = -1)866    (hfac : ∀ k, k ≤ p - 1 → ((k ! : ℕ) : K) ≠ 0) (h1 : 1 ≤ p) (k : ℕ) (hk : k ≤ p - 1) :867    (((k + 1).ascFactorial (p - 1 - k) : ℕ) : K) = (-1) ^ k * (((p - 1 - k) ! : ℕ) : K) := by868  apply mul_left_cancel₀ (hfac k hk)869  have hA : ((k ! : ℕ) : K) * ((k + 1).ascFactorial (p - 1 - k) : ℕ) = -1 := by870    rw [← Nat.cast_mul, Nat.factorial_mul_ascFactorial, Nat.add_sub_cancel' hk, hw]871  linear_combination hA - (-1 : K) ^ k * factorial_mul_reflect p hp0 hw h1 k hk + neg_one_pow_mul_self (K := K) k872873theorem derangements_wall (p : ℕ) (hp0 : (p : K) = 0) (hw : (((p - 1) ! : ℕ) : K) = -1)874    (hfac : ∀ k, k ≤ p - 1 → ((k ! : ℕ) : K) ≠ 0) (h1 : 1 ≤ p) :875    ((numDerangements (p - 1) : ℕ) : K) = (kurepa p : K) := by876  have h := numDerangements_sum (p - 1)877  have hcast : ((numDerangements (p - 1) : ℕ) : K) = ((numDerangements (p - 1) : ℤ) : K) := by878    rw [Int.cast_natCast]879  rw [hcast, h, Int.cast_sum]880  simp only [Int.cast_mul, Int.cast_pow, Int.cast_neg, Int.cast_one, Int.cast_natCast]881  rw [Nat.sub_add_cancel h1]882  unfold kurepa883  rw [Nat.cast_sum, ← sum_range_reflect (fun j => ((j ! : ℕ) : K)) p]884  apply sum_congr rfl885  intro k hk886  have hk' : k ≤ p - 1 := by have := mem_range.1 hk; omega887  rw [ascFactorial_reflect p hp0 hw hfac h1 k hk', ← mul_assoc, neg_one_pow_mul_self, one_mul]888889theorem derangements_succ_cast (n : ℕ) :890    ((numDerangements (n + 1) : ℕ) : K) = ((n : K) + 1) * (numDerangements n : ℕ) - (-1) ^ n := by891  have := congrArg (fun z : ℤ => (z : K)) (numDerangements_succ n)892  simp only [Int.cast_natCast, Int.cast_sub, Int.cast_mul, Int.cast_add, Int.cast_one, Int.cast_pow,893    Int.cast_neg] at this894  exact this895896theorem neg_one_pow_pred_of_odd (p : ℕ) (hodd : Odd p) : (-1 : K) ^ (p - 1) = 1 := by897  obtain ⟨m, hm⟩ := hodd898  rw [hm, Nat.add_sub_cancel, pow_mul]; simp899900theorem derangements_antiperiodic (p : ℕ) (hp0 : (p : K) = 0) (hodd : Odd p) (n : ℕ) :901    ((numDerangements (n + p) : ℕ) : K) = -((numDerangements n : ℕ) : K) := by902  have hneg : (-1 : K) ^ p = -1 := hodd.neg_one_pow903  have h1 : 1 ≤ p := hodd.pos904  induction n with905  | zero =>906    have h := derangements_succ_cast (K := K) (p - 1)907    rw [Nat.sub_add_cancel h1] at h908    rw [zero_add, h, neg_one_pow_pred_of_odd p hodd, numDerangements_zero, Nat.cast_one,909      Nat.cast_sub h1, hp0]910    ring911  | succ n ih =>912    rw [show n + 1 + p = (n + p) + 1 by omega, derangements_succ_cast, ih,913      derangements_succ_cast, pow_add, hneg, Nat.cast_add, hp0]914    ring915916theorem series_duals (p : ℕ) (hp0 : (p : K) = 0) (hw : (((p - 1) ! : ℕ) : K) = -1) (hodd : Odd p) :917    (∑ k ∈ range p, (-1 : K) ^ k * ((k ! : ℕ) : K)⁻¹) = -(kurepa p : K) ∧918    (∑ k ∈ range p, ((k ! : ℕ) : K)⁻¹) = -((altFact p : ℤ) : K) := by919  have h1 : 1 ≤ p := hodd.pos920  constructor921  · unfold kurepa922    rw [Nat.cast_sum, ← sum_range_reflect (fun j => ((j ! : ℕ) : K)) p, ← sum_neg_distrib]923    apply sum_congr rfl924    intro k hk925    have hk' : k ≤ p - 1 := by have := mem_range.1 hk; omega926    rw [wilson_reflection p hp0 hw h1 k hk']927    linear_combination -((((p - 1 - k) ! : ℕ) : K)) * neg_one_pow_mul_self (K := K) k928  · unfold altFact929    rw [Int.cast_sum]930    simp only [Int.cast_mul, Int.cast_pow, Int.cast_neg, Int.cast_one, Int.cast_natCast]931    rw [← sum_range_reflect (fun j => (-1 : K) ^ j * ((j ! : ℕ) : K)) p, ← sum_neg_distrib]932    apply sum_congr rfl933    intro k hk934    have hk' : k ≤ p - 1 := by have := mem_range.1 hk; omega935    rw [wilson_reflection p hp0 hw h1 k hk',936      neg_one_pow_sub_of_pow_eq_one (neg_one_pow_pred_of_odd p hodd) hk']937    ring938939theorem tower_e_exact (p : ℕ) (hp0 : (p : K) = 0) (hodd : Odd p)940    (hfacp : ∀ m, 1 ≤ m → (((m * p) ! : ℕ) : K) = 0) (m : ℕ) (hm : 1 ≤ m) (e δ : K)941    (hδ : δ = (-1) ^ m * e) :942    (((m * p) ! : ℕ) : K) = 0 ∧ ((numDerangements (m * p) : ℕ) : K) = (-1) ^ m ∧943    ((((m * p) ! : ℕ) : K) + δ) / ((numDerangements (m * p) : ℕ) : K) = e := by944  have hder : ∀ m, ((numDerangements (m * p) : ℕ) : K) = (-1) ^ m := by945    intro m946    induction m with947    | zero => rw [Nat.zero_mul, numDerangements_zero, Nat.cast_one, pow_zero]948    | succ m ih => rw [Nat.succ_mul, derangements_antiperiodic p hp0 hodd, ih, pow_succ, mul_neg_one]949  refine ⟨hfacp m hm, hder m, ?_⟩950  rw [hfacp m hm, hder, zero_add, hδ]951  exact mul_div_cancel_left₀ e (pow_ne_zero m (neg_ne_zero.2 one_ne_zero))952953/-- The tail identity: `j! · !(p−1−j) = (−1)^j · (K(p) − K(j))` for `0 ≤ j ≤ p − 1` — the derangement residue954line read from the wall is the sequence of tails `Σ_{m=j}^{p−1} m!` of Kurepa's left factorial. -/955theorem tail_identity (p : ℕ) (hp0 : (p : K) = 0) (hw : (((p - 1) ! : ℕ) : K) = -1)956    (hfac : ∀ k, k ≤ p - 1 → ((k ! : ℕ) : K) ≠ 0) (h1 : 1 ≤ p) (j : ℕ) (hj : j ≤ p - 1) :957    ((j ! : ℕ) : K) * ((numDerangements (p - 1 - j) : ℕ) : K) = (-1) ^ j * ((kurepa p : K) - (kurepa j : K)) := by958  have hcast : ((numDerangements (p - 1 - j) : ℕ) : K) = ((numDerangements (p - 1 - j) : ℤ) : K) := by959    rw [Int.cast_natCast]960  rw [hcast, numDerangements_sum, Int.cast_sum]961  simp only [Int.cast_mul, Int.cast_pow, Int.cast_neg, Int.cast_one, Int.cast_natCast]962  rw [Finset.mul_sum]963  have hterm : ∀ k ∈ range (p - 1 - j + 1),964      ((j ! : ℕ) : K) * ((-1) ^ k * (((k + 1).ascFactorial (p - 1 - j - k) : ℕ) : K)) =965        (-1) ^ j * (((p - 1 - k) ! : ℕ) : K) := by966    intro k hk967    have hk' : k ≤ p - 1 - j := by have := mem_range.1 hk; omega968    have hA : ((k ! : ℕ) : K) * (((k + 1).ascFactorial (p - 1 - j - k) : ℕ) : K) = (((p - 1 - j) ! : ℕ) : K) := by969      rw [← Nat.cast_mul, Nat.factorial_mul_ascFactorial, Nat.add_sub_cancel' hk']970    have hjr := factorial_mul_reflect p hp0 hw h1 j hj971    have hkr := factorial_mul_reflect p hp0 hw h1 k (by omega)972    apply mul_left_cancel₀ (hfac k (by omega))973    linear_combination (-1 : K) ^ k * ((j ! : ℕ) : K) * hA + (-1 : K) ^ k * hjr - (-1 : K) ^ j * hkr974  rw [Finset.sum_congr rfl hterm, ← Finset.mul_sum]975  congr 1976  have hn : p - 1 - j + 1 = p - j := by omega977  rw [hn]978  have hre : ∀ k ∈ range (p - j), (((p - 1 - k) ! : ℕ) : K) = (fun i => (((j + i) ! : ℕ) : K)) ((p - j) - 1 - k) := by979    intro k hk980    have := mem_range.1 hk981    show (((p - 1 - k) ! : ℕ) : K) = (((j + ((p - j) - 1 - k)) ! : ℕ) : K)982    congr 2; omega983  rw [Finset.sum_congr rfl hre, Finset.sum_range_reflect (fun i => (((j + i) ! : ℕ) : K)) (p - j),984    ← Finset.sum_Ico_eq_sum_range (fun m => ((m ! : ℕ) : K)) j p]985  unfold kurepa986  rw [Nat.cast_sum, Nat.cast_sum, eq_sub_iff_add_eq, add_comm, Finset.sum_range_add_sum_Ico _ (by omega)]987988end wall989990/-! ## The prime shell: `K := ZMod p` -/991section prime992993variable (p : ℕ) [hp : Fact p.Prime]994995theorem factorial_ne_zero_zmod (k : ℕ) (hk : k ≤ p - 1) : ((k ! : ℕ) : ZMod p) ≠ 0 := by996  rw [Ne, ZMod.natCast_eq_zero_iff]997  intro h998  have := (hp.out.dvd_factorial).1 h999  have := hp.out.two_le1000  omega10011002theorem factorial_mul_prime_eq_zero (m : ℕ) (hm : 1 ≤ m) : (((m * p) ! : ℕ) : ZMod p) = 0 := by1003  rw [ZMod.natCast_eq_zero_iff]1004  exact (hp.out.dvd_factorial).2 (Nat.le_mul_of_pos_left p hm)10051006/-- 13:F1 — Wilson reflection: `1/k! ≡ −(−1)^k (p−1−k)! (mod p)` for `0 ≤ k ≤ p − 1`, from Wilson's1007theorem `(p−1)! ≡ −1` and `p − j ≡ −j`. -/1008theorem wilson_reflection_zmod (k : ℕ) (hk : k ≤ p - 1) :1009    ((k ! : ℕ) : ZMod p)⁻¹ = -(-1) ^ k * (((p - 1 - k) ! : ℕ) : ZMod p) :=1010  wilson_reflection p (ZMod.natCast_self p) (ZMod.wilsons_lemma p) hp.out.one_le k hk10111012/-- 13:F2, 13:J6 — the wall identity: `!(p−1) ≡ !p (mod p)` for every prime `p` — the derangement number at the wall1013is Kurepa's left factorial (the odd-prime case of the Mijajlović–Šami congruence), from Wilson reflection. -/1014theorem derangements_wall_zmod : ((numDerangements (p - 1) : ℕ) : ZMod p) = (kurepa p : ZMod p) :=1015  derangements_wall p (ZMod.natCast_self p) (ZMod.wilsons_lemma p) (factorial_ne_zero_zmod p) hp.out.one_le10161017/-- 13:F2 — the terminal residue of `e`: `⟦ε_{p−1}⟧ = (p−1)!/!(p−1) = −(!p)⁻¹`, and the terminal link exists1018(`!(p−1) ≢ 0`) exactly when `p ∤ !p`. -/1019theorem terminal_residue :1020    (((p - 1) ! : ℕ) : ZMod p) / ((numDerangements (p - 1) : ℕ) : ZMod p) = -(kurepa p : ZMod p)⁻¹ ∧1021    (((numDerangements (p - 1) : ℕ) : ZMod p) ≠ 0 ↔ ¬ p ∣ kurepa p) := by1022  rw [derangements_wall_zmod, ZMod.wilsons_lemma, div_eq_mul_inv, neg_one_mul, Ne,1023    ZMod.natCast_eq_zero_iff]1024  exact ⟨rfl, Iff.rfl⟩10251026/-- 13:F3 — antiperiodicity: `!(n + p) ≡ −!n (mod p)` for every odd prime `p` and every `n ≥ 0`, so1027`!n mod p` depends on `n mod 2p`; the blind set always contains `n = 1` (`!1 = 0`). -/1028theorem derangements_antiperiodic_zmod (hp2 : p ≠ 2) (n : ℕ) :1029    ((numDerangements (n + p) : ℕ) : ZMod p) = -((numDerangements n : ℕ) : ZMod p) ∧1030    numDerangements 1 = 0 :=1031  ⟨derangements_antiperiodic p (ZMod.natCast_self p) (hp.out.odd_of_ne_two hp2) n, numDerangements_one⟩10321033/-- 13:F4 — the series duals at the wall: `Σ_{k<p} (−1)^k/k! ≡ −!p` and `Σ_{k<p} 1/k! ≡ −A(p)`, `A(p)` the1034alternating factorial sum, for every odd prime `p`. -/1035theorem series_duals_zmod (hp2 : p ≠ 2) :1036    (∑ k ∈ range p, (-1 : ZMod p) ^ k * ((k ! : ℕ) : ZMod p)⁻¹) = -(kurepa p : ZMod p) ∧1037    (∑ k ∈ range p, ((k ! : ℕ) : ZMod p)⁻¹) = -((altFact p : ℤ) : ZMod p) :=1038  series_duals p (ZMod.natCast_self p) (ZMod.wilsons_lemma p) (hp.out.odd_of_ne_two hp2)10391040/-- 13:F7 — the fixed-shell tower of `e` is exact at every grade: `(mp)! ≡ 0` and `!(mp) ≡ (−1)^m (mod p)`1041for `m ≥ 1`, so `q_m = ((mp)! + δ_m)/!(mp)` reads `e_p` on the shell whenever `δ_m ≡ (−1)^m e_p`. -/1042theorem tower_e_exact_zmod (hp2 : p ≠ 2) (m : ℕ) (hm : 1 ≤ m) (e δ : ZMod p) (hδ : δ = (-1) ^ m * e) :1043    (((m * p) ! : ℕ) : ZMod p) = 0 ∧ ((numDerangements (m * p) : ℕ) : ZMod p) = (-1) ^ m ∧1044    ((((m * p) ! : ℕ) : ZMod p) + δ) / ((numDerangements (m * p) : ℕ) : ZMod p) = e :=1045  tower_e_exact p (ZMod.natCast_self p) (hp.out.odd_of_ne_two hp2) (factorial_mul_prime_eq_zero p) m hm e δ hδ10461047/-- 13:F8, 13:Z1 — the tail identity on the shell: `j! · !(p−1−j) ≡ (−1)^j (!p − !j) (mod p)`, `0 ≤ j ≤ p − 1`. -/1048theorem tail_identity_zmod (j : ℕ) (hj : j ≤ p - 1) :1049    ((j ! : ℕ) : ZMod p) * ((numDerangements (p - 1 - j) : ℕ) : ZMod p) =1050      (-1) ^ j * ((kurepa p : ZMod p) - (kurepa j : ZMod p)) :=1051  tail_identity p (ZMod.natCast_self p) (ZMod.wilsons_lemma p) (factorial_ne_zero_zmod p) hp.out.one_le j hj10521053/-- 13:F8, 13:Z1 — the collision reading of the blind set: for `n ≤ p − 1`, `!n ≡ 0 (mod p)` exactly when the partial1054sum `!(p−1−n)` of the left factorial collides with `!p`; Kurepa's hypothesis at `p` is the case `n = p − 1`,1055`!(0) = 0 ≢ !p`; the universal blind scale `n = 1` is `!(p−2) ≡ !p` (the tail `(p−2)! + (p−1)! ≡ 0`). -/1056theorem blind_iff_collision (n : ℕ) (hn : n ≤ p - 1) :1057    (((numDerangements n : ℕ) : ZMod p) = 0 ↔ (kurepa (p - 1 - n) : ZMod p) = (kurepa p : ZMod p)) ∧1058    (kurepa (p - 2) : ZMod p) = (kurepa p : ZMod p) := by1059  have key : ∀ n, n ≤ p - 1 →1060      (((numDerangements n : ℕ) : ZMod p) = 0 ↔ (kurepa (p - 1 - n) : ZMod p) = (kurepa p : ZMod p)) := by1061    intro n hn1062    have h := tail_identity_zmod p (p - 1 - n) (by omega)1063    rw [show p - 1 - (p - 1 - n) = n by omega] at h1064    have hf := factorial_ne_zero_zmod p (p - 1 - n) (by omega)1065    have hs : ((-1 : ZMod p) ^ (p - 1 - n)) ≠ 0 := by1066      apply pow_ne_zero; intro h11067      exact (one_ne_zero : (1 : ZMod p) ≠ 0) (neg_eq_zero.1 h1)1068    constructor1069    · intro h01070      rw [h0, mul_zero] at h1071      have := (mul_eq_zero.1 h.symm).resolve_left hs1072      exact (sub_eq_zero.1 this).symm1073    · intro hc1074      have : ((-1 : ZMod p) ^ (p - 1 - n)) * ((kurepa p : ZMod p) - (kurepa (p - 1 - n) : ZMod p)) = 0 := by1075        rw [hc, sub_self, mul_zero]1076      rw [← h] at this1077      exact (mul_eq_zero.1 this).resolve_left hf1078  refine ⟨key n hn, ?_⟩1079  have h2 := hp.out.two_le1080  have := (key 1 (by omega)).1 (by rw [numDerangements_one, Nat.cast_zero])1081  rwa [show p - 1 - 1 = p - 2 by omega] at this10821083end prime1084108510861087/-! ## The wall hierarchy of `π`: the Wallis chain `w_n = 16^n/(n C_n²)` on the shell -/1088section wallpi10891090variable {K : Type*} [Field K]10911092theorem sq_eq_one_of_eq_neg_one_pow (c : K) (m : ℕ) (h : c = (-1) ^ m) : c ^ 2 = 1 := by1093  rw [h, ← pow_mul, mul_comm, pow_mul]; norm_num10941095/-- `C(p−1, k) ≡ (−1)^k`, from `C(n, k+1)(k+1) = C(n, k)(n − k)` and `p − 1 − k ≡ −(k+1)`. -/1096theorem choose_pred_eq_neg_one_pow (p : ℕ) (hp0 : (p : K) = 0) (h1 : 1 ≤ p)1097    (hunit : ∀ j, 1 ≤ j → j ≤ p - 1 → (j : K) ≠ 0) (k : ℕ) (hk : k ≤ p - 1) :1098    ((choose (p - 1) k : ℕ) : K) = (-1) ^ k := by1099  induction k with1100  | zero => rw [choose_zero_right, Nat.cast_one, pow_zero]1101  | succ k ih =>1102    have hk' : k ≤ p - 1 := Nat.le_of_succ_le hk1103    have h := congrArg (fun m : ℕ => (m : K)) (Nat.choose_succ_right_eq (p - 1) k)1104    simp only [Nat.cast_mul, Nat.cast_add, Nat.cast_one] at h1105    rw [ih hk', Nat.cast_sub hk', Nat.cast_sub h1, hp0] at h1106    have hne : ((k : K) + 1) ≠ 0 := by1107      have := hunit (k + 1) (by omega) hk1108      rwa [Nat.cast_add, Nat.cast_one] at this1109    apply mul_right_cancel₀ hne1110    rw [h, pow_succ]; ring11111112theorem half_wall_generic (m : K) (h2m : (2 : K) * m = -1) (x c : K)1113    (hx : x = 1) (hc : c ^ 2 = 1) :1114    x / (m * c ^ 2) = -2 ∧ m⁻¹ = -2 ∧ (4 : K) * m = -2 := by1115  have hinv : m⁻¹ = -2 := inv_eq_of_mul_eq_one_right (by linear_combination -h2m)1116  refine ⟨?_, hinv, by linear_combination 2 * h2m⟩1117  rw [hx, hc, mul_one, one_div, hinv]11181119theorem quarter_wall_generic (κ a b c : K) (hκ : (4 : K) * κ = -1) (h2 : (2 : K) ≠ 0)1120    (hC : c = 2 * a) (ha : a ≠ 0) (hab : a ^ 2 + b ^ 2 = 0) (x : K) (hx : x = 1) :1121    x / (κ * c ^ 2) = -(a ^ 2)⁻¹ ∧ -(a ^ 2)⁻¹ = (b ^ 2)⁻¹ := by1122  have hκ0 : κ ≠ 0 := by1123    intro h; rw [h, mul_zero] at hκ; exact one_ne_zero (by linear_combination hκ)1124  have hc0 : c ≠ 0 := by rw [hC]; exact mul_ne_zero h2 ha1125  have hinv : (a ^ 2)⁻¹ * a ^ 2 = 1 := inv_mul_cancel₀ (pow_ne_zero 2 ha)1126  constructor1127  · rw [div_eq_iff (mul_ne_zero hκ0 (pow_ne_zero 2 hc0)), hx, hC]1128    linear_combination 4 * κ * hinv + hκ1129  · rw [neg_inv]; congr 1; linear_combination -hab11301131theorem first_revival_generic (x c d : K) (h2 : (2 : K) ≠ 0) (hx : x = 16) (hc : c = 2) (hd : d = 1) :1132    2 * x / (d * c ^ 2) = 8 := by1133  subst hx hc hd; field_simp; ring11341135theorem tower_pi_generic (x c d δ κ : K) (h2 : (2 : K) ≠ 0) (hx : x = 16) (hc : c = 2) (hd : d = 1)1136    (hδ : δ = -34) (hκ : (4 : K) * κ = -1) :1137    (2 * x + δ) / (d * c ^ 2) = 2 * κ := by1138  subst hx hc hd hδ; field_simp; linear_combination -2 * hκ11391140end wallpi11411142section primepi11431144variable (p : ℕ) [hp : Fact p.Prime]11451146theorem natCast_ne_zero_of_lt (j : ℕ) (hj0 : 1 ≤ j) (hj : j < p) : (j : ZMod p) ≠ 0 := by1147  rw [Ne, ZMod.natCast_eq_zero_iff]1148  intro h1149  have := Nat.le_of_dvd (by omega) h1150  omega11511152theorem two_ne_zero_zmod (hp2 : p ≠ 2) : (2 : ZMod p) ≠ 0 := by1153  have := natCast_ne_zero_of_lt p 2 (by omega) (lt_of_le_of_ne hp.out.two_le (Ne.symm hp2))1154  rwa [Nat.cast_ofNat] at this11551156/-- 13:G1 — the legibility window: `p ∤ C(2n,n)` for `1 ≤ n ≤ (p−1)/2` and `p ∣ C(2n,n)` for1157`(p−1)/2 < n < p` — the residue line of the Wallis chain is defined exactly on `[1, (p−1)/2]`. -/1158theorem legibility_window (n : ℕ) :1159    (2 * n ≤ p - 1 → ¬ p ∣ centralBinom n) ∧ (p ≤ 2 * n → n < p → p ∣ centralBinom n) := by1160  have hfac : centralBinom n * n ! * n ! = (2 * n) ! := by1161    have := Nat.choose_mul_factorial_mul_factorial (show n ≤ 2 * n by omega)1162    rwa [show 2 * n - n = n by omega, ← centralBinom_eq_two_mul_choose] at this1163  constructor1164  · intro hn hdvd1165    have : p ∣ (2 * n) ! := hfac ▸ Dvd.dvd.mul_right (Dvd.dvd.mul_right hdvd _) _1166    have := (hp.out.dvd_factorial).1 this1167    have := hp.out.pos1168    omega1169  · intro hn hnp1170    have h1 : p ∣ (2 * n) ! := (hp.out.dvd_factorial).2 hn1171    rw [← hfac] at h11172    have hnf : ¬ p ∣ n ! := fun h => by have := (hp.out.dvd_factorial).1 h; omega1173    rcases (hp.out.dvd_mul).1 h1 with h | h1174    · rcases (hp.out.dvd_mul).1 h with h | h1175      · exact h1176      · exact absurd h hnf1177    · exact absurd h hnf11781179/-- 13:G2 — the half-wall terminus, the calibration face: with `m = (p−1)/2`, `16^m ≡ 1`,1180`C(2m,m)² ≡ 1`, and `⟦w_m⟧ = m⁻¹ = −2` for every odd prime; the identity `4·π_A ≡ −2` beside it. -/1181theorem half_wall_terminus (hp2 : p ≠ 2) (m : ℕ) (hm : p = 2 * m + 1) :1182    (16 : ZMod p) ^ m = 1 ∧ ((centralBinom m : ℕ) : ZMod p) ^ 2 = 1 ∧1183    wallisW m = (-2 : ZMod p) ∧ (m : ZMod p)⁻¹ = -2 ∧ (4 : ZMod p) * m = -2 := by1184  have h2 : (2 : ZMod p) ≠ 0 := two_ne_zero_zmod p hp21185  have h4 : (4 : ZMod p) ≠ 0 := by1186    have : (4 : ZMod p) = 2 * 2 := by norm_num1187    rw [this]; exact mul_ne_zero h2 h21188  have h16 : (16 : ZMod p) ^ m = 1 := by1189    have : (16 : ZMod p) ^ m = (4 : ZMod p) ^ (p - 1) := by1190      rw [show p - 1 = 2 * m by omega, pow_mul]; norm_num1191    rw [this]; exact ZMod.pow_card_sub_one_eq_one h41192  have hC : ((centralBinom m : ℕ) : ZMod p) = (-1) ^ m := by1193    have hm' : m ≤ p - 1 := by omega1194    have := choose_pred_eq_neg_one_pow (K := ZMod p) p (ZMod.natCast_self p) hp.out.one_le1195      (fun j hj0 hj => natCast_ne_zero_of_lt p j hj0 (by omega)) m hm'1196    rw [centralBinom_eq_two_mul_choose, show 2 * m = p - 1 by omega]; exact this1197  have hC2 : ((centralBinom m : ℕ) : ZMod p) ^ 2 = 1 := by1198    exact sq_eq_one_of_eq_neg_one_pow _ m hC1199  have h2m : (2 : ZMod p) * m = -1 := by1200    have : ((2 * m + 1 : ℕ) : ZMod p) = 0 := by rw [← hm]; exact ZMod.natCast_self p1201    push_cast at this1202    exact eq_neg_of_add_eq_zero_left this1203  obtain ⟨hw, hinv, h4m⟩ := half_wall_generic (K := ZMod p) m h2m _ _ h16 hC21204  exact ⟨h16, hC2, hw, hinv, h4m⟩12051206/-- 13:G3 — the quarter-wall two-squares invariant: on `p = 4κ + 1 = a² + b²`, given Gauss's congruence1207`C(2κ,κ) ≡ 2a` (the import A3), `⟦w_κ⟧ = −(a²)⁻¹ = (b²)⁻¹`. -/1208theorem quarter_wall_invariant (κ a b : ℕ) (hκ : p = 4 * κ + 1) (hab : a ^ 2 + b ^ 2 = p)1209    (ha : 0 < a) (hb : 0 < b) (hG : ((centralBinom κ : ℕ) : ZMod p) = 2 * a) :1210    wallisW κ = -((a : ZMod p) ^ 2)⁻¹ ∧ -((a : ZMod p) ^ 2)⁻¹ = ((b : ZMod p) ^ 2)⁻¹ := by1211  have hp2 : p ≠ 2 := by omega1212  have h2 : (2 : ZMod p) ≠ 0 := two_ne_zero_zmod p hp21213  have hκ' : (4 : ZMod p) * κ = -1 := by1214    have : ((4 * κ + 1 : ℕ) : ZMod p) = 0 := by rw [← hκ]; exact ZMod.natCast_self p1215    push_cast at this1216    exact eq_neg_of_add_eq_zero_left this1217  have h16 : (16 : ZMod p) ^ κ = 1 := by1218    have : (16 : ZMod p) ^ κ = (2 : ZMod p) ^ (p - 1) := by1219      rw [show p - 1 = 4 * κ by omega, pow_mul]; norm_num1220    rw [this]; exact ZMod.pow_card_sub_one_eq_one h21221  have hab' : (a : ZMod p) ^ 2 + (b : ZMod p) ^ 2 = 0 := by1222    have : ((a ^ 2 + b ^ 2 : ℕ) : ZMod p) = 0 := by rw [hab]; exact ZMod.natCast_self p1223    push_cast at this; exact this1224  have ha2 : a ≤ a ^ 2 := Nat.le_self_pow (by norm_num) a1225  have hb2 : 1 ≤ b ^ 2 := Nat.one_le_pow _ _ hb1226  have ha' : (a : ZMod p) ≠ 0 := natCast_ne_zero_of_lt p a ha (by omega)1227  exact quarter_wall_generic (K := ZMod p) κ a b _ hκ' h2 hG ha' hab' _ h1612281229/-- Lucas at the first revival and up the tower: `C(2p^{r+1}, p^{r+1}) ≡ C(2p^r, p^r) (mod p)`. -/1230theorem choose_two_mul_pow_succ (r : ℕ) :1231    ((choose (2 * p ^ (r + 1)) (p ^ (r + 1)) : ℕ) : ZMod p) = ((choose (2 * p ^ r) (p ^ r) : ℕ) : ZMod p) := by1232  have hpos : 0 < p := hp.out.pos1233  have h := Choose.choose_modEq_choose_mod_mul_choose_div (p := p) (n := 2 * p ^ (r + 1)) (k := p ^ (r + 1))1234  have e1 : 2 * p ^ (r + 1) % p = 0 := by rw [pow_succ, ← mul_assoc]; exact Nat.mul_mod_left _ _1235  have e2 : p ^ (r + 1) % p = 0 := by rw [pow_succ]; exact Nat.mul_mod_left _ _1236  have e3 : 2 * p ^ (r + 1) / p = 2 * p ^ r := by rw [pow_succ, ← mul_assoc]; exact Nat.mul_div_cancel _ hpos1237  have e4 : p ^ (r + 1) / p = p ^ r := by rw [pow_succ]; exact Nat.mul_div_cancel _ hpos1238  rw [e1, e2, e3, e4, choose_zero_right] at h1239  simp only [Nat.cast_one, one_mul] at h1240  have := (ZMod.intCast_eq_intCast_iff _ _ p).2 h1241  exact_mod_cast this12421243/-- 13:G5, 13:G9 — Lucas on the tower: `C(2p^r, p^r) ≡ 2 (mod p)` for every `r` (the first revival is `r = 1`). -/1244theorem choose_two_mul_pow (r : ℕ) : ((choose (2 * p ^ r) (p ^ r) : ℕ) : ZMod p) = 2 := by1245  induction r with1246  | zero => norm_num1247  | succ r ih => rw [choose_two_mul_pow_succ p r, ih]12481249/-- 13:G5 — the first revival: `⟦v_p⟧ = 2·16^p/((2p+1)·C(2p,p)²) ≡ 8` on every odd prime shell, by Lucas1250(`C(2p,p) ≡ 2`), Fermat (`16^p ≡ 16`) and `2p + 1 ≡ 1`. -/1251theorem first_revival (hp2 : p ≠ 2) :1252    (2 : ZMod p) * 16 ^ p / (((2 * p + 1 : ℕ) : ZMod p) * ((centralBinom p : ℕ) : ZMod p) ^ 2) = 8 := by1253  apply first_revival_generic _ _ _ (two_ne_zero_zmod p hp2)1254  · exact ZMod.pow_card 161255  · rw [centralBinom_eq_two_mul_choose]1256    have := choose_two_mul_pow p 11257    rwa [pow_one] at this1258  · push_cast; rw [ZMod.natCast_self]; ring12591260/-- 13:G9 — the fixed-shell tower of `π`: for `n = p^r`, `r ≥ 1`, `16^n ≡ 16`, `C(2n,n) ≡ 2` and `2n + 1 ≡ 1`,1261so `π̂_{p,r} = (2·16^n + δ)/((2n+1)·C(2n,n)²)` reads `π_A = 2κ` exactly, whenever `δ ≡ −34`. -/1262theorem tower_pi_exact (κ : ℕ) (hκ : p = 4 * κ + 1) (r : ℕ) (hr : 1 ≤ r) (δ : ZMod p) (hδ : δ = -34) :1263    (2 * (16 : ZMod p) ^ (p ^ r) + δ) /1264      (((2 * p ^ r + 1 : ℕ) : ZMod p) * ((centralBinom (p ^ r) : ℕ) : ZMod p) ^ 2) = 2 * κ := by1265  have hp2 : p ≠ 2 := by omega1266  apply tower_pi_generic _ _ _ _ _ (two_ne_zero_zmod p hp2)1267  · exact ZMod.pow_card_pow 161268  · rw [centralBinom_eq_two_mul_choose]; exact choose_two_mul_pow p r1269  · push_cast1270    rw [ZMod.natCast_self, zero_pow (by omega)]; ring1271  · exact hδ1272  · have : ((4 * κ + 1 : ℕ) : ZMod p) = 0 := by rw [← hκ]; exact ZMod.natCast_self p1273    push_cast at this1274    exact eq_neg_of_add_eq_zero_left this12751276end primepi12771278/-! ## The Cayley quarter-turn map (13:C3) -/1279section cayley12801281variable {K : Type*} [Field K]12821283/-- The Cayley quarter-turn map `C(x) = (1 + i x)/(1 − i x)`. -/1284noncomputable def cayley (i x : K) : K := (1 + i * x) / (1 - i * x)12851286/-- 13:C3 — `C(0) = 1` and `C(1) = i` for a quarter turn `i` (`i² = −1`) in characteristic `≠ 2`. -/1287theorem cayley_values (i : K) (hi : i * i = -1) (h2 : (2 : K) ≠ 0) :1288    cayley i 0 = 1 ∧ cayley i 1 = i := by1289  constructor1290  · simp [cayley]1291  · have h1 : 1 - i * 1 ≠ 0 := by1292      intro h; apply h21293      have : i = 1 := by linear_combination -h1294      rw [this] at hi; linear_combination hi1295    unfold cayley1296    rw [div_eq_iff h1]; linear_combination hi12971298/-- 13:C3 — the composition law `C(x)·C(y) = C((x + y)/(1 − xy))`: the rational law is the half-angle form1299of phase composition, with denominators units. -/1300theorem cayley_mul (i x y : K) (hi : i * i = -1) (hx : 1 - i * x ≠ 0) (hy : 1 - i * y ≠ 0)1301    (hxy : 1 - x * y ≠ 0) :1302    cayley i x * cayley i y = cayley i ((x + y) / (1 - x * y)) := by1303  have key : (1 - i * x) * (1 - i * y) = (1 - x * y) - i * (x + y) := by linear_combination x * y * hi1304  have hden : 1 - i * ((x + y) / (1 - x * y)) ≠ 0 := by1305    rw [show 1 - i * ((x + y) / (1 - x * y)) = ((1 - x * y) - i * (x + y)) / (1 - x * y) by1306      field_simp]1307    rw [← key]1308    exact div_ne_zero (mul_ne_zero hx hy) hxy1309  unfold cayley1310  rw [eq_div_iff hden]1311  field_simp1312  linear_combination (-2 * i * x * y * (x + y)) * hi13131314end cayley13151316/-! ## Angular structure: exact calibration of `e` is impossible (13:H3) -/1317section angular13181319open Real13201321/-- 13:H3, 13:I1, 13:I3 — `θ = 2πλ/(p−1) ≠ 1` for every label `λ ≥ 1` and every `p`: `θ = 1` would make `π` rational. -/1322theorem calibration_ne_one (n l : ℕ) (hl : 0 < l) : 2 * π * l / n ≠ 1 := by1323  intro h1324  have hn : (n : ℝ) ≠ 0 := by intro hn; rw [hn, div_zero] at h; exact zero_ne_one h1325  have hl' : (l : ℝ) ≠ 0 := by exact_mod_cast hl.ne'1326  have : π = (n : ℝ) / (2 * l) := by1327    field_simp at h ⊢; linarith1328  exact irrational_pi.ne_rat ((n : ℚ) / (2 * l)) (by rw [this]; push_cast; ring)13291330/-- 13:H3 — `e^{i n} ≠ 1` for every `n ≥ 1`: `e^{i}` is not a root of unity (while `χ(e_p)` is one). -/1331theorem exp_I_ne_one (n : ℕ) (hn : 0 < n) : Complex.exp (n * Complex.I) ≠ 1 := by1332  rw [Ne, Complex.exp_eq_one_iff]1333  rintro ⟨k, hk⟩1334  have h2 : (n : ℂ) * Complex.I = (k * (2 * π)) * Complex.I := by rw [hk]; ring1335  have h1 : (n : ℂ) = k * (2 * π) := mul_right_cancel₀ Complex.I_ne_zero h21336  have h3 : (n : ℝ) = k * (2 * π) := by exact_mod_cast h11337  have hk0 : (k : ℝ) ≠ 0 := by1338    intro h0; rw [h0, zero_mul] at h31339    exact (Nat.cast_pos.2 hn).ne' h31340  exact irrational_pi.ne_rat ((n : ℚ) / (2 * k)) (by push_cast; field_simp; linarith)13411342end angular13431344/-! ## The null experiment: the index condition (13:H5) -/1345section index13461347/-- 13:H5 — the index condition: `u·l ≡ s (mod n)` is solvable with `u` coprime to `n` exactly when1348`gcd(l, n) = gcd(s, n)`. -/1349theorem index_condition (n l s : ℕ) [NeZero n] :1350    (∃ u : ℕ, u.Coprime n ∧ u * l ≡ s [MOD n]) ↔ Nat.gcd l n = Nat.gcd s n := by1351  constructor1352  · rintro ⟨u, hu, h⟩1353    rw [← Nat.ModEq.gcd_eq h, Nat.Coprime.gcd_mul_left_cancel l hu]1354  · intro hg1355    obtain ⟨d, hd⟩ : ∃ d, Nat.gcd l n = d := ⟨_, rfl⟩1356    have hd0 : 0 < d := hd ▸ Nat.gcd_pos_of_pos_right l (NeZero.pos n)1357    obtain ⟨n', hn'⟩ : d ∣ n := hd ▸ Nat.gcd_dvd_right l n1358    obtain ⟨l', hl'⟩ : d ∣ l := hd ▸ Nat.gcd_dvd_left l n1359    obtain ⟨s', hs'⟩ : d ∣ s := (hd ▸ hg : d = Nat.gcd s n) ▸ Nat.gcd_dvd_left s n1360    have hl'c : Nat.Coprime l' n' := by1361      have := Nat.coprime_div_gcd_div_gcd (m := l) (n := n) (hd ▸ hd0)1362      rw [hd] at this1363      rwa [hl', hn', Nat.mul_div_cancel_left _ hd0, Nat.mul_div_cancel_left _ hd0] at this1364    have hs'c : Nat.Coprime s' n' := by1365      have hg' : Nat.gcd s n = d := hd ▸ hg.symm1366      have := Nat.coprime_div_gcd_div_gcd (m := s) (n := n) (hg' ▸ hd0)1367      rw [hg'] at this1368      rwa [hs', hn', Nat.mul_div_cancel_left _ hd0, Nat.mul_div_cancel_left _ hd0] at this1369    have : NeZero n' := ⟨fun h0 => NeZero.ne n (by rw [hn', h0, mul_zero])⟩1370    have hdvd : n' ∣ n := ⟨d, by rw [hn', mul_comm]⟩1371    let U' : (ZMod n')ˣ := ZMod.unitOfCoprime s' hs'c * (ZMod.unitOfCoprime l' hl'c)⁻¹1372    obtain ⟨U, hU⟩ := ZMod.unitsMap_surjective hdvd U'1373    refine ⟨(U : ZMod n).val, ZMod.val_coe_unit_coprime U, ?_⟩1374    have key : (U : ZMod n).val * l' ≡ s' [MOD n'] := by1375      rw [← ZMod.natCast_eq_natCast_iff, Nat.cast_mul, ZMod.natCast_val]1376      have hcast : ((U : ZMod n).cast : ZMod n') = (U' : ZMod n') := by1377        rw [← ZMod.unitsMap_val hdvd, hU]1378      rw [hcast]1379      simp only [U', Units.val_mul, ZMod.coe_unitOfCoprime]1380      rw [mul_assoc, ← ZMod.coe_unitOfCoprime l' hl'c, Units.inv_mul, mul_one]1381    have := Nat.ModEq.mul_left' d key1382    rw [← hn'] at this1383    rw [hl', hs', mul_left_comm]1384    exact this13851386/-- 13:H5 — for an element `g` of order `n` in a monoid: `(g^u)^l = g^s` for some `u` coprime to `n` — some other1387generator of the cycle raised to the label — exactly when `gcd(l, n) = gcd(s, n)`. -/1388theorem index_condition_pow {G : Type*} [Monoid G] (g : G) (hfin : IsOfFinOrder g) (n : ℕ) [NeZero n]1389    (hn : orderOf g = n) (l s : ℕ) :1390    (∃ u : ℕ, u.Coprime n ∧ (g ^ u) ^ l = g ^ s) ↔ Nat.gcd l n = Nat.gcd s n := by1391  rw [← index_condition n l s]1392  apply exists_congr; intro u1393  rw [← pow_mul, hfin.pow_eq_pow_iff_modEq, hn]13941395/-- 13:H5 — the null experiment's index condition on the shell: for a primitive root `g` of `ZMod p`, the1396target `g^s` is `h^l` for some primitive root `h = g^u` (either chirality, `u` coprime to `p − 1`) exactly when1397`gcd(l, p−1) = gcd(s, p−1)`. -/1398theorem index_condition_shell (p : ℕ) [hp : Fact p.Prime] (g : ZMod p) (hg : IsPrimitiveRoot g (p - 1))1399    (l s : ℕ) :1400    (∃ u : ℕ, u.Coprime (p - 1) ∧ (g ^ u) ^ l = g ^ s) ↔ Nat.gcd l (p - 1) = Nat.gcd s (p - 1) := by1401  have h2 := hp.out.two_le1402  have : NeZero (p - 1) := ⟨by omega⟩1403  have hfin : IsOfFinOrder g := orderOf_pos_iff.1 (by rw [← hg.eq_orderOf]; omega)1404  exact index_condition_pow g hfin (p - 1) hg.eq_orderOf.symm l s14051406end index140714081409section calibration1410open Real14111412/-- 13:H4, 13:I1 — the best radian-calibrated shell below `10⁶` (Prop. calib): on `p = 778933`, prime, the residue1413`123966` is a quarter-turn (`123966² ≡ −1 (mod p)`), and the frame angle `θ = 2π·123966/(p − 1)` it labels lies1414within `4·10⁻⁵` of one radian and not within `3.9·10⁻⁵` — the calibration inequality decided from the rational1415bounds `3.141592 < π < 3.141593` of Mathlib, no floating-point value of `π` entering; the count of calibrated shells1416and the nearest-hit comparison are the package's (`e.A1`). -/1417theorem calibrated_778933 :1418    Nat.Prime 778933 ∧ (123966 : ZMod 778933) ^ 2 = -1 ∧1419      |2 * π * 123966 / 778932 - 1| < 4 / 100000 ∧ 39 / 1000000 < |2 * π * 123966 / 778932 - 1| := by1420  have h1 := pi_gt_d61421  have h2 := pi_lt_d61422  refine ⟨by norm_num, by decide, ?_, ?_⟩1423  · rw [abs_lt]; constructor <;> nlinarith1424  · rw [lt_abs]; right; nlinarith14251426end calibration142714281429section wallisQ14301431theorem centralBinom_succ_rat (n : ℕ) :1432    ((centralBinom (n + 1) : ℕ) : ℚ) = 2 * (2 * n + 1) * (centralBinom n : ℚ) / (n + 1) := by1433  have h := congrArg (fun m : ℕ => (m : ℚ)) (Nat.succ_mul_centralBinom_succ n)1434  push_cast at h1435  rw [eq_div_iff (by positivity)]1436  linear_combination h14371438theorem centralBinom_pos_rat (n : ℕ) : (0 : ℚ) < (centralBinom n : ℕ) := by1439  exact_mod_cast centralBinom_pos n14401441/-- 13:E2 — the exact width identity `w_n − v_n = w_n/(2n+1)` for `n ≥ 1`. -/1442theorem wallis_width (n : ℕ) (hn : 1 ≤ n) :1443    wallisW n - wallisV n = (wallisW n : ℚ) / (2 * n + 1) := by1444  have hn' : (0 : ℚ) < n := by exact_mod_cast hn1445  have hC := centralBinom_pos_rat n1446  unfold wallisW wallisV1447  field_simp1448  ring14491450/-- 13:E2 — `v_{n+1} = v_n · 4(n+1)²/((2n+3)(2n+1))`. -/1451theorem wallisV_succ (n : ℕ) :1452    (wallisV (n + 1) : ℚ) = wallisV n * (4 * (n + 1) ^ 2 / ((2 * n + 3) * (2 * n + 1))) := by1453  have hC := centralBinom_pos_rat n1454  unfold wallisV1455  rw [centralBinom_succ_rat]1456  push_cast1457  field_simp1458  ring14591460theorem wallisV_pos (n : ℕ) : (0 : ℚ) < wallisV n := by1461  have hC := centralBinom_pos_rat n1462  unfold wallisV; positivity14631464/-- 13:E2 — the Wallis lower chain `v_n` is strictly increasing. -/1465theorem wallisV_strictMono (n : ℕ) : (wallisV n : ℚ) < wallisV (n + 1) := by1466  rw [wallisV_succ]1467  apply lt_mul_of_one_lt_right (wallisV_pos n)1468  rw [one_lt_div (by positivity)]1469  nlinarith14701471/-- 13:E2 — `w_{n+1} = w_n · 4n(n+1)/(2n+1)²`. -/1472theorem wallisW_succ (n : ℕ) (hn : 1 ≤ n) :1473    (wallisW (n + 1) : ℚ) = wallisW n * (4 * n * (n + 1) / (2 * n + 1) ^ 2) := by1474  have hn' : (0 : ℚ) < n := by exact_mod_cast hn1475  have hC := centralBinom_pos_rat n1476  unfold wallisW1477  rw [centralBinom_succ_rat]1478  push_cast1479  field_simp1480  ring14811482theorem wallisW_pos (n : ℕ) (hn : 1 ≤ n) : (0 : ℚ) < wallisW n := by1483  have hn' : (0 : ℚ) < n := by exact_mod_cast hn1484  have hC := centralBinom_pos_rat n1485  unfold wallisW; positivity14861487/-- 13:E2 — the Wallis upper chain `w_n` is strictly decreasing from `n = 1`. -/1488theorem wallisW_strictAnti (n : ℕ) (hn : 1 ≤ n) : (wallisW (n + 1) : ℚ) < wallisW n := by1489  rw [wallisW_succ n hn]1490  apply mul_lt_of_lt_one_right (wallisW_pos n hn)1491  rw [div_lt_one (by positivity)]1492  nlinarith14931494end wallisQ14951496section wallisR14971498open Real14991500theorem centralBinom_real (n : ℕ) :1501    ((centralBinom n : ℕ) : ℝ) = ((2 * n) ! : ℝ) / ((n ! : ℝ) ^ 2) := by1502  have h : centralBinom n * n ! * n ! = (2 * n) ! := by1503    have := Nat.choose_mul_factorial_mul_factorial (show n ≤ 2 * n by omega)1504    rwa [show 2 * n - n = n by omega, ← centralBinom_eq_two_mul_choose] at this1505  have h' := congrArg (fun m : ℕ => (m : ℝ)) h1506  push_cast at h'1507  rw [eq_div_iff (by positivity)]1508  linear_combination h'15091510theorem wallisV_real (n : ℕ) : ((wallisV n : ℚ) : ℝ) = 2 * Real.Wallis.W n := by1511  rw [Real.Wallis.W_eq_factorial_ratio]1512  unfold wallisV1513  push_cast1514  rw [centralBinom_real]1515  have h1 : (0 : ℝ) < (n ! : ℝ) := by positivity1516  have h2 : (0 : ℝ) < ((2 * n) ! : ℝ) := by positivity1517  rw [show (16 : ℝ) ^ n = 2 ^ (4 * n) by rw [pow_mul]; norm_num]1518  field_simp15191520theorem wallisW_real (n : ℕ) (hn : 1 ≤ n) :1521    ((wallisW n : ℚ) : ℝ) = Real.Wallis.W n * (2 * n + 1) / n := by1522  rw [Real.Wallis.W_eq_factorial_ratio]1523  unfold wallisW1524  push_cast1525  rw [centralBinom_real]1526  have h1 : (0 : ℝ) < (n ! : ℝ) := by positivity1527  have h2 : (0 : ℝ) < ((2 * n) ! : ℝ) := by positivity1528  have hn' : (0 : ℝ) < n := by exact_mod_cast hn1529  rw [show (16 : ℝ) ^ n = 2 ^ (4 * n) by rw [pow_mul]; norm_num]1530  field_simp15311532/-- 13:E2, 13:I2 — the two-sided enclosure `v_n < π < w_n` for every `n ≥ 1`: the lower chain is the doubled Wallis1533partial product `2W_n < 2W_{n+1} ≤ π`, the upper chain is `W_n(2n+1)/n ≥ π(2n+1)²/(4n(n+1)) > π`. -/1534theorem wallis_enclosure (n : ℕ) (hn : 1 ≤ n) :1535    ((wallisV n : ℚ) : ℝ) < π ∧ π < ((wallisW n : ℚ) : ℝ) := by1536  have hn' : (0 : ℝ) < n := by exact_mod_cast hn1537  constructor1538  · rw [wallisV_real]1539    have hs := Real.Wallis.W_succ n1540    have hpos := Real.Wallis.W_pos n1541    have hlt : Real.Wallis.W n < Real.Wallis.W (n + 1) := by1542      rw [hs]1543      apply lt_mul_of_one_lt_right hpos1544      rw [_root_.div_mul_div_comm, one_lt_div (by positivity)]1545      nlinarith1546    have := Real.Wallis.W_le (n + 1)1547    linarith1548  · rw [wallisW_real n hn]1549    have hle := Real.Wallis.le_W n1550    have hpi := Real.pi_pos1551    rw [lt_div_iff₀ hn']1552    have key : π * n < ((2 * n + 1) / (2 * n + 2) * (π / 2)) * (2 * n + 1) := by1553      rw [_root_.div_mul_div_comm, div_mul_eq_mul_div, lt_div_iff₀ (by positivity)]1554      nlinarith1555    calc π * n < ((2 * n + 1) / (2 * n + 2) * (π / 2)) * (2 * n + 1) := key1556      _ ≤ Real.Wallis.W n * (2 * n + 1) := by1557        apply mul_le_mul_of_nonneg_right hle; positivity15581559end wallisR1560156115621563/-! ## The Fermat quotient and the π-Wieferich condition (13:G4, 13:G10)15641565The wall of `π` at second order.  The condition `4^{p−1} ≡ 1 + p (mod p²)` of G4 in its three forms, the exact1566identity `q_p(4) = 2q_p(2) + p·q_p(2)²`, Eisenstein's congruence `2q_p(2) ≡ −H_{(p−1)/2}`, G4's second-order1567clause from Morley's congruence, and the identification of the set with OEIS A355959, `(p+2)^{p−1} ≡ 1 (mod p²)`.1568The ring steps are proved once over any commutative ring with `p² = 0` (section `wieferich`); the sections1569`wieferichp` instantiate `ZMod (p²)` and `ZMod p`. -/15701571/-- The Fermat quotient `q_p(a) = (a^{p−1} − 1)/p` as a natural number. -/1572def fq (a p : ℕ) : ℕ := (a ^ (p - 1) - 1) / p15731574theorem fq_spec {a p : ℕ} (ha : 1 ≤ a) (hdvd : p ∣ a ^ (p - 1) - 1) :1575    a ^ (p - 1) = 1 + p * fq a p := by1576  unfold fq1577  have h1 : 1 ≤ a ^ (p - 1) := Nat.one_le_pow _ _ ha1578  rw [Nat.mul_div_cancel' hdvd]; omega15791580/-- 13:G10 — `q_p(4) = 2 q_p(2) + p q_p(2)²` exactly, from `4^{p−1} = (2^{p−1})²`. -/1581theorem fq_four_eq {p : ℕ} (hp : 0 < p) (h2 : p ∣ 2 ^ (p - 1) - 1) :1582    fq 4 p = 2 * fq 2 p + p * fq 2 p ^ 2 ∧ p ∣ 4 ^ (p - 1) - 1 := by1583  have e2 := fq_spec (a := 2) (by norm_num) h21584  have e4 : 4 ^ (p - 1) = (2 ^ (p - 1)) ^ 2 := by rw [← pow_mul, mul_comm, pow_mul]; norm_num1585  have key : 4 ^ (p - 1) - 1 = p * (2 * fq 2 p + p * fq 2 p ^ 2) := by1586    rw [e4, e2]; ring_nf; omega1587  refine ⟨?_, ⟨_, key⟩⟩1588  show (4 ^ (p - 1) - 1) / p = _1589  rw [key, Nat.mul_div_cancel_left _ hp]15901591section wieferich15921593variable {R : Type*} [CommRing R]15941595/-- 13:G4 — the second order at the half wall from Morley's congruence, the ring step: with1596`x = 4^{p−1} = 1 + p q`, `c² = x²` (`C(p−1,m) ≡ (−1)^m 4^{p−1}`), `2m = p − 1` and `p² = 0`:1597`2·x = 2·(−2 + 2p(q − 1))·m·c²`. -/1598theorem second_order_generic (p q m c x : R) (hpp : p * p = 0) (hx : x = 1 + p * q) (hc2 : c ^ 2 = x ^ 2)1599    (h2m : 2 * m = -1 + p) : 2 * x = 2 * ((-2 + 2 * p * (q - 1)) * (m * c ^ 2)) := by1600  rw [hc2]1601  subst hx1602  linear_combination (-(-2 + 2 * p * (q - 1)) * (1 + p * q) ^ 2) * h2m + (-2 * p ^ 2 * q ^ 3 + 2 * p ^ 2 * q ^ 2 + 2 * p * q ^ 3 - 4 * p * q ^ 2 + 4 * p * q + 2 * q ^ 2 - 2 * q + 2) * hpp16031604/-- `(1 + p u)^n = 1 + n p u` when `p² = 0`. -/1605theorem one_add_mul_pow (p u : R) (hpp : p * p = 0) : ∀ n : ℕ, (1 + p * u) ^ n = 1 + n * (p * u)1606  | 0 => by simp1607  | n + 1 => by1608    rw [pow_succ, one_add_mul_pow p u hpp n]1609    push_cast1610    linear_combination (n * u * u) * hpp16111612/-- The OEIS step: `x (1 + n p i) − 1 = p (q − i)` for `x = 1 + p q`, `n = p − 1`, `p² = 0` (with `i = 2⁻¹` in use). -/1613theorem oeis_generic (p q i n : R) (hpp : p * p = 0) (hn : n = p - 1) (x : R) (hx : x = 1 + p * q) :1614    x * (1 + n * (p * i)) - 1 = p * (q - i) := by1615  subst hx hn1616  linear_combination (i * (1 + p * q) - q * i) * hpp16171618theorem sum_range_two_mul {M : Type*} [AddCommMonoid M] (f : ℕ → M) :1619    ∀ m, ∑ k ∈ Finset.range (2 * m), f k = ∑ j ∈ Finset.range m, (f (2 * j) + f (2 * j + 1))1620  | 0 => rfl1621  | m + 1 => by1622    rw [Finset.sum_range_succ, ← sum_range_two_mul f m, show 2 * (m + 1) = 2 * m + 1 + 1 by ring,1623      Finset.sum_range_succ, Finset.sum_range_succ, add_assoc]16241625end wieferich16261627section wieferichK16281629variable {K : Type*} [Field K]16301631/-- `H_{p−1} = Σ_{k<p−1} (k+1)⁻¹ = 0` over a field with `p = 0` and `2 ≠ 0` (the terms pair off as `k ↔ p − k`). -/1632theorem harmonic_generic (p : ℕ) (hp0 : (p : K) = 0) (h1 : 1 ≤ p) (h2 : (2 : K) ≠ 0) :1633    ∑ k ∈ Finset.range (p - 1), ((k + 1 : ℕ) : K)⁻¹ = 0 := by1634  have hr := Finset.sum_range_reflect (fun k => ((k + 1 : ℕ) : K)⁻¹) (p - 1)1635  have hterm : ∀ k ∈ Finset.range (p - 1), ((p - 1 - 1 - k + 1 : ℕ) : K)⁻¹ = -((k + 1 : ℕ) : K)⁻¹ := by1636    intro k hk1637    have := Finset.mem_range.1 hk1638    rw [show p - 1 - 1 - k + 1 = p - 1 - k by omega, natCast_pred_sub p hp0 h1 k (by omega), inv_neg, Nat.cast_add,1639      Nat.cast_one]1640  rw [Finset.sum_congr rfl hterm, Finset.sum_neg_distrib] at hr1641  have : (2 : K) * ∑ k ∈ Finset.range (p - 1), ((k + 1 : ℕ) : K)⁻¹ = 0 := by linear_combination -hr1642  exact (mul_eq_zero.1 this).resolve_left h216431644/-- Eisenstein's congruence, the field step: from `a = Σ_{k<2m} (−1)^k (k+1)⁻¹` and `H_{2m} = 0`, `a = −H_m`1645(the alternating sum over `[1, 2m]` is `H_{2m} − H_m`). -/1646theorem eisenstein_generic (m : ℕ) (a : K) (h2 : (2 : K) ≠ 0)1647    (hH : ∑ k ∈ Finset.range (2 * m), ((k + 1 : ℕ) : K)⁻¹ = 0)1648    (hc : a = ∑ k ∈ Finset.range (2 * m), (-1) ^ k * ((k + 1 : ℕ) : K)⁻¹) :1649    a = -∑ j ∈ Finset.range m, ((j + 1 : ℕ) : K)⁻¹ := by1650  rw [sum_range_two_mul] at hc hH1651  have key : ∀ j ∈ Finset.range m,1652      ((-1) ^ (2 * j) * ((2 * j + 1 : ℕ) : K)⁻¹ + (-1) ^ (2 * j + 1) * ((2 * j + 1 + 1 : ℕ) : K)⁻¹) =1653      (((2 * j + 1 : ℕ) : K)⁻¹ + ((2 * j + 1 + 1 : ℕ) : K)⁻¹) - ((j + 1 : ℕ) : K)⁻¹ := by1654    intro j hj1655    have e : ((2 * j + 1 + 1 : ℕ) : K)⁻¹ = 2⁻¹ * ((j + 1 : ℕ) : K)⁻¹ := by1656      rw [show 2 * j + 1 + 1 = 2 * (j + 1) by ring, Nat.cast_mul, mul_inv, Nat.cast_ofNat]1657    rw [pow_mul, neg_one_sq, one_pow, one_mul, pow_succ, pow_mul, neg_one_sq, one_pow, one_mul, e]1658    have := mul_inv_cancel₀ h21659    linear_combination (-((j + 1 : ℕ) : K)⁻¹) * this1660  rw [Finset.sum_congr rfl key, Finset.sum_sub_distrib, hH, zero_sub] at hc1661  exact hc16621663end wieferichK166416651666/-! ### On the shell lifted to `p²`: the three forms, the half wall at second order, Eisenstein, OEIS -/1667section wieferichp16681669variable (p : ℕ) [hp : Fact p.Prime]16701671/-- Fermat: `p ∣ 2^{p−1} − 1` for every odd prime. -/1672theorem two_pow_pred_dvd (hp2 : p ≠ 2) : p ∣ 2 ^ (p - 1) - 1 := by1673  rw [← ZMod.natCast_eq_zero_iff, Nat.cast_sub (Nat.one_le_two_pow), Nat.cast_pow, Nat.cast_ofNat, Nat.cast_one]1674  rw [ZMod.pow_card_sub_one_eq_one (two_ne_zero_zmod p hp2), sub_self]16751676omit hp in1677theorem p_sq_eq_zero : ((p : ZMod (p ^ 2)) * p) = 0 := by1678  rw [← Nat.cast_mul, ← pow_two, ZMod.natCast_self]16791680theorem p_mul_natCast_eq_zero_iff (a : ℕ) : ((p : ZMod (p ^ 2)) * a) = 0 ↔ (a : ZMod p) = 0 := by1681  rw [← Nat.cast_mul, ZMod.natCast_eq_zero_iff, ZMod.natCast_eq_zero_iff, pow_two,1682    Nat.mul_dvd_mul_iff_left hp.out.pos]16831684theorem p_mul_intCast_eq_zero_iff (a : ℤ) : ((p : ZMod (p ^ 2)) * a) = 0 ↔ (a : ZMod p) = 0 := by1685  have : ((p : ZMod (p ^ 2)) * a) = ((p * a : ℤ) : ZMod (p ^ 2)) := by push_cast; ring1686  rw [this, ZMod.intCast_zmod_eq_zero_iff_dvd, ZMod.intCast_zmod_eq_zero_iff_dvd, pow_two, Nat.cast_mul,1687    Int.mul_dvd_mul_iff_left (by exact_mod_cast hp.out.ne_zero)]16881689/-- 13:G10 — `4^{p−1} = 1 + p·q_p(4)` in `ZMod (p²)`, and `q_p(4) = 2q_p(2) + p·q_p(2)²`. -/1690theorem four_pow_pred (hp2 : p ≠ 2) :1691    (4 : ZMod (p ^ 2)) ^ (p - 1) = 1 + p * fq 4 p ∧ fq 4 p = 2 * fq 2 p + p * fq 2 p ^ 2 := by1692  obtain ⟨e, h4⟩ := fq_four_eq hp.out.pos (two_pow_pred_dvd p hp2)1693  refine ⟨?_, e⟩1694  have := congrArg (Nat.cast : ℕ → ZMod (p ^ 2)) (fq_spec (a := 4) (by norm_num) h4)1695  push_cast at this1696  exact this16971698/-- 13:G10 — the π-Wieferich condition in its three forms: `4^{p−1} ≡ 1 + p (mod p²)` ⟺1699`q_p(4) ≡ 1 (mod p)` ⟺ `2·q_p(2) ≡ 1 (mod p)` — a prescribed value of the Fermat quotient of `2`. -/1700theorem piWieferich_iff (hp2 : p ≠ 2) :1701    ((4 : ZMod (p ^ 2)) ^ (p - 1) = 1 + p ↔ (fq 4 p : ZMod p) = 1) ∧1702    ((fq 4 p : ZMod p) = 1 ↔ (2 * fq 2 p : ZMod p) = 1) := by1703  obtain ⟨h4, e⟩ := four_pow_pred p hp21704  constructor1705  · rw [h4]1706    have key : (1 : ZMod (p ^ 2)) + p * fq 4 p = 1 + p ↔ (p : ZMod (p ^ 2)) * (((fq 4 p : ℤ) - 1 : ℤ) : ZMod (p ^ 2)) = 0 := by1707      push_cast1708      constructor1709      · intro h; linear_combination h1710      · intro h; linear_combination h1711    rw [key, p_mul_intCast_eq_zero_iff]1712    push_cast1713    exact sub_eq_zero1714  · rw [e]; push_cast; rw [ZMod.natCast_self]; simp17151716/-- 13:G4, 13:I2, 13:J6 — the second order at the half wall: with `m = (p−1)/2` and Morley's congruence1717`C(p−1, m) ≡ (−1)^m 4^{p−1}` taken modulo `p²` (the import A3), `16^m ≡ (−2 + 2p(q_p(4) − 1))·m·C(2m,m)²1718(mod p²)`, i.e. `w_m ≡ −2 + 2p(q_p(4) − 1)`; the universal `−2` persists to `p²` exactly when `q_p(4) ≡ 1`,1719the π-Wieferich condition. -/1720theorem half_wall_second_order (hp2 : p ≠ 2) (m : ℕ) (hm : p = 2 * m + 1)1721    (hM : ((centralBinom m : ℕ) : ZMod (p ^ 2)) = (-1) ^ m * 4 ^ (p - 1)) :1722    (2 : ZMod (p ^ 2)) * 16 ^ m =1723      2 * ((-2 + 2 * p * ((fq 4 p : ZMod (p ^ 2)) - 1)) * (m * ((centralBinom m : ℕ) : ZMod (p ^ 2)) ^ 2)) ∧1724    ((2 : ZMod (p ^ 2)) * 16 ^ m = 2 * (-2 * (m * ((centralBinom m : ℕ) : ZMod (p ^ 2)) ^ 2)) ↔1725      (fq 4 p : ZMod p) = 1) := by1726  obtain ⟨h4, _⟩ := four_pow_pred p hp21727  have h16 : (16 : ZMod (p ^ 2)) ^ m = 4 ^ (p - 1) := by1728    rw [show p - 1 = 2 * m by omega, pow_mul]; norm_num1729  have hc2 : (((centralBinom m : ℕ) : ZMod (p ^ 2))) ^ 2 = ((4 : ZMod (p ^ 2)) ^ (p - 1)) ^ 2 := by1730    rw [hM, mul_pow, ← pow_mul, mul_comm m 2, pow_mul, neg_one_sq, one_pow, one_mul]1731  have h2m : (2 : ZMod (p ^ 2)) * m = -1 + p := by1732    have : ((2 * m + 1 : ℕ) : ZMod (p ^ 2)) = p := by rw [← hm]1733    push_cast at this1734    linear_combination this1735  have key := second_order_generic (p : ZMod (p ^ 2)) (fq 4 p) m _ _ (p_sq_eq_zero p) h4 hc2 h2m1736  rw [h16]1737  refine ⟨key, ?_⟩1738  rw [key]1739  have hm1 : 1 ≤ m := by have := hp.out.two_le; omega1740  have hcop4 : Nat.Coprime 4 p := by1741    rw [Nat.coprime_comm, hp.out.coprime_iff_not_dvd]1742    intro h1743    exact hp2 ((Nat.prime_dvd_prime_iff_eq hp.out Nat.prime_two).1 (hp.out.dvd_of_dvd_pow (show p ∣ 2 ^ 2 by norm_num; exact h)))1744  have hcopm : Nat.Coprime m p := by1745    rw [Nat.coprime_comm, hp.out.coprime_iff_not_dvd]1746    exact Nat.not_dvd_of_pos_of_lt hm1 (by omega)1747  have hcopC : Nat.Coprime (centralBinom m) p := by1748    rw [Nat.coprime_comm, hp.out.coprime_iff_not_dvd]1749    intro hdvd1750    have hfac : centralBinom m * m ! * m ! = (2 * m) ! := by1751      have := Nat.choose_mul_factorial_mul_factorial (show m ≤ 2 * m by omega)1752      rwa [show 2 * m - m = m by omega, ← centralBinom_eq_two_mul_choose] at this1753    have : p ∣ (2 * m) ! := hfac ▸ Dvd.dvd.mul_right (Dvd.dvd.mul_right hdvd _) _1754    have := (hp.out.dvd_factorial).1 this1755    omega1756  have hu4 : IsUnit ((4 : ℕ) : ZMod (p ^ 2)) := (ZMod.isUnit_iff_coprime 4 (p ^ 2)).2 (hcop4.pow_right 2)1757  have hum : IsUnit ((m : ℕ) : ZMod (p ^ 2)) := (ZMod.isUnit_iff_coprime m (p ^ 2)).2 (hcopm.pow_right 2)1758  have huC : IsUnit ((centralBinom m : ℕ) : ZMod (p ^ 2)) :=1759    (ZMod.isUnit_iff_coprime _ (p ^ 2)).2 (hcopC.pow_right 2)1760  have hunit : IsUnit (((4 : ℕ) : ZMod (p ^ 2)) * (m * ((centralBinom m : ℕ) : ZMod (p ^ 2)) ^ 2)) :=1761    hu4.mul (hum.mul (huC.pow 2))1762  have hiff := p_mul_intCast_eq_zero_iff p ((fq 4 p : ℤ) - 1)1763  push_cast at hiff1764  rw [sub_eq_zero] at hiff1765  constructor1766  · intro h1767    have h0 : ((p : ZMod (p ^ 2)) * ((fq 4 p : ZMod (p ^ 2)) - 1)) *1768        (((4 : ℕ) : ZMod (p ^ 2)) * (m * ((centralBinom m : ℕ) : ZMod (p ^ 2)) ^ 2)) = 0 := by1769      push_cast; linear_combination h1770    exact hiff.1 ((hunit.mul_left_eq_zero).1 h0)1771  · intro h1772    have h0 := hiff.2 h1773    linear_combination (4 * (m * ((centralBinom m : ℕ) : ZMod (p ^ 2)) ^ 2)) * h017741775/-- `C(p−1, k) ≡ (−1)^k (mod p)`. -/1776theorem choose_pred_zmod (k : ℕ) (hk : k ≤ p - 1) : ((choose (p - 1) k : ℕ) : ZMod p) = (-1) ^ k :=1777  choose_pred_eq_neg_one_pow (K := ZMod p) p (ZMod.natCast_self p) hp.out.one_le1778    (fun j hj0 hj => natCast_ne_zero_of_lt p j hj0 (by omega)) k hk17791780/-- The lift: `a ≡ b (mod p)` gives `p·a = p·b` in `ZMod (p²)`. -/1781theorem p_mul_congr (a b : ℤ) (h : (a : ZMod p) = b) : (p : ZMod (p ^ 2)) * a = p * b := by1782  have := (p_mul_intCast_eq_zero_iff p (a - b)).2 (by push_cast; rw [h, sub_self])1783  push_cast at this; linear_combination this17841785/-- `C(p, k+1)·(k+1) = p·(−1)^k` in `ZMod (p²)` for `k + 1 ≤ p − 1`. -/1786theorem choose_succ_mul_eq (k : ℕ) (hk : k + 1 ≤ p - 1) :1787    ((choose p (k + 1) : ℕ) : ZMod (p ^ 2)) * ((k + 1 : ℕ) : ZMod (p ^ 2)) = p * (-1) ^ k := by1788  have h := Nat.add_one_mul_choose_eq (p - 1) k1789  rw [Nat.sub_add_cancel hp.out.one_le] at h1790  have hc := choose_pred_zmod p k (by omega)1791  have hl := p_mul_congr p (choose (p - 1) k : ℕ) ((-1) ^ k) (by push_cast; exact hc)1792  push_cast at hl1793  have := congrArg (fun m : ℕ => (m : ZMod (p ^ 2))) h1794  push_cast at this ⊢1795  rw [← this, hl]17961797theorem coprime_succ_sq (k : ℕ) (hk : k + 1 ≤ p - 1) : Nat.Coprime (k + 1) (p ^ 2) := by1798  apply Nat.Coprime.pow_right1799  rw [Nat.coprime_comm, hp.out.coprime_iff_not_dvd]1800  exact Nat.not_dvd_of_pos_of_lt (by omega) (by omega)18011802/-- `C(p, k+1) = p·(−1)^k·(k+1)⁻¹` in `ZMod (p²)`. -/1803theorem choose_succ_eq (k : ℕ) (hk : k + 1 ≤ p - 1) :1804    ((choose p (k + 1) : ℕ) : ZMod (p ^ 2)) = p * (-1) ^ k * ((k + 1 : ℕ) : ZMod (p ^ 2))⁻¹ := by1805  have hu := ZMod.coe_mul_inv_eq_one (k + 1) (coprime_succ_sq p k hk)1806  have h := choose_succ_mul_eq p k hk1807  calc ((choose p (k + 1) : ℕ) : ZMod (p ^ 2))1808      = ((choose p (k + 1) : ℕ) : ZMod (p ^ 2)) * (((k + 1 : ℕ) : ZMod (p ^ 2)) * ((k + 1 : ℕ) : ZMod (p ^ 2))⁻¹) := by1809        rw [hu, mul_one]1810    _ = p * (-1) ^ k * ((k + 1 : ℕ) : ZMod (p ^ 2))⁻¹ := by rw [← mul_assoc, h]18111812/-- `2^p − 2 = p · Σ_{k<p−1} (−1)^k (k+1)⁻¹` in `ZMod (p²)`. -/1813theorem two_pow_sub_two (hp2 : p ≠ 2) :1814    (2 : ZMod (p ^ 2)) * p * fq 2 p = p * ∑ k ∈ Finset.range (p - 1), (-1) ^ k * ((k + 1 : ℕ) : ZMod (p ^ 2))⁻¹ := by1815  have hsum := Nat.sum_range_choose p1816  have h1 : p + 1 = (p - 1) + 1 + 1 := by have := hp.out.one_le; omega1817  rw [h1, Finset.sum_range_succ, Finset.sum_range_succ', show p - 1 + 1 = p by have := hp.out.one_le; omega,1818    choose_self, choose_zero_right] at hsum1819  have hc := congrArg (fun m : ℕ => (m : ZMod (p ^ 2))) hsum1820  push_cast at hc1821  have hq := congrArg (fun m : ℕ => (m : ZMod (p ^ 2))) (fq_spec (a := 2) (by norm_num) (two_pow_pred_dvd p hp2))1822  push_cast at hq1823  have h2p : (2 : ZMod (p ^ 2)) ^ p = 2 * 2 ^ (p - 1) := by1824    have := pow_succ' (2 : ZMod (p ^ 2)) (p - 1)1825    rwa [Nat.sub_add_cancel hp.out.one_le] at this1826  rw [Finset.mul_sum]1827  have hterm : ∀ k ∈ Finset.range (p - 1), ((choose p (k + 1) : ℕ) : ZMod (p ^ 2)) =1828      (p : ZMod (p ^ 2)) * ((-1) ^ k * ((k + 1 : ℕ) : ZMod (p ^ 2))⁻¹) := by1829    intro k hk1830    have := Finset.mem_range.1 hk1831    rw [choose_succ_eq p k (by omega), mul_assoc]1832  rw [Finset.sum_congr rfl hterm] at hc1833  linear_combination -hc - 2 * hq - h2p18341835/-- `p·x = 0` in `ZMod (p²)` exactly when `x` reduces to `0` in `ZMod p`. -/1836theorem p_mul_eq_zero_iff_cast (x : ZMod (p ^ 2)) :1837    (p : ZMod (p ^ 2)) * x = 0 ↔ ((x.cast : ZMod p) = 0) := by1838  conv_lhs => rw [← ZMod.natCast_zmod_val x]1839  rw [p_mul_natCast_eq_zero_iff, ZMod.natCast_val]18401841theorem cast_inv_succ (k : ℕ) (hk : k + 1 ≤ p - 1) :1842    ((((k + 1 : ℕ) : ZMod (p ^ 2))⁻¹).cast : ZMod p) = ((k + 1 : ℕ) : ZMod p)⁻¹ := by1843  have hu := ZMod.coe_mul_inv_eq_one (k + 1) (coprime_succ_sq p k hk)1844  have hdvd : p ∣ p ^ 2 := dvd_pow_self p two_ne_zero1845  have := congrArg (ZMod.castHom hdvd (ZMod p)) hu1846  rw [map_mul, map_one, ZMod.castHom_apply, ZMod.castHom_apply, ZMod.cast_natCast hdvd] at this1847  exact eq_inv_of_mul_eq_one_right this18481849/-- `H_{p−1} = Σ_{k<p−1} (k+1)⁻¹ = 0` in `ZMod p`. -/1850theorem harmonic_pred_eq_zero (hp2 : p ≠ 2) : ∑ k ∈ Finset.range (p - 1), ((k + 1 : ℕ) : ZMod p)⁻¹ = 0 :=1851  harmonic_generic p (ZMod.natCast_self p) hp.out.one_le (two_ne_zero_zmod p hp2)18521853/-- `p·x = p·y` in `ZMod (p²)` exactly when `x` and `y` agree in `ZMod p`. -/1854theorem p_mul_eq_iff_cast (x y : ZMod (p ^ 2)) :1855    (p : ZMod (p ^ 2)) * x = (p : ZMod (p ^ 2)) * y ↔ (x.cast : ZMod p) = y.cast := by1856  have hdvd : p ∣ p ^ 2 := dvd_pow_self p two_ne_zero1857  have e : ((x - y).cast : ZMod p) = x.cast - y.cast := ZMod.cast_sub hdvd x y1858  constructor1859  · intro h1860    have h0 := (p_mul_eq_zero_iff_cast p (x - y)).1 (by rw [mul_sub, h, sub_self])1861    rw [e] at h01862    exact sub_eq_zero.1 h01863  · intro h1864    have h0 : ((x - y).cast : ZMod p) = 0 := by rw [e, h]; exact sub_self _1865    have := (p_mul_eq_zero_iff_cast p (x - y)).2 h01866    rw [mul_sub, sub_eq_zero] at this1867    exact this18681869/-- 13:G10 — Eisenstein's congruence: `2 q_p(2) ≡ −H_{(p−1)/2} (mod p)`, `H_m = Σ_{j<m} (j+1)⁻¹`. -/1870theorem eisenstein (m : ℕ) (hm : p = 2 * m + 1) :1871    (2 * fq 2 p : ZMod p) = -∑ j ∈ Finset.range m, ((j + 1 : ℕ) : ZMod p)⁻¹ := by1872  have hp2 : p ≠ 2 := by omega1873  have hdvd : p ∣ p ^ 2 := dvd_pow_self p two_ne_zero1874  have h := two_pow_sub_two p hp21875  have h0 : (p : ZMod (p ^ 2)) * ((2 * fq 2 p : ℕ) : ZMod (p ^ 2)) =1876      p * ∑ k ∈ Finset.range (p - 1), (-1) ^ k * ((k + 1 : ℕ) : ZMod (p ^ 2))⁻¹ := by1877    rw [Nat.cast_mul, Nat.cast_ofNat]; linear_combination h1878  have hc := (p_mul_eq_iff_cast p ((2 * fq 2 p : ℕ) : ZMod (p ^ 2)) _).1 h01879  rw [← ZMod.castHom_apply (h := hdvd), ← ZMod.castHom_apply (h := hdvd), map_natCast, map_sum] at hc1880  have hterm : ∀ k ∈ Finset.range (p - 1), ZMod.castHom hdvd (ZMod p) ((-1) ^ k * ((k + 1 : ℕ) : ZMod (p ^ 2))⁻¹) =1881      (-1) ^ k * ((k + 1 : ℕ) : ZMod p)⁻¹ := by1882    intro k hk1883    have := Finset.mem_range.1 hk1884    rw [map_mul, map_pow, map_neg, map_one, ZMod.castHom_apply, cast_inv_succ p k (by omega)]1885  rw [Finset.sum_congr rfl hterm] at hc1886  have hH := harmonic_pred_eq_zero p hp21887  rw [show p - 1 = 2 * m by omega] at hc hH1888  have key := eisenstein_generic (K := ZMod p) m _ (two_ne_zero_zmod p hp2) hH hc1889  exact_mod_cast key18901891/-- 13:G10 — the π-Wieferich condition in harmonic form: `4^{p−1} ≡ 1 + p (mod p²)` exactly when1892`H_{(p−1)/2} = Σ_{j=1}^{(p−1)/2} 1/j ≡ −1 (mod p)`. -/1893theorem piWieferich_iff_harmonic (m : ℕ) (hm : p = 2 * m + 1) :1894    (4 : ZMod (p ^ 2)) ^ (p - 1) = 1 + p ↔ ∑ j ∈ Finset.range m, ((j + 1 : ℕ) : ZMod p)⁻¹ = -1 := by1895  have hp2 : p ≠ 2 := by omega1896  obtain ⟨h1, h2⟩ := piWieferich_iff p hp21897  rw [h1, h2, eisenstein p m hm]1898  exact neg_eq_iff_eq_neg18991900/-- 13:G10 — the π-Wieferich set is OEIS A355959: `(p + 2)^{p−1} ≡ 1 (mod p²)` exactly when1901`2 q_p(2) ≡ 1 (mod p)`, i.e. exactly when `4^{p−1} ≡ 1 + p (mod p²)`. -/1902theorem piWieferich_iff_oeis (hp2 : p ≠ 2) :1903    ((p : ZMod (p ^ 2)) + 2) ^ (p - 1) = 1 ↔ (2 * fq 2 p : ZMod p) = 1 := by1904  have hcop : Nat.Coprime 2 (p ^ 2) := by1905    apply Nat.Coprime.pow_right1906    rw [Nat.coprime_comm, hp.out.coprime_iff_not_dvd]1907    intro h; exact hp2 ((Nat.prime_dvd_prime_iff_eq hp.out Nat.prime_two).1 h)1908  have h2i := ZMod.coe_mul_inv_eq_one 2 hcop1909  set i : ZMod (p ^ 2) := ((2 : ℕ) : ZMod (p ^ 2))⁻¹ with hi1910  have h2i' : (2 : ZMod (p ^ 2)) * i = 1 := by rw [hi]; exact_mod_cast h2i1911  have hu2 : IsUnit (2 : ZMod (p ^ 2)) := ⟨⟨2, i, h2i', by rw [mul_comm]; exact h2i'⟩, rfl⟩1912  have hq := congrArg (Nat.cast : ℕ → ZMod (p ^ 2)) (fq_spec (a := 2) (by norm_num) (two_pow_pred_dvd p hp2))1913  push_cast at hq1914  have hfac : ((p : ZMod (p ^ 2)) + 2) = 2 * (1 + p * i) := by linear_combination (-(p : ZMod (p ^ 2))) * h2i'1915  have hn : ((p - 1 : ℕ) : ZMod (p ^ 2)) = p - 1 := by rw [Nat.cast_sub hp.out.one_le, Nat.cast_one]1916  have key : ((p : ZMod (p ^ 2)) + 2) ^ (p - 1) - 1 = p * ((fq 2 p : ZMod (p ^ 2)) - i) := by1917    rw [hfac, mul_pow, one_add_mul_pow _ _ (p_sq_eq_zero p), hn]1918    exact oeis_generic (p : ZMod (p ^ 2)) (fq 2 p) i _ (p_sq_eq_zero p) rfl _ hq1919  have hiff := p_mul_intCast_eq_zero_iff p (2 * (fq 2 p : ℤ) - 1)1920  push_cast at hiff1921  rw [sub_eq_zero] at hiff1922  rw [← sub_eq_zero, key, ← hiff]1923  constructor1924  · intro h1925    have : (2 : ZMod (p ^ 2)) * ((p : ZMod (p ^ 2)) * ((fq 2 p : ZMod (p ^ 2)) - i)) = 0 := by rw [h, mul_zero]1926    linear_combination this + (p : ZMod (p ^ 2)) * h2i'1927  · intro h1928    have h' : (2 : ZMod (p ^ 2)) * ((p : ZMod (p ^ 2)) * ((fq 2 p : ZMod (p ^ 2)) - i)) = 0 := by1929      linear_combination h - (p : ZMod (p ^ 2)) * h2i'1930    exact (hu2.mul_right_eq_zero).1 h'19311932end wieferichp19331934-- Ledger predicates of 13-epi (generated by make_predicates.py from docs/13-epi/13-epi-ledger.json; edit the ledger, not this section)1935set_option linter.defProp false in1936/-- 13:C2 (p13013) — The derangement selector: the registration statistics are generated by the rencontres polynomial $P_n(X)=n!\sum_{k\le n}(X-1)^{k}/k!$ (an exact double-counting identity), the normalised kernel $Z_n$ has $Z_n(1)=1$, $Z_n(0)=\dr{n}/n!$, and the unit registration ratio $R_n=n!/\dr{n}$ is forced; relative to the declared completion of $Z_n$ to $e^{X-1}$ the external value of the chain is uniquely $\eR$. -/1937def p13013 := And.intro @FRC.Epi.rencontres (And.intro @FRC.Epi.rencontres_rat (And.intro @FRC.Epi.rencontres_one (@FRC.Epi.rencontres_zero)))1938/-- 13:C3 (p13014) — The Cayley quarter-turn map $C(x)=(1+\im x)/(1-\im x)$ on $\Fp$ (denominators units): $C(0)=1$, $C(1)=\im$, and $C(x)C(y)=C\bigl((x+y)/(1-xy)\bigr)$, the rational composition law being the half-angle form of phase composition; shell arithmetic only. -/1939theorem p13014 : (∀ {K : Type u_1} [Field K] (i : K), i * i = (-1 : K) → (2 : K) ≠ (0 : K) → FRC.Epi.cayley i (0 : K) = (1 : K) ∧ FRC.Epi.cayley i (1 : K) = i) ∧ ∀ {K : Type u_2} [Field K] (i x y : K), i * i = (-1 : K) → (1 : K) - i * x ≠ (0 : K) → (1 : K) - i * y ≠ (0 : K) → (1 : K) - x * y ≠ (0 : K) → FRC.Epi.cayley i x * FRC.Epi.cayley i y = FRC.Epi.cayley i ((x + y) / ((1 : K) - x * y)) :=1940  And.intro @FRC.Epi.cayley_values (@FRC.Epi.cayley_mul)1941set_option linter.defProp false in1942/-- 13:C5 (p13016) — The joint-return tally: with $C_n=\Cb{n}$ the returning $\pm1$ histories of length $2n$ in one direction, the paired histories in the directions $1$ and $\im$ number $16^{n}$ and the joint returns $C_n^{2}$, and $\piR=\lim16^{n}/(nC_n^{2})$ by the Wallis bounds (E2). -/1943def p13016 := And.intro @FRC.Epi.joint_return_tally (@FRC.Epi.tendsto_wallis_chain)1944/-- 13:D2 (p13018) — The tail form: $\dr{n}=n!/\eR+(-1)^{n}\delta_n$ with $\delta_n\in(1/(n+2),1/(n+1))$, so $\dr{n}$ is the nearest integer to $n!/\eR$. -/1945theorem p13018 : (∀ (n : ℕ), (1 : ℝ) / (↑n + (2 : ℝ)) < FRC.Epi.tailDelta n ∧ FRC.Epi.tailDelta n < (1 : ℝ) / (↑n + (1 : ℝ))) ∧ ∀ (n : ℕ), ↑(numDerangements n) = ↑n.factorial * Real.exp (-1 : ℝ) + (-1 : ℝ) ^ n * FRC.Epi.tailDelta n :=1946  And.intro @FRC.Epi.tailDelta_strict (@FRC.Epi.numDerangements_eq_tailDelta)1947/-- 13:D3 (p13019) — Superexponential enclosure: $|\varepsilon_n-\eR|\le\eR(\eR+1)/(n+1)!<10.2/(n+1)!$ with $\operatorname{sign}(\varepsilon_n-\eR)=(-1)^{n+1}$, hence $\varepsilon_{2m}<\eR<\varepsilon_{2m+1}$, a nested sequence of $\fQ$-native intervals; the sharper constant $8$ for $2\le n\le60$. -/1948theorem p13019 : (∀ (n : ℕ), (2 : ℕ) ≤ n → |FRC.Epi.epsChain n - Real.exp (1 : ℝ)| ≤ Real.exp (1 : ℝ) * (Real.exp (1 : ℝ) + (1 : ℝ)) / ↑(n + (1 : ℕ)).factorial ∧ Real.exp (1 : ℝ) * (Real.exp (1 : ℝ) + (1 : ℝ)) / ↑(n + (1 : ℕ)).factorial < 10.2 / ↑(n + (1 : ℕ)).factorial) ∧ ∀ (n : ℕ), (2 : ℕ) ≤ n → (0 : ℝ) < (-1 : ℝ) ^ (n + (1 : ℕ)) * (FRC.Epi.epsChain n - Real.exp (1 : ℝ)) :=1949  And.intro @FRC.Epi.epsChain_enclosure (@FRC.Epi.epsChain_sign)1950/-- 13:D4 (p13020) — Horizon determination of the readout: for $n\ge n_0(k)=\Theta(k/\log k)$ the readout $\ro(\varepsilon_n)$ lies within one ulp of $\ro(\eR)$, and equals it from the plateau threshold $n_1(k)$, the least $n$ from which the readouts agree, decided through the rounding cell of $\eR$ ($n_1\le n_0+1$ for $k<200$, equality at eight precisions); the binary64 constant is the readout of $\varepsilon_{18}=18!/\dr{18}$, $n=18$ minimal; $\varepsilon_{70}$ fixes $100$ digits. -/1951theorem p13020 : (|Real.exp (1 : ℝ) - FRC.Epi.binary64E| < (1 : ℝ) / (2 : ℝ) ^ (52 : ℕ) ∧ |FRC.Epi.epsChain (18 : ℕ) - FRC.Epi.binary64E| < (1 : ℝ) / (2 : ℝ) ^ (52 : ℕ) ∧ ∀ (n : ℕ), (2 : ℕ) ≤ n → n ≤ (17 : ℕ) → (1 : ℝ) / (2 : ℝ) ^ (52 : ℕ) < |FRC.Epi.epsChain n - FRC.Epi.binary64E|) ∧ (∀ (k n : ℕ), (2 : ℕ) ≤ k → (2 : ℕ) ≤ n → Real.exp (1 : ℝ) * (Real.exp (1 : ℝ) + (1 : ℝ)) / ↑(n + (1 : ℕ)).factorial < (1 : ℝ) / (2 : ℝ) ^ k → |FRC.Epi.roundTo k (FRC.Epi.epsChain n) - FRC.Epi.roundTo k (Real.exp (1 : ℝ))| ≤ (1 : ℝ) / (2 : ℝ) ^ (k - (2 : ℕ))) ∧ (∀ (k n : ℕ), (2 : ℕ) ≤ n → Real.exp (1 : ℝ) * (Real.exp (1 : ℝ) + (1 : ℝ)) / ↑(n + (1 : ℕ)).factorial < FRC.Epi.cellDist k (Real.exp (1 : ℝ)) → FRC.Epi.roundTo k (FRC.Epi.epsChain n) = FRC.Epi.roundTo k (Real.exp (1 : ℝ))) ∧ FRC.Epi.roundTo (6 : ℕ) (FRC.Epi.epsChain (5 : ℕ)) = (44 / 16 : ℝ) ∧ FRC.Epi.roundTo (6 : ℕ) (Real.exp (1 : ℝ)) = (43 / 16 : ℝ) ∧ Real.exp (1 : ℝ) * (Real.exp (1 : ℝ) + (1 : ℝ)) / ↑((5 : ℕ) + (1 : ℕ)).factorial < (1 : ℝ) / (2 : ℝ) ^ (6 : ℕ) :=1952  And.intro @FRC.Epi.readout_binary64 (And.intro @FRC.Epi.readout_within_ulp (And.intro @FRC.Epi.readout_plateau (@FRC.Epi.readout_six_bits)))1953/-- 13:D5 (p13021) — Feasibility selection: the compound chain $(1+1/n)^{n}$ costs $n\asymp2^{k}$ steps for $k$ bits against $n_0(k)=\Theta(k/\log k)$ for the derangement chain ($n=11,18,70$ at $k=24,53,333$); within a horizon $H$ the compound chain realises $O(\log H)$ bits and the factorial chain $\Theta(H\log H)$; under the feasibility principle the derangement representation is the canonical finite definition of $e$. -/1954theorem p13021 : (((8 : ℚ) / ↑(Nat.factorial (12 : ℕ)) < (1 : ℚ) / (2 : ℚ) ^ (24 : ℕ) ∧ ∀ m < (11 : ℕ), ¬(8 : ℚ) / ↑(m + (1 : ℕ)).factorial < (1 : ℚ) / (2 : ℚ) ^ (24 : ℕ)) ∧ ((8 : ℚ) / ↑(Nat.factorial (19 : ℕ)) < (1 : ℚ) / (2 : ℚ) ^ (53 : ℕ) ∧ ∀ m < (18 : ℕ), ¬(8 : ℚ) / ↑(m + (1 : ℕ)).factorial < (1 : ℚ) / (2 : ℚ) ^ (53 : ℕ)) ∧ (8 : ℚ) / ↑(Nat.factorial (71 : ℕ)) < (1 : ℚ) / (2 : ℚ) ^ (333 : ℕ) ∧ ∀ m < (70 : ℕ), ¬(8 : ℚ) / ↑(m + (1 : ℕ)).factorial < (1 : ℚ) / (2 : ℚ) ^ (333 : ℕ)) ∧ ∀ (n : ℕ), (5 : ℕ) ≤ n → ((1 : ℝ) + (1 : ℝ) / ↑n) ^ n ≤ Real.exp (1 : ℝ) * ((4 : ℝ) * ↑n) / ((4 : ℝ) * ↑n + (1 : ℝ)) :=1955  And.intro @FRC.Epi.derangement_cost (@FRC.Epi.compound_cost)1956/-- 13:E2 (p13023) — Two-sided monotone enclosure: $v_n$ strictly increasing, $w_n$ strictly decreasing, $v_n<\piR<w_n$, and the exact width identity $w_n-v_n=w_n/(2n+1)$, certifying $\approx\log_2n$ bits by nested $\fQ$-intervals; the identification of the common limit with $\piR$ is the Wallis import (A6); verified for $n\le300$ against Machin brackets of width below $10^{-420}$. -/1957theorem p13023 : And (∀ (n : Nat), @LE.le Nat instLENat (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))) n → And (@LT.lt Real Real.instLT (@Rat.cast Real Real.instRatCast (@FRC.Epi.wallisV Rat Rat.instField n)) Real.pi) (@LT.lt Real Real.instLT Real.pi (@Rat.cast Real Real.instRatCast (@FRC.Epi.wallisW Rat Rat.instField n)))) (And (∀ (n : Nat), @LE.le Nat instLENat (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))) n → @Eq Rat (@HSub.hSub Rat Rat Rat (@instHSub Rat Rat.instSub) (@FRC.Epi.wallisW Rat Rat.instField n) (@FRC.Epi.wallisV Rat Rat.instField n)) (@HDiv.hDiv Rat Rat Rat (@instHDiv Rat Rat.instDiv) (@FRC.Epi.wallisW Rat Rat.instField n) (@HAdd.hAdd Rat Rat Rat (@instHAdd Rat Rat.instAdd) (@HMul.hMul Rat Rat Rat (@instHMul Rat Rat.instMul) (@OfNat.ofNat Rat (nat_lit 2) (@Rat.instOfNat (nat_lit 2))) (@Nat.cast Rat Rat.instNatCast n)) (@OfNat.ofNat Rat (nat_lit 1) (@Rat.instOfNat (nat_lit 1)))))) (And (∀ (n : Nat), @LT.lt Rat Rat.instLT (@FRC.Epi.wallisV Rat Rat.instField n) (@FRC.Epi.wallisV Rat Rat.instField (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) n (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))) (∀ (n : Nat), @LE.le Nat instLENat (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))) n → @LT.lt Rat Rat.instLT (@FRC.Epi.wallisW Rat Rat.instField (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) n (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@FRC.Epi.wallisW Rat Rat.instField n)))) :=1958  And.intro @FRC.Epi.wallis_enclosure (And.intro @FRC.Epi.wallis_width (And.intro @FRC.Epi.wallisV_strictMono (@FRC.Epi.wallisW_strictAnti)))1959/-- 13:E3 (p13024) — The arcsin chain $s_n=3\sum_{k\le n}\Cb{k}/((2k+1)16^{k})\in\fQ$ with external completion $\piR=6\arcsin\frac12$ and tail bound $|\piR-s_n|<4^{-n}/(2n+3)$ for $n\ge1$: geometric rate from the same combinatorial atoms as the Wallis pair. -/1960theorem p13024 : (56982451095683495439374565467485478486061627198245408555021816811556209980957932490824931053425856737444302864615815079280095539452134822710663747992660383090256176690756 / 18138077522740431478132504469278196026908888402936691374051205499784758924249616118578433027852823624088713136757082253607690672547607224629473421373404562473297119140625 : ℝ) ≤ Real.pi ∧ Real.pi ≤ (130195783561461477719700582162729520693370052310728319298679169305810308737653928066126520396560009514814646871106941551053006194003594103465911391825667397563687081581706376 / 41442605047058247458496271511585593410122504578565869919087156374128208580482492892372746919359245529262855323388051816332995956263674891122406052090809680521488189697265625 : ℝ) :=1961  @FRC.Epi.pi_bracket_241962/-- 13:E4 (p13025) — Horizon determination for $\pi$: the Machin chain $M_N\in\fQ$ has $|M_N-\piR|<17/((2N+3)5^{2N+3})$; the binary64 constant $884279719003555/281474976710656$ is the readout of $M_{10}$ with $N=10$ minimal; the first $100$ decimal digits are fixed by $M_{71}$; alternating pairing of the two arctangent series gives certified two-sided $\fQ$-enclosures at every truncation, the Gregory brackets $4S_{2m+1}<\piR<4S_{2m}$ of width $4/(4m+3)$ the base case. -/1963theorem p13025 : (∀ (N : ℕ), |FRC.Epi.machin N - Real.pi| < (17 : ℝ) / (((2 : ℝ) * ↑N + (3 : ℝ)) * (5 : ℝ) ^ ((2 : ℕ) * N + (3 : ℕ)))) ∧ (|Real.pi - FRC.Epi.binary64Pi| < (1 : ℝ) / (2 : ℝ) ^ (52 : ℕ) ∧ |FRC.Epi.machin (10 : ℕ) - FRC.Epi.binary64Pi| < (1 : ℝ) / (2 : ℝ) ^ (52 : ℕ) ∧ ∀ N ≤ (9 : ℕ), (1 : ℝ) / (2 : ℝ) ^ (52 : ℕ) < |FRC.Epi.machin N - FRC.Epi.binary64Pi|) ∧ |FRC.Epi.machin (71 : ℕ) - Real.pi| < (1 : ℝ) / (10 : ℝ) ^ (100 : ℕ) ∧ (∀ {x : ℝ}, (0 : ℝ) ≤ x → x < (1 : ℝ) → ∀ (k : ℕ), FRC.Epi.arctanSum x ((2 : ℕ) * k + (1 : ℕ)) ≤ Real.arctan x ∧ Real.arctan x ≤ FRC.Epi.arctanSum x ((2 : ℕ) * k)) ∧ (∀ (m : ℕ), FRC.Epi.machinLo m ≤ Real.pi ∧ Real.pi ≤ FRC.Epi.machinHi m) ∧ ∀ (m : ℕ), FRC.Epi.leibnizSum ((2 : ℕ) * m) ≤ Real.pi / (4 : ℝ) ∧ Real.pi / (4 : ℝ) ≤ FRC.Epi.leibnizSum ((2 : ℕ) * m + (1 : ℕ)) ∧ FRC.Epi.leibnizSum ((2 : ℕ) * m + (1 : ℕ)) - FRC.Epi.leibnizSum ((2 : ℕ) * m) = (1 : ℝ) / ((4 : ℝ) * ↑m + (1 : ℝ)) :=1964  And.intro @FRC.Epi.machin_bound (And.intro @FRC.Epi.readout_binary64_pi (And.intro @FRC.Epi.machin_hundred_digits (And.intro @FRC.Epi.arctan_pairing (And.intro @FRC.Epi.machin_pairing (@FRC.Epi.gregory_brackets)))))1965/-- 13:E5 (p13026) — The feasibility hierarchy: among $\fQ$-native constructors of $\pi$ the best known rate is geometric, $\Theta(k)$ steps (Machin, arcsin), against $\Theta(k/\log k)$ for the derangement chain of $e$; the circle count and the Leibniz/Wallis chains sit at $2^{k}$; the AGM is not $\fQ$-native. A factorial-rate chain exists for every real by rounding (and for $\pi$ by rounding the Machin chain), so the split is by kind of chain --- E-partial sums ($e$) against G-partial sums ($\pi$), master C26; whether $\piR$ is the value of an E-function with rational coefficients at a rational point is a question of the continuum (Fischler--Rivoal's conjecture $\operatorname{Frac}\mathcal E\cap\operatorname{Frac}\mathcal G=\overline{\Q}$ would answer it negatively), not a predicate of the frame. -/1966theorem p13026 : (∀ (x : ℝ) (n : ℕ), |x - ↑⌊x * ↑n.factorial⌋ / ↑n.factorial| < (1 : ℝ) / ↑n.factorial) ∧ (∀ (N : ℕ), |FRC.Epi.machin N - Real.pi| < (17 : ℝ) / (((2 : ℝ) * ↑N + (3 : ℝ)) * (5 : ℝ) ^ ((2 : ℕ) * N + (3 : ℕ)))) ∧ (∀ (m : ℕ), FRC.Epi.leibnizSum ((2 : ℕ) * m) ≤ Real.pi / (4 : ℝ) ∧ Real.pi / (4 : ℝ) ≤ FRC.Epi.leibnizSum ((2 : ℕ) * m + (1 : ℕ)) ∧ FRC.Epi.leibnizSum ((2 : ℕ) * m + (1 : ℕ)) - FRC.Epi.leibnizSum ((2 : ℕ) * m) = (1 : ℝ) / ((4 : ℝ) * ↑m + (1 : ℝ))) ∧ ∀ (n : ℕ), (5 : ℕ) ≤ n → ((1 : ℝ) + (1 : ℝ) / ↑n) ^ n ≤ Real.exp (1 : ℝ) * ((4 : ℝ) * ↑n) / ((4 : ℝ) * ↑n + (1 : ℝ)) :=1967  And.intro @FRC.Epi.rounding_chain (And.intro @FRC.Epi.machin_bound (And.intro @FRC.Epi.gregory_brackets (@FRC.Epi.compound_cost)))1968/-- 13:F1 (p13027) — Wilson reflection: for an odd prime $\p$ and $0\le k\le\p-1$, $1/k!\equiv-(-1)^{k}(\p-1-k)!\pmod\p$. -/1969theorem p13027 : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], ∀ k ≤ p - (1 : ℕ), (↑k.factorial)⁻¹ = -(-1 : ZMod p) ^ k * ↑(p - (1 : ℕ) - k).factorial :=1970  @FRC.Epi.wilson_reflection_zmod1971set_option linter.defProp false in1972/-- 13:F2 (p13028) — The wall identity and the terminal residue of $e$: $\dr{(\p-1)}\equiv\Ku{\p}\pmod\p$ (the odd-prime case of the Mijajlovi\'c--\v Sami congruence, A4), hence $\rep{\varepsilon_{\p-1}}=-(\Ku{\p})^{-1}$ whenever $\p\nmid\Ku{\p}$; existence of the terminal link on a shell is equivalent to $\p\nmid\Ku{\p}$, universal existence over the shells of the totality to the vanishing of Kurepa's certificate (Z1); re-verified in the derangement form for all $121{,}126$ odd primes $\p<1.6\times10^{6}$ with zero failures of either condition. Beyond the wall $n!\equiv0$: $n=\p-1$ is the factorial horizon. -/1973def p13028 := And.intro @FRC.Epi.derangements_wall_zmod (@FRC.Epi.terminal_residue)1974set_option linter.defProp false in1975/-- 13:F3 (p13029) — Antiperiodicity: $\dr{(n+\p)}\equiv-\dr{n}\pmod\p$ for every odd prime $\p$ and every $n\ge0$ of the totality, so $\dr{n}\bmod\p$ depends on $n\bmod2\p$; the blind set $Z_0(\p)=\{n<\p:\dr{n}\equiv0\}$ always contains $1$, and Kurepa's hypothesis is $\p-1\notin Z_0(\p)$ for every odd prime $\p$ of the totality. -/1976def p13029 := @FRC.Epi.derangements_antiperiodic_zmod1977set_option linter.defProp false in1978/-- 13:F4 (p13030) — Series duals at the wall: $\sum_{k<\p}(-1)^{k}/k!\equiv-\Ku{\p}$ and $\sum_{k<\p}1/k!\equiv-A(\p)$, $A(\p)$ the alternating factorial sum; the group law $\exp(1)\exp(-1)=1$ does not survive, $\Ku{\p}A(\p)\equiv3,0,21,28,132,258$ at $\p=7,13,29,101,257,1009$; on $\p=13$ the direct series residue vanishes ($A(13)\equiv0$) while the derangement side survives ($\Ku{13}\equiv10$) --- a second ground for the canonicity of D5. -/1979def p13030 := @FRC.Epi.series_duals_zmod1980/-- 13:F7 (p13033) — The fixed-shell tower of $e$: with $\delta_m=\ctr{(-1)^{m}\eP}$ and $q_m=((m\p)!+\delta_m)/\dr{(m\p)}$, $\rep{q_m}=\eP$ exactly at every grade (since $(m\p)!\equiv0$ and $\dr{(m\p)}\equiv(-1)^{m}$ by F3) while $q_m\to\eR$ with the certificate $|q_m-\eR|<(m\p)!/(\dr{(m\p)}\dr{(m\p+1)})+2\kap/\dr{(m\p)}$; on $\p=13$, $q_2$ differs from $\eR$ by $3.98\times10^{-26}$ and every member reads $6$. Compatibility, not selection. -/1981theorem p13033 : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], p ≠ (2 : ℕ) → ∀ (m : ℕ), (1 : ℕ) ≤ m → ∀ (e δ : ZMod p), δ = (-1 : ZMod p) ^ m * e → ↑(m * p).factorial = (0 : ZMod p) ∧ ↑(numDerangements (m * p)) = (-1 : ZMod p) ^ m ∧ (↑(m * p).factorial + δ) / ↑(numDerangements (m * p)) = e :=1982  @FRC.Epi.tower_e_exact_zmod1983set_option linter.defProp false in1984/-- 13:F8 (p13066) — The tail identity: $j!\,\dr{(\p-1-j)}\equiv(-1)^{j}\bigl(\Ku{\p}-\Ku{j}\bigr)\pmod\p$ for $0\le j\le\p-1$ ($j=0$ is F2); hence $n\in Z_0(\p)$ iff $\Ku{(\p-1-n)}\equiv\Ku{\p}$: the blind set counts the collisions of the partial sums of the left factorial with their total, $n=1$ is the forced collision $\Ku{(\p-2)}\equiv\Ku{\p}$, and Kurepa's hypothesis is the return-to-origin question of the walk with steps $j!$. -/1985def p13066 := And.intro @FRC.Epi.tail_identity_zmod (@FRC.Epi.blind_iff_collision)1986/-- 13:G1 (p13034) — The legibility window: with $m=(\p-1)/2$, $\p\nmid\Cb{n}$ for $1\le n\le m$ and $\p\mid\Cb{n}$ for $m<n<\p$ (Kummer, A3): the residue line of the Wallis chain is defined on exactly $[1,m]$, blind-free below the wall and totally blind on $(m,\p)$; on a frame shell the last legible scale $n=2\kap$ is the angular address of $-1$. -/1987theorem p13034 : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ), ((2 : ℕ) * n ≤ p - (1 : ℕ) → ¬p ∣ n.centralBinom) ∧ (p ≤ (2 : ℕ) * n → n < p → p ∣ n.centralBinom) :=1988  @FRC.Epi.legibility_window1989/-- 13:G2 (p13035) — The half-wall terminus, the calibration face: $\rep{w_m}=m^{-1}=\piA^{-1}=4\piA\equiv-2$ for every odd prime of the totality, the return statistics trivialising at the wall ($16^{m}\equiv1$, $\Cb{m}^{2}\equiv1$) and exposing the naked inverse scale; the identities are the calibration web of $2\piA\equiv-1$, and $\rep{w_{\piA}}\piA\equiv1\iff(4\kap)^{2}\equiv1$; the lower chain is blind at the wall and nowhere below. -/1990theorem p13035 : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], p ≠ (2 : ℕ) → ∀ (m : ℕ), p = (2 : ℕ) * m + (1 : ℕ) → (16 : ZMod p) ^ m = (1 : ZMod p) ∧ ↑m.centralBinom ^ (2 : ℕ) = (1 : ZMod p) ∧ FRC.Epi.wallisW m = (-2 : ZMod p) ∧ (↑m)⁻¹ = (-2 : ZMod p) ∧ (4 : ZMod p) * ↑m = (-2 : ZMod p) :=1991  @FRC.Epi.half_wall_terminus1992set_option linter.defProp false in1993/-- 13:G3 (p13036) — The quarter-wall two-squares invariant: for $\p\equiv1\pmod4$, $\p=a^{2}+b^{2}$ with $a$ odd, $a\equiv1\pmod4$, at the quarter scale $n=\kap$ (the address of $\im$) $\rep{w_\kap}=\kap^{-1}(2a)^{-2}=-(a^{2})^{-1}=(b^{2})^{-1}$, by Gauss's congruence (A3) with $\kap\equiv-4^{-1}$; the invariant exists precisely under the frame condition; verified for all $211$ primes $\p\equiv1\pmod4$ below $3000$. -/1994def p13036 := @FRC.Epi.quarter_wall_invariant1995/-- 13:G4 (p13037) — Second order at the half wall: $w_m\equiv-2+2\p(q_\p(4)-1)\pmod{\p^{2}}$ with $q_\p(4)\equiv2q_\p(2)$, exact to $\p^{3}$ through Morley (A3); the universal $-2$ persists to $\p^{2}$ exactly for the $\pi$-Wieferich primes $4^{\p-1}\equiv1+\p\pmod{\p^{2}}$ (OEIS A355959, G10), which are exactly $5$ and $45827$ below $1.08\times10^{11}$ \cite{oeisA355959}, re-verified here to $2^{35}$ (\src{pi\_wieferich128}; $45827\equiv3\pmod4$, so $\p=5$ is the only Subject shell among them; two below $10^{6}$ against the range frequency $\sum_{\p<10^{6}}1/\p\approx2.4$); the normalised quotients equidistribute empirically \apx. -/1996theorem p13037 : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], p ≠ (2 : ℕ) → ∀ (m : ℕ), p = (2 : ℕ) * m + (1 : ℕ) → ↑m.centralBinom = (-1 : ZMod (p ^ (2 : ℕ))) ^ m * (4 : ZMod (p ^ (2 : ℕ))) ^ (p - (1 : ℕ)) → (2 : ZMod (p ^ (2 : ℕ))) * (16 : ZMod (p ^ (2 : ℕ))) ^ m = (2 : ZMod (p ^ (2 : ℕ))) * (((-2 : ZMod (p ^ (2 : ℕ))) + (2 : ZMod (p ^ (2 : ℕ))) * ↑p * (↑(FRC.Epi.fq (4 : ℕ) p) - (1 : ZMod (p ^ (2 : ℕ))))) * (↑m * ↑m.centralBinom ^ (2 : ℕ))) ∧ ((2 : ZMod (p ^ (2 : ℕ))) * (16 : ZMod (p ^ (2 : ℕ))) ^ m = (2 : ZMod (p ^ (2 : ℕ))) * ((-2 : ZMod (p ^ (2 : ℕ))) * (↑m * ↑m.centralBinom ^ (2 : ℕ))) ↔ ↑(FRC.Epi.fq (4 : ℕ) p) = (1 : ZMod p)) :=1997  @FRC.Epi.half_wall_second_order1998/-- 13:G5 (p13038) — Lucas revivals and self-similarity: beyond the wall $n\ge\p$ is legible for $w$ precisely when every base-$\p$ digit of $n$ is at most $m$ and $\p\nmid n$ (on $\p=13$ the two-digit revivals number $(2\kap)^{2}=36$); on revival scales $\Cb{n}$ factorises digitwise (Lucas, A3); at the first revival $\rep{v_\p}\equiv8$ universally and $v_\p\equiv8+16\p(2q_\p(2)-1)\pmod{\p^{2}}$ by Wolstenholme. -/1999theorem p13038 : (∀ (p : ℕ) [hp : Fact (Nat.Prime p)], p ≠ (2 : ℕ) → (2 : ZMod p) * (16 : ZMod p) ^ p / (↑((2 : ℕ) * p + (1 : ℕ)) * ↑p.centralBinom ^ (2 : ℕ)) = (8 : ZMod p)) ∧ ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (r : ℕ), ↑(((2 : ℕ) * p ^ r).choose (p ^ r)) = (2 : ZMod p) :=2000  And.intro @FRC.Epi.first_revival (@FRC.Epi.choose_two_mul_pow)2001/-- 13:G9 (p13042) — The fixed-shell tower of $\pi$: for $n=\p^{r}$, with $\delta_\p=\ctr{\piA B_n-A_n}=\ctr{-34}$, the member $\widehat\pi_{\p,r}=(2\cdot16^{\p^{r}}+\delta_\p)/((2\p^{r}+1)\Cb{\p^{r}}^{2})$ reads $\rep{\widehat\pi_{\p,r}}=\piA$ exactly for every $r$ (Lucas and Fermat give $\Cb{n}\equiv2$, $16^{n}\equiv16$, $B_n\equiv4$) while converging externally to $\piR$; on $\p=13$, $\delta_{13}=5$. -/2002theorem p13042 : (∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (κ : ℕ), p = (4 : ℕ) * κ + (1 : ℕ) → ∀ (r : ℕ), (1 : ℕ) ≤ r → ∀ (δ : ZMod p), δ = (-34 : ZMod p) → ((2 : ZMod p) * (16 : ZMod p) ^ p ^ r + δ) / (↑((2 : ℕ) * p ^ r + (1 : ℕ)) * ↑(p ^ r).centralBinom ^ (2 : ℕ)) = (2 : ZMod p) * ↑κ) ∧ ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (r : ℕ), ↑(((2 : ℕ) * p ^ r).choose (p ^ r)) = (2 : ZMod p) :=2003  And.intro @FRC.Epi.tower_pi_exact (@FRC.Epi.choose_two_mul_pow)2004/-- 13:G10 (p13067) — The $\pi$-Wieferich condition in three forms: $4^{\p-1}\equiv1+\p\pmod{\p^{2}}$ iff $q_\p(4)\equiv1$ iff $2q_\p(2)\equiv1\pmod\p$, with $q_\p(4)=2q_\p(2)+\p\,q_\p(2)^{2}$ exactly; Eisenstein's $2q_\p(2)\equiv-H_{(\p-1)/2}\pmod\p$ ($H_m=\sum_{j\le m}1/j$) makes it $H_{(\p-1)/2}\equiv-1$, and $(\p+2)^{\p-1}\equiv1\pmod{\p^{2}}$ identifies it with OEIS A355959 \cite{oeisA355959}. -/2005theorem p13067 : (∀ (p : ℕ) [hp : Fact (Nat.Prime p)], p ≠ (2 : ℕ) → ((4 : ZMod (p ^ (2 : ℕ))) ^ (p - (1 : ℕ)) = (1 : ZMod (p ^ (2 : ℕ))) + ↑p ↔ ↑(FRC.Epi.fq (4 : ℕ) p) = (1 : ZMod p)) ∧ (↑(FRC.Epi.fq (4 : ℕ) p) = (1 : ZMod p) ↔ (2 : ZMod p) * ↑(FRC.Epi.fq (2 : ℕ) p) = (1 : ZMod p))) ∧ (∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (m : ℕ), p = (2 : ℕ) * m + (1 : ℕ) → (2 : ZMod p) * ↑(FRC.Epi.fq (2 : ℕ) p) = -∑ j ∈ Finset.range m, (↑(j + (1 : ℕ)))⁻¹) ∧ (∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (m : ℕ), p = (2 : ℕ) * m + (1 : ℕ) → ((4 : ZMod (p ^ (2 : ℕ))) ^ (p - (1 : ℕ)) = (1 : ZMod (p ^ (2 : ℕ))) + ↑p ↔ ∑ j ∈ Finset.range m, (↑(j + (1 : ℕ)))⁻¹ = (-1 : ZMod p))) ∧ ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], p ≠ (2 : ℕ) → ((↑p + (2 : ZMod (p ^ (2 : ℕ)))) ^ (p - (1 : ℕ)) = (1 : ZMod (p ^ (2 : ℕ))) ↔ (2 : ZMod p) * ↑(FRC.Epi.fq (2 : ℕ) p) = (1 : ZMod p)) :=2006  And.intro @FRC.Epi.piWieferich_iff (And.intro @FRC.Epi.eisenstein (And.intro @FRC.Epi.piWieferich_iff_harmonic (@FRC.Epi.piWieferich_iff_oeis)))2007/-- 13:H3 (p13045) — Exact calibration of $e$ is impossible: with $\theta=2\piR\lambda(\im)/(\p-1)$ the frame angle of $\eP$, $\theta\ne1$ in every shell ($\theta=1$ would make $\piR$ rational, A2); $\chi(\eP)$ is a root of unity while $e^{\imR}$ is not, so the identification is intrinsically horizon-limited. -/2008theorem p13045 : (∀ (n l : ℕ), (0 : ℕ) < l → (2 : ℝ) * Real.pi * ↑l / ↑n ≠ (1 : ℝ)) ∧ ∀ (n : ℕ), (0 : ℕ) < n → Complex.exp (↑n * Complex.I) ≠ (1 : ℂ) :=2009  And.intro @FRC.Epi.calibration_ne_one (@FRC.Epi.exp_I_ne_one)2010/-- 13:H4 (p13069) — Calibrated shells at every fixed precision $\varepsilon\le1$: the $\varepsilon$-calibrated shells have asymptotic density $2\varepsilon/\piR$ among the shells $\p\equiv1\pmod4$ (A7), so large enough ranges hold them, $\chi(\eP)$ within $\varepsilon$ of $e^{\imR}$ there; the uniform model reads $N$ shells down to the nearest-hit scale $\piR/(2N)$ \apx. Below $10^{6}$: $260$ shells within $0.01$ against $249$ predicted; the best, $\p=778933$, within $4\times10^{-5}$, decided exactly. -/2011theorem p13069 : Nat.Prime (778933 : ℕ) ∧ (123966 : ZMod (778933 : ℕ)) ^ (2 : ℕ) = (-1 : ZMod (778933 : ℕ)) ∧ |(2 : ℝ) * Real.pi * (123966 : ℝ) / (778932 : ℝ) - (1 : ℝ)| < (4 / 100000 : ℝ) ∧ (39 / 1000000 : ℝ) < |(2 : ℝ) * Real.pi * (123966 : ℝ) / (778932 : ℝ) - (1 : ℝ)| :=2012  @FRC.Epi.calibrated_7789332013/-- 13:H5 (p13047) — The null experiment: whether $\gen^{\lambda(\pm\im)}\equiv-(\Ku{\p})^{-1}$ for some primitive root and either orientation, varied independently, is the index condition $\gcd(s,\p-1)=\gcd(\lambda(\pm\im),\p-1)$; over the $210$ primes $\p\equiv1\pmod4$, $5<\p<3000$, it holds for $94$ against $96.0\pm6.6$ expected under independence ($54$ against $57.9\pm6.2$ with the orientation tied to the generator), the correlation of the two angular addresses $-0.10$ at deviation $\approx0.07$ \apx: no invariant pointwise identification of the angular and radial carriers of $e$. -/2014theorem p13047 : (∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (g : ZMod p), IsPrimitiveRoot g (p - (1 : ℕ)) → ∀ (l s : ℕ), (∃ u, u.Coprime (p - (1 : ℕ)) ∧ (g ^ u) ^ l = g ^ s) ↔ l.gcd (p - (1 : ℕ)) = s.gcd (p - (1 : ℕ))) ∧ ∀ (n l s : ℕ) [NeZero n], (∃ u, u.Coprime n ∧ u * l ≡ s [MOD n]) ↔ l.gcd n = s.gcd n :=2015  And.intro @FRC.Epi.index_condition_shell (@FRC.Epi.index_condition)2016/-- 13:I1 (p13048) — Emergence of the classical $e$: (i) in every shell with $\p>n_1+|Z_0(\p)|+1$ a non-blind scale in $[n_1,n_1+|Z_0(\p)|]$ reads out $\ro(\eR)$, at binary64 exactly $18!/\dr{18}$; (ii) the frame-internal continuation is the residue line, antiperiodic in its derangement denominators, blind on $Z_0(\p)$, terminating on $-(\Ku{\p})^{-1}$, read out beyond $n_1$ as one dyadic rational; (iii) $\chi(\eP)$ approaches $e^{\imR}$ along the calibrated shells, exact calibration impossible, no pointwise link between the carriers. Composed from D4, F2, F3, F5, H3--H5. -/2017theorem p13048 : (|Real.exp (1 : ℝ) - FRC.Epi.binary64E| < (1 : ℝ) / (2 : ℝ) ^ (52 : ℕ) ∧ |FRC.Epi.epsChain (18 : ℕ) - FRC.Epi.binary64E| < (1 : ℝ) / (2 : ℝ) ^ (52 : ℕ) ∧ ∀ (n : ℕ), (2 : ℕ) ≤ n → n ≤ (17 : ℕ) → (1 : ℝ) / (2 : ℝ) ^ (52 : ℕ) < |FRC.Epi.epsChain n - FRC.Epi.binary64E|) ∧ (∀ (n l : ℕ), (0 : ℕ) < l → (2 : ℝ) * Real.pi * ↑l / ↑n ≠ (1 : ℝ)) ∧ Nat.Prime (778933 : ℕ) ∧ (123966 : ZMod (778933 : ℕ)) ^ (2 : ℕ) = (-1 : ZMod (778933 : ℕ)) ∧ |(2 : ℝ) * Real.pi * (123966 : ℝ) / (778932 : ℝ) - (1 : ℝ)| < (4 / 100000 : ℝ) ∧ (39 / 1000000 : ℝ) < |(2 : ℝ) * Real.pi * (123966 : ℝ) / (778932 : ℝ) - (1 : ℝ)| :=2018  And.intro @FRC.Epi.readout_binary64 (And.intro @FRC.Epi.calibration_ne_one (@FRC.Epi.calibrated_778933))2019set_option linter.defProp false in2020/-- 13:I2 (p13049) — Emergence of the classical $\pi$: (i) the plateau readout of $\fQ$-native chains, at binary64 exactly $M_{10}$, the Wallis pair certifying two-sided enclosures at every scale; (ii) the residue line on $[1,2\kap]$ with the quarter-wall invariant $-(a^{2})^{-1}$, the half-wall terminus $-2$, the second-order Fermat quotient with $\pi$-Wieferich set $\{5,45827\}$, Morley exactness at $\p^{3}$, total blindness beyond the address of $-1$, Lucas revivals, the arcsin wall vanishing to $\p^{2}$ with the Bernoulli third order and the Euler content displaced beyond the wall; (iii) $\chi(-1)=e^{\imR\piR}$ exactly. Composed from E2, E4, G1--G7, H2. -/2021def p13049 := And.intro @FRC.Epi.readout_binary64_pi (And.intro @FRC.Epi.wallis_enclosure (@FRC.Epi.half_wall_second_order))2022/-- 13:I3 (p13050) — The duality: $\pi$ is angular-exact and wall-trivial (tautological carrier, terminus the calibration face $-2$, Fermat quotient one order down, two-squares quarter invariant, empty blind set below the wall, geometric $\fQ$-rate, the series law split Bernoulli/Euler across the wall) and $e$ angular-approximate and wall-wild (calibration impossible, terminus the open Kurepa quantity, no quarter invariant, Poisson blind set, factorial $\fQ$-rate, the group law broken at the wall); each constant exact on the axis where the other is approximate: $\pi$ a structural, $e$ a statistical constant of the finite frame. -/2023theorem p13050 : (∀ (n l : ℕ), (0 : ℕ) < l → (2 : ℝ) * Real.pi * ↑l / ↑n ≠ (1 : ℝ)) ∧ (∀ (N : ℕ), |FRC.Epi.machin N - Real.pi| < (17 : ℝ) / (((2 : ℝ) * ↑N + (3 : ℝ)) * (5 : ℝ) ^ ((2 : ℕ) * N + (3 : ℕ)))) ∧ ∀ (n : ℕ), (5 : ℕ) ≤ n → ((1 : ℝ) + (1 : ℝ) / ↑n) ^ n ≤ Real.exp (1 : ℝ) * ((4 : ℝ) * ↑n) / ((4 : ℝ) * ↑n + (1 : ℝ)) :=2024  And.intro @FRC.Epi.calibration_ne_one (And.intro @FRC.Epi.machin_bound (@FRC.Epi.compound_cost))2025set_option linter.defProp false in2026/-- 13:J6 (p13057) — Two constants, two walls: both attach their full-resolution shell content to sparse-prime problems (Kurepa non-vanishing for $e$, a prescribed Fermat quotient of Wieferich type for $\pi$); for each shell the bounded observer holds an exact finite certificate and holds no uniform certificate across all shells --- per-instance decidability without a uniform bound, the characteristic shape of statements at the arithmetic horizon; Kurepa's hypothesis is not thereby decided; the frequency of the persistence shells is a range reading (G4), their totality not a predicate of the paper. -/2027def p13057 := And.intro @FRC.Epi.derangements_wall_zmod (@FRC.Epi.half_wall_second_order)2028-- end ledger predicates20292030end FRC.Epi2031