IndisputableMonolith.Physics.WignerRotationFromJCost
Module linking Wigner rotation (the spatial rotation from composing non-collinear Lorentz boosts) to the Recognition Science J-cost. It defines a domain cost, a canonical positive threshold, and a WignerRotCert bundle with an inhabited certificate. Relativity and RS workers cite it when tying boost composition geometry to the cost functional. Structure is definitional plus nonnegativity and inhabitation lemmas over Constants and Cost.
claimOn the RS cost $J$, the module introduces a domain cost $C$, proves $C\ge 0$, fixes a canonical threshold $\theta>0$, and packages a Wigner-rotation certificate $\mathrm{WignerRotCert}$ that is inhabited. The intended reading is that the geometric rotation angle arising from successive boosts is controlled by $J$-cost excess relative to $\theta$.
background
Recognition Science takes the unique cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) forced by the Recognition Composition Law. Constants supplies the RS time quantum $\tau_0=1$ tick; Cost supplies the $J$-apparatus used throughout the monolith.
Wigner rotation is the pure spatial rotation that appears when two non-collinear Lorentz boosts are composed: the product is a boost times a rotation. In an RS setting one expects that rotation (or a proxy angle) to be measured by excess $J$-cost on an appropriate domain, rather than by an independent kinematic postulate.
This module sits in the Physics layer. It does not re-derive the Lorentz group; it sets up the cost-side objects (domain cost, canonical threshold, certificate type) needed to state that the Wigner angle is $J$-controlled.
proof idea
Definition module with supporting lemmas, not a single deep theorem. It introduces domainCost and records evaluation and nonnegativity (domainCost_nonneg). It defines canonicalThreshold and proves positivity. It then packages WignerRotCert and exhibits an inhabited certificate (cert, cert_inhabited). Argument structure is: define cost on the domain from $J$, pin a positive threshold, bundle the certificate so downstream physics can assume the Wigner link without rebuilding the cost side.
why it matters in Recognition Science
Connects a standard special-relativistic effect (Wigner rotation under boost composition) to the forced RS cost $J$, so boost geometry is not an extra axiom. Feeds the Physics domain's kinematic certificates; used_by is currently empty at the graph head, so this is a leaf provider rather than a mid-chain lemma. Aligns with the forcing chain's uniqueness of $J$ (T5) and the composition law: once $J$ is the only admissible cost, rotation angles extracted from successive boosts should be $J$-measurable. Closes a definitional gap between Cost and concrete relativistic kinematics without claiming a full Lorentz-group reconstruction.
scope and limits
- Does not derive the Lorentz group or prove boost composition formulas from first principles.
- Does not compute a numerical Wigner angle for concrete velocities.
- Does not claim the certificate implies experimental bounds beyond the cost inequality.
- Does not connect to eight-tick, $D=3$, or mass-ladder results in this module.
- Does not discharge downstream physics theorems; used_by is empty at graph head.