PresentedMixedExhaustion.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Construct the common mixed exhaustion from its actual real subfamily. Only physical functions and terminal widths must agree; auxiliary chart choices and dummy singular labels need not be identical as dependent structures.

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_mixed_model_exhaustion_of_real_subfamily line 16