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

identity_implies_normalized

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)

 167theorem identity_implies_normalized (C : ComparisonOperator)
 168    (hId : Identity C) :
 169    IsNormalized (derivedCost C) := by

proof body

Term-mode proof.

 170  unfold IsNormalized derivedCost
 171  exact hId 1 one_pos
 172
 173/-- **Translation lemma 2 (Non-contradiction + Scale invariance ⇒ Reciprocity)**:
 174If a comparison operator is single-valued under argument reordering and
 175depends only on ratios, then the derived cost function is invariant under
 176inversion of its argument: F(x) = F(1/x).
 177
 178The chain of equalities:
 179  F(x) = C(x, 1)                       definition of derivedCost
 180       = C(1, x)                       non-contradiction
 181       = C(x⁻¹·1, x⁻¹·x)               scale invariance (multiply both args by x⁻¹)
 182       = C(x⁻¹, 1)                     simplify (x⁻¹·1 = x⁻¹, x⁻¹·x = 1)
 183       = F(x⁻¹)                        definition of derivedCost
 184-/

used by (2)

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

depends on (22)

Lean names referenced from this declaration's body.