Presentation.lean`

68 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Release075.ReducedWalk line 8
Source documentation
Internal reduction of an edge walk; no condition is imposed at the closing seam.
```
def ReducedWalk {V : Type*} {G : SimpleGraph V} {a b : V} (p : G.Walk a b) : Prop :=
…
```
theorem OAI.Release075.ReducedWalk.tail line 11
def OAI.Release075.LocallyInjective line 18
Source documentation
A locally injective graph homomorphism preserves internal reduction.
```
def LocallyInjective {V W : Type*} {G : SimpleGraph V} {H : SimpleGraph W}
    (f : G →g H) : Prop :=
…
```
theorem OAI.Release075.ReducedWalk.map line 22
theorem OAI.Release075.reduced_path_or_cycle line 34
Source documentation
A reduced walk which is not a simple path contains a cycle of no greater length. In particular, a nonempty reduced closed walk need not be reduced at its seam.
```
theorem reduced_path_or_cycle {V : Type*} {G : SimpleGraph V} {a b : V}
    (p : G.Walk a b) (hp : ReducedWalk p) :
    p.IsPath ∨ ∃ (c : V) (w : G.Walk c c), w.IsCycle ∧ w.length ≤ p.length := by
…
```
Mentions: OAI.Release075.ReducedWalk
theorem OAI.Release075.reduced_closed_length_ge line 65

theorem OAI.Release075.immersion_fiber_distance line 76

Source documentation

The same girth bound controls a reduced path between distinct vertices of one fiber of an immersion, even without a closing-seam condition.

theorem immersion_fiber_distance {V W : Type*} {G : SimpleGraph V} {H : SimpleGraph W}
    (f : G →g H) (hf : LocallyInjective f) (k : ℕ)
    (hgirth : ∀ a (w : H.Walk a a), w.IsCycle → k ≤ w.length)
    {a b : V} (hneq : a ≠ b) (heq : f a = f b) (p : G.Walk a b)
    (hp : ReducedWalk p) : k ≤ p.length := by
…

Mentions: OAI.Release075.LocallyInjective, OAI.Release075.ReducedWalk

theorem OAI.Release075.ReducedWalk.of_isPath line 90
Source documentation
Simple paths are internally reduced.
```
theorem ReducedWalk.of_isPath {V : Type*} {G : SimpleGraph V} {a b : V}
    {p : G.Walk a b} (hp : p.IsPath) : ReducedWalk p := by
…
```
Mentions: OAI.Release075.ReducedWalk
theorem OAI.Release075.relationGraph_cycle_length line 98
Source documentation
Bipartiteness gives four as the least possible cycle length, without a finiteness assumption.
```
theorem relationGraph_cycle_length {A B : Type*} (R : A → B → Prop)
    (a : A ⊕ B) (p : (relationGraph R).Walk a a) (hp : p.IsCycle) : 4 ≤ p.length := by
…
```
Mentions: OAI.Release075.relationGraph
theorem OAI.Release075.fin_natCast_injective line 109
Source documentation
The shift by a number in [0,r) remains injective modulo any modulus at least r.
```
theorem fin_natCast_injective (r s : ℕ) (hs : r ≤ s) :
    Function.Injective (fun v : Fin r => (v.val : ZMod s)) := by
…
```
structure OAI.Release075.ShiftScheme line 124
Source documentation
Data of either of the two small-angle links. At V use the first block coordinate; at W use the second and swap u,v. The membership and uniqueness fields are exactly the partition of I(z) into blocks, not geometric conclusions.
```
structure ShiftScheme (I P B : Type*) (r : ℕ) (inc : P → Finset I) where
…
```
abbrev OAI.Release075.ShiftScheme.XDirection line 136
abbrev OAI.Release075.ShiftScheme.LDirection line 137
def OAI.Release075.ShiftScheme.attached line 139
def OAI.Release075.ShiftScheme.link line 143
def OAI.Release075.ShiftScheme.projection line 146
theorem OAI.Release075.ShiftScheme.projection_locallyInjective line 158
theorem OAI.Release075.ShiftScheme.link_cycle_length line 204
Source documentation
Girth transfers through the locally injective projection.
```
theorem link_cycle_length (k : ℕ)
    (hgirth : ∀ a (w : (relationGraph (fun i z => i ∈ inc z)).Walk a a),
      w.IsCycle → k ≤ w.length)
    (a : XDirection (I := I) (r := r) ⊕ d.LDirection)
…
```
Mentions: OAI.Release075.relationGraph, OAI.Release075.ShiftScheme.XDirection

theorem OAI.Release075.ShiftScheme.same_label_path_length line 226

Source documentation

Distinct directions of one x-label are separated by the full incidence girth.

theorem same_label_path_length (k : ℕ)
    (hgirth : ∀ a (w : (relationGraph (fun i z => i ∈ inc z)).Walk a a),
      w.IsCycle → k ≤ w.length)
    (i : I) (u v u' v' : Fin r) (hne : (u,v) ≠ (u',v'))
    (p : d.link.Walk (.inl (i,u,v)) (.inl (i,u',v'))) (hp : p.IsPath) :
    k ≤ p.length := by
…

Mentions: OAI.Release075.relationGraph

structure OAI.Release075.BlockPresentation line 246
Source documentation
Pick one block and one leaf index for the two edges in the spanning tree.
```
structure BlockPresentation (I B : Type*) (r : ℕ) where
…
```
abbrev OAI.Release075.BlockPresentation.XEdge line 254
abbrev OAI.Release075.BlockPresentation.LEdge line 255
abbrev OAI.Release075.BlockPresentation.REdge line 256
abbrev OAI.Release075.BlockPresentation.Edge line 257
def OAI.Release075.BlockPresentation.triangleWord line 260
Source documentation
The orientation of a face is L x R⁻¹, not a permuted product.
```
def triangleWord (b : B) (i : (d.block b).labels) (u v : Fin r) : FreeGroup d.Edge :=
…
```
def OAI.Release075.BlockPresentation.treeL line 265
def OAI.Release075.BlockPresentation.treeR line 266
def OAI.Release075.BlockPresentation.relators line 268
abbrev OAI.Release075.BlockPresentation.GroupType line 272
def OAI.Release075.BlockPresentation.edge line 274
def OAI.Release075.BlockPresentation.x line 276
def OAI.Release075.BlockPresentation.l line 277
def OAI.Release075.BlockPresentation.rr line 279

theorem OAI.Release075.BlockPresentation.triangle_relation line 283

Source documentation

The triangle faces impose precisely the factorization used by the rank proof.

theorem triangle_relation (b : B) (i : (d.block b).labels) (u v : Fin r) :
    d.x i u v = (d.l b u (((d.block b).coordinates i).1 + (v.val : ZMod (d.block b).s)))⁻¹ *
      d.rr b v (((d.block b).coordinates i).2 + (u.val : ZMod (d.block b).t)) := by
…

theorem OAI.Release075.BlockPresentation.block_relations line 292
theorem OAI.Release075.BlockPresentation.treeL_eq_one line 295
theorem OAI.Release075.BlockPresentation.treeR_eq_one line 298
theorem OAI.Release075.BlockPresentation.edge_closure line 301

theorem OAI.Release075.BlockPresentation.rectangle_ne_one_iff line 306

Source documentation

A rectangular word is nontrivial exactly when it lies outside the actual normal closure of the triangle and tree relators. This does not assume that nonmembership.

theorem rectangle_ne_one_iff (i : I) (u u' v v' : Fin r) :
    d.x i u v * (d.x i u' v)⁻¹ * d.x i u' v' * (d.x i u v')⁻¹ ≠ 1 ↔
      FreeGroup.of (.inl (i,u,v) : d.Edge) * (FreeGroup.of (.inl (i,u',v) : d.Edge))⁻¹ *
      FreeGroup.of (.inl (i,u',v') : d.Edge) * (FreeGroup.of (.inl (i,u,v') : d.Edge))⁻¹ ∉
        Subgroup.normalClosure d.relators := by
…

def OAI.Release075.cayleyLeft line 317
Source documentation
Left translation is an automorphism of the right-generator Cayley graph.
```
def cayleyLeft {G : Type*} [Group G] (S : Set G) (a : G) :
    SimpleGraph.mulCayley S →g SimpleGraph.mulCayley S where
