theorem
proved
uniqueness_three_indep
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.CostFromDistinction on GitHub at line 275.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
272configurations. The same argument extends by induction to any
273finite pairwise-independent decomposition.
274-/
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
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
294theorem then says that any other cost function `κ'` agreeing with
295`κ` on `α` and on the chosen indecomposable inconsistent
296configurations agrees with `κ` everywhere expressible as
297independent joins of those generators.
298-/
299structure Calibration (κ : CostFunction Config) where
300 /-- A distinguished inconsistent configuration. -/
301 α : Config
302 /-- The chosen positive cost value. -/
303 δ : ℝ
304 /-- The chosen value is positive. -/
305 δ_pos : 0 < δ