theorem
proved
tactic proof
polyCost_pos
show as:
view Lean formalization →
formal statement (Lean)
200theorem polyCost_pos {f : Polynomial F}
201 (hf : f ≠ 0) (h_not_unit : ¬ IsUnit f)
202 (hF : 2 ≤ Fintype.card F) :
203 0 < polyCost f := by
proof body
Tactic-mode proof.
204 -- Since f is a nonzero non-unit, normalizedFactors f is nonempty.
205 have h_factors_ne : normalizedFactors f ≠ 0 := by
206 intro h_empty
207 have h_prod : (normalizedFactors f).prod = normalize f :=
208 prod_normalizedFactors_eq hf
209 rw [h_empty, Multiset.prod_zero] at h_prod
210 have h_norm_unit : IsUnit (normalize f) := h_prod ▸ isUnit_one
211 have h_f_unit : IsUnit f :=
212 (associated_normalize f).symm.isUnit h_norm_unit
213 exact h_not_unit h_f_unit
214 -- Pick a factor P from normalizedFactors f.
215 obtain ⟨P, hP_mem⟩ := Multiset.exists_mem_of_ne_zero h_factors_ne
216 have hP_irr : Irreducible P := irreducible_of_normalized_factor P hP_mem
217 have hP_deg : 0 < P.natDegree := irreducible_natDegree_pos hP_irr
218 have hP_pos : 0 < polyPrimeCost P := polyPrimeCost_pos hP_deg hF
219 -- Decompose the multiset sum: P contributes hP_pos, others ≥ 0.
220 unfold polyCost
221 have h_decomp :
222 (normalizedFactors f).map polyPrimeCost
223 = polyPrimeCost P ::ₘ ((normalizedFactors f).erase P).map polyPrimeCost := by
224 rw [← Multiset.map_cons polyPrimeCost P]
225 congr 1
226 exact (Multiset.cons_erase hP_mem).symm
227 rw [h_decomp, Multiset.sum_cons]
228 apply add_pos_of_pos_of_nonneg hP_pos
229 apply Multiset.sum_nonneg
230 intro x hx
231 obtain ⟨Q, _, hQ_eq⟩ := Multiset.mem_map.mp hx
232 rw [← hQ_eq]
233 exact polyPrimeCost_nonneg Q
234
235/-! ## Cost spectrum certificate -/
236
237/-- Master certificate: the elementary properties of the polynomial
238 cost spectrum. Mirrors `cost_spectrum_certificate` from the integer
239 module. Used by the companion paper. -/