The first pressure numerator stays positive for the actual evolving normal and the actual homogeneous transverse velocity. Initial plateau data are the only geometric inputs; all time equations are constructed.

theorem EulerBaseEulerGuards.source_normal_initial {G : EulerParentPacketFrames.Parent} {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (x : EulerSmoothLimit.Space) : ((G.transverseData m hm R S hS).normal.field G.zeroTime) x = m

theorem EulerBaseEulerGuards.source_frame_initial {G : EulerParentPacketFrames.Parent} {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (ξ : U) (x : EulerSmoothLimit.Space) : (((G.transverseData m hm R S hS).frame.field G.zeroTime) x) ξ = ↑(R ξ)

theorem EulerBaseEulerGuards.source_numerator_pos {G : EulerParentPacketFrames.Parent} (L : EulerParentPacketFrames.LabelData G) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (ξ : U) (hξ : ‖ξ‖ = 1) (x : EulerSmoothLimit.Space) (h0 : inner ℝ m ((G.initialStrain.field x) ↑(R ξ)) = 1) (hshort : coefficientCost L.K * G.T ≤ 1 / 2) (hsmall : EulerPacketFirstPressureSign.firstSignRate (coefficientCost L.K) (coefficientCost L.K) * G.T ≤ 1 / 2) (t : ↑(Set.Icc 0 G.T)) : 1 / 2 ≤ inner ℝ (((G.transverseData m hm R S hS).normal.field t) x) (((G.strain.field t) x) (EulerPacketForwardFactorization.uncutVelocity (G.transverseData m hm R S hS) ξ (↑t) x))

theorem EulerBaseEulerGuards.source_numerator_pos_on {G : EulerParentPacketFrames.Parent} (L : EulerParentPacketFrames.LabelData G) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (T : ℝ) (hT : 0 < T) (hTG : T ≤ G.T) (hguard : T ≤ guardTime G.T L.K) (ξ : U) (hξ : ‖ξ‖ = 1) (x : EulerSmoothLimit.Space) (h0 : inner ℝ m ((G.initialStrain.field x) ↑(R ξ)) = 1) (t : ↑(Set.Icc 0 T)) : 1 / 2 ≤ inner ℝ ((((G.restrictTime T hT hTG).transverseData m hm R S hS).normal.field t) x) ((((G.restrictTime T hT hTG).strain.field t) x) (EulerPacketForwardFactorization.uncutVelocity ((G.restrictTime T hT hTG).transverseData m hm R S hS) ξ (↑t) x))