Actual center initial data for the geometric propagation theorem. The selected terminal coordinate drives the same stationary history and homogeneous continuation used in the constructed packet.

Actual activation data for the packet's own stationary history. The terminal coordinate and its signed velocity components are constructed from the source Dirichlet-to-Neumann argument.

Uniqueness and trial independence for the actual nonzero-terminal transverse inverse. Equal terminal traces and actual tangency place differences in the existing zero-endpoint Hilbert space; the proved energy coercivity then identifies all constructions of the same weak solution.

theorem EulerTransverseEndpointUniqueness.sub_mem_transverse_of_terminal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (m : ↑(Set.Icc 0 T) → E) (u v : ↥(EulerTimeLp.TimeLp T E)) (hu : ∀ (t : ↑(Set.Icc 0 T)), inner ℝ (m t) (EulerInitialTimePrimitive.initialRealPrimitive T u ↑t) = 0) (hv : ∀ (t : ↑(Set.Icc 0 T)), inner ℝ (m t) (EulerInitialTimePrimitive.initialRealPrimitive T v ↑t) = 0) (hterminal : EulerInitialTimePrimitive.initialRealPrimitive T u T = EulerInitialTimePrimitive.initialRealPrimitive T v T) : u - v ∈ EulerTransverseVariationalInverse.transverseDerivatives T hT m

This is membership in the actual zero-endpoint space, obtained from paths and traces rather than supplied as a compatibility assumption.

