Pointwise parity and canonical normalization of the assembled actual pressure.

theorem EulerGraphPressurePotential.cylinderGraph_neg (period k : ℝ) (m x : EulerLiftedGradientSpace.Vector3) : cylinderGraph period k m (-x) = -cylinderGraph period k m x

The physical phase graph respects joint spatial and angular reflection.

theorem EulerCanonicalGraphPotential.radialPotential_even (V : EulerLiftedGradientSpace.Vector3 → EulerLiftedGradientSpace.Vector3) (hV : ∀ (x : EulerLiftedGradientSpace.Vector3), V (-x) = -V x) (x : EulerLiftedGradientSpace.Vector3) : radialPotential V (-x) = radialPotential V x

The canonical radial scalar potential of an odd vector field is even. This identity does not need a choice of additive gauge or a potential-existence assumption.

theorem EulerCorrectionAssembly.FiniteFamily.pointPressure_odd (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (C : ComparisonData period hT A) (P : ParityData period A) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) : pointPressure period F t (-x) = -pointPressure period F t x

The canonical pressure representative is pointwise odd, as a consequence of genuine PDE uniqueness and parity of the prescribed data.

theorem EulerCorrectionAssembly.FiniteFamily.graphPressure_odd (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (C : ComparisonData period hT A) (P : ParityData period A) (k : ℝ) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3) : graphPressure period F k t (-x) = -graphPressure period F k t x

The actual signed pressure-gradient vector on the physical phase graph is odd.

theorem EulerCorrectionAssembly.FiniteFamily.normalizedGraphPotential_even (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (C : ComparisonData period hT A) (P : ParityData period A) (k : ℝ) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3) : normalizedGraphPotential period F k t (-x) = normalizedGraphPotential period F k t x

The origin-normalized scalar pressure is even at every time. In particular parity is an exact identity, not merely equality modulo a constant.

theorem EulerCorrectionAssembly.FiniteFamily.normalizedGraphPotential_eq_sub (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (k : ℝ) (t : ↑(Set.Icc 0 T)) (q : EulerLiftedGradientSpace.Vector3 → ℝ) (hq : ContDiff ℝ (↑⊤) q) (hgrad : ∀ (x : EulerLiftedGradientSpace.Vector3), gradient q x = graphPressure period F k t x) (x : EulerLiftedGradientSpace.Vector3) : normalizedGraphPotential period F k t x = q x - q 0

Any smooth potential of the same graph field agrees with the canonical radial potential after subtracting its value at the origin.

theorem EulerCorrectionAssembly.FiniteFamily.normalizedGraphPotential_unique (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (k : ℝ) (t : ↑(Set.Icc 0 T)) (q : EulerLiftedGradientSpace.Vector3 → ℝ) (hq : ContDiff ℝ (↑⊤) q) (hgrad : ∀ (x : EulerLiftedGradientSpace.Vector3), gradient q x = graphPressure period F k t x) (hq0 : q 0 = 0) : normalizedGraphPotential period F k t = q

The constructed scalar pressure is the unique smooth potential of its graph field with the prescribed zero value at the origin.