OAI/Analysis/CircleDomains/Transfer/GeometricGridAssembly.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Complete geometric assembly for a selected real-coordinate grid

The bands themselves provide the terminal oscillation budgets. After selecting physical terminals off the core, the descending grid construction fills the remaining dust and retains its actual one-active-coordinate boundary condition. No disk family or containment conclusion is assumed.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.boundary_oscillation_le_of_band line 23
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_geometric_grid_assembly line 44