TargetPhase

formal source

  40  complement_phase : c ∣ N + boxComplement box
  41
  42/-- The target phase in the residual quotient. -/
  43def TargetPhase (N c : ℕ) : ZMod c :=
  44  -(N : ZMod c)
  45
  46/-- The generated divisor phase. -/
  47def generatedDivisorPhase {n c : ℕ} (hit : SubsetProductPhaseHit n c) : ZMod c :=
  48  (boxDivisor hit.box : ZMod c)
  49
  50/-- The complementary divisor phase. -/
  51def generatedComplementPhase {n c : ℕ} (hit : SubsetProductPhaseHit n c) : ZMod c :=
  52  (boxComplement hit.box : ZMod c)
  53
  54/-- A generated target phase gives the box-phase predicate used by the
  55Erdős-Straus closure module. -/
  56theorem generated_phase_hit_gives_HitsBalancedPhase {n c : ℕ}
  57    (hit : SubsetProductPhaseHit n c) :
  58    HitsBalancedPhase n c := by
  59  refine ⟨hit.x, hit.N, hit.box,
  60    hit.n_pos, hit.c_pos, hit.x_pos, hit.N_pos,
  61    hit.N_eq, hit.c_eq, hit.divisor_phase, hit.complement_phase⟩
  62
  63/-- Hence a generated target phase gives the rational Erdős-Straus
  64representation. -/
  65theorem generated_phase_hit_gives_repr {n c : ℕ}
  66    (hit : SubsetProductPhaseHit n c) :
  67    ErdosStrausRCL.HasRationalErdosStrausRepr (n : ℚ) :=
  68  box_phase_hit_gives_repr (generated_phase_hit_gives_HitsBalancedPhase hit)
  69
  70/-- Converse: a `HitsBalancedPhase` predicate gives a `SubsetProductPhaseHit`
  71witness.  The two are isomorphic (Prop existential vs Type structure). -/
  72theorem subsetProductPhaseHit_of_hitsBalancedPhase {n c : ℕ}
  73    (h : HitsBalancedPhase n c) :