SubsetProductPhaseHit

formal source

  26generator.  The divisibility conditions say that both the generated divisor
  27and its complementary divisor land in the target phase `-N` modulo `c`.
  28-/
  29structure SubsetProductPhaseHit (n c : ℕ) where
  30  x : ℕ
  31  N : ℕ
  32  box : DivisorExponentBox N
  33  n_pos : 0 < n
  34  c_pos : 0 < c
  35  x_pos : 0 < x
  36  N_pos : 0 < N
  37  N_eq : N = n * x
  38  c_eq : c = 4 * x - n
  39  divisor_phase : c ∣ N + boxDivisor box
  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,