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

coherence_collapse_cert

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)

 141theorem coherence_collapse_cert : CoherenceCollapseCert where
 142  C_is_2A := C_equals_2A

proof body

Tactic-mode proof.

 143  born_positive := born_weight_pos
 144  normalization := born_normalization
 145  threshold_nanogram := by unfold m_coh_kg; norm_num
 146
 147end
 148
 149end CoherenceCollapseBridge
 150end Gravity
 151end IndisputableMonolith

depends on (6)

Lean names referenced from this declaration's body.