claimroutineinferred_dep
Laplacian of segment energy equals full determinant
Shows equals with no wall term
full-determinant part of the flux identity
Statement (paper)
Integrating with in and dividing by gives, in the sense of distributions, , with no boundary contribution: on one has , since the restricted form is singular, and . Moreover gives , and this identity holds pointwise because the volume integral is smooth in by .
In plain English
In the sense of distributions in , the Laplacian of the segment energy equals the fiber integral , with no boundary term from the moving wall.
Why it's here
Applying the moving-domain Green formula with and integrating in turns the left side into and the interior term into the full determinant. The wall flux vanishes because the restricted form is singular, so on , and gives the pointwise identity . 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.
Uses
Used by
Nothing in the paper
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
- infoinferred_depoutline: "Laplacian of segment energy equals full determinant" rests on claim-prop-energy-flux-1