`finite_phase_completeness`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.FinitePhaseCompleteness
domain: NumberTheory
line: 26 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.NumberTheory.FinitePhaseCompleteness on GitHub at line 26.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.