Standard Model Higgs Cosh Bsmpredictions

The cosh potential and its predictions

The Standard Model's Higgs field is usually drawn as a Mexican hat: a quartic polynomial that gives the Higgs boson its mass and its self-interactions. The framework called Recognition Science (RS) starts from a different shape, the hyperbolic cosine, or cosh. Its potential is V(h) = Λ⁴·(cosh(h/v) − 1), where h is the Higgs field, v is its vacuum value, and Λ sets the energy scale. Unlike the Mexican hat's finite polynomial, the cosh is an infinite series with only even powers of h; all odd Taylor coefficients vanish.

That evenness is the first proved difference. In the machine-checked library of formal theorems, V_cosh_is_even shows the cosh potential is symmetric under h → −h, while the Standard Model's Mexican-hat potential is not. The library proves V_cosh_neq_V_SM: for any nonzero Higgs mass and positive vacuum value, the two functions disagree at some field value. A concrete witness sits at h = 1 and h = −1, where the cosh matches itself but the Mexican hat does not.

Under the bridge that identifies the collider Higgs field linearly with the RS log coordinate, the library derives three quantitative predictions. The trilinear self-coupling modifier κ_λ3 equals 0, because the cosh has no cubic term. The quartic modifier κ_λ4 equals 1/3, a factor of three below the Standard Model. And a genuine beyond-Standard-Model vertex appears at sixth order, with strength λ₆ = m_H²/(720v⁴), positive for any physical mass and vacuum value. These are theorem-encoded in kappa_lambda_3_RS_eq_zero, kappa_lambda_4_RS_eq_one_third, and lambda_6_RS_pos.

The library packages these into a single falsifier statement, HiggsCoshBSMFalsifier, proved as a theorem. The name is deliberate: the predictions are testable. HL-LHC di-Higgs production, targeting a precision of ±0.5 on κ_λ, can rule the zero-trilinear prediction in or out. FCC-hh tri-Higgs events would probe the quartic. If the cosh is right, the Standard Model's cubic self-coupling should be absent; if the Standard Model is right, the cosh is dead.

One frontier remains open. The predictions above assume the canonical kinetic term ½(∂ε)² in RS-native units. A different substrate kinetic term K(ε)·(∂ε)² would change the field redefinition and shift the coefficients. The library records this as kinetic_term_shape_frontier, a placeholder for a derivation that does not yet exist. Until that frontier closes, the framework predicts a non-trivial deviation from the Standard Model, but its exact magnitude depends on the kinetic-term shape.

/-- The cosh potential is invariant under `h ↦ -h`. -/
theorem V_cosh_is_even (m_H v h : ℝ) : V_cosh m_H v (-h) = V_cosh m_H v h := by
  unfold V_cosh
  have hneg : (-h) / v = -(h / v) := by ring
  rw [hneg, Real.cosh_neg]

/-- The SM Mexican-hat is **not** even: `V_SM(1) - V_SM(-1) = m_H²/v`,
    which is nonzero for any nonzero `m_H` and `v ≠ 0`. -/
theorem V_SM_difference_not_zero
    {m_H v : ℝ} (hmH : m_H ≠ 0) (hv : 0 < v) :
    V_SM m_H v 1 - V_SM m_H v (-1) = m_H ^ 2 / v := by
  rw [V_SM_at_one, V_SM_at_neg_one]; ring

/-- **THEOREM**: `V_cosh` and `V_SM` are not equal as functions whenever
    `m_H ≠ 0` and `v > 0`. The two potentials disagree at some real `h`.

    Concrete witness: at `h = 1` and `h = -1`, `V_cosh` agrees with itself
    (cosh is even) while `V_SM` does not (`V_SM(1) - V_SM(-1) = m_H²/v ≠ 0`).
    Therefore at least one of `h = 1` or `h = -1` gives `V_cosh ≠ V_SM`. -/
theorem V_cosh_neq_V_SM
    {m_H v : ℝ} (hmH : m_H ≠ 0) (hv : 0 < v) :
    ∃ h : ℝ, V_cosh m_H v h ≠ V_SM m_H v h := by
  by_contra h_all
  push_neg at h_all
  -- V_cosh agrees with V_SM at every h.
  have h1  := h_all 1
  have hm1 := h_all (-1)
  -- Cosh is even at h = 1.
  have heven : V_cosh m_H v 1 = V_cosh m_H v (-1) := by
    have := V_cosh_is_even m_H v 1
    linarith [this]
  -- Therefore V_SM(1) = V_SM(-1).
  have hSM_eq : V_SM m_H v 1 = V_SM m_H v (-1) := by
    rw [← h1, ← hm1]; exact heven
  -- But V_SM(1) - V_SM(-1) = m_H²/v ≠ 0.
  have hdiff := V_SM_difference_not_zero hmH hv
  have hzero : V_SM m_H v 1 - V_SM m_H v (-1) = 0 := by
    rw [hSM_eq]; ring
  rw [hzero] at hdiff
  -- 0 = m_H²/v with v > 0 forces m_H² = 0, hence m_H = 0; contradiction.
  have hv_ne : v ≠ 0 := ne_of_gt hv
  have hmH2_zero : m_H ^ 2 = 0 := by
    have h_eq : m_H ^ 2 / v * v = m_H ^ 2 := by field_simp
    have h_eq2 : (0 : ℝ) * v = m_H ^ 2 := by rw [← hdiff] at h_eq; linarith
    have : m_H ^ 2 = 0 := by linarith [h_eq2]
    exact this
  exact hmH (pow_eq_zero_iff (n := 2) (by norm_num) |>.mp hmH2_zero)

theorem kappa_lambda_3_RS_eq_zero : kappa_lambda_3_RS = 0 := rfl

theorem kappa_lambda_4_RS_eq_one_third : kappa_lambda_4_RS = 1 / 3 := rfl

theorem lambda_6_RS_pos {m_H v : ℝ} (hmH : 0 < m_H) (hv : 0 < v) :
    0 < lambda_6_RS m_H v := by
  unfold lambda_6_RS
  have h_num : 0 < m_H ^ 2 := by positivity
  have h_den : 0 < 720 * v ^ 4 := by positivity
  exact div_pos h_num h_den

theorem higgsCoshBSMFalsifier : HiggsCoshBSMFalsifier where
  kappa_3_zero  := kappa_lambda_3_RS_eq_zero
  kappa_4_third := kappa_lambda_4_RS_eq_one_third
  lambda_6_pos  := fun _ _ hmH hv => lambda_6_RS_pos hmH hv
  cosh_neq_SM   := fun _ _ hmH hv => V_cosh_neq_V_SM hmH hv

What this page does not claim

The framework does not claim the substrate kinetic-term shape is derived; it remains open. The framework does not claim the cosh potential is the true Higgs potential; it is a falsifiable prediction. The framework does not claim the Standard Model is wrong; it claims a specific, testable deviation.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/StandardModel/HiggsCoshBSMPredictions.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: