Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

A lower bound of three chiral-event variables

Abstract

Any two continuous invariant parity-odd real variables vanish together on a chiral four-particle event in each of the two event classes.

Definition 1.1 (Ordered four-particle events).

Formalization. D5/S3/Geometry/Lorentz/ChiralEventParityMinimality.event (✓ std3).

Citation. Christopher G. Lester; Ward Haddadin; Ben Gripaios (2022). Lorentz and permutation invariants of particles III: constraining non-standard sources of parity violation. DOI: 10.1142/S0217751X22500932. URL: https://arxiv.org/abs/2008.05206v6.

Commentary.

An event is an ordered quadruple of four-vectors, indexed in the order p, q, a, b. Each four-vector has type Fin 4 → ℝ, with coordinate zero the energy and coordinates one, two and three the spatial momentum, as in prelims.tex:21–23 of arXiv:2008.05206v6. The two interchangeable pairs are the first two and last two entries. The source’s two event classes and their common symmetry group are specified in prelims.tex:656–666. The ambient type itself imposes no forward-cone or collision condition.

Definition 1.2 (The Minkowski metric matrix).

Formalization. D5/S3/Geometry/Lorentz/ChiralEventParityMinimality.eta (✓ std3).

Citation. Christopher G. Lester; Ward Haddadin; Ben Gripaios (2022). Lorentz and permutation invariants of particles III: constraining non-standard sources of parity violation. DOI: 10.1142/S0217751X22500932. URL: https://arxiv.org/abs/2008.05206v6.

Commentary.

The diagonal matrix has signature (+,−,−,−), the convention of the source’s Minkowski product. It also represents spatial parity on a four-vector.

Definition 1.3 (A proper spatial rotation).

Formalization. D5/S3/Geometry/Lorentz/ChiralEventParityMinimality.rotation (✓ std3).

Source. Repository-derived.

Acknowledgement. Christopher G. Lester; Ward Haddadin; Ben Gripaios (2022). Lorentz and permutation invariants of particles III: constraining non-standard sources of parity violation. DOI: 10.1142/S0217751X22500932. URL: https://arxiv.org/abs/2008.05206v6.

Commentary.

The matrix fixes time and sends the spatial coordinates (x,y,z) to (−y,−x,−z). It preserves the Minkowski metric, has determinant one and has time-time entry one. Composing it with parity exchanges the first two spatial coordinates.

Definition 1.4 (The Minkowski product).

Formalization. D5/S3/Geometry/Lorentz/ChiralEventParityMinimality.minkowski (✓ std3).

Citation. Christopher G. Lester; Ward Haddadin; Ben Gripaios (2022). Lorentz and permutation invariants of particles III: constraining non-standard sources of parity violation. DOI: 10.1142/S0217751X22500932. URL: https://arxiv.org/abs/2008.05206v6.

Commentary.

The bilinear product multiplies the time coordinates and subtracts the three spatial coordinate products. The collision condition in prelims.tex:433–443 uses this product and its associated squared masses.

Definition 1.5 (Forward nonspacelike four-vectors).

Formalization. D5/S3/Geometry/Lorentz/ChiralEventParityMinimality.forwardCone (✓ std3).

Citation. Christopher G. Lester; Ward Haddadin; Ben Gripaios (2022). Lorentz and permutation invariants of particles III: constraining non-standard sources of parity violation. DOI: 10.1142/S0217751X22500932. URL: https://arxiv.org/abs/2008.05206v6.

Commentary.

The time coordinate is nonnegative and its square bounds the squared spatial norm. Thus the zero vector and future null vectors are included, as in the set of four-vectors defined in prelims.tex:25–27.

Definition 1.6 (Proper orthochronous Lorentz matrices).

Formalization. D5/S3/Geometry/Lorentz/ChiralEventParityMinimality.properOrthochronous (✓ std3).

Citation. Christopher G. Lester; Ward Haddadin; Ben Gripaios (2022). Lorentz and permutation invariants of particles III: constraining non-standard sources of parity violation. DOI: 10.1142/S0217751X22500932. URL: https://arxiv.org/abs/2008.05206v6.

Commentary.

The matrix preserves eta, has determinant one and has positive time-time entry. These conditions express the proper orthochronous Lorentz transformations used in the symmetry group of prelims.tex:190–193.

Definition 1.7 (Parity of a four-vector).

Formalization. D5/S3/Geometry/Lorentz/ChiralEventParityMinimality.parityVector (✓ std3).

Citation. Christopher G. Lester; Ward Haddadin; Ben Gripaios (2022). Lorentz and permutation invariants of particles III: constraining non-standard sources of parity violation. DOI: 10.1142/S0217751X22500932. URL: https://arxiv.org/abs/2008.05206v6.

