reciprocalIntegerLedger_of_logicInt

formal source

  34
  35/-- Convert a non-identity recovered integer ledger into the Nat-level
  36reciprocal ledger used by finite phase completeness. -/
  37def reciprocalIntegerLedger_of_logicInt
  38    {z : LogicInt}
  39    (h : LogicIntNonIdentityReciprocal z) :
  40    ReciprocalIntegerLedger where
  41  carrier := Int.natAbs (logicIntToInt z)
  42  carrier_pos := natAbs_pos_of_logicInt_pos h.pos
  43  nonidentity := by
  44    intro hcarrier
  45    have h_toInt_abs : Int.natAbs (logicIntToInt z) = 1 := hcarrier
  46    have h_toInt : logicIntToInt z = 1 := by
  47      have habs_cast : (Int.natAbs (logicIntToInt z) : Int) = 1 := by
  48        exact_mod_cast h_toInt_abs
  49      rw [Int.natAbs_of_nonneg (le_of_lt h.pos)] at habs_cast
  50      exact habs_cast
  51    exact h.nonidentity h_toInt
  52  has_reciprocal_budget := by
  53    rcases h.reciprocal_budget with ⟨N, _hNpos, hdiv⟩
  54    exact ⟨N, hdiv⟩
  55
  56/-- Recovered non-identity integer ledgers have a finite phase separating
  57them from identity. -/
  58theorem logicInt_finite_phase_separates
  59    {z : LogicInt}
  60    (h : LogicIntNonIdentityReciprocal z) :
  61    ∃ c : ℕ, 0 < c ∧
  62      ((reciprocalIntegerLedger_of_logicInt h).carrier : ZMod c) ≠ 1 :=
  63  finite_phase_separates_nonidentity (reciprocalIntegerLedger_of_logicInt h)
  64
  65end LogicLedgerInterop
  66end NumberTheory
  67end IndisputableMonolith