ModelPriorityPairs.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Every new pair in the actual two-coordinate append operation is null. The support constancy is precisely the common flattened neighborhood property used when choosing the cutoffs.

theorem OAI.CircleDomainRigidity.CompactScalarModel.flattened_priority_trace_pairs line 16