PVES Electron-Proton Asymmetry Interfaces

This module introduces electron-proton (ep) beam-helicity asymmetry interfaces with hadronic weak-current assumptions and DIS-kinematics compatibility contracts.

def EpsilonEridani.QFT.Scattering.DIS.PVES.Processes.EP.IsDISObservablePoint (V : Type) [AddCommGroup V] [Module ℝ V] (g : Kinematics.Bilin V) (K : Kinematics.DisKinematics V) (x y : ℝ) : Prop

Contract that (x, y) is the DIS point extracted from process kinematics.

Equations

• One or more equations did not get rendered due to their size.

structure EpsilonEridani.QFT.Scattering.DIS.PVES.Processes.EP.HadronicWeakCurrentAssumptions (V : Type) [AddCommGroup V] [Module ℝ V] (g : Kinematics.Bilin V) (K : Kinematics.DisKinematics V) (W : Kinematics.Bilin V) : Prop

Conservation of the hadronic neutral weak current, as a statement about an explicit hadronic tensor W.

Two deliberate choices:

• W is an argument. The previous version of this structure took only g and K and carried three Prop-plus-witness field pairs (weakCurrentConserved, hasResponseModel, parityViolatingCompatible). That form is not a hypothesis at all: Examples.toyHadronicAssumptions instantiated it as ⟨True, trivial, True, trivial, True, trivial⟩, which is available for every g and K.
• There is no symmetry field. Tensors.Hadronic.Assumptions assumes W.IsSymm, which is the parity-even electromagnetic case; the neutral weak hadronic tensor carries the parity-odd F₃ structure and is not symmetric, so assuming symmetry here would assume away the effect being measured.

The two fields that had no honest statement at this fidelity, hasResponseModel and parityViolatingCompatible, are dropped rather than restated: nothing in this module has a structure-function decomposition to which they could refer.

• conserved_left (v : V) : (W K.q) v = 0

  Current conservation in the first tensor slot, q_μ W^{μν} = 0.

• conserved_right (v : V) : (W v) K.q = 0

  Current conservation in the second tensor slot, W^{μν} q_ν = 0.

theorem EpsilonEridani.QFT.Scattering.DIS.PVES.Processes.EP.HadronicWeakCurrentAssumptions.of_hadronicAssumptions (V : Type) [AddCommGroup V] [Module ℝ V] {g : Kinematics.Bilin V} {K : Kinematics.DisKinematics V} {W : Kinematics.Bilin V} (h : Tensors.Hadronic.Assumptions g K W) : HadronicWeakCurrentAssumptions V g K W

The parity-even electromagnetic assumptions of Tensors.Hadronic are strictly stronger: they imply weak-current conservation, and additionally impose covariance and symmetry.

theorem EpsilonEridani.QFT.Scattering.DIS.PVES.Processes.EP.not_hadronicWeakCurrentAssumptions_of_ne_zero (V : Type) [AddCommGroup V] [Module ℝ V] {g : Kinematics.Bilin V} {K : Kinematics.DisKinematics V} {W : Kinematics.Bilin V} {v : V} (hv : (W K.q) v ≠ 0) : ¬HadronicWeakCurrentAssumptions V g K W

The assumptions have content: a tensor that is nonzero against q in the first slot fails them.

structure EpsilonEridani.QFT.Scattering.DIS.PVES.Processes.EP.CrossSectionModel (V : Type) [AddCommGroup V] [Module ℝ V] (g : Kinematics.Bilin V) (K : Kinematics.DisKinematics V) : Type

Helicity-resolved ep cross-section proxy model at DIS variables (x, y).

• sigmaPlus : ℝ → ℝ → ℝ

  Positive-helicity (right-handed) beam proxy.

• sigmaMinus : ℝ → ℝ → ℝ

  Negative-helicity (left-handed) beam proxy.

• pointCompatible : ℝ → ℝ → Prop

  Domain contract selecting kinematic points where the model is valid.

• hPointCompatible (x y : ℝ) : self.pointCompatible x y → IsDISObservablePoint V g K x y

  Compatibility witness with DIS kinematics.

