Physics Spontaneous Symmetry Breaking2 From Jcost

The cost threshold

Spontaneous symmetry breaking is a common pattern in physics: the equations that govern a system are symmetric, but the state the system actually settles into is not. A familiar example is a ball resting at the rim of a wine bottle. The bottle is symmetric around its axis, but the ball must roll to one side, picking a particular direction and breaking the symmetry. In quantum field theory, the same idea explains how particles acquire mass: the vacuum, the lowest-energy state, is not symmetric under the full symmetry group, even though the underlying laws are.

In Recognition Science, the framework models this phenomenon through its cost function, a measure of how expensive a recognition event is, forced by five plain conditions to take the form J(x) = (x + 1/x)/2 - 1. The framework's library of machine-checked theorems defines a quantity called domainCost for two positive numbers m and e as J(m/e), and proves three general facts about it. First, the cost vanishes when m equals e. Second, the cost is never negative for positive inputs. Third, the number phi - 3/2, where phi is the golden ratio, is positive.

These three facts are the entire content of the module. The framework's research note proposes an interpretation: spontaneous symmetry breaking occurs when J(sigma/sigma_max) exceeds J(phi), where sigma is an order parameter, a quantity that is zero in the symmetric phase and nonzero in the broken phase. Below that threshold, the system stays symmetric; above it, the symmetry breaks and the order parameter becomes nonzero. The threshold itself, phi - 3/2, is not a free parameter but a number that emerges from the cost function's forced form.

The module proves no physics. It proves three general facts about the cost function, and it packages them into a certificate structure. What would make it a theorem about spontaneous symmetry breaking is a definition of m and e in the subject's own terms, a definition the module does not supply. The framework's own honesty note says the paragraph above is a research note recording where the idea was meant to go, not a result. The value of the module is that it isolates the exact piece that is proved, and the exact piece that remains a proposal.

theorem domainCost_at_eq (r : ℝ) (h : r ≠ 0) : domainCost r r = 0 := by
  unfold domainCost; rw [div_self h]; exact Jcost_unit0

theorem domainCost_nonneg (m e : ℝ) (hm : 0 < m) (he : 0 < e) : 0 ≤ domainCost m e := by
  unfold domainCost; exact Jcost_nonneg (div_pos hm he)

theorem canonicalThreshold_pos : 0 < canonicalThreshold := by
  unfold canonicalThreshold; linarith [phi_gt_onePointFive]

What this page does not claim

The module proves no statement specific to spontaneous symmetry breaking; it proves general facts about the cost function. The interpretation of the threshold as a phase boundary is a research note, not a theorem. No claim is made that any physical system exhibits this threshold.

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/Physics/SpontaneousSymmetryBreaking2FromJCost.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: