HiggsFalsifier
plain-language theorem explainer
The HiggsFalsifier structure records a potential experimental counterexample to the J-cost derivation of the Higgs mechanism. A physicist testing Recognition Science mass predictions would instantiate it with a discrepancy label, a model value, an observed value, and a check that their relative difference exceeds 10 percent. The definition is a plain record type that directly encodes the four falsification criteria stated in the module documentation.
Claim. A Higgs falsifier consists of a string describing the type of discrepancy, a predicted real number from the J-cost model, an observed real number, and the predicate that the absolute relative difference satisfies $|predicted - observed| / predicted > 0.1$.
background
The module derives spontaneous symmetry breaking and the Higgs mechanism from the J-cost functional. J is defined by J(x) = ½(x + 1/x) - 1 for x > 0; it is symmetric under x ↔ 1/x and attains its global minimum of zero at x = 1. When the vacuum selects the golden-ratio fixed point, the symmetry breaks and particle masses arise proportional to the recognition cost evaluated at that point.
proof idea
This is a structure definition that packages the four components of a falsifying observation. No lemmas or tactics are invoked; the declaration simply assembles the fields listed in the module doc-comment.
why it matters
The definition supplies the concrete falsification interface for the Higgs mechanism derived from J-cost symmetry breaking. It directly implements the four test conditions enumerated in the module documentation and supports the target of deriving the mechanism from the J-cost functional, as proposed for a PRL paper on recognition-cost mass generation. No downstream theorems currently depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.