pith. machine review for the scientific record. sign in
theorem proved term proof

hard_problem_dissolution_consistent

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)

 212theorem hard_problem_dissolution_consistent : HardProblemDissolution := {

proof body

Term-mode proof.

 213  identity := fun q => q.valence_is_neg_strain,
 214  no_gap := fun _ _ => True.intro,
 215  not_emergent := fun _ _ => True.intro
 216}
 217
 218end RRF.Foundation
 219end IndisputableMonolith

depends on (4)

Lean names referenced from this declaration's body.