Z_dropQ4

formal source

  20  if tildeQ i > 0 then (tildeQ i)^2 + (tildeQ i)^4 else 0
  21
  22/-- Drop the Q^4 term everywhere in Z. -/
  23noncomputable def Z_dropQ4 (i : Species) : Int :=
  24  if tildeQ i > 0 then 4 + (tildeQ i)^2 else 0
  25
  26/-- Break the integerization ˜Q = 6Q by using ˜Q' = 3Q (integerized) instead. -/
  27-- Provided above as a parameter `tildeQ_broken3`.
  28
  29/-- Recompute Z with the broken integerization. -/
  30noncomputable def Z_break6Q (i : Species) : Int :=
  31  4 + (tildeQ_broken3 i)^2 + (tildeQ_broken3 i)^4
  32
  33/-- Anchor-equality predicate for a candidate Z-map: residues must match the original. -/
  34def AnchorEq (Z' : Species → Int) : Prop := ∀ i, Fgap (Z' i) = Fgap (Z i)
  35
  36/-- If anchor-equality holds for a transformed Z, then Z' must agree with Z on nonnegative values. -/
  37lemma anchorEq_implies_Zeq_nonneg
  38  {Z' : Species → Int} (h : AnchorEq (Species:=Species) (Z:=Z) (Fgap:=Fgap) Z')
  39  (h_inj : ∀ a b : ℤ, 0 ≤ a → 0 ≤ b → Fgap a = Fgap b → a = b)
  40  {i : Species} (hZnonneg : 0 ≤ Z i) (hZ'nonneg : 0 ≤ Z' i) : Z' i = Z i := by
  41  have h_eq := h i
  42  exact h_inj (Z' i) (Z i) hZ'nonneg hZnonneg h_eq
  43
  44/-- If anchor-equality held under any ablation, it would contradict the certified anchor. -/
  45def ablation_contradictions : Prop :=
  46  (¬ AnchorEq (Species:=Species) (Z:=Z) (Fgap:=Fgap) (Z_dropPlus4 (Species:=Species) (tildeQ:=tildeQ))) ∧
  47  (¬ AnchorEq (Species:=Species) (Z:=Z) (Fgap:=Fgap) (Z_dropQ4 (Species:=Species) (tildeQ:=tildeQ))) ∧
  48  (¬ AnchorEq (Species:=Species) (Z:=Z) (Fgap:=Fgap) (Z_break6Q (Species:=Species) (tildeQ_broken3:=tildeQ_broken3)))
  49
  50end
  51
  52end Ablation
  53end IndisputableMonolith