OAI/Analysis/CircleDomains/Modulus/VerticalTerminalPayment.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Vertical-line payment for an actual normalized finite model

The round holes are taken from the model's terminal assignment. Their cluster costs are derived from the real function on the physical terminal boundaries. This joins line payment to the finite-transfer construction.

  1. theorem OAI.CircleDomainRigidity.TerminalComponentAssignment.vertical_line_payment line 24
  2. theorem OAI.CircleDomainRigidity.TerminalComponentAssignment.vertical_line_payment_source_energy line 83