IndisputableMonolith.NumberTheory.SubsetProductPhase

   1import Mathlib
   2import IndisputableMonolith.NumberTheory.ErdosStrausBoxPhase
   3
   4/-!
   5# Subset-Product Phase Layer
   6
   7This module isolates the finite subgroup-generation layer needed by the
   8Erdős-Straus residual proof.
   9
  10The analytic prime-distribution theorem should not be asked to construct
  11the unit fractions directly.  It should only supply a square-budget divisor
  12whose phase is the target phase.  The finite layer below converts that phase
  13hit into the already-proved `HitsBalancedPhase` predicate.
  14-/
  15
  16namespace IndisputableMonolith
  17namespace NumberTheory
  18namespace SubsetProductPhase
  19
  20open ErdosStrausBoxPhase
  21open ErdosStrausRotationHierarchy
  22
  23/-- A phase-generating subset-product witness.
  24
  25The `box` field is the square-budget divisor selected by the prime-phase
  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,
  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,
  82   fun ⟨hit⟩ => generated_phase_hit_gives_HitsBalancedPhase hit⟩
  83
  84end SubsetProductPhase
  85end NumberTheory
  86end IndisputableMonolith
  87