OAI/Analysis/CircleDomains/Transfer/PrincipalSubordinateGraphTransfer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Construct the finite masked model directly from subordinate branch neighborhoods and the physical contour graph avoidance. The active label, real collars and absent-coordinate replacements are all derived here.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.principal_subordinate_graph_transfer line 22