ContiguousSplit.lean`

38 declarations, 0 contain sorry, 0 declared as axioms

Algebraic disk-picture certificates. The relator words are retained literally, not replaced by their reduced representatives. Connector words may be arbitrary. No planar-surface realization or minimal-band theorem is assumed here.

lemma OAI.TorsionFreeZeroDivisors.ContiguousSplit.rotate_val line 11
abbrev OAI.TorsionFreeZeroDivisors.ContiguousSplit.O line 24
def OAI.TorsionFreeZeroDivisors.ContiguousSplit.split line 25
def OAI.TorsionFreeZeroDivisors.ContiguousSplit.joined line 26
lemma OAI.TorsionFreeZeroDivisors.ContiguousSplit.joined_commutes line 27
lemma OAI.TorsionFreeZeroDivisors.ContiguousSplit.joined_conjugate line 73
lemma OAI.TorsionFreeZeroDivisors.ContiguousSplit.joined_sameCycle line 78
theorem OAI.TorsionFreeZeroDivisors.ContiguousSplit.genusZero line 86
Source documentation
A literal contiguous cut of one cyclic boundary preserves genus zero for any actual involutive matching, including bands across the cut.
```
theorem genusZero (α : Equiv.Perm (O n m)) (hi : Function.Involutive α)
    (hz : MapEuler.GenusZero (joined n m) α) : MapEuler.GenusZero (split n m) α := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.ContiguousSplit.O, OAI.TorsionFreeZeroDivisors.MapEuler.GenusZero, OAI.TorsionFreeZeroDivisors.ContiguousSplit.joined, OAI.TorsionFreeZeroDivisors.ContiguousSplit.split

inductive OAI.TorsionFreeZeroDivisors.BoundaryRefinement.Cuts line 113

Source documentation

Finite sequences of actual vertex cuts. This retains the whole matching; only cyclic boundary order changes. Cuts must occur on the same current cycle.

inductive Cuts : Equiv.Perm O → Equiv.Perm O → Prop
  | refl (σ) : Cuts σ σ
  | step (σ) (p q : O) (hne : p≠q) (hcycle : σ.SameCycle p q) :
      Cuts σ (Equiv.swap p q*σ)
  | trans {σ τ υ} : Cuts σ τ → Cuts τ υ → Cuts σ υ
variable [Fintype O]

lemma OAI.TorsionFreeZeroDivisors.BoundaryRefinement.preserves line 119
lemma OAI.TorsionFreeZeroDivisors.BoundaryRefinement.mapped_sameCycle line 128
lemma OAI.TorsionFreeZeroDivisors.BoundaryRefinement.conjugate line 140
lemma OAI.TorsionFreeZeroDivisors.BoundaryRefinement.left line 156
lemma OAI.TorsionFreeZeroDivisors.BoundaryRefinement.right line 173
lemma OAI.TorsionFreeZeroDivisors.BlockBoundary.fin_cut line 182
def OAI.TorsionFreeZeroDivisors.BlockBoundary.Occ line 240
Source documentation
Each original block has its own actual finite cyclic boundary. Empty blocks contribute no occurrences, rather than an artificial marked vertex.
```
def Occ : List ℕ→Type
  | []=>Empty
  | n::ns=>Fin n⊕Occ ns
```
instance OAI.TorsionFreeZeroDivisors.BlockBoundary.(instance at line 243) line 243
def OAI.TorsionFreeZeroDivisors.BlockBoundary.coordinates line 250
def OAI.TorsionFreeZeroDivisors.BlockBoundary.rotation line 254
def OAI.TorsionFreeZeroDivisors.BlockBoundary.full line 257
theorem OAI.TorsionFreeZeroDivisors.BlockBoundary.refinement line 261
Source documentation
Split the flattened boundary at every literal word boundary. The matching is retained in full, including pairs joining different blocks.
```
theorem refinement (ns : List ℕ) : Cuts (full ns) (rotation ns) := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.BlockBoundary.full, OAI.TorsionFreeZeroDivisors.BlockBoundary.rotation
theorem OAI.TorsionFreeZeroDivisors.BlockBoundary.genusZero line 286
Source documentation
Any actual disk word matching induces a genus-zero matching on all its literal blocks. This alone does not remove conjugator occurrences.
```
theorem genusZero (d : WordPairing.Data inv label) :
    MapEuler.GenusZero (rotation ns) ((coordinates ns).symm.permCongr d.partner) :=
…
```
Mentions: OAI.TorsionFreeZeroDivisors.WordPairing.Data, OAI.TorsionFreeZeroDivisors.MapEuler.GenusZero, OAI.TorsionFreeZeroDivisors.BlockBoundary.rotation, OAI.TorsionFreeZeroDivisors.BlockBoundary.coordinates
structure OAI.TorsionFreeZeroDivisors.AlgebraicPictures.Term line 299
def OAI.TorsionFreeZeroDivisors.AlgebraicPictures.Term.core line 305
def OAI.TorsionFreeZeroDivisors.AlgebraicPictures.Term.word line 306
def OAI.TorsionFreeZeroDivisors.AlgebraicPictures.Term.flip line 307
lemma OAI.TorsionFreeZeroDivisors.AlgebraicPictures.Term.core_flip line 308
lemma OAI.TorsionFreeZeroDivisors.AlgebraicPictures.Term.word_flip line 311
def OAI.TorsionFreeZeroDivisors.AlgebraicPictures.word line 317
def OAI.TorsionFreeZeroDivisors.AlgebraicPictures.relations line 318
lemma OAI.TorsionFreeZeroDivisors.AlgebraicPictures.word_append line 319
lemma OAI.TorsionFreeZeroDivisors.AlgebraicPictures.word_reverse_flip line 321
lemma OAI.TorsionFreeZeroDivisors.AlgebraicPictures.term_mem line 330
lemma OAI.TorsionFreeZeroDivisors.AlgebraicPictures.word_mem line 342
theorem OAI.TorsionFreeZeroDivisors.AlgebraicPictures.expansion line 352
Source documentation
Literal normal-closure expansion, with each actual relator and its sign.
```
theorem expansion {g : FreeGroup A} (h : g∈Subgroup.normalClosure (relations rel)) :
    ∃ ts : List (Term (A:=A) (I:=I)),mk (word rel ts)=g := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.AlgebraicPictures.relations, OAI.TorsionFreeZeroDivisors.AlgebraicPictures.Term, OAI.TorsionFreeZeroDivisors.AlgebraicPictures.word
def OAI.TorsionFreeZeroDivisors.AlgebraicPictures.cutWord line 372
theorem OAI.TorsionFreeZeroDivisors.AlgebraicPictures.quotient_identity line 378
Source documentation
A null word in the literal quotient has an actual finite inverse-letter noncrossing matching after cutting along its conjugating paths. This is the algebraic cancellation step; it does not assert the later band reduction.
```
theorem quotient_identity (h : PresentedGroup.mk (relations rel) (mk outer)=1) :
    ∃ ts : List (Term (A:=A) (I:=I)),
…
```
Mentions: OAI.TorsionFreeZeroDivisors.AlgebraicPictures.relations, OAI.TorsionFreeZeroDivisors.AlgebraicPictures.Term
lemma OAI.TorsionFreeZeroDivisors.AlgebraicPictures.empty_relators line 387
Source documentation
The empty-relator case is not silently excluded: its boundary must itself be a free-group identity.
```
lemma empty_relators (h : mk (word rel [])=mk outer) : mk outer=1 := h.symm
…
```
Mentions: OAI.TorsionFreeZeroDivisors.AlgebraicPictures.word