OAI/Combinatorics/PolynomialVacuum/Cylinder/StackRecovery.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolynomialVacuumCylinder.spinOfCharge line 9
2. theorem OAI.PolynomialVacuumCylinder.charge_spinOfCharge line 12
3. theorem OAI.PolynomialVacuumCylinder.localIce_values line 16
4. theorem OAI.PolynomialVacuumCylinder.supported_ice_values line 24
5. def OAI.PolynomialVacuumCylinder.recoverVertical line 39
6. def OAI.PolynomialVacuumCylinder.recoverAuxiliary line 41
7. def OAI.PolynomialVacuumCylinder.recoverInternal line 43
8. theorem OAI.PolynomialVacuumCylinder.outside_vertical_zero line 46
9. theorem OAI.PolynomialVacuumCylinder.outside_horizontal_zero line 56
10. theorem OAI.PolynomialVacuumCylinder.recover_stack line 66