`RSPrimePhaseEquidistribution`

definition

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.EffectivePrimePhaseInput
domain: NumberTheory
line: 61 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.EffectivePrimePhaseInput on GitHub at line 61.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  58
  59/-- The intended RS source theorem.  This is the final remaining input:
  60derive `EffectivePrimePhaseInput` from the RCL prime-ledger machinery. -/
  61structure RSPrimePhaseEquidistribution where
  62  effective_input : EffectivePrimePhaseInput
  63  /-- Marker: this theorem is meant to be sourced from RCL/J-cost prime-ledger
  64  phase distribution, not from finite search. -/
  65  from_rcl_prime_ledger : True
  66
  67def effectivePrimePhaseInput_of_rsPrimePhaseEquidistribution
  68    (rs : RSPrimePhaseEquidistribution) :
  69    EffectivePrimePhaseInput :=
  70  rs.effective_input
  71
  72theorem erdos_straus_residual_from_rsPrimePhaseEquidistribution
  73    (rs : RSPrimePhaseEquidistribution)
  74    {n : ℕ} (hn : ResidualTrap n) :
  75    ErdosStrausRCL.HasRationalErdosStrausRepr (n : ℚ) :=
  76  erdos_straus_residual_from_effectivePrimePhaseInput
  77    (effectivePrimePhaseInput_of_rsPrimePhaseEquidistribution rs) hn
  78
  79end PrimePhaseInput
  80end NumberTheory
  81end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.