structure
definition
RegistryPredictionsCert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Unification.RegistryPredictionsProved on GitHub at line 169.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
166/-! ## Section: Combined Registry Certificate -/
167
168/-- **CERTIFICATE**: Registry predictions with calculated bounds. -/
169structure RegistryPredictionsCert where
170 omega_lambda_upper : 11/16 - (alpha / Real.pi) < 11/16
171 omega_lambda_lower : 0 < 11/16 - (alpha / Real.pi)
172 phi_6_lower : (17 : ℝ) < (phi : ℝ)^6
173 phi_6_upper : (phi : ℝ)^6 < (18 : ℝ)
174 phi_11_lower : (180 : ℝ) < (phi : ℝ)^11
175 hierarchy_exists : ∀ (Δr : ℕ), Δr > 0 →
176 ∃ (ratio : ℝ), ratio = (phi : ℝ)^Δr ∧ ratio > 1
177
178/-- **THEOREM**: Registry predictions certificate is inhabited. -/
179theorem registry_predictions_cert_exists : ∃ _ : RegistryPredictionsCert, True :=
180 ⟨⟨omega_lambda_lt_11_16,
181 omega_lambda_positive,
182 phi_6_hierarchy_bounds.1,
183 phi_6_hierarchy_bounds.2,
184 phi_11_hierarchy_lower,
185 fun Δr hΔr => hierarchy_phi_power_structure Δr hΔr⟩,
186 trivial⟩
187
188end RegistryPredictionsProved
189end Unification
190end IndisputableMonolith