multiplicative_identity

formal source

 146
 147/-- **(L1) Identity.** The derived cost vanishes at the multiplicative
 148identity. -/
 149theorem multiplicative_identity (m : MultiplicativeRecognizer 𝒞) :
 150    m.cost 1 = 0 := by
 151  show m.comparator 1 1 = 0
 152  exact m.laws.identity 1 (by norm_num)
 153
 154/-- **(L2) Reciprocal symmetry.** The derived cost is symmetric under
 155reciprocation, a consequence of non-contradiction plus scale invariance. -/
 156theorem multiplicative_reciprocal_symmetry
 157    (m : MultiplicativeRecognizer 𝒞) :
 158    ∀ x : ℝ, 0 < x → m.cost x = m.cost (x⁻¹) := by
 159  intro x hx
 160  show m.comparator x 1 = m.comparator (x⁻¹) 1
 161  -- C(x, 1) = C(1, x) (non-contradiction) = C(x⁻¹, 1) (scale by x⁻¹)
 162  have hsymm : m.comparator x 1 = m.comparator 1 x :=
 163    m.laws.non_contradiction x 1 hx (by norm_num)
 164  have hxinv : (0 : ℝ) < x⁻¹ := inv_pos.mpr hx
 165  have hscale : m.comparator (x⁻¹ * x) (x⁻¹ * 1) = m.comparator x 1 :=
 166    m.laws.scale_invariant x 1 (x⁻¹) hx (by norm_num) hxinv
 167  -- (x⁻¹ * x) = 1 and (x⁻¹ * 1) = x⁻¹
 168  have hxx : x⁻¹ * x = 1 := inv_mul_cancel₀ (ne_of_gt hx)
 169  rw [hxx, mul_one] at hscale
 170  -- so C(1, x⁻¹) = C(x, 1)
 171  -- chain: C(x, 1) = C(1, x) (above), and C(1, x⁻¹) = C(x, 1) gives
 172  -- C(1, x) and C(1, x⁻¹) both equal C(x, 1)... use non-contradiction on x⁻¹
 173  have hsymm2 : m.comparator (x⁻¹) 1 = m.comparator 1 (x⁻¹) :=
 174    m.laws.non_contradiction (x⁻¹) 1 hxinv (by norm_num)
 175  rw [hsymm2, ← hscale]
 176
 177/-! ## Headline Certificate -/
 178
 179/-- **L4-from-Multiplicative-Recognizer Certificate.**