structure
definition
EffectivePrimePhaseInput
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NumberTheory.EffectivePrimePhaseInput on GitHub at line 27.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
24
25/-- Effective prime phase input: for every trapped ledger, bounded prime
26phase supply produces an actual subset-product phase hit. -/
27structure EffectivePrimePhaseInput where
28 bound : ℕ → ℕ
29 supplies_generators :
30 ∀ n : ℕ, ResidualTrap n →
31 ∃ c : ℕ, c ≤ bound n ∧ AdmissibleHardGate c ∧ Nonempty (SubsetProductPhaseHit n c)
32
33/-- Effective prime phase supply gives the exact distribution statement
34required by the residual Erdős-Straus chain. -/
35def primePhaseBoxDistribution_of_effectivePrimePhaseInput
36 (input : EffectivePrimePhaseInput) :
37 PrimePhaseBoxDistribution where
38 bound := input.bound
39 hits := by
40 intro n hn
41 rcases input.supplies_generators n hn with ⟨c, hcbound, hc, ⟨hit⟩⟩
42 exact ⟨c, hcbound, hc, generated_phase_hit_gives_HitsBalancedPhase hit⟩
43
44/-- Effective prime phase supply gives bounded balanced search. -/
45def boundedBalancedSearch_of_effectivePrimePhaseInput
46 (input : EffectivePrimePhaseInput) :
47 BoundedBalancedSearchEngine :=
48 boundedBalancedSearch_of_primePhaseBoxDistribution
49 (primePhaseBoxDistribution_of_effectivePrimePhaseInput input)
50
51/-- Effective prime phase supply solves the residual trapped class. -/
52theorem erdos_straus_residual_from_effectivePrimePhaseInput
53 (input : EffectivePrimePhaseInput)
54 {n : ℕ} (hn : ResidualTrap n) :
55 ErdosStrausRCL.HasRationalErdosStrausRepr (n : ℚ) :=
56 erdos_straus_residual_from_prime_phase_box_distribution
57 (primePhaseBoxDistribution_of_effectivePrimePhaseInput input) hn