Commentary.

Parity fixes energy and negates all three spatial coordinates, as in prelims.tex:228–238.

Definition 1.8 (Parity of an event).

Formalization. D5/S3/Geometry/Lorentz/ChiralEventParityMinimality.parity (✓ std3).

Citation. Christopher G. Lester; Ward Haddadin; Ben Gripaios (2022). Lorentz and permutation invariants of particles III: constraining non-standard sources of parity violation. DOI: 10.1142/S0217751X22500932. URL: https://arxiv.org/abs/2008.05206v6.

Commentary.

Apply four-vector parity to each of the four event entries. This is the componentwise event parity of prelims.tex:228–238.

Definition 1.9 (Lorentz transformations and pair permutations).

Formalization. D5/S3/Geometry/Lorentz/ChiralEventParityMinimality.act (✓ std3).

Citation. Christopher G. Lester; Ward Haddadin; Ben Gripaios (2022). Lorentz and permutation invariants of particles III: constraining non-standard sources of parity violation. DOI: 10.1142/S0217751X22500932. URL: https://arxiv.org/abs/2008.05206v6.

Commentary.

The permutation sigma selects entries within the p,q pair and tau selects entries within the a,b pair; the same matrix lam then acts on every selected four-vector. Fin.castAdd embeds the first pair’s indices into Fin 4, while Fin.natAdd shifts the second pair’s indices by two. The formula defines the action for every real matrix; membership in the Lorentz group is required where the symmetry is used. This is the action described in prelims.tex:190–193 and 260–267.

Definition 1.10 (Chiral events).

Formalization. D5/S3/Geometry/Lorentz/ChiralEventParityMinimality.chiral (✓ std3).

Citation. Christopher G. Lester; Ward Haddadin; Ben Gripaios (2022). Lorentz and permutation invariants of particles III: constraining non-standard sources of parity violation. DOI: 10.1142/S0217751X22500932. URL: https://arxiv.org/abs/2008.05206v6.

Commentary.

An event is chiral if no proper orthochronous Lorentz matrix and no independent pair permutations carry it to its parity image. This is the characterization in prelims.tex:240–243 and 265–268, extended as a predicate on the ambient event type.

Definition 1.11 (The full forward-cone event class).

Formalization. D5/S3/Geometry/Lorentz/ChiralEventParityMinimality.allEvents (✓ std3).

Citation. Christopher G. Lester; Ward Haddadin; Ben Gripaios (2022). Lorentz and permutation invariants of particles III: constraining non-standard sources of parity violation. DOI: 10.1142/S0217751X22500932. URL: https://arxiv.org/abs/2008.05206v6.

Commentary.

Every one of the four entries belongs to the forward cone. With the common pair-permutation and Lorentz symmetries, this is the class of all (pq)(ab) events in prelims.tex:662–666. There is no additional momentum-conservation constraint.

Definition 1.12 (The collision event class).

Formalization. D5/S3/Geometry/Lorentz/ChiralEventParityMinimality.collisionEvents (✓ std3).

Citation. Christopher G. Lester; Ward Haddadin; Ben Gripaios (2022). Lorentz and permutation invariants of particles III: constraining non-standard sources of parity violation. DOI: 10.1142/S0217751X22500932. URL: https://arxiv.org/abs/2008.05206v6.

Commentary.

A collision event is a forward-cone event for which the product of the squared masses of p and q is strictly less than the square of their Minkowski product. This is the collision condition of prelims.tex:433–443 and the class (pq) to (ab) plus X in prelims.tex:656–660.

Definition 1.13 (Continuous invariant parity-odd variables).

Formalization. D5/S3/Geometry/Lorentz/ChiralEventParityMinimality.admissible (✓ std3).

Citation. Christopher G. Lester; Ward Haddadin; Ben Gripaios (2022). Lorentz and permutation invariants of particles III: constraining non-standard sources of parity violation. DOI: 10.1142/S0217751X22500932. URL: https://arxiv.org/abs/2008.05206v6.

Commentary.

The variable is real-valued, continuous on om, invariant under every allowed Lorentz matrix and both pair permutations at every event in om, and parity odd there. These are the first four requirements in goals.tex:1–10. No continuity or symmetry condition is imposed outside om.

Definition 1.14 (The two-variable obstruction).

Formalization. D5/S3/Geometry/Lorentz/ChiralEventParityMinimality.claim (✓ std3).

Citation. Christopher G. Lester; Ward Haddadin; Ben Gripaios (2022). Lorentz and permutation invariants of particles III: constraining non-standard sources of parity violation. DOI: 10.1142/S0217751X22500932. URL: https://arxiv.org/abs/2008.05206v6.

