OAI/Analysis/CircleDomains/Topology/SignedScalarCircleModel.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite signed compact tests have a common circle model. The proof uses the proved unit-test construction, and recovers all original tests by an exact linear combination on the same model.

  1. theorem OAI.CircleDomainRigidity.exists_signed_compact_scalar_circle_model line 21