pith. machine review for the scientific record. sign in
structure definition def or abbrev

Resolution

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 206structure Resolution where
 207  /-- Status: RESOLVED by layer separation -/
 208  status : String := "RESOLVED_BY_LAYER_SEPARATION"

proof body

Definition body.

 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 -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (17)

Lean names referenced from this declaration's body.