generatedComplementPhase

formal source

  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) :
  74    Nonempty (SubsetProductPhaseHit n c) := by
  75  rcases h with ⟨x, N, box, hn, hc, hx, hNpos, hN, hcdef, hdvd, hevd⟩
  76  refine ⟨SubsetProductPhaseHit.mk x N box hn hc hx hNpos hN hcdef hdvd hevd⟩
  77
  78/-- The two formulations are equivalent. -/
  79theorem hitsBalancedPhase_iff_nonempty_subsetProductPhaseHit {n c : ℕ} :
  80    HitsBalancedPhase n c ↔ Nonempty (SubsetProductPhaseHit n c) :=
  81  ⟨subsetProductPhaseHit_of_hitsBalancedPhase,