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

metaCost_eq_zero_iff

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)

 100theorem metaCost_eq_zero_iff (R S : MetaCarrier) :
 101    metaCost R S = 0 ↔ R = S := by

proof body

Term-mode proof.

 102  unfold metaCost
 103  by_cases h : R = S
 104  · simp [h]
 105  · simp [h]
 106
 107/-! ## Forced-Arithmetic Invariance: The Meta-Theorem -/
 108
 109/-- **The meta-theorem reified.** For any two realizations, the canonical
 110equivalence between their forced arithmetic objects exists. This is
 111exactly `universal_forcing_via_NNO`, packaged as the comparison law of
 112the meta-realization. -/

used by (1)

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

depends on (19)

Lean names referenced from this declaration's body.