Related estimates used together by the same construction modules.

Same-radius fixed-H6 estimates for actual cylinder products

The product is the literal pointwise product already constructed in H6. Both input word sums pass directly through the bilinear Leibniz formula. The only norm equivalence constant is the fixed size of the H6 array.

Fixed Sobolev path norms and actual external word sums

The finite Sobolev array gives equivalent norms with constants depending only on its fixed order. No tensor norm conversion or external-order alphabet factor enters either comparison.

The finite sum of nested genuine derivative words is the corresponding longer word sum.

theorem EulerParameterWordGevrey.sum_wordSum_wordDerivative {P : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] (directions : ι → P) (f : P → E) (hf : ContDiff ℝ (↑⊤) f) (k n : ℕ) (x : P) : ∑ w : Fin k → ι, wordSum directions (wordDerivative directions f w) n x = wordSum directions f (k + n) x

noncomputable def EulerCylinderSmoothOrbit.pathWordOperator (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] {q : ℕ} (w : EulerCylinderSobolevSpace.SobolevWord q) : C(K, ↥(EulerCylinderSobolevSpace.SobolevSpace P q)) →L[ℝ] C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))

Path word operator, given by (wordOperator P w).compLeftContinuous ℝ K.

Equations

• EulerCylinderSmoothOrbit.pathWordOperator P w = ContinuousLinearMap.compLeftContinuous ℝ K (EulerCylinderSobolevSpace.wordOperator P w)

theorem EulerCylinderSmoothOrbit.pathWordOperator_norm_le (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {q : ℕ} (w : EulerCylinderSobolevSpace.SobolevWord q) (u : C(K, ↥(EulerCylinderSobolevSpace.SobolevSpace P q))) : ‖(pathWordOperator P w) u‖ ≤ ‖u‖

theorem EulerCylinderSmoothOrbit.path_norm_le_sum_words (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {q : ℕ} (u : C(K, ↥(EulerCylinderSobolevSpace.SobolevSpace P q))) : ‖u‖ ≤ ∑ w : EulerCylinderSobolevSpace.SobolevWord q, ‖(pathWordOperator P w) u‖

theorem EulerCylinderSmoothOrbit.pathWordOperator_sobolevOrbit (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (q : ℕ) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (w : EulerCylinderSobolevSpace.SobolevWord q) : ⇑(pathWordOperator P w) ∘ sobolevOrbit P q p hp = EulerParameterWordGevrey.wordDerivative EulerCylinderSobolev.standardDirection (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) w.snd

theorem EulerCylinderSmoothOrbit.sobolevOrbit_word_coordinate (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (q : ℕ) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) {n : ℕ} (v : Fin n → Fin 4) (w : EulerCylinderSobolevSpace.SobolevWord q) (a : EulerLiftedGradientSpace.LiftTangent) : (pathWordOperator P w) (EulerParameterWordGevrey.wordDerivative EulerCylinderSobolev.standardDirection (sobolevOrbit P q p hp) v a) = EulerParameterWordGevrey.wordDerivative EulerCylinderSobolev.standardDirection (EulerParameterWordGevrey.wordDerivative EulerCylinderSobolev.standardDirection (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) p) w.snd) v a

theorem EulerCylinderSmoothOrbit.sum_sobolev_word_levels (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (q : ℕ) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (n : ℕ) (a : EulerLiftedGradientSpace.LiftTangent) : ∑ w : EulerCylinderSobolevSpace.SobolevWord q, EulerParameterWordGevrey.wordSum EulerCylinderSobolev.standardDirection (EulerParameterWordGevrey.wordDerivative EulerCylinderSobolev.standardDirection (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) p) w.snd) n a = EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) p) n a

theorem EulerCylinderSmoothOrbit.sobolevOrbit_wordSum_le_block (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (q : ℕ) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (n : ℕ) (a : EulerLiftedGradientSpace.LiftTangent) : EulerParameterWordGevrey.wordSum EulerCylinderSobolev.standardDirection (sobolevOrbit P q p hp) n a ≤ EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) p) n a

Promotion to the actual Hq path norm costs no external-order factor.