noncomputable def EpsilonEridani.QFT.Scattering.DIS.PVES.Processes.EP.beamHelicityAsymmetry (V : Type) [AddCommGroup V] [Module ℝ V] {g : Kinematics.Bilin V} {K : Kinematics.DisKinematics V} (M : CrossSectionModel V g K) (x y epsilonReg : ℝ) : ℝ

ep beam-helicity asymmetry with denominator regularizer.

Equations

• EpsilonEridani.QFT.Scattering.DIS.PVES.Processes.EP.beamHelicityAsymmetry V M x y epsilonReg = (M.sigmaPlus x y - M.sigmaMinus x y) / (|M.sigmaPlus x y + M.sigmaMinus x y| + epsilonReg)

def EpsilonEridani.QFT.Scattering.DIS.PVES.Processes.EP.IsolationAssumptions (V : Type) [AddCommGroup V] [Module ℝ V] {g : Kinematics.Bilin V} {K : Kinematics.DisKinematics V} (D : Electroweak.NeutralCurrentDecomposition) (M : CrossSectionModel V g K) : Prop

Isolation assumptions for ep helicity channels induced by a neutral-current piecewise decomposition.

Equations

• One or more equations did not get rendered due to their size.

theorem EpsilonEridani.QFT.Scattering.DIS.PVES.Processes.EP.beamHelicityAsymmetry_eq_interferenceRatio_of_isolation (V : Type) [AddCommGroup V] [Module ℝ V] {g : Kinematics.Bilin V} {K : Kinematics.DisKinematics V} (D : Electroweak.NeutralCurrentDecomposition) (M : CrossSectionModel V g K) (x y epsilonReg : ℝ) (hIso : IsolationAssumptions V D M) : beamHelicityAsymmetry V M x y epsilonReg = 2 * D.gammaZInterference x y / (|2 * (D.photon x y + D.zBoson x y)| + epsilonReg)

ep asymmetry bridge theorem parallel to the ee case.

Assumptions discharged. The previous statement also carried hHad : HadronicWeakCurrentAssumptions V g K and hPoint : M.pointCompatible x y. Neither was used: the proof bound them to _-prefixed hypotheses and then proceeded from hIso alone. Both are removed here, which strengthens the result -- helicity-interference isolation is by itself sufficient, at every (x, y) including points the model does not declare compatible. That is a statement about the reach of the present formalization, not a physics claim: the asymmetry chain in this module is algebra on NeutralCurrentDecomposition and never touches the hadronic side.

def EpsilonEridani.QFT.Scattering.DIS.PVES.Processes.EP.canonicalModelOfDecomposition (V : Type) [AddCommGroup V] [Module ℝ V] (g : Kinematics.Bilin V) (K : Kinematics.DisKinematics V) (D : Electroweak.NeutralCurrentDecomposition) : CrossSectionModel V g K

Canonical ep cross-section model induced by Task 4 decomposition and a fixed DIS kinematic point.

Equations

• One or more equations did not get rendered due to their size.

theorem EpsilonEridani.QFT.Scattering.DIS.PVES.Processes.EP.canonicalModel_isolationAssumptions (V : Type) [AddCommGroup V] [Module ℝ V] {g : Kinematics.Bilin V} {K : Kinematics.DisKinematics V} (D : Electroweak.NeutralCurrentDecomposition) : IsolationAssumptions V D (canonicalModelOfDecomposition V g K D)

theorem EpsilonEridani.QFT.Scattering.DIS.PVES.Processes.EP.canonical_beamHelicityAsymmetry_eq_interferenceRatio (V : Type) [AddCommGroup V] [Module ℝ V] (g : Kinematics.Bilin V) (K : Kinematics.DisKinematics V) (D : Electroweak.NeutralCurrentDecomposition) (x y epsilonReg : ℝ) : beamHelicityAsymmetry V (canonicalModelOfDecomposition V g K D) x y epsilonReg = 2 * D.gammaZInterference x y / (|2 * (D.photon x y + D.zBoson x y)| + epsilonReg)