logicIntToInt

formal source

  16open FinitePhaseCompleteness
  17
  18abbrev LogicInt := Foundation.IntegersFromLogic.LogicInt
  19abbrev logicIntToInt : LogicInt → Int := Foundation.IntegersFromLogic.LogicInt.toInt
  20
  21/-- A recovered integer ledger is non-identity when its `Int` recovery is
  22positive and not equal to one. -/
  23structure LogicIntNonIdentityReciprocal (z : LogicInt) : Prop where
  24  pos : 0 < logicIntToInt z
  25  nonidentity : logicIntToInt z ≠ 1
  26  reciprocal_budget : ∃ N : ℕ, 0 < N ∧ Int.natAbs (logicIntToInt z) ∣ N ^ 2
  27
  28/-- Positive recovered integers yield positive natural carriers. -/
  29theorem natAbs_pos_of_logicInt_pos
  30    {z : LogicInt}
  31    (hz : 0 < logicIntToInt z) :
  32    0 < Int.natAbs (logicIntToInt z) := by
  33  exact Int.natAbs_pos.mpr (ne_of_gt hz)
  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