DivisorExponentBoxLogic

formal source

  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