ConcreteGroup.lean`

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.TorsionFreeZeroDivisors.ConcreteGroup.equal_value_picture line 16
Source documentation
Equal values at distinct endpoints within one graph component have an actual reduced lifted disk picture. This is the precise obstruction needed for the nonvanishing of the authors' factors, with no graph embedding assumed.
```
theorem equal_value_picture {z w : VA rep⊕VB rep}
    (hp : (ShortClosure.simpleGraph (Γ rep r)).Reachable z w) (hzw : z≠w)
    (hv : value rep r z=value rep r w) :
    ∃n,∃a : FinitePicture.Data (O:=Fin n) (Γ rep r) (SampleGraph.label rep) Types.inverse z w,
…
```
Mentions: OAI.TorsionFreeZeroDivisors.ShortClosure.simpleGraph, OAI.TorsionFreeZeroDivisors.ConcreteGroup.Γ, OAI.TorsionFreeZeroDivisors.ConcreteGroup.value, OAI.TorsionFreeZeroDivisors.FinitePicture.Data, OAI.TorsionFreeZeroDivisors.SampleGraph.label, OAI.TorsionFreeZeroDivisors.Types.inverse
def OAI.TorsionFreeZeroDivisors.SampleGraph.Picture.SeparatorObligation line 34
Source documentation
The exact remaining sharp-separator obligation for the literal prepared interaction graphs of disk pictures. This is NOT proved or inserted as a hypothesis into the main target: it records the unclosed dependency.
```
def SeparatorObligation : Prop :=
…
```
theorem OAI.TorsionFreeZeroDivisors.SampleGraph.Picture.root_path_nontrivial line 45
Source documentation
The actual disk/path endpoint, conditional on exactly the still-missing sharp-separator dependency, not a replacement main theorem.
```
theorem root_path_nontrivial (hsample : r∈ActualPatternEvent.samples rep)
    (hsep : SeparatorObligation r x y hL hd)
    (havoid : IsEmpty (BoundedSystem (PlanarParameters.C PathSystem.ε ClosedWords.D)
      (PlanarParameters.K PathSystem.ε ClosedWords.D) (PlanarParameters.sides PathSystem.ε ClosedWords.D) rep r x y))
    {z w : VA rep⊕VB rep} (p : GraphPresentation.Path (graph rep r) z w)
    (hzw : z≠w) (hz : z=Sum.inl x ∨ z=Sum.inr y) :
    p.eval (ConcreteGroup.letter rep r ∘ label rep)≠1 := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.ActualPatternEvent.samples, OAI.TorsionFreeZeroDivisors.SampleGraph.Picture.SeparatorObligation, OAI.TorsionFreeZeroDivisors.SampleGraph.BoundedSystem, OAI.TorsionFreeZeroDivisors.PlanarParameters.C, OAI.TorsionFreeZeroDivisors.SampleGraph.PathSystem.ε, OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.D, OAI.TorsionFreeZeroDivisors.PlanarParameters.K, OAI.TorsionFreeZeroDivisors.PlanarParameters.sides, OAI.TorsionFreeZeroDivisors.SampleGraph.VA, OAI.TorsionFreeZeroDivisors.SampleGraph.VB, OAI.TorsionFreeZeroDivisors.GraphPresentation.Path, OAI.TorsionFreeZeroDivisors.SampleGraph.graph, OAI.TorsionFreeZeroDivisors.ConcreteGroup.letter, OAI.TorsionFreeZeroDivisors.SampleGraph.label
lemma OAI.TorsionFreeZeroDivisors.BoundaryRefinement.fiber line 65
Source documentation
Performing literal vertex cuts in one boundary fiber performs the same cuts in the whole occurrence set, leaving every other fiber unchanged.
```
lemma fiber {i : I} {σ τ : Equiv.Perm (O i)} (h : Cuts σ τ)
    (ρ : ∀j,Equiv.Perm (O j)) :
    Cuts (Equiv.sigmaCongrRight (Function.update ρ i σ))
      (Equiv.sigmaCongrRight (Function.update ρ i τ)) := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.BoundaryRefinement.Cuts
lemma OAI.TorsionFreeZeroDivisors.BoundaryRefinement.sigma line 104
Source documentation
All of a finite family's contiguous boundary refinements may be carried out simultaneously, with the matching on the whole occurrence set retained.
```
lemma sigma {σ τ : ∀i,Equiv.Perm (O i)} (h : ∀i,Cuts (σ i) (τ i)) :
    Cuts (Equiv.sigmaCongrRight σ) (Equiv.sigmaCongrRight τ) := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.BoundaryRefinement.Cuts
lemma OAI.TorsionFreeZeroDivisors.BoundaryRefinement.finCongr_rotate line 132
lemma OAI.TorsionFreeZeroDivisors.BoundaryRefinement.sigmaCongrLeft_rotation line 136
lemma OAI.TorsionFreeZeroDivisors.BoundaryRefinement.sumSigma_rotation line 145
lemma OAI.TorsionFreeZeroDivisors.BoundaryRefinement.uniqueSigma_rotation line 152
lemma OAI.TorsionFreeZeroDivisors.BoundaryRefinement.fin_refinement line 160
Source documentation
The pinned finSigmaFinEquiv is the literal consecutive sum indexing; cutting exactly at its fiber boundaries preserves the entire matching.
```
lemma fin_refinement {m : ℕ} (n : Fin m→ℕ) :
    Cuts (finSigmaFinEquiv.symm.permCongr (finRotate (∑i,n i)))
      (Equiv.sigmaCongrRight fun i=>finRotate (n i)) := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.BoundaryRefinement.Cuts
lemma OAI.TorsionFreeZeroDivisors.BoundaryRefinement.fin_index_refinement line 225
lemma OAI.TorsionFreeZeroDivisors.BalancedGenus.join_refinement line 240
lemma OAI.TorsionFreeZeroDivisors.BalancedGenus.position_refinement line 267
lemma OAI.TorsionFreeZeroDivisors.BalancedGenus.refinement line 273
lemma OAI.TorsionFreeZeroDivisors.BalancedGenus.genusZero line 282
lemma OAI.TorsionFreeZeroDivisors.ExtendComparisons.rel_iff line 298
Source documentation
Added closure letters are fixed; they introduce no interaction between DIFFERENT boundary pieces. This statement does not discard self-loops silently.
```
lemma rel_iff {p q : T} (hpq : p≠q) :
    PairingClusters.Rel (fun x : Position more=>x.1) (partner C hle) p q ↔
      PairingClusters.Rel (fun x : Position len=>x.1) C.pairing.partner p q := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.PairingClusters.Rel, OAI.TorsionFreeZeroDivisors.ExtendComparisons.partner
def OAI.TorsionFreeZeroDivisors.RecursiveSeparator.Split.changeDecidableEq line 316
def OAI.TorsionFreeZeroDivisors.RecursiveSeparator.Split.of_off_diagonal line 322
Source documentation
Loops have no effect on separator closure.
```
def of_off_diagonal (h : ∀p q,p≠q→(R p q↔Q p q)) (P : RecursiveSeparator.Split R S) :
    RecursiveSeparator.Split Q S where
…
```
Mentions: OAI.TorsionFreeZeroDivisors.RecursiveSeparator.q, OAI.TorsionFreeZeroDivisors.RecursiveSeparator.Split
lemma OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.closed_rel line 344