IndisputableMonolith.NumberTheory.LogicLedgerInterop

   1import Mathlib
   2import IndisputableMonolith.Foundation.IntegersFromLogic
   3import IndisputableMonolith.NumberTheory.FinitePhaseCompleteness
   4
   5/-!
   6# Logic Ledger Interop
   7
   8Transfers the recovered `LogicInt` ledger to the existing integer-ledger
   9phase-budget surface.
  10-/
  11
  12namespace IndisputableMonolith
  13namespace NumberTheory
  14namespace LogicLedgerInterop
  15
  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
  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
  68