OAI/Analysis/CircleDomains/Transfer/ModelFlattenedSelection.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous selection of the actual old-test flattenings, height flattening, and small-support horizontal priority coordinate. All fields are constructed from the existing model and the stated energy budgets.

  1. structure OAI.CircleDomainRigidity.CompactScalarModel.FlattenedSourceSelection line 19
  2. theorem OAI.CircleDomainRigidity.CompactScalarModel.exists_flattened_source_selection line 67