claimroutineinferred_dep

Laplacian of segment energy equals full determinant

Shows ΔzEz(u)\Delta_zE_z(u) equals ∫det⁡H(B0+u)\int\det H(B_0+u) with no wall term
full-determinant part of the flux identity
Claim·§4.3 Cancelling the full determinant·inside propEnergy flux identity with full wall normal

Statement (paper)

Integrating with M=C(H(B0+θu))M=C(H(B_0+\theta u)) in θ\theta and dividing by λ\lambda gives, in the sense of distributions, ΔzEz(u)=∫Ωzdet⁡H(B0+u)  dζ\Delta_z E_z(u)=\int_{\Omega_z}\det H(B_0+u)\,\dd\zeta, with no boundary contribution: on r=0r=0 one has ν∗Mν=0\nu^*M\nu=0, since the restricted form is singular, and MTT=det⁡DθuM_{TT}=\det D_{\theta u}. Moreover det⁡B=0\det B=0 gives ∫01M:H(u)  dθ=det⁡H(B0+u)\int_0^1 M:H(u)\,\dd\theta=\det H(B_0+u), and this identity holds pointwise because the volume integral is smooth in zz by .

In plain English

In the sense of distributions in z=(T,τ)z=(T,\tau), the Laplacian ΔzEz(u)\Delta_z E_z(u) of the segment energy equals the fiber integral ∫Ωzdet⁡H(B0+u)  dζ\int_{\Omega_z}\det H(B_0+u)\,\dd\zeta, with no boundary term from the moving wall.

Why it's here

Applying the moving-domain Green formula with M=C(H(B0+θu))M=C(H(B_0+\theta u)) and integrating in θ\theta turns the left side into ΔzEz\Delta_z E_z and the interior term into the full determinant. The wall flux vanishes because the restricted form is singular, so ν∗Mν=0\nu^*M\nu=0 on r=0r=0, and det⁡B=0\det B=0 gives the pointwise identity ∫01M:H(u)  dθ=det⁡H(B0+u)\int_0^1 M:H(u)\,\dd\theta=\det H(B_0+u). This determinant identity is the full-determinant cancellation used in the energy-flux proposition.
Classified routine:
A direct consequence of the preceding moving-domain Green formula combined with the cofactor divergence-free property and the fundamental theorem of calculus in θ applied to the Moore determinant (det B=0). This is bookkeeping assembled from earlier nodes.

Sources

PaperOpen
Section
§4.3 Cancelling the full determinant
Page
—
Label
—
Line
sections/energy.tex:257
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Laplacian of segment energy equals full determinant" rests on claim-prop-energy-flux-1