Commentary.

For each of the full and collision event classes, any two admissible real variables vanish together at some chiral event. This expresses the lower-bound assertion of the minimality conjecture in introduction.tex:103–104: neither one nor two such variables can be sufficient. The one-variable case follows by taking both variables equal. The statement supplies no construction or sufficiency proof for a three-variable set.

Definition 1.15 (A sphere of four-particle events).

Formalization. D5/S3/Geometry/Lorentz/ChiralEventParityMinimality.family (✓ std3).

Source. Repository-derived.

Acknowledgement. Christopher G. Lester; Ward Haddadin; Ben Gripaios (2022). Lorentz and permutation invariants of particles III: constraining non-standard sources of parity violation. DOI: 10.1142/S0217751X22500932. URL: https://arxiv.org/abs/2008.05206v6.

Commentary.

For v on the unit sphere, write s, t and d for its three real coordinates and aa and bb for the indicated positive square roots. The first two momenta are fixed; the final two encode the sphere coordinates in their energies, transverse lengths and opposite longitudinal coordinates. The formula is defined on all of Euclidean three-space; its collision membership and chirality are used on the unit sphere.

Theorem 1.16 (A common zero on a chiral event).

Proof. Machine-checked in Lean as D5/S3/Geometry/Lorentz/ChiralEventParityMinimality.result (✓ std3). ∎

Resolves. Problems/lester-haddadin-gripaios-2022-chiral-event-parity-minimality (proved) by D5/S3/Geometry/Lorentz/ChiralEventParityMinimality.result.

Source. Repository-derived.

Acknowledgement. Christopher G. Lester; Ward Haddadin; Ben Gripaios (2022). Lorentz and permutation invariants of particles III: constraining non-standard sources of parity violation. DOI: 10.1142/S0217751X22500932. URL: https://arxiv.org/abs/2008.05206v6.

Commentary.

First consider the displayed family on the unit sphere. Its coordinates satisfy s² + t² + d² = 1, so s and t lie between minus one and one. The squared transverse lengths are 4+t and 4−t. Both energies 10+s and 10−s are positive, and the squared masses of the last two momenta are 95+20s+2s²−t+t² and 95−20s+2s²+t+t², each at least 74. All four momenta therefore lie in the forward cone. The first two squared masses are 899 and 399 and their Minkowski product is 601; 899 times 399 is strictly less than 601 squared. Every event of the sphere is consequently a collision event. Each coordinate depends continuously on v, including the square roots, so the family is continuous.

To establish chirality, suppose an allowed matrix lam and pair permutations carry such an event to its parity image. First let sigma fix the first pair and put h = eta times lam. Then h preserves eta, fixes p and q, and has determinant minus one. The two fixed vectors span the time-longitudinal plane. Solving their coordinate equations and using preservation of eta shows that h fixes this plane pointwise and has no mixed entries with the transverse plane. If tau fixes the second pair, h fixes the two nonzero independent transverse vectors (aa,0) and (0,bb). Its remaining block is the identity, so h is the identity, contradicting its determinant. If tau exchanges the second pair, the time and longitudinal coordinates give s = d = 0. Preservation of the Minkowski squared norm gives aa = bb; their squared values then give t = 0, contradicting the unit-sphere equation. Finally, if sigma exchanges p and q, preservation of their squared norms would equate 899 and 399. This rules out every pair of permutations.

Direct coordinate comparison gives the antipodal identity below: rotation, together with exchange of the last pair, carries the parity image of the event at v to the event at −v.

Whenever collisionEvents is contained in om, composing either admissible variable with the family is continuous on the sphere. The closed expression below sends each pair of real variables to its complex-valued pullback. For admissible variables this pullback is continuous on the sphere. Parity preserves the forward cone and the collision inequality, hence preserves both event domains. The displayed rotation preserves eta, has determinant one and has positive time-time entry; its determinant follows by writing it as the spatial coordinate exchange times eta. Invariance applied at the parity image, followed by parity oddness and the antipodal identity, makes each real pullback odd. The same holds after the explicit inclusions into the complex numbers, so their displayed complex combination is odd.

For om equal to allEvents, use the inclusion of collisionEvents into allEvents. Apply the planar odd-map zero theorem, Borsuk’s Satz II (1933) for n=2, reviewed in Library note D5/L/Topology/borsuk1933spheres, to the complex combination and obtain a unit vector where it vanishes. The family event there is in om and is chiral; taking real and imaginary parts gives f₁ = f₂ = 0. For om equal to collisionEvents, use the identity inclusion and repeat the same argument. These are the two possibilities for om, which proves the full assertion.

References