`Resolution`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.QuarkCoordinateReconciliation
domain: Physics
line: 206 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.QuarkCoordinateReconciliation on GitHub at line 206.

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

 203/-! ## Resolution Status -/
 204
 205/-- Formal resolution of Gap 6 -/
 206structure Resolution where
 207  /-- Status: RESOLVED by layer separation -/
 208  status : String := "RESOLVED_BY_LAYER_SEPARATION"
 209  /-- Resolution method: explicit layer assignment, not equivalence -/
 210  method : String := "Layer separation (Core vs Hypothesis)"
 211  /-- Core convention: integer rungs -/
 212  core_convention : Convention := .IntegerRung
 213  /-- Hypothesis convention: quarter-ladder -/
 214  hypothesis_convention : Convention := .QuarterLadder
 215  /-- Whether equivalence was proved: NO (and not required) -/
 216  equivalence_proved : Bool := false
 217  /-- Reason equivalence not needed -/
 218  equivalence_note : String := "Conventions serve different purposes; equivalence not expected"
 219  /-- Summary for reviewers -/
 220  summary : String :=
 221    "Gap 6 resolved: Integer rungs are CORE (parameter-free); " ++
 222    "Quarter-ladder is HYPOTHESIS (phenomenological). " ++
 223    "No equivalence claimed. Claims depending on quarter-ladder " ++
 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",

papers checked against this theorem

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