boxComplementLogic

formal source

  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