LogicIntNonIdentityReciprocal

formal source

  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
  50      exact habs_cast
  51    exact h.nonidentity h_toInt
  52  has_reciprocal_budget := by
  53    rcases h.reciprocal_budget with ⟨N, _hNpos, hdiv⟩