…
```
theorem OAI.Release075.cayley_reachable_mul_left line 324

theorem OAI.Release075.cayley_connected_of_closure line 329

Source documentation

The connected Cayley graph is derived from generation, not included as data.

theorem cayley_connected_of_closure {G : Type*} [Group G] (S : Set G)
    (hS : Subgroup.closure S = ⊤) : (SimpleGraph.mulCayley S).Connected := by
…

instance OAI.Release075.BlockPresentation.(instance at line 351) line 351
theorem OAI.Release075.BlockPresentation.generators_finite line 355
theorem OAI.Release075.BlockPresentation.cayley_connected line 358
theorem OAI.Release075.mem_puncturedLine_iff_incidence line 371
Source documentation
The two formalizations of puncturing remove exactly parameter zero / the line's own mark. Other marked points are retained in both.
```
theorem mem_puncturedLine_iff_incidence {T K : Type*} [Fintype T] [Field K] [Fintype K]
    (a z : T → K) (d : Projectivization K (T → K)) :
    z ∈ puncturedLine a d.rep ↔ PuncturedIncidence a z d := by
…
```
Mentions: OAI.Release075.puncturedLine, OAI.Release075.PuncturedIncidence
structure OAI.Release075.TwoBlockPartition line 394
Source documentation
A chosen two-block partition. The fields contain only finite combinatorial partition data, no geometric or group-theoretic conclusion.
```
structure TwoBlockPartition (I : Type*) (r : ℕ) (A : Finset I) where
…
```
def OAI.Release075.MarkedLineData.incidences line 403
theorem OAI.Release075.MarkedLineData.mem_incidences line 406
theorem OAI.Release075.MarkedLineData.incidences_card_ge line 412
abbrev OAI.Release075.MarkedLineData.Regular line 419
abbrev OAI.Release075.MarkedLineData.BlockIndex line 420
instance OAI.Release075.MarkedLineData.(instance at line 422) line 422
def OAI.Release075.MarkedLineData.partition line 424
def OAI.Release075.MarkedLineData.block line 433
theorem OAI.Release075.MarkedLineData.block_incident line 436
theorem OAI.Release075.MarkedLineData.block_unique line 444
def OAI.Release075.MarkedLineData.presentation line 459
Source documentation
The presentation is fixed from the finite data, before any quotient or putative separation homomorphism is considered.
```
noncomputable def presentation (hr : 0 < r) : BlockPresentation d.Label d.BlockIndex r where
…
```
Mentions: OAI.Release075.BlockPresentation
def OAI.Release075.MarkedLineData.RectangularNontriviality line 464
theorem OAI.Release075.MarkedLineData.presentation_not_residuallyFinite line 469
Source documentation
The complete finite-quotient argument applied to the actual fixed presentation. The geometric nontriviality premise is established below.
```
theorem presentation_not_residuallyFinite (hr : 0 < r) (hq : r < q) (hq200 : 200 ≤ q)
    (hrect : d.RectangularNontriviality hr) :
    ¬ Group.ResiduallyFinite (d.presentation hr).GroupType := by
…
```
def OAI.Release075.MarkedLineData.vShift line 485
Source documentation
Small-angle link at V.
```
noncomputable def vShift (hr : 0 < r) :
    ShiftScheme d.Label (Fin 20 → ZMod q) d.BlockIndex r d.incidences where
…
```
Mentions: OAI.Release075.ShiftScheme
def OAI.Release075.MarkedLineData.wShift line 496
Source documentation
Small-angle link at W, with u,v interchanged.
```
noncomputable def wShift (hr : 0 < r) :
    ShiftScheme d.Label (Fin 20 → ZMod q) d.BlockIndex r d.incidences where
…
```
Mentions: OAI.Release075.ShiftScheme
def OAI.Release075.MarkedLineData.swapIncidence line 507
Source documentation
Switch the two incidence-graph parts without altering any incidence.
```
def swapIncidence : relationGraph (fun i z => i ∈ d.incidences z) →g
    relationGraph (fun z i => PuncturedIncidence (d.mark i) z (d.direction i)) where
…
```
Mentions: OAI.Release075.relationGraph, OAI.Release075.PuncturedIncidence
theorem OAI.Release075.MarkedLineData.incidences_girth line 520
theorem OAI.Release075.MarkedLineData.v_link_girth line 536
theorem OAI.Release075.MarkedLineData.w_link_girth line 540
theorem OAI.Release075.MarkedLineData.v_same_label_distance line 544
theorem OAI.Release075.MarkedLineData.w_same_label_distance line 550