propositionroutineinferred_dep

Wave current is positive and divergence-free

Wave-mode current A0=χχ∗A^0=\chi\chi^* is positive semidefinite and divergence-free
supplies the conserved positive current for the barrier
Proposition·prop:current·§2.3 Coordinates adapted to the wave

Statement (paper)

For any finite superposition , set χ=∑κ,vVv ιe(uκ,v‾) mκ,v,A0=χχ∗. \chi=\sum_{\kappa,v} V^v\,\iota_e(\overline{u_{\kappa,v}}) \,m_{\kappa,v},\qquad A^0=\chi\chi^* . On Y≠0Y\ne0 the matrix A0A^0 is smooth and positive semidefinite, (∂Φ)A0=0(\partial\Phi)A^0=0, and each column of (A0)R(A^0)^{\RR} has zero real divergence. These conclusions hold also after the orthogonal change from null to physical coordinates. In particular, VTv=(1+W⋅v/2)/2,ATT0=∣χT∣2. V_T^v=(1+W\cdot v/2)/\sqrt2,\qquad A^0_{TT}=|\chi_T|^2 .

In plain English

For a finite superposition of wave modes, the matrix A0=χχ∗A^0=\chi\chi^* built from χ=∑Vv ιe(uκ,v‾) mκ,v\chi=\sum V^v\,\iota_e(\overline{u_{\kappa,v}})\,m_{\kappa,v} is smooth and positive semidefinite on Y≠0Y\ne0, satisfies (∂Φ)A0=0(\partial\Phi)A^0=0, and has columns of (A0)R(A^0)^{\RR} with zero real divergence. This persists after the orthogonal change from null to physical coordinates, where VTv=(1+W⋅v/2)/2V_T^v=(1+W\cdot v/2)/\sqrt2 and ATT0=∣χT∣2A^0_{TT}=|\chi_T|^2.

Why it's here

This applies the abstract divergence-free positive tensor of the current-flow lemma to the actual wave superposition, giving a concrete conserved, nonnegative current A0A^0 in the wave-adapted coordinates. The later barrier arguments use this current as a conserved flux, and the explicit TTTT component ∣χT∣2|\chi_T|^2 gives a directly computable density along the time direction.}}</br>"`json</br>"`</br>{
Classified routine:
Direct application of the paper's current-flow lemma (divergence-free positive tensor from a holomorphic flow) to the specific finite wave superposition, plus an explicit computation of the components after an orthogonal change of coordinates.

Uses

lemDivergence-free positive source tensor from holomorphic flow

Used by

propEnergy barrier on a fixed fiberclaimCurrent and density bounds with wall decayclaimEnergy and wall flux boundsclaimInterior density lower bound by Gaussian inversion

Sources

PaperOpen
Section
§2.3 Coordinates adapted to the wave
Page
—
Label
prop:current
Line
sections/current.tex:313
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    critique: Prop-current's zero-divergence claim comes from the pushforward computation (current.tex:240-257), where "The first sum vanishes by Lemma ". Its proof (current.tex:329) identifies the column of , which is built from the tensor of that lemma.