The actual joined primary solves the homogeneous transverse equation. The physical normal field is pointwise; it is never treated as one L² vector. All equations below are for genuine cylinder representatives.

theorem EulerTransversePacketPrimary.balance_ae {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y : EulerTransversePacketProvider.InitialData P D) (t : ↑(Set.Icc 0 D.T)) : ∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain P) ∂EulerLiftedGradientSpace.liftMeasure P, ↑↑((derivativePath τ hτ hτT B Y) t) x + ((D.M.field t) x.1) (↑↑((velocityPath τ hτ hτT B Y) t) x) + (-(2 * inner ℝ ((D.normal.field t) x.1) (((D.M.field t) x.1) (↑↑((velocityPath τ hτ hτT B Y) t) x))) / ‖(D.normal.field t) x.1‖ ^ 2) • (D.normal.field t) x.1 = 0

theorem EulerTransversePacketPrimary.tangent_ae {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y : EulerTransversePacketProvider.InitialData P D) (t : ↑(Set.Icc 0 D.T)) : ∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain P) ∂EulerLiftedGradientSpace.liftMeasure P, inner ℝ ((D.normal.field t) x.1) (↑↑((velocityPath τ hτ hτT B Y) t) x) = 0