theorem EulerCylinderSmoothOrbit.block_le_card_sobolevOrbit_wordSum (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (q : ℕ) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (n : ℕ) (a : EulerLiftedGradientSpace.LiftTangent) : EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) p) n a ≤ ↑(Fintype.card (EulerCylinderSobolevSpace.SobolevWord q)) * EulerParameterWordGevrey.wordSum EulerCylinderSobolev.standardDirection (sobolevOrbit P q p hp) n a

Returning to the source derivative sum costs only the fixed Hq array size.

@[instance_reducible]

noncomputable def EulerCylinderPathProduct.instCylinderPathProductBounds1 (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : NormedAddCommGroup C(K, ↥(EulerCylinderSobolevSpace.SobolevSpace P 6))

Cache the standard NormedAddCommGroup (C(K,SobolevSpace P 6)) instance to shorten typeclass synthesis.

Equations

• EulerCylinderPathProduct.instCylinderPathProductBounds1 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderPathProduct.instCylinderPathProductBounds2 (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : NormedSpace ℝ C(K, ↥(EulerCylinderSobolevSpace.SobolevSpace P 6))

Cache the standard NormedSpace ℝ (C(K,SobolevSpace P 6)) instance to shorten typeclass synthesis.

Equations

• EulerCylinderPathProduct.instCylinderPathProductBounds2 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderPathProduct.instCylinderPathProductBounds3 (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : NormedAddCommGroup (C(K, ↥(EulerCylinderSobolevSpace.SobolevSpace P 6)) →L[ℝ] C(K, ↥(EulerCylinderSobolevSpace.SobolevSpace P 6)))

Cache the standard NormedAddCommGroup (C(K,SobolevSpace P 6) →L[ℝ] C(K,SobolevSpace P 6)) instance to shorten typeclass synthesis.

Equations

• EulerCylinderPathProduct.instCylinderPathProductBounds3 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderPathProduct.instCylinderPathProductBounds4 (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : NormedSpace ℝ (C(K, ↥(EulerCylinderSobolevSpace.SobolevSpace P 6)) →L[ℝ] C(K, ↥(EulerCylinderSobolevSpace.SobolevSpace P 6)))

Cache the standard NormedSpace ℝ (C(K,SobolevSpace P 6) →L[ℝ] C(K,SobolevSpace P 6)) instance to shorten typeclass synthesis.

Equations

• EulerCylinderPathProduct.instCylinderPathProductBounds4 P = inferInstance

theorem EulerCylinderPathProduct.scalarProductPath_sobolevOrbit (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (L : EulerSmoothLimit.Space →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (p q : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) (a : EulerLiftedGradientSpace.LiftTangent) : EulerCylinderSmoothOrbit.sobolevOrbit P 6 (scalarProductPath P L hL p q hp hq) ⋯ a = ((pathBilinear (EulerSobolevL2Product.productHqBilinear P scalarProductPath_sobolevOrbit._proof_1 L hL)) (EulerCylinderSmoothOrbit.sobolevOrbit P 6 p hp a)) (EulerCylinderSmoothOrbit.sobolevOrbit P 6 q hq a)

noncomputable def EulerCylinderPathProduct.productBlockConstant (P : ℝ) [Fact (0 < P)] : ℝ

A numerical fixed-order constant, independent of external derivative order and grade.

Equations

• EulerCylinderPathProduct.productBlockConstant P = ↑(Fintype.card (EulerCylinderSobolevSpace.SobolevWord 6)) * EulerSobolevL2Product.sobolevProductConstant P 6

theorem EulerCylinderPathProduct.productBlockConstant_nonneg (P : ℝ) [Fact (0 < P)] : 0 ≤ productBlockConstant P

theorem EulerCylinderPathProduct.productH6PathBilinear_norm (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (L : EulerSmoothLimit.Space →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) : ‖pathBilinear (EulerSobolevL2Product.productHqBilinear P scalarProductPath_sobolevOrbit._proof_1 L hL)‖ ≤ EulerSobolevL2Product.sobolevProductConstant P 6

theorem EulerCylinderPathProduct.scalarProductPath_block_bound (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (L : EulerSmoothLimit.Space →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (p q : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) (n : ℕ) (a : EulerLiftedGradientSpace.LiftTangent) : EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection 6 (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) (scalarProductPath P L hL p q hp hq)) n a ≤ productBlockConstant P * EulerJetProductBounds.leibnizConvolution (fun (k : ℕ) => EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection 6 (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) p) k a) (fun (k : ℕ) => EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection 6 (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) q) k a) n

Actual external word blocks of the genuine product obey the H6 algebra convolution.

theorem EulerCylinderPathProduct.scalarProductPath_majorant (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (L : EulerSmoothLimit.Space →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (p q : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) (R A C : ℝ) (hR : 0 ≤ R) (hA : 0 ≤ A) (hC : 0 ≤ C) (d e : ℕ) (a : EulerLiftedGradientSpace.LiftTangent) (hb : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection 6 (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) p) n a ≤ A * EulerGevrey.majorant R d n) (hc : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection 6 (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) q) n a ≤ C * EulerGevrey.majorant R e n) (n : ℕ) : EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection 6 (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) (scalarProductPath P L hL p q hp hq)) n a ≤ 3 * productBlockConstant P * A * C * EulerGevrey.majorant R (d + e) n

The actual product retains the input radius and adds only the two factorial shifts.

Literal bounded bilinear nonlinearities preserve smooth continuous cylinder L² paths.

noncomputable def EulerCylinderPathProduct.component (i : Fin 3) : EulerSmoothLimit.Space →L[ℝ] ℝ

Component, given by EuclideanSpace.proj i.

Equations

• EulerCylinderPathProduct.component i = EuclideanSpace.proj i

theorem EulerCylinderPathProduct.component_norm (i : Fin 3) : ‖component i‖ ≤ 1

noncomputable def EulerCylinderPathProduct.basisVector (i : Fin 3) : EulerSmoothLimit.Space

Basis vector, given by EuclideanSpace.single i 1.

Equations

• EulerCylinderPathProduct.basisVector i = EuclideanSpace.single i 1

theorem EulerCylinderPathProduct.sum_components (u : EulerSmoothLimit.Space) : ∑ i : Fin 3, (component i) u • basisVector i = u

theorem EulerCylinderPathProduct.bilinear_components (B : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (u v : EulerSmoothLimit.Space) : ∑ i : Fin 3, (B (basisVector i)) ((component i) u • v) = (B u) v

noncomputable def EulerCylinderPathProduct.bilinearTerm (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (B : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (p q : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) (i : Fin 3) : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))

Bilinear term, given by pathMap P (B (basisVector i)) (scalarProductPath P (component i) (component_norm i) p q hp hq).

Equations

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

theorem EulerCylinderPathProduct.bilinearTerm_orbit (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (B : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (p q : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) (i : Fin 3) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (bilinearTerm P B p q hp hq i)

noncomputable def EulerCylinderPathProduct.bilinearProductPath (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (B : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (p q : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))

An arbitrary fixed bilinear vector operation on the actual L² paths.

Equations

• EulerCylinderPathProduct.bilinearProductPath P B p q hp hq = ∑ i : Fin 3, EulerCylinderPathProduct.bilinearTerm P B p q hp hq i

theorem EulerCylinderPathProduct.bilinearProductPath_orbit (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (B : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (p q : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (bilinearProductPath P B p q hp hq)

theorem EulerCylinderPathProduct.bilinearTerm_ae (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (B : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (p q : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) (i : Fin 3) (t : K) : ↑↑((bilinearTerm P B p q hp hq i) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] fun (x : EulerLiftedGradientSpace.LiftDomain P) => (B (basisVector i)) ((component i) (EulerCylinderSmoothOrbit.pointField P p hp t x) • EulerCylinderSmoothOrbit.pointField P q hq t x)

theorem EulerCylinderPathProduct.bilinearProductPath_ae (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (B : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (p q : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) (t : K) : ↑↑((bilinearProductPath P B p q hp hq) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] fun (x : EulerLiftedGradientSpace.LiftDomain P) => (B (EulerCylinderSmoothOrbit.pointField P p hp t x)) (EulerCylinderSmoothOrbit.pointField P q hq t x)

theorem EulerCylinderPathProduct.pointField_bilinearProductPath (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (B : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (p q : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) (t : K) (x : EulerLiftedGradientSpace.LiftDomain P) : EulerCylinderSmoothOrbit.pointField P (bilinearProductPath P B p q hp hq) ⋯ t x = (B (EulerCylinderSmoothOrbit.pointField P p hp t x)) (EulerCylinderSmoothOrbit.pointField P q hq t x)

The reconstructed field agrees everywhere with the literal nonlinearity.