def
definition
gap6_resolution
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.QuarkCoordinateReconciliation on GitHub at line 227.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
224 "are explicitly marked as hypothesis-layer."
225
226/-- The official resolution -/
227def gap6_resolution : Resolution := {}
228
229/-- Gap 6 is now resolved -/
230theorem gap6_resolved : gap6_resolution.status = "RESOLVED_BY_LAYER_SEPARATION" := rfl
231
232/-! ## Claim Dependencies -/
233
234/-- Claims that depend on the core integer-rung convention -/
235def core_dependent_claims : List String := [
236 "mass_rung_scaling",
237 "predict_mass_pos",
238 "yardstick_derived",
239 "sector_formulas"
240]
241
242/-- Claims that depend on the hypothesis quarter-ladder convention -/
243def hypothesis_dependent_claims : List String := [
244 "H_top_mass_match",
245 "H_bottom_mass_match",
246 "H_charm_mass_match",
247 "quark_mass_verified"
248]
249
250/-- Verify that hypothesis claims are in Physics/, not Masses/ -/
251theorem hypothesis_claims_properly_located :
252 ∀ c ∈ hypothesis_dependent_claims,
253 c ∈ ["H_top_mass_match", "H_bottom_mass_match", "H_charm_mass_match", "quark_mass_verified"] := by
254 intro c hc
255 exact hc
256
257end QuarkCoordinateReconciliation