IndisputableMonolith.NumberTheory.LogicErdosStrausBoxPhase

   1import Mathlib
   2import IndisputableMonolith.Foundation.ArithmeticFromLogic
   3import IndisputableMonolith.NumberTheory.ErdosStrausBoxPhase
   4import IndisputableMonolith.NumberTheory.LogicErdosStrausRCL
   5
   6/-!
   7  LogicErdosStrausBoxPhase.lean
   8
   9  Logic-native adapter for the Erdős-Straus square-budget box phase.
  10
  11  The native combinatorial structures are given over `LogicNat`; the final
  12  theorem transports to the existing `ℕ` box-phase theorem, then returns the
  13  result as a `LogicRat` representation via `LogicErdosStrausRCL`.
  14-/
  15
  16namespace IndisputableMonolith
  17namespace NumberTheory
  18namespace LogicErdosStrausBoxPhase
  19
  20open Foundation.ArithmeticFromLogic
  21open Foundation.ArithmeticFromLogic.LogicNat
  22open Foundation.RationalsFromLogic.LogicRat
  23open LogicErdosStrausRCL
  24
  25/-- Divisibility over recovered naturals. -/
  26def DvdL (a b : LogicNat) : Prop := ∃ k : LogicNat, b = a * k
  27
  28/-- A recovered divisor exponent-box point. -/
  29structure DivisorExponentBoxLogic (N : LogicNat) where
  30  d : LogicNat
  31  e : LogicNat
  32  d_pos : 0 < d
  33  e_pos : 0 < e
  34  square_budget : d * e = N * N
  35
  36def boxDivisorLogic {N : LogicNat} (box : DivisorExponentBoxLogic N) : LogicNat :=
  37  box.d
  38
  39def boxComplementLogic {N : LogicNat} (box : DivisorExponentBoxLogic N) : LogicNat :=
  40  box.e
  41
  42theorem box_logic_toNat_square_budget {N : LogicNat} (box : DivisorExponentBoxLogic N) :
  43    toNat box.d * toNat box.e = toNat N ^ 2 := by
  44  have h := congrArg toNat box.square_budget
  45  rw [toNat_mul, toNat_mul] at h
  46  simpa [pow_two] using h
  47
  48/-- Logic-native box-phase hit, transported to the current classical hit
  49predicate. This keeps the finite phase proof surface stable while recording
  50that the carrier is recovered from the Law of Logic. -/
  51def HitsBalancedPhaseLogic (n c : LogicNat) : Prop :=
  52  ErdosStrausBoxPhase.HitsBalancedPhase (toNat n) (toNat c)
  53
  54theorem hitsBalancedPhaseLogic_iff_classical (n c : LogicNat) :
  55    HitsBalancedPhaseLogic n c ↔
  56      ErdosStrausBoxPhase.HitsBalancedPhase (toNat n) (toNat c) :=
  57  Iff.rfl
  58
  59/-- A recovered box-phase hit gives the logic-native rational
  60Erdős-Straus representation. -/
  61theorem box_phase_hit_gives_repr_logic {n c : LogicNat}
  62    (h : HitsBalancedPhaseLogic n c) :
  63    HasRationalErdosStrausReprLogic (fromRat (toNat n : ℚ)) := by
  64  apply reprLogic_fromRat_of_classical
  65  exact ErdosStrausBoxPhase.box_phase_hit_gives_repr h
  66
  67end LogicErdosStrausBoxPhase
  68end NumberTheory
  69end IndisputableMonolith
  70