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

extension_to_consistent

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)

 324theorem extension_to_consistent
 325    (κ₁ κ₂ : CostFunction Config)
 326    (cal₁ : Calibration κ₁) (cal₂ : Calibration κ₂)
 327    (h_same_α : cal₁.α = cal₂.α)
 328    (h_same_δ : cal₁.δ = cal₂.δ)
 329    (Γ : Config) (h_consistent : IsConsistent Γ)
 330    (h_indep : Independent cal₁.α Γ) :
 331    κ₁.C (join cal₁.α Γ) = κ₂.C (join cal₁.α Γ) := by

proof body

Tactic-mode proof.

 332  have h₁ : κ₁.C (join cal₁.α Γ) = κ₁.C cal₁.α + κ₁.C Γ :=
 333    κ₁.additivity cal₁.α Γ h_indep
 334  have h_indep₂ : Independent cal₂.α Γ := h_same_α ▸ h_indep
 335  have h₂ : κ₂.C (join cal₂.α Γ) = κ₂.C cal₂.α + κ₂.C Γ :=
 336    κ₂.additivity cal₂.α Γ h_indep₂
 337  have h_α_eq : κ₁.C cal₁.α = κ₂.C cal₂.α := by
 338    rw [cal₁.agrees, cal₂.agrees, h_same_δ]
 339  have h_Γ_eq : κ₁.C Γ = κ₂.C Γ := by
 340    rw [cost_zero_of_consistent κ₁ Γ h_consistent,
 341        cost_zero_of_consistent κ₂ Γ h_consistent]
 342  rw [h₁, h_α_eq, h_Γ_eq, ← h₂, h_same_α]
 343
 344end Calibration
 345
 346/-! ### Master constraint certificate -/
 347
 348/--
 349**Master certificate**: bundles the recognition-work constraint

depends on (6)

Lean names referenced from this declaration's body.