IndisputableMonolith.Verification.ZMapConstraintPass2

   1import Mathlib
   2
   3/-!
   4# Z-Map Constraint Pass 2
   5
   6This module gives a partial derivational closure for the `Z`-map polynomial:
   7
   8`Z = c + a·Q̃² + b·Q̃⁴`.
   9
  10Using the quark family targets
  11- up-type: `Z_u = 276` at `Q̃ = 4`,
  12- down-type: `Z_d = 24` at `Q̃ = -2`,
  13
  14and mild structural constraints
  15- `0 ≤ a` (quadratic weight nonnegative),
  16- `0 < b` (quartic term present),
  17
  18we prove the coefficients are uniquely forced:
  19- `a = 1`,
  20- `b = 1`,
  21- `c = 4`.
  22
  23This does not yet derive the polynomial from first principles of recognition
  24topology, but it removes a large part of coefficient arbitrariness.
  25-/
  26
  27namespace IndisputableMonolith
  28namespace Verification
  29namespace ZMapConstraintPass2
  30
  31/-- Quartic-even charge polynomial template. -/
  32def Zpoly (c a b q : ℤ) : ℤ :=
  33  c + a * q ^ (2 : ℕ) + b * q ^ (4 : ℕ)
  34
  35/-- Quark constraints force `(a,b,c) = (1,1,4)` under mild structural assumptions. -/
  36theorem quark_constraints_force_coeffs
  37    {c a b : ℤ}
  38    (h_up   : Zpoly c a b 4    = 276)
  39    (h_down : Zpoly c a b (-2) = 24)
  40    (ha_nonneg : 0 ≤ a)
  41    (hb_pos : 0 < b) :
  42    a = 1 ∧ b = 1 ∧ c = 4 := by
  43  have hup : c + 16 * a + 256 * b = 276 := by
  44    simpa [Zpoly, mul_comm, mul_left_comm, mul_assoc, add_comm, add_left_comm, add_assoc]
  45      using h_up
  46  have hdown : c + 4 * a + 16 * b = 24 := by
  47    simpa [Zpoly, mul_comm, mul_left_comm, mul_assoc, add_comm, add_left_comm, add_assoc]
  48      using h_down
  49  have hrel : a + 20 * b = 21 := by
  50    linarith [hup, hdown]
  51  have hb_one : b = 1 := by
  52    omega
  53  have ha_one : a = 1 := by
  54    omega
  55  have hc_four : c = 4 := by
  56    linarith [hdown, ha_one, hb_one]
  57  exact ⟨ha_one, hb_one, hc_four⟩
  58
  59/-- With the forced coefficients and lepton offset `c = 0`, the lepton value is fixed. -/
  60theorem lepton_value_with_forced_coeffs :
  61    Zpoly 0 1 1 (-6) = 1332 := by
  62  norm_num [Zpoly]
  63
  64/-- Quark values with forced coefficients are exactly the two family anchors. -/
  65theorem quark_values_with_forced_coeffs :
  66    Zpoly 4 1 1 4 = 276 ∧ Zpoly 4 1 1 (-2) = 24 := by
  67  constructor <;> norm_num [Zpoly]
  68
  69end ZMapConstraintPass2
  70end Verification
  71end IndisputableMonolith
  72