`RSPrimePhaseBoxTheorem`

definition

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.PrimePhaseDistribution
domain: NumberTheory
line: 68 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.PrimePhaseDistribution on GitHub at line 68.

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

  65
  66/-- The missing first-principles bridge from the RS prime ledger to
  67Erdős-Straus square-budget phase hits. -/
  68structure RSPrimePhaseBoxTheorem : Type where
  69  distribution : PrimePhaseBoxDistribution
  70  /-- Marker that the theorem is intended to be derived from RCL/J-cost prime
  71  ledger machinery rather than inserted as an arithmetic oracle. -/
  72  from_rcl_prime_ledger : True
  73
  74/-- Once the RS prime phase box theorem is derived, it supplies the desired
  75bounded balanced search engine. -/
  76def boundedBalancedSearch_of_rsPrimePhaseBoxTheorem
  77    (rs : RSPrimePhaseBoxTheorem) :
  78    BoundedBalancedSearchEngine :=
  79  boundedBalancedSearch_of_primePhaseBoxDistribution rs.distribution
  80
  81/-- Final conditional form, with the remaining theorem named explicitly. -/
  82theorem erdos_straus_residual_from_rs_prime_phase_box
  83    (rs : RSPrimePhaseBoxTheorem)
  84    {n : ℕ} (hn : ResidualTrap n) :
  85    ErdosStrausRCL.HasRationalErdosStrausRepr (n : ℚ) :=
  86  bounded_balanced_search_solved
  87    (boundedBalancedSearch_of_rsPrimePhaseBoxTheorem rs) hn
  88
  89end PrimePhaseDistribution
  90end NumberTheory
  91end IndisputableMonolith

papers checked against this theorem

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