OAI/Analysis/CircleDomains/Rigidity/ConductivityLocalEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The exact finite-disk energy balance for the constructed conductivity system. The Jacobian and the vertical boundary flux remain explicit; neither is replaced by an assumed energy estimate.

  1. theorem OAI.CircleDomainRigidity.PlaneLocalWeakComplex.conductivity_local_energy_balance line 14