pith. machine review for the scientific record. sign in
theorem proved term proof

erdos_straus_residual_from_prime_phase_box_distribution

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  46theorem erdos_straus_residual_from_prime_phase_box_distribution
  47    (dist : PrimePhaseBoxDistribution)
  48    {n : ℕ} (hn : ResidualTrap n) :
  49    ErdosStrausRCL.HasRationalErdosStrausRepr (n : ℚ) :=

proof body

Term-mode proof.

  50  bounded_balanced_search_solved
  51    (boundedBalancedSearch_of_primePhaseBoxDistribution dist) hn
  52
  53/-! ## Existing RS prime-distribution surface
  54
  55The imported prime modules currently provide:
  56
  57* prime ledger cost additivity (`PrimeCostSpectrum`);
  58* an RH/frustration-spectrum bridge to aggregate prime distribution
  59  (`PrimeDistributionBridge`, currently an upstream repair target under
  60  the active Lean toolchain).
  61
  62They do not yet prove the square-budget residue-box hit required above.
  63The following structure records the exact extra theorem needed from the
  64RS prime-distribution program. -/
  65
  66/-- The missing first-principles bridge from the RS prime ledger to
  67Erdős-Straus square-budget phase hits. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (14)

Lean names referenced from this declaration's body.