IndisputableMonolith.NumberTheory.LogicErdosStrausRCL

   1import Mathlib
   2import IndisputableMonolith.Foundation.RationalsFromLogic
   3import IndisputableMonolith.NumberTheory.ErdosStrausRCL
   4
   5/-!
   6  LogicErdosStrausRCL.lean
   7
   8  Logic-native Erdős-Straus rational representation adapter.
   9
  10  The rational layer is stated over `LogicRat`; all algebraic content is
  11  transported through `LogicRat.toRat` to the existing `ℚ` theorem surface.
  12-/
  13
  14namespace IndisputableMonolith
  15namespace NumberTheory
  16namespace LogicErdosStrausRCL
  17
  18open Foundation.RationalsFromLogic
  19open Foundation.RationalsFromLogic.LogicRat
  20
  21/-- Logic-native Erdős-Straus rational representation. -/
  22def HasRationalErdosStrausReprLogic (n : LogicRat) : Prop :=
  23  ErdosStrausRCL.HasRationalErdosStrausRepr (toRat n)
  24
  25theorem reprLogic_iff_classical (n : LogicRat) :
  26    HasRationalErdosStrausReprLogic n ↔
  27      ErdosStrausRCL.HasRationalErdosStrausRepr (toRat n) :=
  28  Iff.rfl
  29
  30theorem reprLogic_of_classical {n : LogicRat}
  31    (h : ErdosStrausRCL.HasRationalErdosStrausRepr (toRat n)) :
  32    HasRationalErdosStrausReprLogic n :=
  33  h
  34
  35theorem classical_of_reprLogic {n : LogicRat}
  36    (h : HasRationalErdosStrausReprLogic n) :
  37    ErdosStrausRCL.HasRationalErdosStrausRepr (toRat n) :=
  38  h
  39
  40/-- Transport a classical rational representation to the recovered rational
  41whose image is the given classical rational. -/
  42theorem reprLogic_fromRat_of_classical {n : ℚ}
  43    (h : ErdosStrausRCL.HasRationalErdosStrausRepr n) :
  44    HasRationalErdosStrausReprLogic (fromRat n) := by
  45  simpa [HasRationalErdosStrausReprLogic, toRat_fromRat] using h
  46
  47end LogicErdosStrausRCL
  48end NumberTheory
  49end IndisputableMonolith
  50