OAI/Analysis/CircleDomains/Modulus/TerminalLinePayment.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Parallel-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.parallel_line_payment line 23