propositionroutineinferred_depunresolved_ref

Energy flux identity with full wall normal

Bounds ΔzF\Delta_z\mathcal F above by a wall flux with the full normal
one-sided Laplacian bound on the fiber energy
Proposition·prop:energy-flux·§4.3 Cancelling the full determinant

Statement (paper)

The energy F\mathcal F is smooth on a<∣τ∣<4a<|\tau|<4. Let ρ\rho denote the boundary value of u/ru/r, which extends smoothly from the interior. In the three variables z=(T,τ)z=(T,\tau) one has ΔzF(z)+∫ΩzA:Σ  dζ=∫ρ G(r)∗AwG(r) δ(r) dζ. \Delta_z\mathcal F(z)+\int_{\Omega_z} A:\Sigma\,\dd\zeta =\int \rho\,G(r)^*A_{\rm w}G(r)\,\delta(r)\dd\zeta . The normal seen by the current is that of the moving wall in the total space, so G(r)G(r) is the full gradient. The integration is on one fiber: δ(r) dζ= dSfib/∣∇fibr∣\delta(r)\dd\zeta=\dd S_{\rm fib}/|\nabla_{\rm fib}r|, where the spatial gradient is nonzero by the ellipsoid chart. Since A:Σ≥0A:\Sigma\ge0, the boundary integral bounds ΔzF\Delta_z\mathcal F from above.

In plain English

The energy F\mathcal F is smooth for a<∣τ∣<4a<|\tau|<4, and its Laplacian in z=(T,τ)z=(T,\tau) plus the interior term ∫ΩzA:Σ  dζ\int_{\Omega_z}A:\Sigma\,\dd\zeta equals the wall flux ∫ρ G(r)∗AwG(r) δ(r) dζ\int\rho\,G(r)^*A_{\rm w}G(r)\,\delta(r)\dd\zeta on one fiber, where G(r)G(r) is the full gradient and ρ\rho is the boundary value of u/ru/r. Since A:Σ≥0A:\Sigma\ge0, this wall integral bounds ΔzF\Delta_z\mathcal F from above.

Why it's here

The identity combines the two earlier claims: the AA-part gives the wall flux minus the interior term A:ΣA:\Sigma, and the full-determinant part contributes no wall term because the moving-wall flux vanishes. What remains is a one-sided bound on ΔzF\Delta_z\mathcal F by a boundary integral with the full normal, which the barrier and pencil arguments then use to control the energy.
Classified routine:
A divergence-theorem computation that combines the earlier lemmas: the column-divergence-free Hessian cofactor, the Moore determinant and cofactor properties, and the fiber geometry. It yields a flux identity of the usual kind obtained by integrating a divergence-free current against a moving boundary.

Uses

lemHessian cofactor is column-divergence-freelemFiber Hessian geometry and JacobianlemMoore determinant and cofactor propertieslemHessian calculus in quaternionic coordinates

Used by

propEnergy barrier on a fixed fiberclaimEnergy and wall flux boundsclaimDeterminant energy and balance on pencil fibers

Inside the proof

claimGreen formula on moving total domainclaimLaplacian of X_0 gives wall flux minus interiorclaimLaplacian of segment energy equals full determinant

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    The proof relies on the Hessian calculus: "Green's formula ", the Schur energy identity, and the boundary restriction. These are in the Hessian calculus section (§3.1), which probably holds that lemma.
  • warn
    unresolved_ref
    Interior term relies on the Schur-complement identity eq:schur-energy-identity and Green formula eq:calculus-green, equations rather than statements.