Rectangles.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Release075.MarkedLineData.rectangle_turn_large line 9
theorem OAI.Release075.MarkedLineData.rectangular_nontriviality line 53
Source documentation
Every actual rectangular word in the fixed presentation is nontrivial: nullhomotopy gives a minimal labelled planar filling, whose reduced link sectors contradict its Euler-characteristic-one angular identity.
```
theorem rectangular_nontriviality : d.RectangularNontriviality hr := by
…
```
theorem OAI.Release075.MarkedLineData.ribbon_closed_strict line 100
theorem OAI.Release075.MarkedLineData.ribbon_boundary_length line 108
theorem OAI.Release075.MarkedLineData.reduced_linear_active_bound line 125
theorem OAI.Release075.MarkedLineData.exists_linear_filling line 147
Source documentation
An actual finite nullhomotopy has a genuine planar filling of linearly bounded size, not an assumed Dehn-function estimate. This estimate is a necessary bridge to the uniform Cayley thinness argument below.
```
theorem exists_linear_filling (hf : Fillable (d.presentation hr).flipEdge
    (d.presentation hr).edgeTarget (d.presentation hr).TriangleFace w) :
    ∃ D : TriangleFilling (d.presentation hr).flipEdge (d.presentation hr).edgeTarget
      (d.presentation hr).TriangleFace w, D.activeCount ≤ 19*w.length := by
…
```
Mentions: OAI.Release075.Fillable, OAI.Release075.TriangleFilling
theorem OAI.Release075.MarkedLineData.actual_presentation_not_residuallyFinite line 168
Source documentation
The fixed presentation's non-residual-finiteness is now unconditional in its finite incidence data; no rectangular nontriviality premise remains.
```
theorem actual_presentation_not_residuallyFinite (hq : r < q) (hq200 : 200 ≤ q) :
    ¬ Group.ResiduallyFinite (d.presentation hr).GroupType :=
…
```