theorem EulerTransverseEndpointUniqueness.endpointDerivative_unique {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] (T : ℝ) (hT : 0 ≤ T) (m : ↑(Set.Icc 0 T) → E) (H : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (K : ℝ) (hK : 0 ≤ K) (hH : ∀ (t : ↑(Set.Icc 0 T)) (x : E), inner ℝ ((H t) x) x ≤ K * ‖x‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) (L : V →L[ℝ] ↥(EulerTimeLp.TimeLp T E)) (Y : V) (hL : ∀ (t : ↑(Set.Icc 0 T)), inner ℝ (m t) (EulerInitialTimePrimitive.initialRealPrimitive T (L Y) ↑t) = 0) (u : ↥(EulerTimeLp.TimeLp T E)) (hu : ∀ (t : ↑(Set.Icc 0 T)), inner ℝ (m t) (EulerInitialTimePrimitive.initialRealPrimitive T u ↑t) = 0) (hterminal : EulerInitialTimePrimitive.initialRealPrimitive T u T = EulerInitialTimePrimitive.initialRealPrimitive T (L Y) T) (hweak : ∀ (v : ↥(EulerTransverseVariationalInverse.transverseDerivatives T hT m)), inner ℝ u ↑v - inner ℝ ((EulerTimeLp.timeMultiplier T hT H) ((EulerInitialTimePrimitive.initialPrimitiveTimeLp T hT) u)) ((EulerTransverseVariationalInverse.transversePrimitive T hT m) v) = 0) : u = (EulerTransverseEndpointEnergy.endpointDerivative T hT m H K hK hH hsmall L) Y

Any actual weak endpoint solution equals the constructed inverse output.

theorem EulerTransverseEndpointUniqueness.endpointDerivative_eq_of_trial_terminal {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] (T : ℝ) (hT : 0 ≤ T) (m : ↑(Set.Icc 0 T) → E) (H : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (K : ℝ) (hK : 0 ≤ K) (hH : ∀ (t : ↑(Set.Icc 0 T)) (x : E), inner ℝ ((H t) x) x ≤ K * ‖x‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) (L₁ L₂ : V →L[ℝ] ↥(EulerTimeLp.TimeLp T E)) (hL₁ : ∀ (Y : V) (t : ↑(Set.Icc 0 T)), inner ℝ (m t) (EulerInitialTimePrimitive.initialRealPrimitive T (L₁ Y) ↑t) = 0) (hL₂ : ∀ (Y : V) (t : ↑(Set.Icc 0 T)), inner ℝ (m t) (EulerInitialTimePrimitive.initialRealPrimitive T (L₂ Y) ↑t) = 0) (hterminal : ∀ (Y : V), EulerInitialTimePrimitive.initialRealPrimitive T (L₁ Y) T = EulerInitialTimePrimitive.initialRealPrimitive T (L₂ Y) T) : EulerTransverseEndpointEnergy.endpointDerivative T hT m H K hK hH hsmall L₁ = EulerTransverseEndpointEnergy.endpointDerivative T hT m H K hK hH hsmall L₂

The stationary output depends only on the terminal trace, not on the trial lift.

theorem EulerTransverseEndpointUniqueness.dirichletToNeumann_eq_of_trial_terminal {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] (T : ℝ) (hT : 0 ≤ T) (m : ↑(Set.Icc 0 T) → E) (H : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (K : ℝ) (hK : 0 ≤ K) (hH : ∀ (t : ↑(Set.Icc 0 T)) (x : E), inner ℝ ((H t) x) x ≤ K * ‖x‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) [CompleteSpace V] (L₁ L₂ : V →L[ℝ] ↥(EulerTimeLp.TimeLp T E)) (hL₁ : ∀ (Y : V) (t : ↑(Set.Icc 0 T)), inner ℝ (m t) (EulerInitialTimePrimitive.initialRealPrimitive T (L₁ Y) ↑t) = 0) (hL₂ : ∀ (Y : V) (t : ↑(Set.Icc 0 T)), inner ℝ (m t) (EulerInitialTimePrimitive.initialRealPrimitive T (L₂ Y) ↑t) = 0) (hterminal : ∀ (Y : V), EulerInitialTimePrimitive.initialRealPrimitive T (L₁ Y) T = EulerInitialTimePrimitive.initialRealPrimitive T (L₂ Y) T) : EulerTransverseEndpointEnergy.dirichletToNeumann T hT m H K hK hH hsmall L₁ = EulerTransverseEndpointEnergy.dirichletToNeumann T hT m H K hK hH hsmall L₂

The stationary path selected by the actual activation argument is the same history used by the packet, after matching its physical terminal trace.

noncomputable def EulerPacketActivationHistory.stationaryDerivative {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup V] [InnerProductSpace ℝ V] {D : EulerTransversePacketProvider.Data U} (B : EulerTransversePacketProvider.HistoryData D) (x : EulerSmoothLimit.Space) (L : V →L[ℝ] ↥(EulerTimeLp.TimeLp D.T EulerSmoothLimit.Space)) : V →L[ℝ] ↥(EulerTimeLp.TimeLp D.T EulerSmoothLimit.Space)

Stationary derivative, constructed using endpointDerivative.

Equations

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

noncomputable def EulerPacketActivationHistory.stationaryCorrectedVelocity {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup V] [InnerProductSpace ℝ V] {D : EulerTransversePacketProvider.Data U} (B : EulerTransversePacketProvider.HistoryData D) (x : EulerSmoothLimit.Space) (L : V →L[ℝ] ↥(EulerTimeLp.TimeLp D.T EulerSmoothLimit.Space)) (Y : V) (t : ↑(Set.Icc 0 D.T)) : EulerSmoothLimit.Space

Stationary corrected velocity, constructed using physicalVelocityPath.

Equations

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

theorem EulerPacketActivationHistory.history_eq_stationary_of_terminal {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup V] [InnerProductSpace ℝ V] {D : EulerTransversePacketProvider.Data U} (B : EulerTransversePacketProvider.HistoryData D) (x : EulerSmoothLimit.Space) (L : V →L[ℝ] ↥(EulerTimeLp.TimeLp D.T EulerSmoothLimit.Space)) (hL : ∀ (Y : V) (t : ↑(Set.Icc 0 D.T)), inner ℝ ((D.normal.field t) x) (((EulerInitialTimePrimitive.initialPrimitive D.T ⋯) (L Y)) t) = 0) (Y : V) (ξ : U) (hterminal : EulerInitialTimePrimitive.initialRealPrimitive D.T (L Y) D.T = ((D.frame.field ⟨D.T, ⋯⟩) x) ξ) (t : ↑(Set.Icc 0 D.T)) : ((B.coefficients.labelVelocity x) ξ) t = stationaryCorrectedVelocity B x L Y t

theorem EulerPacketActivationHistory.select_history_coordinate {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {D : EulerTransversePacketProvider.Data U} (B : EulerTransversePacketProvider.HistoryData D) (R : V →ₗᵢ[ℝ] EulerSmoothLimit.Space) (hR : ∀ (Y : V), inner ℝ ((D.normal.field ⟨D.T, ⋯⟩) 0) (R Y) = 0) (hHs : ∀ (t : ↑(Set.Icc 0 D.T)), (↑((B.H.field t) 0)).IsSymmetric) (h CM CH ε : ℝ) (hh : 0 < h) (hLayer : 1 ≤ h * D.T) (hCM : 0 ≤ CM) (hCH : 0 ≤ CH) (hε : 0 ≤ ε) (hM : ∀ (t : ↑(Set.Icc 0 D.T)), ‖(D.M.field t) 0‖ ≤ CM * h) (hHnorm : ‖B.coefficients.labelHessian 0‖ ≤ CH * h ^ 2) (p q : V) (hp : ‖p‖ = 1) (hq : ‖q‖ = 1) (hpq : inner ℝ p q = 0) (hεsmall : 16 * (EulerTransverseActivationSelection.activationConstant CM CH + 1) * ε ≤ 1) (hB : ‖EulerTransverseActivationSelection.terminalPerturbation D.T ⋯ R ((EulerTransverseSourceCoefficientPath.pathEvaluation 0) D.M.field) p q h‖ ≤ ε * h) (hBpp : inner ℝ ((EulerTransverseActivationSelection.terminalPerturbation D.T ⋯ R ((EulerTransverseSourceCoefficientPath.pathEvaluation 0) D.M.field) p q h) p) p < 0) : ∃ (ξ : U), ξ ≠ 0 ∧ inner ℝ (((B.coefficients.labelVelocity 0) ξ) ⟨D.T, ⋯⟩) (R q) = 1 ∧ -8 * (EulerTransverseActivationSelection.activationConstant CM CH + 1) ≤ inner ℝ (((B.coefficients.labelVelocity 0) ξ) ⟨D.T, ⋯⟩) (R p) ∧ inner ℝ (((B.coefficients.labelVelocity 0) ξ) ⟨D.T, ⋯⟩) (R p) ≤ 0 ∧ ‖ξ‖ ≤ 8 * (EulerTransverseActivationSelection.activationConstant CM CH + 1) * D.inverseBound / h

Source activation in the actual physical tangent plane. Ambient strain error and compression bounds imply the compressed terminal-matrix hypotheses, so no abstract endpoint matrix or plane isometry is supplied.

theorem EulerPacketActivationHistory.terminalPerturbation_compression {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (T : ℝ) (hT : 0 ≤ T) (R : V →ₗᵢ[ℝ] EulerSmoothLimit.Space) (M : C(↑(Set.Icc 0 T), EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (p q : V) (h : ℝ) : EulerTransverseActivationSelection.terminalPerturbation T hT R M p q h = ContinuousLinearMap.adjoint R.toContinuousLinearMap ∘SL (M ⟨T, ⋯⟩ - h • ((InnerProductSpace.rankOne ℝ) (R q)) (R p)) ∘SL R.toContinuousLinearMap

theorem EulerPacketActivationHistory.terminalPerturbation_norm_le {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (T : ℝ) (hT : 0 ≤ T) (R : V →ₗᵢ[ℝ] EulerSmoothLimit.Space) (M : C(↑(Set.Icc 0 T), EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (p q : V) (h : ℝ) : ‖EulerTransverseActivationSelection.terminalPerturbation T hT R M p q h‖ ≤ ‖M ⟨T, ⋯⟩ - h • ((InnerProductSpace.rankOne ℝ) (R q)) (R p)‖

theorem EulerPacketActivationHistory.terminalPerturbation_diagonal {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (T : ℝ) (hT : 0 ≤ T) (R : V →ₗᵢ[ℝ] EulerSmoothLimit.Space) (M : C(↑(Set.Icc 0 T), EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (p q : V) (h : ℝ) (hpq : inner ℝ p q = 0) : inner ℝ ((EulerTransverseActivationSelection.terminalPerturbation T hT R M p q h) p) p = inner ℝ ((M ⟨T, ⋯⟩) (R p)) (R p)

theorem EulerPacketActivationHistory.select_physical_history_coordinate {U : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (B : EulerTransversePacketProvider.HistoryData D) (hHs : ∀ (t : ↑(Set.Icc 0 D.T)), (↑((B.H.field t) 0)).IsSymmetric) (h CM CH ε : ℝ) (hh : 0 < h) (hLayer : 1 ≤ h * D.T) (hCM : 0 ≤ CM) (hCH : 0 ≤ CH) (hε : 0 ≤ ε) (hM : ∀ (t : ↑(Set.Icc 0 D.T)), ‖(D.M.field t) 0‖ ≤ CM * h) (hHnorm : ‖B.coefficients.labelHessian 0‖ ≤ CH * h ^ 2) (p q : EulerSmoothLimit.Space) (hp : ‖p‖ = 1) (hq : ‖q‖ = 1) (hpq : inner ℝ p q = 0) (hpm : inner ℝ ((D.normal.field ⟨D.T, ⋯⟩) 0) p = 0) (hqm : inner ℝ ((D.normal.field ⟨D.T, ⋯⟩) 0) q = 0) (hεsmall : 16 * (EulerTransverseActivationSelection.activationConstant CM CH + 1) * ε ≤ 1) (hB : ‖(D.M.field ⟨D.T, ⋯⟩) 0 - h • ((InnerProductSpace.rankOne ℝ) q) p‖ ≤ ε * h) (hBpp : inner ℝ (((D.M.field ⟨D.T, ⋯⟩) 0) p) p < 0) : ∃ (ξ : U), ξ ≠ 0 ∧ inner ℝ (((B.coefficients.labelVelocity 0) ξ) ⟨D.T, ⋯⟩) q = 1 ∧ -8 * (EulerTransverseActivationSelection.activationConstant CM CH + 1) ≤ inner ℝ (((B.coefficients.labelVelocity 0) ξ) ⟨D.T, ⋯⟩) p ∧ inner ℝ (((B.coefficients.labelVelocity 0) ξ) ⟨D.T, ⋯⟩) p ≤ 0 ∧ ‖ξ‖ ≤ 8 * (EulerTransverseActivationSelection.activationConstant CM CH + 1) * D.inverseBound / h

theorem EulerPacketActivationHistory.exists_activated_primary {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τ ⋯)) (m v : ℝ → EulerSmoothLimit.Space) (hm : m τ ≠ 0) (hv : v τ ≠ 0) (hmv : inner ℝ (m τ) (v τ) = 0) (hchoice : D.m₀ = EulerPacketMovingFrame.activationDirection (D.deformationEquiv ⟨τ, ⋯⟩ 0) (EulerPacketCrossProduct.cross (EulerPacketNormalizedPrimary.unit (m τ)) (EulerPacketNormalizedPrimary.unit (v τ)))) (hHs : ∀ (t : ↑(Set.Icc 0 (D.initial τ hτ ⋯).T)), (↑((B.H.field t) 0)).IsSymmetric) (h CM CH ζ a ε : ℝ) (hh : 0 < h) (hLayer : 1 ≤ h * τ) (hCM : 0 ≤ CM) (hCH : 0 ≤ CH) (hζ : 0 ≤ ζ) (hε : 0 < ε) (hM : ∀ (t : ↑(Set.Icc 0 τ)), ‖((D.initial τ hτ ⋯).M.field t) 0‖ ≤ CM * h) (hHnorm : ‖B.coefficients.labelHessian 0‖ ≤ CH * h ^ 2) (hζsmall : 16 * (EulerTransverseActivationSelection.activationConstant CM CH + 1) * ζ ≤ 1) (hB : ‖(D.M.field ⟨τ, ⋯⟩) 0 - h • ((InnerProductSpace.rankOne ℝ) (EulerPacketNormalizedPrimary.unit (v τ))) (EulerPacketNormalizedPrimary.unit (m τ))‖ ≤ ζ * h) (hBpp : inner ℝ (((D.M.field ⟨τ, ⋯⟩) 0) (EulerPacketNormalizedPrimary.unit (m τ))) (EulerPacketNormalizedPrimary.unit (m τ)) < 0) : have s₀ := EulerPacketMovingFrame.activationRayScale (D.deformationEquiv ⟨τ, ⋯⟩ 0) (EulerPacketCrossProduct.cross (EulerPacketNormalizedPrimary.unit (m τ)) (EulerPacketNormalizedPrimary.unit (v τ))); 0 < s₀ ∧ EulerPacketMovingFrame.scaledRay m v (fun (s : ℝ) => (D.normal.field (D.clamp s)) 0) s₀ τ a ε 0 = ![0, 0, 1] ∧ ∃ (ξ : U) (lam : ℝ), ξ ≠ 0 ∧ 0 ≤ lam ∧ lam ≤ 8 * (EulerTransverseActivationSelection.activationConstant CM CH + 1) / ε ∧ ‖ξ‖ ≤ 8 * (EulerTransverseActivationSelection.activationConstant CM CH + 1) * D.inverseBound / h ∧ EulerPacketMovingFrame.scaledVelocity m v (fun (s : ℝ) => EulerPacketPrimaryFactorization.uncutVelocity τ hτ hτT B ξ s 0) τ a ε 0 0 = -lam ∧ EulerPacketMovingFrame.scaledVelocity m v (fun (s : ℝ) => EulerPacketPrimaryFactorization.uncutVelocity τ hτ hτT B ξ s 0) τ a ε 0 1 = 1