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

uniqueness_three_indep

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)

 275theorem uniqueness_three_indep
 276    (κ₁ κ₂ : CostFunction Config)
 277    (S : Set Config)
 278    (h_agree : ∀ Γ ∈ S, κ₁.C Γ = κ₂.C Γ) :
 279    ∀ Γ₁ Γ₂ Γ₃, Γ₁ ∈ S → Γ₂ ∈ S → Γ₃ ∈ S →
 280      Independent Γ₁ Γ₂ → Independent Γ₁ Γ₃ → Independent Γ₂ Γ₃ →
 281      Independent Γ₁ (join Γ₂ Γ₃) →
 282      κ₁.C (join Γ₁ (join Γ₂ Γ₃)) = κ₂.C (join Γ₁ (join Γ₂ Γ₃)) := by

proof body

Term-mode proof.

 283  intro Γ₁ Γ₂ Γ₃ h₁_mem h₂_mem h₃_mem h₁₂ h₁₃ h₂₃ h₁_join
 284  rw [additive_three κ₁ Γ₁ Γ₂ Γ₃ h₁₂ h₁₃ h₂₃ h₁_join,
 285      additive_three κ₂ Γ₁ Γ₂ Γ₃ h₁₂ h₁₃ h₂₃ h₁_join,
 286      h_agree Γ₁ h₁_mem, h_agree Γ₂ h₂_mem, h_agree Γ₃ h₃_mem]
 287
 288/-! ### Calibration: a canonical cost-unit -/
 289
 290/--
 291A **calibration** of a cost function on a configuration space is a
 292choice of distinguished inconsistent configuration `α` and a positive
 293value `δ` such that `κ.C α = δ`. The recognition-work constraint

depends on (28)

Lean names referenced from this declaration's body.