IndisputableMonolith.NumberTheory.FinitePhaseCompleteness

   1import Mathlib
   2
   3/-!
   4# Finite Phase Completeness
   5
   6The first phase-budget theorem: a non-identity integer ledger has a finite
   7cyclic quotient in which its phase is not the identity phase.
   8
   9This is the finite arithmetic content behind the RS statement that a
  10non-identity reciprocal ledger cannot be invisible in all finite phase
  11quotients.
  12-/
  13
  14namespace IndisputableMonolith
  15namespace NumberTheory
  16namespace FinitePhaseCompleteness
  17
  18/-- A reciprocal integer ledger carrier. -/
  19structure ReciprocalIntegerLedger where
  20  carrier : ℕ
  21  carrier_pos : 0 < carrier
  22  nonidentity : carrier ≠ 1
  23  has_reciprocal_budget : ∃ N : ℕ, carrier ∣ N ^ 2
  24
  25/-- Every reciprocal integer ledger has a finite cyclic phase quotient. -/
  26theorem finite_phase_completeness (L : ReciprocalIntegerLedger) :
  27    ∃ c : ℕ, 0 < c ∧ Nonempty (ZMod c) := by
  28  exact ⟨L.carrier, L.carrier_pos, ⟨0⟩⟩
  29
  30/-- A non-identity positive integer is separated from the identity in a finite
  31cyclic quotient.  We use the quotient `Z/(carrier+1)Z`: the carrier has phase
  32`-1`, not `1`. -/
  33theorem finite_phase_separates_nonidentity (L : ReciprocalIntegerLedger) :
  34    ∃ c : ℕ, 0 < c ∧ (L.carrier : ZMod c) ≠ 1 := by
  35  refine ⟨L.carrier + 1, Nat.succ_pos L.carrier, ?_⟩
  36  intro h
  37  have hmod := (ZMod.natCast_eq_natCast_iff' L.carrier 1 (L.carrier + 1)).mp h
  38  have hleft : L.carrier % (L.carrier + 1) = L.carrier :=
  39    Nat.mod_eq_of_lt (Nat.lt_succ_self L.carrier)
  40  have hright : 1 % (L.carrier + 1) = 1 := by
  41    apply Nat.mod_eq_of_lt
  42    exact Nat.succ_lt_succ L.carrier_pos
  43  rw [hleft, hright] at hmod
  44  exact L.nonidentity hmod
  45
  46end FinitePhaseCompleteness
  47end NumberTheory
  48end IndisputableMonolith
  49