IndexedFillingValue.lean`

736 declarations, 0 contain sorry, 0 declared as axioms

The integral filling value of a literal nullword. This is a consequence of constructed disks and sphere vanishing, not a replacement hypothesis.

def OAI.HyperbolicObstruction.IndexedFilling.SphereZero line 32
def OAI.HyperbolicObstruction.IndexedFilling.HasChain line 35
def OAI.HyperbolicObstruction.IndexedFilling.Null line 39
lemma OAI.HyperbolicObstruction.IndexedFilling.HasChain.empty line 44
lemma OAI.HyperbolicObstruction.IndexedFilling.HasChain.exists_of_null line 48
lemma OAI.HyperbolicObstruction.IndexedFilling.HasChain.unique line 54
lemma OAI.HyperbolicObstruction.IndexedFilling.HasChain.free_unique line 62
lemma OAI.HyperbolicObstruction.IndexedFilling.HasChain.add line 71
lemma OAI.HyperbolicObstruction.IndexedFilling.HasChain.mirror line 89
lemma OAI.HyperbolicObstruction.IndexedFilling.HasChain.rotate line 94
lemma OAI.HyperbolicObstruction.IndexedFilling.HasChain.freePair line 99
lemma OAI.HyperbolicObstruction.IndexedFilling.HasChain.conjugateLetter line 102
lemma OAI.HyperbolicObstruction.IndexedFilling.HasChain.conjugate line 112
lemma OAI.HyperbolicObstruction.IndexedFilling.HasChain.cell line 122
def OAI.HyperbolicObstruction.IndexedFilling.value line 128
Source documentation
Chosen only from genuine, exactly marked genus-zero disks.
```
def value (w : Word E) : A :=
…
```
lemma OAI.HyperbolicObstruction.IndexedFilling.value_spec line 131
lemma OAI.HyperbolicObstruction.IndexedFilling.value_of_has line 137
lemma OAI.HyperbolicObstruction.IndexedFilling.value_cell line 143
inductive OAI.HyperbolicObstruction.SignedWalks.Walk line 158
lemma OAI.HyperbolicObstruction.SignedWalks.Walk.nil_iff line 165
lemma OAI.HyperbolicObstruction.SignedWalks.Walk.cons_iff line 170
lemma OAI.HyperbolicObstruction.SignedWalks.Walk.single line 176
lemma OAI.HyperbolicObstruction.SignedWalks.Walk.append line 179
lemma OAI.HyperbolicObstruction.SignedWalks.Walk.reverse line 184
lemma OAI.HyperbolicObstruction.SignedWalks.Walk.head line 193
lemma OAI.HyperbolicObstruction.SignedWalks.Walk.take_drop line 196
lemma OAI.HyperbolicObstruction.SignedWalks.Walk.get_start line 207
lemma OAI.HyperbolicObstruction.SignedWalks.Walk.adjacent line 215
lemma OAI.HyperbolicObstruction.SignedWalks.Walk.first line 222
lemma OAI.HyperbolicObstruction.SignedWalks.Walk.last line 226
lemma OAI.HyperbolicObstruction.SignedWalks.Walk.closed_rotate line 233
def OAI.HyperbolicObstruction.SignedWalks.reach line 253
Source documentation
Reachability in the actual signed graph, not equality of word images.
```
def reach : Setoid V where
…
```
def OAI.HyperbolicObstruction.SignedWalks.root line 259
lemma OAI.HyperbolicObstruction.SignedWalks.root_reach line 260
def OAI.HyperbolicObstruction.SignedWalks.rootWord line 263
lemma OAI.HyperbolicObstruction.SignedWalks.rootWord_walk line 264
lemma OAI.HyperbolicObstruction.SignedWalks.root_eq line 267
lemma OAI.HyperbolicObstruction.SignedWalks.edge_root line 270
def OAI.HyperbolicObstruction.SignedWalks.correction line 273
lemma OAI.HyperbolicObstruction.SignedWalks.correction_walk line 276
lemma OAI.HyperbolicObstruction.SignedWalks.Walk.ofFn_vertices line 288
lemma OAI.HyperbolicObstruction.SignedWalks.Walk.ofFn_closed line 305
lemma OAI.HyperbolicObstruction.SignedWalks.correction_telescope line 327
Source documentation
Product of rooted edge corrections is exactly the rooted original path; all intermediate paths cancel in the free group, before taking any quotient.
```
lemma correction_telescope (root : V → Word E) {x y : V} {u : Word E}
    (h : Walk start x y u) :
    FreeGroup.mk (u.flatMap (fun e => root (start e) ++ [e] ++ FreeGroup.invRev (root (start (invLetter e))))) =
      FreeGroup.mk (root x ++ u ++ FreeGroup.invRev (root y)) := by
…
```
Mentions: OAI.HyperbolicObstruction.SignedWalks.root, OAI.HyperbolicObstruction.SignedWalks.Walk
lemma OAI.HyperbolicObstruction.SignedWalks.correction_reverse line 345
def OAI.HyperbolicObstruction.IndexedFilling.letterChain line 367
def OAI.HyperbolicObstruction.IndexedFilling.cellBoundary line 370
def OAI.HyperbolicObstruction.IndexedFilling.boundary line 371
lemma OAI.HyperbolicObstruction.IndexedFilling.correction_null line 377
lemma OAI.HyperbolicObstruction.IndexedFilling.HasChain.words line 381
lemma OAI.HyperbolicObstruction.IndexedFilling.HasChain.flatMap line 390
def OAI.HyperbolicObstruction.IndexedFilling.edgeValue line 400
def OAI.HyperbolicObstruction.IndexedFilling.leftInverse line 401
lemma OAI.HyperbolicObstruction.IndexedFilling.correction_value_reverse line 404
lemma OAI.HyperbolicObstruction.IndexedFilling.leftInverse_letter line 413
lemma OAI.HyperbolicObstruction.IndexedFilling.leftInverse_cell line 424
lemma OAI.HyperbolicObstruction.IndexedFilling.leftInverse_boundary line 437
theorem OAI.HyperbolicObstruction.IndexedFilling.boundary_injective line 448
Source documentation
Exact d₂ injectivity, once closed graph loops have actual disks and every closed genus-zero diagram has zero full independent-cell chain.
```
theorem boundary_injective (hrev : B.rev = invLetter)
    (hz : SphereZero B (fun c => Finsupp.single c (1 : ℤ)))
    (hloop : ∀ x w, Walk B.start x x w → Null B w) :
    Function.Injective (boundary B) := by
…
```
Mentions: OAI.HyperbolicObstruction.IndexedFilling.SphereZero, OAI.HyperbolicObstruction.IndexedFilling.Null, OAI.HyperbolicObstruction.IndexedFilling.boundary
def OAI.HyperbolicObstruction.PictureSwitch.PermInsertion.perm line 473
Source documentation
Insert exactly one separately indexed point after every point satisfying p.
```
def perm : Perm (D ⊕ Subtype p) where
…
```
def OAI.HyperbolicObstruction.PictureSwitch.PermInsertion.collapse line 489
lemma OAI.HyperbolicObstruction.PictureSwitch.PermInsertion.collapse_step line 492
lemma OAI.HyperbolicObstruction.PictureSwitch.PermInsertion.collapse_sameCycle line 503
lemma OAI.HyperbolicObstruction.PictureSwitch.PermInsertion.base_step line 509
lemma OAI.HyperbolicObstruction.PictureSwitch.PermInsertion.base_sameCycle line 519
lemma OAI.HyperbolicObstruction.PictureSwitch.PermInsertion.collapse_base_cycle line 525
def OAI.HyperbolicObstruction.PictureSwitch.PermInsertion.orbitEquiv line 536
Source documentation
Subdivision gives a genuine equivalence of orbit quotients, including fixed points and the empty type.
```
def orbitEquiv : Quotient (SameCycle.setoid (perm f p)) ≃ Quotient (SameCycle.setoid f) where
…
```
Mentions: OAI.HyperbolicObstruction.PictureSwitch.PermInsertion.perm
lemma OAI.HyperbolicObstruction.PictureSwitch.PermInsertion.cycles_eq line 548
lemma OAI.HyperbolicObstruction.PictureSwitch.cycles_equiv line 563
abbrev OAI.HyperbolicObstruction.PictureSwitch.ConeExpansion.Point line 584
def OAI.HyperbolicObstruction.PictureSwitch.ConeExpansion.freeFace line 585
def OAI.HyperbolicObstruction.PictureSwitch.ConeExpansion.face line 587
def OAI.HyperbolicObstruction.PictureSwitch.ConeExpansion.edge line 614
def OAI.HyperbolicObstruction.PictureSwitch.ConeExpansion.map line 626
def OAI.HyperbolicObstruction.PictureSwitch.ConeExpansion.vertexEquiv line 637
Source documentation
Arrange the old vertices, their inserted corners, and the new apices.
```
def vertexEquiv : ((D ⊕ {d // p (M.edge d)}) ⊕ Subtype p) ≃ Point p where
…
```
Mentions: OAI.HyperbolicObstruction.PictureSwitch.ConeExpansion.Point
lemma OAI.HyperbolicObstruction.PictureSwitch.ConeExpansion.vertex_equiv line 650
lemma OAI.HyperbolicObstruction.PictureSwitch.ConeExpansion.vertex_cycles line 658
def OAI.HyperbolicObstruction.PictureSwitch.ConeExpansion.frozenFace line 662
def OAI.HyperbolicObstruction.PictureSwitch.ConeExpansion.faceClass line 664
lemma OAI.HyperbolicObstruction.PictureSwitch.ConeExpansion.faceClass_step line 670
lemma OAI.HyperbolicObstruction.PictureSwitch.ConeExpansion.frozen_step line 682
def OAI.HyperbolicObstruction.PictureSwitch.ConeExpansion.faceOrbitEquiv line 688
Source documentation
New triangular faces are indexed by the old free sides, not merely by an unlabelled area count. All other face orbits are literally unchanged.
```
def faceOrbitEquiv : Quotient (SameCycle.setoid (face M p hf)) ≃
    (Quotient (SameCycle.setoid (frozenFace M p hf)) ⊕ Subtype p) where
…
```
Mentions: OAI.HyperbolicObstruction.PictureSwitch.ConeExpansion.face, OAI.HyperbolicObstruction.PictureSwitch.ConeExpansion.frozenFace
lemma OAI.HyperbolicObstruction.PictureSwitch.ConeExpansion.face_cycles line 720
lemma OAI.HyperbolicObstruction.PictureSwitch.ConeExpansion.euler_eq line 725
def OAI.HyperbolicObstruction.PictureSwitch.ConeExpansion.collapse line 736
lemma OAI.HyperbolicObstruction.PictureSwitch.ConeExpansion.collapse_face line 739
lemma OAI.HyperbolicObstruction.PictureSwitch.ConeExpansion.collapse_edge line 750
lemma OAI.HyperbolicObstruction.PictureSwitch.ConeExpansion.components_bound line 759
theorem OAI.HyperbolicObstruction.PictureSwitch.ConeExpansion.genusZero_of_expansion line 771
Source documentation
Removing all radial stars from a genus-zero triangulated side-pairing preserves genus zero. This is a consequence of the permutation counts.
```
theorem genusZero_of_expansion (h : (map M p hf).GenusZero) : M.GenusZero := by
…
```
Mentions: OAI.HyperbolicObstruction.PictureSwitch.ConeExpansion.map
lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.euler_equiv line 791
lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.components_equiv line 798
lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.components_card_equiv line 818
lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.genusZero_equiv line 833
structure OAI.HyperbolicObstruction.PictureSwitch.TriangleMarking line 847
Source documentation
The three roles are old side (0), incoming radial side (1), and outgoing radial side (2). Frozen polygons have only old sides. These are local incidence conditions on an existing side-pairing, not a genus or chain assumption.
```
structure TriangleMarking (M : PictureMap D) where
…
```
Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap
abbrev OAI.HyperbolicObstruction.PictureSwitch.TriangleMarking.Base line 860
def OAI.HyperbolicObstruction.PictureSwitch.TriangleMarking.free line 862
lemma OAI.HyperbolicObstruction.PictureSwitch.TriangleMarking.top_of_role line 865
lemma OAI.HyperbolicObstruction.PictureSwitch.TriangleMarking.top_prev line 871
lemma OAI.HyperbolicObstruction.PictureSwitch.TriangleMarking.prev_eq line 876
lemma OAI.HyperbolicObstruction.PictureSwitch.TriangleMarking.role_next0 line 881
lemma OAI.HyperbolicObstruction.PictureSwitch.TriangleMarking.role_next1 line 884
lemma OAI.HyperbolicObstruction.PictureSwitch.TriangleMarking.role_next2 line 888
lemma OAI.HyperbolicObstruction.PictureSwitch.TriangleMarking.role_prev0 line 892
lemma OAI.HyperbolicObstruction.PictureSwitch.TriangleMarking.role_prev1 line 896
lemma OAI.HyperbolicObstruction.PictureSwitch.TriangleMarking.role_prev2 line 900
def OAI.HyperbolicObstruction.PictureSwitch.TriangleMarking.next line 905
def OAI.HyperbolicObstruction.PictureSwitch.TriangleMarking.prev line 906
lemma OAI.HyperbolicObstruction.PictureSwitch.TriangleMarking.next_role line 909
lemma OAI.HyperbolicObstruction.PictureSwitch.TriangleMarking.next_top line 918
lemma OAI.HyperbolicObstruction.PictureSwitch.TriangleMarking.prev_role line 927
lemma OAI.HyperbolicObstruction.PictureSwitch.TriangleMarking.prev_top line 936
lemma OAI.HyperbolicObstruction.PictureSwitch.TriangleMarking.prev_next line 945
lemma OAI.HyperbolicObstruction.PictureSwitch.TriangleMarking.next_prev line 954
def OAI.HyperbolicObstruction.PictureSwitch.TriangleMarking.face line 964
Source documentation
Each macro face walks through consecutive radial triangles around one actual apex. Frozen face cycles are unchanged.
```
def face : Perm H.Base where
…
```
lemma OAI.HyperbolicObstruction.PictureSwitch.TriangleMarking.edge_invariant line 971
def OAI.HyperbolicObstruction.PictureSwitch.TriangleMarking.contraction line 974
lemma OAI.HyperbolicObstruction.PictureSwitch.TriangleMarking.free_invariant line 981
def OAI.HyperbolicObstruction.PictureSwitch.TriangleMarking.expand line 987
Source documentation
Each elementary dart has its own retained old side, with the two radial copies kept separately until the final contraction.
```
def expand : ConeExpansion.Point H.free → D
  | .inl x => x.val
  | .inr (.inl x) => M.face x.val.val
  | .inr (.inr x) => M.face (M.face x.val.val)

omit [Fintype D] [DecidableEq D] in
```
Mentions: OAI.HyperbolicObstruction.PictureSwitch.ConeExpansion.Point
lemma OAI.HyperbolicObstruction.PictureSwitch.TriangleMarking.expand_injective line 993
lemma OAI.HyperbolicObstruction.PictureSwitch.TriangleMarking.expand_surjective line 1024
def OAI.HyperbolicObstruction.PictureSwitch.TriangleMarking.expandEquiv line 1037
lemma OAI.HyperbolicObstruction.PictureSwitch.TriangleMarking.expand_face line 1041
lemma OAI.HyperbolicObstruction.PictureSwitch.TriangleMarking.expand_edge line 1056
theorem OAI.HyperbolicObstruction.PictureSwitch.TriangleMarking.contraction_genusZero line 1073
Source documentation
The contraction is a genuine genus-zero map with all old sides retained. No surface classification, drawing, or asserted Euler correction is used.
```
theorem contraction_genusZero (h : M.GenusZero) : H.contraction.GenusZero := by
…
```
abbrev OAI.HyperbolicObstruction.ConeSkeleton.ElementaryLiftSide line 1092
def OAI.HyperbolicObstruction.ConeSkeleton.elementaryTop line 1094
def OAI.HyperbolicObstruction.ConeSkeleton.elementaryRole line 1099
def OAI.HyperbolicObstruction.ConeSkeleton.elementarySideRole line 1104
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryTop_next line 1107
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryRole_frozen line 1111
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryRole_turn line 1118
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryTop_period line 1126
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryRole_rev0 line 1135
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryRole_rev1 line 1140
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryRole_rev2 line 1145
def OAI.HyperbolicObstruction.ConeSkeleton.elementaryRawTarget line 1155
Source documentation
Raw cellular target: coefficients always identify actual lifted elementary cells; the boolean used here only disables unrelated normalization machinery.
```
def elementaryRawTarget := (elementaryLiftedBoundary n w d v hv hcell).target
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.elementaryLiftedBoundary, OAI.HyperbolicObstruction.ConeSkeleton.target
def OAI.HyperbolicObstruction.ConeSkeleton.elementaryMarking line 1160
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryContraction_genusZero line 1195
def OAI.HyperbolicObstruction.ConeSkeleton.elementaryWalkIndex line 1212
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryTop_walk line 1216
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryOld_injective line 1221
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryOffset_frozen line 1226
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementary_old_label line 1233
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementary_incoming line 1274
Source documentation
Incoming radial dart after the old side, using the actual top basepoint.
```
lemma elementary_incoming (s : ElementaryLiftSide n w d v hv hcell)
    (h : elementarySideRole n w d v hv hcell s = 0)
    (g : G) (a : Top n w) (e : MacroGraph.graph.Dart)
    (he : elementaryWalkIndex n w d v hv hcell s = (g,.inl (a,e))) :
    (elementaryLiftedBoundary n w d v hv hcell).sideLabel
      ((elementaryLiftedBoundary n w d v hv hcell).next s) =
      (g * macroPotential n w v a e.snd, (.inr (a,e.snd),false)) := by
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.ElementaryLiftSide, OAI.HyperbolicObstruction.ConeSkeleton.elementarySideRole, OAI.HyperbolicObstruction.ConeSkeleton.Top, OAI.HyperbolicObstruction.ConeSkeleton.elementaryWalkIndex, OAI.HyperbolicObstruction.ConeSkeleton.elementaryLiftedBoundary, OAI.HyperbolicObstruction.ConeSkeleton.macroPotential
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementary_outgoing line 1302
Source documentation
Outgoing radial dart before the old side; its deck coordinate is EXACTLY that of the independent lifted elementary-cell coordinate.
```
lemma elementary_outgoing (s : ElementaryLiftSide n w d v hv hcell)
    (h : elementarySideRole n w d v hv hcell s = 0)
    (g : G) (a : Top n w) (e : MacroGraph.graph.Dart)
    (he : elementaryWalkIndex n w d v hv hcell s = (g,.inl (a,e))) :
    (elementaryLiftedBoundary n w d v hv hcell).sideLabel
      ((elementaryLiftedBoundary n w d v hv hcell).next
        ((elementaryLiftedBoundary n w d v hv hcell).next s)) =
      (g, (.inr (a,e.fst),true)) := by
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.ElementaryLiftSide, OAI.HyperbolicObstruction.ConeSkeleton.elementarySideRole, OAI.HyperbolicObstruction.ConeSkeleton.Top, OAI.HyperbolicObstruction.ConeSkeleton.elementaryWalkIndex, OAI.HyperbolicObstruction.ConeSkeleton.elementaryLiftedBoundary
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryWalkIndex_frozen_injective line 1340
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementary_frozen_next line 1359
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementary_frozen_kind line 1367
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementary_frozen_closed line 1376
abbrev OAI.HyperbolicObstruction.ConeSkeleton.ElementaryBases line 1414
def OAI.HyperbolicObstruction.ConeSkeleton.elementaryContractIndex line 1416
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryContract_top_next line 1419
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryContract_frozen_next line 1469
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryContract_incidence line 1479
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryContract_paired line 1503
def OAI.HyperbolicObstruction.ConeSkeleton.elementaryMacroPicture line 1529
Source documentation
A constructed macro picture, not an extra producer hypothesis. Exact coordinate equality and frozen indexing are proved separately below.
```
def elementaryMacroPicture : WalkPicture (liftedWalkTarget n w d v hv hcell tc hc fc) where
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.liftedWalkTarget
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryMacro_frozenMapped line 1553
def OAI.HyperbolicObstruction.ConeSkeleton.elementaryMacroWeight line 1591
def OAI.HyperbolicObstruction.ConeSkeleton.elementaryMarkPosition line 1595
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementary_selected_weight line 1599
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryMacro_chain line 1630
def OAI.HyperbolicObstruction.ConeSkeleton.elementaryTopWeight line 1666
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryTopWeight_symm line 1669
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryMacroWeight_eq line 1674
theorem OAI.HyperbolicObstruction.ConeSkeleton.uniform_elementary_sphere_chain_zero line 1684
Source documentation
The cutoff precedes all realizations and independent lift coefficients.
```
theorem uniform_elementary_sphere_chain_zero {α β δ : ℝ}
    (ha : 0 < α) (hb : 7*α < β) (hd : 0 < δ) :
    ∃ M : ℕ, 0 < M ∧ ∀ (n : ℕ)
      (w : TableModel.Entry (A := Alphabet n) rowSupport → Bool)
…
```
Mentions: OAI.HyperbolicObstruction.TableModel.Entry
lemma OAI.HyperbolicObstruction.VoltageWords.invRev_singleton line 1717
def OAI.HyperbolicObstruction.VoltageWords.voltage line 1719
def OAI.HyperbolicObstruction.VoltageWords.total line 1721
lemma OAI.HyperbolicObstruction.VoltageWords.voltage_inv line 1723
lemma OAI.HyperbolicObstruction.VoltageWords.total_nil line 1727
lemma OAI.HyperbolicObstruction.VoltageWords.total_cons line 1728
lemma OAI.HyperbolicObstruction.VoltageWords.total_append line 1730
lemma OAI.HyperbolicObstruction.VoltageWords.total_inv line 1733
def OAI.HyperbolicObstruction.VoltageWords.liftLetter line 1742
lemma OAI.HyperbolicObstruction.VoltageWords.liftLetter_inv line 1745
def OAI.HyperbolicObstruction.VoltageWords.liftWord line 1749
lemma OAI.HyperbolicObstruction.VoltageWords.liftWord_nil line 1753
lemma OAI.HyperbolicObstruction.VoltageWords.liftWord_cons line 1754
lemma OAI.HyperbolicObstruction.VoltageWords.liftWord_append line 1757
lemma OAI.HyperbolicObstruction.VoltageWords.liftWord_inv line 1763
lemma OAI.HyperbolicObstruction.VoltageWords.total_step line 1776
lemma OAI.HyperbolicObstruction.VoltageWords.liftWord_step line 1782
def OAI.HyperbolicObstruction.VoltageWords.Relators line 1793
Source documentation
Relators of the actual voltage-cover edge presentation, not a quotient of base-cell coefficients. Every deck coordinate remains an independent index.
```
def Relators (v : A → G) (R : Set (Word A)) : Set (Word (G × A)) :=
…
```
lemma OAI.HyperbolicObstruction.VoltageWords.move_total line 1796
lemma OAI.HyperbolicObstruction.VoltageWords.homotopy_total line 1804
lemma OAI.HyperbolicObstruction.VoltageWords.move_lift line 1813
theorem OAI.HyperbolicObstruction.VoltageWords.homotopy_lift line 1830
Source documentation
An actual area-preserving homotopy lift. Closed relators, free cancellation and both orientations are derived, not assumed as a cover's simple connectivity.
```
theorem homotopy_lift (v : A → G) {R : Set (Word A)}
    (hR : ∀ w ∈ R, total v w = 1) {w z : Word A} {n : ℕ} (h : Homotopy R w z n) (g : G) :
    Homotopy (Relators v R) (liftWord v g w) (liftWord v g z) n := by
…
```
Mentions: OAI.HyperbolicObstruction.VoltageWords.total, OAI.HyperbolicObstruction.VoltageWords.Relators, OAI.HyperbolicObstruction.VoltageWords.liftWord
lemma OAI.HyperbolicObstruction.VoltageWords.liftWord_ofFn line 1844
lemma OAI.HyperbolicObstruction.VoltageWords.liftWord_ofFn' line 1857
def OAI.HyperbolicObstruction.VoltageWords.encode line 1868
Source documentation
Encoding the shifted reversal of a voltage cover as a true signed edge. The negative generator is based at the initial point of its positive reverse.
```
def encode (v : A → G) : G × (A × Bool) ≃ (G × A) × Bool where
…
```
lemma OAI.HyperbolicObstruction.VoltageWords.encode_reverse line 1874
def OAI.HyperbolicObstruction.VoltageWords.liftedStart line 1878
lemma OAI.HyperbolicObstruction.VoltageWords.liftedStart_encode line 1882
def OAI.HyperbolicObstruction.VoltageWords.liftedBoundary line 1891
Source documentation
All individual lifted polygons, expressed in genuine signed lift edges.
```
def liftedBoundary : PolygonTarget.Boundary (G × C) ((G × A) × Bool) (G × V) where
…
```
lemma OAI.HyperbolicObstruction.VoltageWords.lifted_attachingWord line 1907
lemma OAI.HyperbolicObstruction.VoltageWords.lifted_relators line 1913
theorem OAI.HyperbolicObstruction.VoltageWords.lifted_nullWord line 1924
Source documentation
A null word in the base polygon bouquet, lifted from any deck coordinate, is a null word in the actual independently indexed cover presentation.
```
theorem lifted_nullWord (g : G) (w : Word A)
    (hw : PresentedGroup.mk (FreeGroup.mk '' Set.range B.attachingWord) (FreeGroup.mk w) = 1) :
    PresentedGroup.mk (FreeGroup.mk '' Set.range (liftedBoundary B v hinv hc).attachingWord)
      (FreeGroup.mk (liftWord v g w)) = 1 := by
…
```
Mentions: OAI.HyperbolicObstruction.VoltageWords.liftedBoundary, OAI.HyperbolicObstruction.VoltageWords.liftWord
lemma OAI.HyperbolicObstruction.GraphGroupWalk.eval_potential line 1946
lemma OAI.HyperbolicObstruction.ConeSkeleton.macroCell_eq_or_symm line 1958
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementary_radial_relation line 1975
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementary_old_cell line 2002
abbrev OAI.HyperbolicObstruction.ConeSkeleton.ElementaryPolygonGroup line 2021
Source documentation
The literal edge-bouquet presentation of the elementary cells.
```
abbrev ElementaryPolygonGroup := PresentedGroup
…
```
def OAI.HyperbolicObstruction.ConeSkeleton.elementaryPolygonValue line 2024
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryPolygonValue_rev line 2027
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryPolygonValue_word line 2033
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryPolygonValue_cell line 2043
def OAI.HyperbolicObstruction.ConeSkeleton.elementaryFreeComparison line 2062
Source documentation
Inclusion of original letters in the literal elementary edge bouquet.
```
def elementaryFreeComparison : FreeGroup (Fin (n+1)) →* ElementaryPolygonGroup n w d :=
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.ElementaryPolygonGroup
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryFreeComparison_letter line 2066
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryFreeComparison_word line 2073
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryFreeComparison_relator line 2080
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryRelatorClosure_le line 2104
def OAI.HyperbolicObstruction.ConeSkeleton.elementaryComparison line 2112
Source documentation
The original presentation maps to the elementary edge-bouquet group. No fundamental-group equivalence, asphericity, or infinitude is assumed here.
```
def elementaryComparison : LetterPresentation.Group n w d →* ElementaryPolygonGroup n w d :=
…
```
Mentions: OAI.HyperbolicObstruction.LetterPresentation.Group, OAI.HyperbolicObstruction.ConeSkeleton.ElementaryPolygonGroup
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryComparison_letter line 2117
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryComparison_word line 2122
lemma OAI.HyperbolicObstruction.ConeSkeleton.nullWord_to_elementary line 2129
Source documentation
Literal null words in the original generators have elementary-cell disks.
```
lemma nullWord_to_elementary (z : List (Alphabet n))
    (hz : PresentedGroup.mk (Relator n w d) (FreeGroup.mk z) = 1) :
    PresentedGroup.mk (FreeGroup.mk '' Set.range (elementaryBoundary n w d).attachingWord)
      (FreeGroup.mk (z.map (elementaryOld n w ∘ letterDart n w))) = 1 := by
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.elementaryBoundary, OAI.HyperbolicObstruction.ConeSkeleton.elementaryOld, OAI.HyperbolicObstruction.ConeSkeleton.letterDart
abbrev OAI.HyperbolicObstruction.ConeSkeleton.elementaryOldValue line 2145
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryOldValue_rev line 2148
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryOldValue_cell line 2152
lemma OAI.HyperbolicObstruction.ConeSkeleton.base_fanVertex line 2157
def OAI.HyperbolicObstruction.ConeSkeleton.fanBase line 2161
def OAI.HyperbolicObstruction.ConeSkeleton.oldGauge line 2165
Source documentation
The gauge at an old apex is its literal radial edge to the fixed fan base. The bouquet vertex has gauge one.
```
def oldGauge : Vertex n w → ElementaryPolygonGroup n w d
  | .inl _ => 1
  | .inr f => elementaryOldValue n w d (.inr ⟨f,fanBase f.val.1⟩,true)
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.Vertex, OAI.HyperbolicObstruction.ConeSkeleton.ElementaryPolygonGroup, OAI.HyperbolicObstruction.ConeSkeleton.elementaryOldValue, OAI.HyperbolicObstruction.ConeSkeleton.fanBase
lemma OAI.HyperbolicObstruction.ConeSkeleton.radial_gauge line 2169
lemma OAI.HyperbolicObstruction.ConeSkeleton.old_gauge line 2198
Source documentation
Every old edge equals its prescribed letter voltage, up to endpoint gauge. This removes the extra free factors of the edge-bouquet only on CLOSED paths.
```
lemma old_gauge (e : Dart n w) :
    elementaryOldValue n w d e = oldGauge n w d (start n w e) *
      elementaryComparison n w d (letterVoltage n w d e) *
        (oldGauge n w d (start n w (rev n w e)))⁻¹ := by
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.Dart, OAI.HyperbolicObstruction.ConeSkeleton.elementaryOldValue, OAI.HyperbolicObstruction.ConeSkeleton.oldGauge, OAI.HyperbolicObstruction.ConeSkeleton.start, OAI.HyperbolicObstruction.ConeSkeleton.elementaryComparison, OAI.HyperbolicObstruction.ConeSkeleton.letterVoltage, OAI.HyperbolicObstruction.ConeSkeleton.rev
lemma OAI.HyperbolicObstruction.ConeSkeleton.macro_old_gauge line 2219
def OAI.HyperbolicObstruction.ConeSkeleton.elementaryGauge line 2239
Source documentation
The gauge at a top apex is based at the fixed macro root.
```
def elementaryGauge : ElementaryVertex n w → ElementaryPolygonGroup n w d
  | .inl v => oldGauge n w d v
  | .inr a => elementaryPolygonValue n w d (.inr (a,MacroGraph.point 0),true) *
      oldGauge n w d (macroVertex n w a (MacroGraph.point 0))
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.ElementaryVertex, OAI.HyperbolicObstruction.ConeSkeleton.ElementaryPolygonGroup, OAI.HyperbolicObstruction.ConeSkeleton.oldGauge, OAI.HyperbolicObstruction.ConeSkeleton.elementaryPolygonValue, OAI.HyperbolicObstruction.MacroGraph.point, OAI.HyperbolicObstruction.ConeSkeleton.macroVertex
lemma OAI.HyperbolicObstruction.ConeSkeleton.top_radial_gauge line 2244
theorem OAI.HyperbolicObstruction.ConeSkeleton.elementary_gauge line 2260
Source documentation
The full elementary graph has exactly its prescribed voltages modulo endpoint gauges, proved using the literal fan and top cone triangles.
```
theorem elementary_gauge (e : ElementaryDart n w) :
    elementaryPolygonValue n w d e = elementaryGauge n w d (elementaryStart n w e) *
      elementaryComparison n w d (elementaryVoltage n w (letterVoltage n w d) e) *
        (elementaryGauge n w d (elementaryStart n w (elementaryRev n w e)))⁻¹ := by
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.ElementaryDart, OAI.HyperbolicObstruction.ConeSkeleton.elementaryPolygonValue, OAI.HyperbolicObstruction.ConeSkeleton.elementaryGauge, OAI.HyperbolicObstruction.ConeSkeleton.elementaryStart, OAI.HyperbolicObstruction.ConeSkeleton.elementaryComparison, OAI.HyperbolicObstruction.ConeSkeleton.elementaryVoltage, OAI.HyperbolicObstruction.ConeSkeleton.letterVoltage, OAI.HyperbolicObstruction.ConeSkeleton.elementaryRev
lemma OAI.HyperbolicObstruction.prod_gauge_telescope line 2280

lemma OAI.HyperbolicObstruction.prod_gauge_cycle line 2291

Source documentation

Ordered, noncommutative telescope around a cyclic boundary.

lemma prod_gauge_cycle {H : Type*} [Group H] {k : ℕ} (hk : 0 < k)
    (u x : Fin k → H) :
    (List.ofFn (fun i => u i * x i * (u (finRotate k i))⁻¹)).prod =
      u ⟨0,hk⟩ * (List.ofFn x).prod * (u ⟨0,hk⟩)⁻¹ := by
…

theorem OAI.HyperbolicObstruction.ConeSkeleton.elementary_closed_null line 2322
Source documentation
Every closed elementary boundary with trivial original-group voltage is null in the elementary-cell edge-bouquet. Open paths are deliberately excluded: the extra fan/top apex gauges do not vanish on open paths.
```
theorem elementary_closed_null {ell : ℕ} (hell : 0 < ell) (word : Fin ell → ElementaryDart n w)
    (closed : ∀ i, elementaryStart n w (word (finRotate ell i)) =
      elementaryStart n w (elementaryRev n w (word i)))
    (hvol : (List.ofFn (fun i => elementaryVoltage n w (letterVoltage n w d) (word i))).prod = 1) :
    PresentedGroup.mk (FreeGroup.mk '' Set.range (elementaryBoundary n w d).attachingWord)
      (FreeGroup.mk (List.ofFn word)) = 1 := by
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.ElementaryDart, OAI.HyperbolicObstruction.ConeSkeleton.elementaryStart, OAI.HyperbolicObstruction.ConeSkeleton.elementaryRev, OAI.HyperbolicObstruction.ConeSkeleton.elementaryVoltage, OAI.HyperbolicObstruction.ConeSkeleton.letterVoltage, OAI.HyperbolicObstruction.ConeSkeleton.elementaryBoundary
lemma OAI.HyperbolicObstruction.VoltageWords.decode_inverse line 2349

lemma OAI.HyperbolicObstruction.VoltageWords.cycle_deck_prefix line 2357

Source documentation

The deck coordinate at every corner is forced by the literal prefix.

lemma cycle_deck_prefix (v : A → G) {m : ℕ} (hm : 0 < m)
    (w : Fin m → A × Bool) (g : Fin m → G)
    (hg : ∀ i, g (finRotate m i) = g i * voltage v (w i)) (i : Fin m) :
    g i = g ⟨0,hm⟩ * ((List.ofFn (voltage v ∘ w)).take i.val).prod := by
…

Mentions: OAI.HyperbolicObstruction.VoltageWords.voltage

lemma OAI.HyperbolicObstruction.VoltageWords.cycle_voltage line 2385
lemma OAI.HyperbolicObstruction.VoltageWords.closed_decks line 2403
lemma OAI.HyperbolicObstruction.VoltageWords.projected_closed line 2410
lemma OAI.HyperbolicObstruction.VoltageWords.closed_is_lift line 2416
lemma OAI.HyperbolicObstruction.VoltageWords.projected_voltage line 2427
def OAI.HyperbolicObstruction.ConeSkeleton.elementaryPositiveVoltage line 2444
Source documentation
Positive voltages of the genuine elementary indexed edges.
```
def elementaryPositiveVoltage (e : ElementaryEdge n w) : LetterPresentation.Group n w d :=
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.ElementaryEdge, OAI.HyperbolicObstruction.LetterPresentation.Group
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryVoltage_signed line 2447
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryTotal_cell line 2455
def OAI.HyperbolicObstruction.ConeSkeleton.elementaryEncodedBoundary line 2463
Source documentation
Same individual cells and deck coordinates as elementaryLetterLiftedBoundary, encoded using signed positive lifted edges rather than shifted dart reversal.
```
def elementaryEncodedBoundary := VoltageWords.liftedBoundary (elementaryBoundary n w d)
…
```
Mentions: OAI.HyperbolicObstruction.VoltageWords.liftedBoundary, OAI.HyperbolicObstruction.ConeSkeleton.elementaryBoundary
theorem OAI.HyperbolicObstruction.ConeSkeleton.elementary_encoded_null line 2475
Source documentation
Every closed loop in this incidence cover is a null word in its exact lifted polygon presentation. This is not a topological universal-cover assertion.
```
theorem elementary_encoded_null :
    PresentedGroup.mk (FreeGroup.mk '' Set.range (elementaryEncodedBoundary n w d).attachingWord)
      (FreeGroup.mk (List.ofFn word)) = 1 := by
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.elementaryEncodedBoundary

theorem OAI.HyperbolicObstruction.ConeSkeleton.elementary_cover_disk line 2494

Source documentation

Every nonempty closed elementary loop has a genuinely genus-zero labelled disk, carrying all independent lift-cell coordinates, and exactly one exterior. The exterior coefficient is zero; no relator identities are conflated.

theorem elementary_cover_disk :
    ∃ (Q : CellPicture.{0} ((elementaryEncodedBoundary n w d).outsideTarget ell hell word closed
      (fun c => Finsupp.single c (1 : ℤ)) (fun _ => false) (by intro _ h; cases h)))
      (xs : List Q.Dart), IsBoundary Q.pairing.face xs ∧
      xs.map (((elementaryEncodedBoundary n w d).outsideTarget ell hell word closed
        (fun c => Finsupp.single c (1 : ℤ)) (fun _ => false) (by intro _ h; cases h)).edge ∘ Q.index) =
          List.ofFn word ∧
      ∀ x, (elementaryEncodedBoundary n w d).outsideTag ell hell word closed (Q.index x) =
        if x ∈ xs then some true else none := by
…

Mentions: OAI.HyperbolicObstruction.ConeSkeleton.elementaryEncodedBoundary

lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryEncoded_label line 2517
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryEncoded_rev line 2526
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryEncoded_side line 2535
def OAI.HyperbolicObstruction.ConeSkeleton.elementaryDecodePicture line 2554
Source documentation
Decode only the edge alphabet. Every cell, side, face and coefficient is unchanged. The geometric incidence conditions follow from the actual target.
```
def elementaryDecodePicture
    (P : CellPicture ((elementaryEncodedBoundary n w d).target weight
      (fun _ => false) (by intro _ h; cases h))) :
    CellPicture (elementaryRawTarget n w d (letterVoltage n w d)
      (letterVoltage_rev n w d) (letterVoltage_cell n w d) weight) where
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.elementaryEncodedBoundary, OAI.HyperbolicObstruction.ConeSkeleton.target, OAI.HyperbolicObstruction.ConeSkeleton.elementaryRawTarget, OAI.HyperbolicObstruction.ConeSkeleton.letterVoltage, OAI.HyperbolicObstruction.ConeSkeleton.letterVoltage_rev, OAI.HyperbolicObstruction.ConeSkeleton.letterVoltage_cell
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryDecode_chain line 2575
theorem OAI.HyperbolicObstruction.ConeSkeleton.uniform_elementary_indexed_sphere_zero line 2581
Source documentation
Uniform diagram uniqueness for exactly marked disks on the actual cover.
```
theorem uniform_elementary_indexed_sphere_zero {α β δ : ℝ}
    (ha : 0 < α) (hb : 7*α < β) (hd : 0 < δ) :
    ∃ M : ℕ, 0 < M ∧ ∀ (n : ℕ)
      (w : TableModel.Entry (A := Alphabet n) rowSupport → Bool)
…
```
Mentions: OAI.HyperbolicObstruction.TableModel.Entry
theorem OAI.HyperbolicObstruction.ConeSkeleton.elementary_encoded_walk_null line 2609
Source documentation
Every componentwise closed walk, including the empty walk, has an actual literal nullword certificate. No graph-connectedness hypothesis is needed.
```
theorem elementary_encoded_walk_null (x) (u)
    (h : Walk (elementaryEncodedBoundary n w d).start x x u) :
    IndexedFilling.Null (elementaryEncodedBoundary n w d) u := by
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.elementaryEncodedBoundary, OAI.HyperbolicObstruction.ConeSkeleton.start, OAI.HyperbolicObstruction.IndexedFilling.Null
def OAI.HyperbolicObstruction.ConeSkeleton.elementaryPolygons line 2632
abbrev OAI.HyperbolicObstruction.ConeSkeleton.LetterC₂ line 2640
abbrev OAI.HyperbolicObstruction.ConeSkeleton.LetterC₁ line 2641
abbrev OAI.HyperbolicObstruction.ConeSkeleton.LetterC₀ line 2642
def OAI.HyperbolicObstruction.ConeSkeleton.letterBoundary₁ line 2644
def OAI.HyperbolicObstruction.ConeSkeleton.letterBoundary₂ line 2647
theorem OAI.HyperbolicObstruction.ConeSkeleton.letterBoundary_boundary line 2652
Source documentation
Actual lifted elementary incidence, not an augmented base-cell differential. Every cell-voltage equation used here was proved from the original relators.
```
theorem letterBoundary_boundary (z : LetterC₂ n w d) :
    letterBoundary₁ n w d (letterBoundary₂ n w d z) = 0 :=
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.LetterC₂, OAI.HyperbolicObstruction.ConeSkeleton.letterBoundary₁, OAI.HyperbolicObstruction.ConeSkeleton.letterBoundary₂
def OAI.HyperbolicObstruction.ConeSkeleton.LetterCycles₂ line 2659
Source documentation
The exact algebraic cycle space whose sphere producer is needed.
```
def LetterCycles₂ : Submodule ℤ (LetterC₂ n w d) := LinearMap.ker (letterBoundary₂ n w d)
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.LetterC₂, OAI.HyperbolicObstruction.ConeSkeleton.letterBoundary₂
lemma OAI.HyperbolicObstruction.VoltageWords.letterChain_encode line 2671
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryEncoded_cellBoundary line 2682
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryEncoded_boundary line 2696
theorem OAI.HyperbolicObstruction.ConeSkeleton.uniform_elementary_boundary_injective line 2703
Source documentation
No cycle-representation hypothesis remains: the original standing bounded test assumptions imply injectivity of the ACTUAL uncompressed lifted d₂.
```
theorem uniform_elementary_boundary_injective {α β δ : ℝ}
    (ha : 0 < α) (hb : 7*α < β) (hd : 0 < δ) :
    ∃ M : ℕ, 0 < M ∧ ∀ (n : ℕ)
      (w : TableModel.Entry (A := Alphabet n) rowSupport → Bool)
…
```
Mentions: OAI.HyperbolicObstruction.TableModel.Entry
theorem OAI.HyperbolicObstruction.ConeSkeleton.uniform_elementary_cycles_zero line 2719
Source documentation
In particular the full algebraic cellular cycle module is zero. This is not yet an identification with topological universal-cover homology.
```
theorem uniform_elementary_cycles_zero {α β δ : ℝ}
    (ha : 0 < α) (hb : 7*α < β) (hd : 0 < δ) :
    ∃ M : ℕ, 0 < M ∧ ∀ (n : ℕ)
      (w : TableModel.Entry (A := Alphabet n) rowSupport → Bool)
…
```
Mentions: OAI.HyperbolicObstruction.TableModel.Entry
abbrev OAI.HyperbolicObstruction.IncidenceTemplate.finalSize line 2741
abbrev OAI.HyperbolicObstruction.IncidenceTemplate.finalMaster line 2742
abbrev OAI.HyperbolicObstruction.IncidenceTemplate.finalSix line 2743
lemma OAI.HyperbolicObstruction.IncidenceTemplate.finalDiagramStage_elementary_sphere_zero line 2745
lemma OAI.HyperbolicObstruction.IncidenceTemplate.finalDiagramStage_indexed_sphere_zero line 2764
theorem OAI.HyperbolicObstruction.IncidenceTemplate.finalDiagramStage_boundary_injective line 2781
Source documentation
Injectivity of the full d₂ for the selected arrays.
```
theorem finalDiagramStage_boundary_injective (m : ℕ) :
    Function.Injective (letterBoundary₂ (finalSize m) (finalMaster m) (finalSix m)) := by
…
```
Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.finalSize, OAI.HyperbolicObstruction.IncidenceTemplate.finalMaster, OAI.HyperbolicObstruction.IncidenceTemplate.finalSix
lemma OAI.HyperbolicObstruction.IncidenceTemplate.finalDiagramStage_indexed_sphere_zero_weight line 2796
theorem OAI.HyperbolicObstruction.IncidenceTemplate.finalDiagramStage_extend_cochain line 2813
Source documentation
The literal lifted-edge cochain whose coboundary is any prescribed independent lifted-cell cochain. No sphere-map producer is assumed.
```
theorem finalDiagramStage_extend_cochain (m : ℕ) (A : Type) [AddCommGroup A]
    (weight : LetterPresentation.Group (finalSize m) (finalMaster m) (finalSix m) ×
      ElementaryCell (finalSize m) (finalMaster m) (finalSix m) → A) :
    ∀ c, IndexedFilling.leftInverse
      (elementaryEncodedBoundary (finalSize m) (finalMaster m) (finalSix m)) weight
      (IndexedFilling.cellBoundary
        (elementaryEncodedBoundary (finalSize m) (finalMaster m) (finalSix m)) c) = weight c :=
…
```
Mentions: OAI.HyperbolicObstruction.LetterPresentation.Group, OAI.HyperbolicObstruction.IncidenceTemplate.finalSize, OAI.HyperbolicObstruction.IncidenceTemplate.finalMaster, OAI.HyperbolicObstruction.IncidenceTemplate.finalSix, OAI.HyperbolicObstruction.IndexedFilling.leftInverse, OAI.HyperbolicObstruction.IndexedFilling.cellBoundary
def OAI.HyperbolicObstruction.FinitePolyhedron.reindex line 2835
lemma OAI.HyperbolicObstruction.FinitePolyhedron.rename_mem line 2840
lemma OAI.HyperbolicObstruction.FinitePolyhedron.reindexPi_apply line 2859
Source documentation
Coordinate permutation, restricted to the exact two carrier subtypes.
```
lemma reindexPi_apply (e : V ≃ W) (x : V → ℝ) (j : W) :
    Homeomorph.piCongrLeft (Y := fun _ : W => ℝ) e x j = x (e.symm j) := by
…
```
def OAI.HyperbolicObstruction.FinitePolyhedron.reindexHomeomorph line 2863
lemma OAI.HyperbolicObstruction.FinitePolyhedron.reindexHomeomorph_apply line 2871
lemma OAI.HyperbolicObstruction.FinitePolyhedron.reindexHomeomorph_vertex line 2876
def OAI.HyperbolicObstruction.FinitePolyhedron.toFiniteComplex line 2887
Source documentation
The exact finite-complex representation in the release reference.
```
def toFiniteComplex (K : AbstractSimplicialComplex V) : FiniteComplex :=
…
```
Mentions: OAI.HyperbolicObstruction.FiniteComplex
def OAI.HyperbolicObstruction.FinitePolyhedron.toFiniteComplexHomeomorph line 2890
instance OAI.HyperbolicObstruction.FiniteComplex.(instance at line 2897) line 2897
def OAI.HyperbolicObstruction.ConeSkeleton.elementaryPolygonData line 2915
abbrev OAI.HyperbolicObstruction.ConeSkeleton.elementarySimplicialComplex line 2923
abbrev OAI.HyperbolicObstruction.ConeSkeleton.elementaryPolyhedron line 2924
def OAI.HyperbolicObstruction.ConeSkeleton.elementaryBaseVertex line 2926
def OAI.HyperbolicObstruction.ConeSkeleton.elementaryBasepoint line 2929
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementary_old_connected line 2932
instance OAI.HyperbolicObstruction.ConeSkeleton.elementaryPolyhedron_pathConnected line 2946
def OAI.HyperbolicObstruction.ConeSkeleton.elementaryFiniteComplex line 2950
Source documentation
Literal conversion into the finite complex type.
```
def elementaryFiniteComplex : FiniteComplex :=
…
```
Mentions: OAI.HyperbolicObstruction.FiniteComplex
def OAI.HyperbolicObstruction.ConeSkeleton.elementaryFiniteHomeomorph line 2953
def OAI.HyperbolicObstruction.ConeSkeleton.elementaryFiniteBasepoint line 2957
instance OAI.HyperbolicObstruction.ConeSkeleton.elementaryFinite_pathConnected line 2960
lemma OAI.HyperbolicObstruction.group_cycle_transport line 2971
lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.triangle_of_facet line 3014
lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.voltage_on_facet line 3023
lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.graph_edge_first line 3029
lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.graph_edge_middle line 3036
def OAI.HyperbolicObstruction.FinitePolygonModel.Data.graphTransport line 3041
Source documentation
A full signed original edge is exactly its three path segments.
```
def graphTransport (e : E × Bool) : G :=
…
```
lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.graphTransport_reverse line 3047
lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.graphTransport_signed line 3058
def OAI.HyperbolicObstruction.FinitePolygonModel.Data.capTransport line 3066
Source documentation
A cap supplies a literal potential at every actual boundary occurrence.
```
def capTransport (q : P.Position) : G :=
…
```
lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.capTransport_next line 3070
lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.capTransport_side line 3086
lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.graphTransport_cell line 3107
Source documentation
No relation in the original polygon presentation is merely assumed.
```
lemma graphTransport_cell (c : C) :
    (List.ofFn (fun i => P.graphTransport W (P.side c i))).prod = 1 :=
…
```
lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.outer_base_edge line 3122
lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.apex_outer_edge line 3126
abbrev OAI.HyperbolicObstruction.FinitePolygonModel.Data.edgeClass line 3129
def OAI.HyperbolicObstruction.FinitePolygonModel.Data.graphChain line 3133
Source documentation
All three literal subdivisions of an indexed signed graph edge.
```
def graphChain (e : E × Bool) :
    EdgeChain P.complex (P.old (P.start e)) (P.old (P.start (e.1,!e.2))) :=
…
```
lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.graphChain_eval line 3140
abbrev OAI.HyperbolicObstruction.FinitePolygonModel.Data.OldRoutes line 3145
def OAI.HyperbolicObstruction.FinitePolygonModel.Data.graphRoutes line 3149
def OAI.HyperbolicObstruction.FinitePolygonModel.Data.baseRoutes line 3154
def OAI.HyperbolicObstruction.FinitePolygonModel.Data.outerRoutes line 3162
def OAI.HyperbolicObstruction.FinitePolygonModel.Data.firstPosition line 3166

def OAI.HyperbolicObstruction.FinitePolygonModel.Data.routes line 3170

Source documentation

Contracting only the new subdivision/collar tree; no original edge is collapsed by this choice.

def routes : ∀ a : P.Vertex,
    Path.Homotopic.Quotient (vertex P.complex (P.old o)) (vertex P.complex a)
  | .inl a => P.graphRoutes o R a
  | .inr (.inr q) => P.outerRoutes o R q
  | .inr (.inl c) => (P.outerRoutes o R (P.firstPosition c)).trans
      (P.edgeClass (P.apex_outer_edge (P.firstPosition c))).symm

lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.routes_old line 3177
lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.routes_base line 3178
lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.based_eq_one_of_route line 3182
lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.based_eq_one_of_rev_route line 3187
abbrev OAI.HyperbolicObstruction.FinitePolygonModel.Data.rootedVoltage line 3194
lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.rooted_first line 3196
lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.rooted_last line 3203
lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.rooted_outer_base line 3207
lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.rooted_apex_first line 3217
lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.rooted_graphTransport line 3225
lemma OAI.HyperbolicObstruction.FinitePolyhedron.RootedPaths.eq_top_of_edge_mem line 3238
lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.finRotate_noWrap line 3266
lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.position_induction line 3273
lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.rooted_base_next_mem line 3298
lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.rooted_outer_diagonal_mem line 3317
lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.rooted_outer_next_mem line 3327
lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.rooted_apex_mem line 3337
lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.voltage_facet_mem line 3352
lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.rooted_facet_mem line 3362
lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.rooted_group_generated line 3421
Source documentation
Only original graph generators are needed for the actual pi1.
```
lemma rooted_group_generated (hR : R o = .refl _) : H = ⊤ := by
…
```
def OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.detect line 3444
lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.detect_eq_iff line 3454
lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.smul_vertexFiber line 3463
lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.detect_chain line 3470
lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.detect_based_chain line 3477
lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.detect_edgeLoop line 3490
lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.graphTransport_voltage line 3511
lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.rooted_graphChain line 3518
lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.lift_graphTransport line 3523
abbrev OAI.HyperbolicObstruction.FinitePolygonModel.Data.PolygonGroup line 3534
lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.polygonRelation_valid line 3536
def OAI.HyperbolicObstruction.FinitePolygonModel.Data.polygonToTopology line 3543
lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.polygonToTopology_value line 3546
abbrev OAI.HyperbolicObstruction.ConeSkeleton.elementaryRoot line 3570
def OAI.HyperbolicObstruction.ConeSkeleton.elementaryCoreRoutes line 3572
def OAI.HyperbolicObstruction.ConeSkeleton.elementaryOldRoutes line 3582
Source documentation
Only literal radial edges are chosen as old-vertex routes.
```
def elementaryOldRoutes : (elementaryPolygonData n w d).OldRoutes (elementaryRoot n w)
  | .inl v => elementaryCoreRoutes n w d v
  | .inr a => (elementaryCoreRoutes n w d (macroVertex n w a (MacroGraph.point 0))).trans
      ((elementaryPolygonData n w d).graphChain (.inr (a,MacroGraph.point 0),true)).pathClass.symm
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.elementaryPolygonData, OAI.HyperbolicObstruction.ConeSkeleton.elementaryRoot, OAI.HyperbolicObstruction.ConeSkeleton.elementaryCoreRoutes, OAI.HyperbolicObstruction.ConeSkeleton.macroVertex, OAI.HyperbolicObstruction.MacroGraph.point
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryOldRoutes_root line 3587
abbrev OAI.HyperbolicObstruction.ConeSkeleton.ElementaryPiOne line 3590
abbrev OAI.HyperbolicObstruction.ConeSkeleton.elementaryRootedVoltage line 3592
def OAI.HyperbolicObstruction.ConeSkeleton.elementaryPolygonToTopology line 3595
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryPolygonToTopology_value line 3598
def OAI.HyperbolicObstruction.ConeSkeleton.elementaryLetterToTopology line 3603
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryLetterToTopology_letter line 3606
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementary_oldGauge_toTopology line 3613
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementary_gauge_toTopology line 3623
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryLetterToTopology_surjective line 3637
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementarySignedVoltage line 3664
def OAI.HyperbolicObstruction.ConeSkeleton.elementarySourceVoltage line 3673
def OAI.HyperbolicObstruction.ConeSkeleton.elementaryTopologyToLetter line 3679
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryLetterToTopology_loop line 3682
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryTopologyToLetter_letter line 3689
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryTopology_leftInverse line 3703
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryLetterToTopology_injective line 3709
def OAI.HyperbolicObstruction.ConeSkeleton.elementaryTopologyEquiv line 3717
Source documentation
The actual letter group equals the actual topological pi1-op of the finite literal elementary polygon realization.
```
def elementaryTopologyEquiv : LetterPresentation.Group n w d ≃* ElementaryPiOne n w d :=
…
```
Mentions: OAI.HyperbolicObstruction.LetterPresentation.Group, OAI.HyperbolicObstruction.ConeSkeleton.ElementaryPiOne
lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.map_edgeChain line 3729
def OAI.HyperbolicObstruction.IncidenceTemplate.finalTrianglePolygonWeight line 3745
def OAI.HyperbolicObstruction.IncidenceTemplate.finalTriangleEdgeWeight line 3749
lemma OAI.HyperbolicObstruction.IncidenceTemplate.finalTriangleEdgeWeight_equation line 3753
lemma OAI.HyperbolicObstruction.simplyConnected_of_fundamentalGroup_subsingleton line 3781
lemma OAI.HyperbolicObstruction.Covering.pathConnected_of_monodromy_surjective line 3800
lemma OAI.HyperbolicObstruction.Covering.fundamentalGroup_subsingleton_of_monodromy_injective line 3815
lemma OAI.HyperbolicObstruction.Covering.simplyConnected_of_monodromy_bijective line 3823
lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.monodromy_bijective_of_detect line 3842
lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.simplyConnected_of_detect line 3857
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryTopologyToLetter_bijective line 3879
instance OAI.HyperbolicObstruction.ConeSkeleton.elementarySourceUniversalCover_simplyConnected line 3891
instance OAI.HyperbolicObstruction.HigherCovering.cube_contractible line 3914

def OAI.HyperbolicObstruction.HigherCovering.facePath line 3919

Source documentation

A path in a single face of the cube boundary.

def facePath [DecidableEq N] (x y : Cube.boundary N) (i : N) (a : I)
    (ha : a = 0 ∨ a = 1) (hx : x.val i = a) (hy : y.val i = a) : Path x y where
…

instance OAI.HyperbolicObstruction.HigherCovering.boundary_pathConnected line 3943
def OAI.HyperbolicObstruction.HigherCovering.loopMap line 3958
Source documentation
Postcomposition of actual cube-relative loops.
```
def loopMap (f : C(E,X)) {e : E} (a : GenLoop N E e) : GenLoop N X (f e) :=
…
```
lemma OAI.HyperbolicObstruction.HigherCovering.loopMap_homotopic line 3961
def OAI.HyperbolicObstruction.HigherCovering.homotopyMap line 3966
Source documentation
The actual induced map on the cube-relative homotopy quotient.
```
def homotopyMap (N : Type*) (f : C(E,X)) (e : E) :
    HomotopyGroup N E e → HomotopyGroup N X (f e) :=
…
```
lemma OAI.HyperbolicObstruction.HigherCovering.homotopyMap_injective line 3972
lemma OAI.HyperbolicObstruction.HigherCovering.loopMap_surjective line 3983
lemma OAI.HyperbolicObstruction.HigherCovering.homotopyMap_surjective line 4002
def OAI.HyperbolicObstruction.HigherCovering.homotopyEquiv line 4011
Source documentation
Coverings preserve the genuine higher homotopy sets/groups.
```
def homotopyEquiv [DecidableEq N] [Nontrivial N] :
    HomotopyGroup N E e ≃ HomotopyGroup N X (p e) :=
…
```
lemma OAI.HyperbolicObstruction.HigherCovering.subsingleton_higher_iff line 4017
abbrev OAI.HyperbolicObstruction.ConeSkeleton.elementaryUniversalBasepoint line 4039
def OAI.HyperbolicObstruction.ConeSkeleton.elementaryHigherCoverEquiv line 4044
Source documentation
This is the literal cover already proved simply connected, not an abstract cover named in a premise.
```
def elementaryHigherCoverEquiv (k : ℕ) :
    HomotopyGroup.Pi (k+2) (elementarySourceVoltage n w d).TotalSpace
      (elementaryUniversalBasepoint n w d) ≃
    HomotopyGroup.Pi (k+2) (elementaryFiniteComplex n w d).Carrier
      (elementaryFiniteBasepoint n w d) :=
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.elementarySourceVoltage, OAI.HyperbolicObstruction.ConeSkeleton.elementaryUniversalBasepoint, OAI.HyperbolicObstruction.ConeSkeleton.elementaryFiniteComplex, OAI.HyperbolicObstruction.ConeSkeleton.elementaryFiniteBasepoint
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryAspherical_iff line 4053
def OAI.HyperbolicObstruction.BasedHigherContraction.nullhomotopy line 4073
lemma OAI.HyperbolicObstruction.BasedHigherContraction.subsingleton line 4085
lemma OAI.HyperbolicObstruction.FiniteComplex.DiskHomotopy.contextual line 4104
lemma OAI.HyperbolicObstruction.FiniteComplex.DiskHomotopy.append_both line 4118
lemma OAI.HyperbolicObstruction.FiniteComplex.DiskHomotopy.reverse line 4125
abbrev OAI.HyperbolicObstruction.FiniteComplex.Chain line 4145
def OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.nodes line 4150
def OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.starts line 4154
def OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.steps line 4158
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.nodes_eq_starts line 4162
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.nodes_eq_steps line 4167
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.nodes_append line 4172
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.nodes_append' line 4178
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.append_nil line 4183
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.append_assoc line 4188
def OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.single line 4194
def OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.reverse line 4196
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.nodes_reverse line 4200
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.nodes_injective line 4207
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.reverse_reverse line 4238
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.reverse_append line 4242
abbrev OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.Homotopy line 4252
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.Homotopy.refl line 4255
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.Homotopy.symm line 4256
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.Homotopy.trans line 4257
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.Homotopy.trans_zero line 4259
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.Homotopy.zero_trans line 4261
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.Homotopy.append_right line 4263
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.Homotopy.append_left line 4267
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.Homotopy.reverse line 4271
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.cancel line 4276
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.cancel_left line 4289
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.single_self line 4301
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.triangle line 4306
def OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.based line 4324
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.based_nil line 4327
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.based_append line 4329
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.based_reverse line 4334
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.based_homotopy line 4338
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.based_route line 4342
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.unbase line 4346
abbrev OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.Generator line 4379
def OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.freeEval line 4381
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.freeEval_nil line 4387
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.freeEval_cons line 4389
inductive OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.Relation line 4394
abbrev OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.PresentationGroup line 4401
def OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.gen line 4404
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.gen_self line 4408
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.gen_triangle line 4412
def OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.voltage line 4422
Source documentation
The canonical cocycle of the finite edge presentation.
```
def voltage : Voltage K (PresentationGroup K o R) where
…
```
Mentions: OAI.HyperbolicObstruction.FinitePolyhedron.Voltage, OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.PresentationGroup
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.voltage_value line 4433
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.eval_eq_mk line 4437
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.eval_route line 4444
abbrev OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.routeClasses line 4448
abbrev OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.topGenerator line 4449
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.lift_freeEval line 4452
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.relation_valid line 4463
def OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.toTopology line 4479
Source documentation
The presented edge group maps into the actual topological pi1.
```
def toTopology (hR : R o = .nil o) : PresentationGroup K o R →* RootedPaths.PiOne (K := K) o :=
…
```
Mentions: OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.PresentationGroup, OAI.HyperbolicObstruction.FinitePolyhedron.RootedPaths.PiOne
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.toTopology_gen line 4482
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.toTopology_mk line 4486
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.toTopology_chain line 4490
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.toTopology_injective line 4494
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.toTopology_surjective line 4507
def OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.equivFundamentalGroup line 4519
Source documentation
A genuine isomorphism to the actual topological fundamental group.
```
def equivFundamentalGroup (hR : R o = .nil o) :
    PresentationGroup K o R ≃* RootedPaths.PiOne (K := K) o :=
…
```
Mentions: OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.PresentationGroup, OAI.HyperbolicObstruction.FinitePolyhedron.RootedPaths.PiOne
def OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.canonicalEquiv line 4525
Source documentation
No route-existence hypothesis is needed for a connected realization.
```
def canonicalEquiv [PathConnectedSpace (Carrier K)] :
    PresentationGroup K o (edgeRoutes K o) ≃* RootedPaths.PiOne (K := K) o :=
…
```
Mentions: OAI.HyperbolicObstruction.FinitePolyhedron.Carrier, OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.PresentationGroup, OAI.HyperbolicObstruction.FinitePolyhedron.edgeRoutes, OAI.HyperbolicObstruction.FinitePolyhedron.RootedPaths.PiOne
def OAI.HyperbolicObstruction.WordPictures.signedWords line 4538
lemma OAI.HyperbolicObstruction.WordPictures.signedWords_rev line 4541
lemma OAI.HyperbolicObstruction.WordPictures.signedWords_eval line 4546
lemma OAI.HyperbolicObstruction.WordPictures.flatMap_eval line 4555
lemma OAI.HyperbolicObstruction.WordPictures.exists_word line 4564
lemma OAI.HyperbolicObstruction.WordPictures.Homotopy.append_both line 4573
lemma OAI.HyperbolicObstruction.WordPictures.Homotopy.of_null_difference line 4580
lemma OAI.HyperbolicObstruction.WordPictures.Homotopy.compare_flatMap line 4589
Source documentation
A finite per-letter change of boundary words accumulates only linearly.
```
lemma compare_flatMap {B : Type*} (f : B × Bool → Word A) (g : B × Bool → Word A)
    (D : ℕ) (h : ∀ b, ∃ k ≤ D, Homotopy R (f b) (g b) k) (z : Word B) :
    ∃ k ≤ D*z.length, Homotopy R (z.flatMap f) (z.flatMap g) k := by
…
```
Mentions: OAI.HyperbolicObstruction.WordPictures.Word, OAI.HyperbolicObstruction.WordPictures.Homotopy
lemma OAI.HyperbolicObstruction.WordPictures.flatMap_length_le line 4602

lemma OAI.HyperbolicObstruction.WordPictures.linear_of_substitutions line 4613

Source documentation

Main quantitative substitution calculation. Both comparison disks and old-relator disks are supplied as explicit literal Homotopy certificates.

lemma linear_of_substitutions {R : Set (Word A)} {S : Set (Word B)}
    (p : FreeGroup A →* G) (q : FreeGroup B →* G)
    (c : B × Bool → Word A) (d : A × Bool → Word B)
    (hd : ∀ a, d (a.1,!a.2) = FreeGroup.invRev (d a))
    (hc : ∀ b, p (FreeGroup.mk (c b)) = q (FreeGroup.mk [b]))
    (M D L : ℕ) (C : ℝ) (hC : 0 ≤ C)
    (hlength : ∀ b, (c b).length ≤ L)
    (hR : ∀ z ∈ R, ∃ a ≤ M, Homotopy S (z.flatMap d) [] a)
    (hcomp : ∀ b, ∃ a ≤ D, Homotopy S [b] ((c b).flatMap d) a)
    (hfill : ∀ z : Word A, p (FreeGroup.mk z) = 1 →
      ∃ a, Homotopy R z [] a ∧ (a : ℝ) ≤ C*z.length) :
    ∀ z : Word B, q (FreeGroup.mk z) = 1 →
…

Mentions: OAI.HyperbolicObstruction.WordPictures.Word, OAI.HyperbolicObstruction.WordPictures.Homotopy

lemma OAI.HyperbolicObstruction.WordPictures.finitely_bounded line 4648

theorem OAI.HyperbolicObstruction.WordPictures.finite_change line 4653

Source documentation

The target completeness premise is only the unquantified normal-closure criterion, proved independently for every presentation used below.

theorem finite_change [Finite B] {R : Set (Word A)} {S : Set (Word B)}
    (p : FreeGroup A →* G) (hp : Function.Surjective p)
    (q : FreeGroup B →* G) (hq : Function.Surjective q)
    (finR : R.Finite) (validR : ∀ z ∈ R, p (FreeGroup.mk z) = 1)
    (completeS : ∀ z : Word B, q (FreeGroup.mk z) = 1 → ∃ k, Homotopy S z [] k)
    (C : ℝ) (hC : 0 ≤ C)
    (fillR : ∀ z : Word A, p (FreeGroup.mk z) = 1 →
      ∃ k, Homotopy R z [] k ∧ (k : ℝ) ≤ C*z.length) :
    ∃ D : ℝ, 0 ≤ D ∧ ∀ z : Word B, q (FreeGroup.mk z) = 1 →
      ∃ k, Homotopy S z [] k ∧ (k : ℝ) ≤ D*z.length := by
…

Mentions: OAI.HyperbolicObstruction.WordPictures.Word, OAI.HyperbolicObstruction.WordPictures.Homotopy

def OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.chainWord line 4705
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.mk_chainWord line 4710
inductive OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.WordRelation line 4719
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.relation_image line 4727
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.wordRelation_finite line 4741
def OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.wordToTopology line 4759
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.wordToTopology_surjective line 4762
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgePresentation.word_to_disk line 4765
abbrev OAI.HyperbolicObstruction.FiniteComplex.EdgeGenerator line 4783
def OAI.HyperbolicObstruction.FiniteComplex.generatorChain line 4785
def OAI.HyperbolicObstruction.FiniteComplex.signedChain line 4786
def OAI.HyperbolicObstruction.FiniteComplex.wordChain line 4789
lemma OAI.HyperbolicObstruction.FiniteComplex.wordChain_append line 4793
lemma OAI.HyperbolicObstruction.FiniteComplex.signedChain_reverse line 4799
lemma OAI.HyperbolicObstruction.FiniteComplex.wordChain_reverse line 4804
lemma OAI.HyperbolicObstruction.FiniteComplex.wordChain_context line 4814
lemma OAI.HyperbolicObstruction.FiniteComplex.wordChain_free line 4821
lemma OAI.HyperbolicObstruction.FiniteComplex.wordChain_homotopy line 4831
lemma OAI.HyperbolicObstruction.FiniteComplex.wordChain_chainWord line 4854
lemma OAI.HyperbolicObstruction.FiniteComplex.wordChain_relator line 4861
lemma OAI.HyperbolicObstruction.FiniteComplex.word_disk_realization line 4879
Source documentation
A literal word disk in the intrinsic triangular presentation becomes an actual disk of no more triangular faces; route cancellations have zero area.
```
lemma word_disk_realization (hR : R o = .nil o)
    {z : WordPictures.Word K.EdgeGenerator} {a : ℕ}
    (h : WordPictures.Homotopy (EdgePresentation.WordRelation K.complex o R) z [] a) :
    ∃ k ≤ a, (wordChain K o R z).Homotopy (.nil o) k := by
…
```
Mentions: OAI.HyperbolicObstruction.WordPictures.Word, OAI.HyperbolicObstruction.WordPictures.Homotopy, OAI.HyperbolicObstruction.FiniteComplex.wordChain
def OAI.HyperbolicObstruction.FiniteComplex.pathValue line 4892
lemma OAI.HyperbolicObstruction.FiniteComplex.pathValue_prefix line 4897
lemma OAI.HyperbolicObstruction.FiniteComplex.diskMove_sound line 4907
lemma OAI.HyperbolicObstruction.FiniteComplex.diskHomotopy_sound line 4924
lemma OAI.HyperbolicObstruction.FiniteComplex.chain_pathValue line 4932
def OAI.HyperbolicObstruction.GeometricAction.pullback line 4950
lemma OAI.HyperbolicObstruction.NoGeometricCATZeroAction.of_mulEquiv line 4963
def OAI.HyperbolicObstruction.groupOppositeEquiv line 4975
Source documentation
Inversion identifies a group with the opposite group without any commutativity assumption.
```
def groupOppositeEquiv (G : Type v) [Group G] : Gᵐᵒᵖ ≃* G where
…
```
def OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.ofListEnd line 4994
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.nodes_ofListEnd line 5000
lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.chainWord_length line 5007
lemma OAI.HyperbolicObstruction.FiniteComplex.disk_word_null line 5021

theorem OAI.HyperbolicObstruction.FiniteComplex.linearDiskFilling_of_intrinsic line 5032

Source documentation

Intrinsic word area gives literal triangular disk area with no loss.

theorem linearDiskFilling_of_intrinsic (C : ℝ) (_ : 0 ≤ C)
    (fill : ∀ z : WordPictures.Word K.EdgeGenerator,
      EdgePresentation.wordToTopology K.complex o R hR (FreeGroup.mk z) = 1 →
      ∃ k, WordPictures.Homotopy (EdgePresentation.WordRelation K.complex o R) z [] k ∧
        (k : ℝ) ≤ C*z.length) : K.LinearDiskFilling C := by
…

Mentions: OAI.HyperbolicObstruction.WordPictures.Word, OAI.HyperbolicObstruction.WordPictures.Homotopy

theorem OAI.HyperbolicObstruction.FiniteComplex.linearDiskFilling_of_presentation line 5059
Source documentation
Quantitative finite-presentation change, followed by literal geometric realization, produces the exact main's triangular filling assertion.
```
theorem linearDiskFilling_of_presentation {A G : Type*} [Group G]
    (S : Set (WordPictures.Word A)) (p : FreeGroup A →* G) (hp : Function.Surjective p)
    (e : G ≃* RootedPaths.PiOne (K := K.complex) o)
…
```
Mentions: OAI.HyperbolicObstruction.WordPictures.Word
lemma OAI.HyperbolicObstruction.FiniteComplex.nonempty_vertex line 5078

theorem OAI.HyperbolicObstruction.FiniteComplex.linearDiskFilling_of_piOne line 5085

Source documentation

Basepoint-independent form of the faithful finite-presentation transfer.

theorem linearDiskFilling_of_piOne [PathConnectedSpace K.Carrier]
    {A G : Type*} [Group G] (x : K.Carrier)
    (S : Set (WordPictures.Word A)) (p : FreeGroup A →* G) (hp : Function.Surjective p)
    (e : G ≃* FundamentalGroup K.Carrier x)
    (finS : S.Finite) (validS : ∀ z ∈ S, p (FreeGroup.mk z) = 1)
    (C : ℝ) (hC : 0 ≤ C)
    (fill : ∀ z : WordPictures.Word A, p (FreeGroup.mk z) = 1 →
      ∃ k, WordPictures.Homotopy S z [] k ∧ (k : ℝ) ≤ C*z.length) :
    ∃ D : ℝ, 0 ≤ D ∧ K.LinearDiskFilling D := by
…

Mentions: OAI.HyperbolicObstruction.WordPictures.Word, OAI.HyperbolicObstruction.WordPictures.Homotopy

def OAI.HyperbolicObstruction.fundamentalGroupHomotopyEquiv line 5110
def OAI.HyperbolicObstruction.ConeSkeleton.elementaryFinitePiOneEquiv line 5132
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryFinite_noAction line 5138
abbrev OAI.HyperbolicObstruction.ConeSkeleton.SixChain line 5154
abbrev OAI.HyperbolicObstruction.ConeSkeleton.OriginalEdgeChain line 5155
def OAI.HyperbolicObstruction.ConeSkeleton.sixCellIndex line 5157
def OAI.HyperbolicObstruction.ConeSkeleton.originalEdgeIndex line 5161
lemma OAI.HyperbolicObstruction.ConeSkeleton.sixCellIndex_injective line 5165
lemma OAI.HyperbolicObstruction.ConeSkeleton.originalEdgeIndex_injective line 5171
def OAI.HyperbolicObstruction.ConeSkeleton.sixFaceBoundary line 5177
def OAI.HyperbolicObstruction.ConeSkeleton.sixBoundary line 5183
lemma OAI.HyperbolicObstruction.ConeSkeleton.originalEdgeChain_map line 5186
lemma OAI.HyperbolicObstruction.ConeSkeleton.sixFaceBoundary_map line 5195
lemma OAI.HyperbolicObstruction.ConeSkeleton.sixBoundary_map line 5206
lemma OAI.HyperbolicObstruction.ConeSkeleton.sixBoundary_injective line 5219
lemma OAI.HyperbolicObstruction.ConeSkeleton.six_card_le_of_finite line 5228
theorem OAI.HyperbolicObstruction.ConeSkeleton.infinite_of_boundary_and_six line 5236
Source documentation
An exact algebraic infinitude criterion for the actual presentation.
```
theorem infinite_of_boundary_and_six (h : Function.Injective (letterBoundary₂ n w d))
    (hs : n+1 < Fintype.card (Six n d)) : Infinite (LetterPresentation.Group n w d) := by
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.letterBoundary₂, OAI.HyperbolicObstruction.ConeSkeleton.Six, OAI.HyperbolicObstruction.LetterPresentation.Group
lemma OAI.HyperbolicObstruction.SixTable.included_pair_of_good line 5250
lemma OAI.HyperbolicObstruction.SixTable.card_included_at_least_pairs line 5272
lemma OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage.many_six line 5286
instance OAI.HyperbolicObstruction.IncidenceTemplate.finalDiagramStage_infinite line 5307
Source documentation
Infinitude via the independent six-cell rank obstruction, with all finite-table/cardinality and d₂ hypotheses discharged.
```
instance finalDiagramStage_infinite (m : ℕ) :
    Infinite (SamplingStage.LetterGroup finalDiagramStage m) :=
…
```
Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage.LetterGroup, OAI.HyperbolicObstruction.IncidenceTemplate.finalDiagramStage
theorem OAI.HyperbolicObstruction.IncidenceTemplate.finalDiagramStage_noAction line 5314
Source documentation
The no-action conclusion for the selected original groups, without an infinitude assumption.
```
theorem finalDiagramStage_noAction :
    ∀ᶠ m in Filter.atTop, NoGeometricCATZeroAction (SamplingStage.LetterGroup finalDiagramStage m) :=
…
```
Mentions: OAI.HyperbolicObstruction.NoGeometricCATZeroAction, OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage.LetterGroup, OAI.HyperbolicObstruction.IncidenceTemplate.finalDiagramStage
theorem OAI.HyperbolicObstruction.IncidenceTemplate.exists_infinite_linear_noAction line 5320
Source documentation
A single finite letter presentation, infinite with linear nullword filling and no geometric action on any proper complete CAT(0) space.
```
theorem exists_infinite_linear_noAction : ∃ m : ℕ,
    Infinite (SamplingStage.LetterGroup finalDiagramStage m) ∧
    NoGeometricCATZeroAction (SamplingStage.LetterGroup finalDiagramStage m) ∧
    ∃ C : ℝ, 0 < C ∧ ∀ word : List (Alphabet (finalSize m)),
      PresentedGroup.mk (Relator (finalSize m) (finalMaster m) (finalSix m)) (FreeGroup.mk word) = 1 →
      ∃ a, WordPictures.Homotopy (SimpleWordRelator (finalSize m) (finalMaster m) (finalSix m))
        word [] a ∧ (a : ℝ) ≤ C * word.length := by
…
```
Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage.LetterGroup, OAI.HyperbolicObstruction.IncidenceTemplate.finalDiagramStage, OAI.HyperbolicObstruction.NoGeometricCATZeroAction, OAI.HyperbolicObstruction.IncidenceTemplate.finalSize, OAI.HyperbolicObstruction.IncidenceTemplate.finalMaster, OAI.HyperbolicObstruction.IncidenceTemplate.finalSix, OAI.HyperbolicObstruction.WordPictures.Homotopy
def OAI.HyperbolicObstruction.IncidenceTemplate.finalFiniteComplex line 5335
def OAI.HyperbolicObstruction.IncidenceTemplate.finalFiniteBasepoint line 5338
instance OAI.HyperbolicObstruction.IncidenceTemplate.finalFinite_pathConnected line 5341
def OAI.HyperbolicObstruction.IncidenceTemplate.finalFinitePiOneEquiv line 5344
instance OAI.HyperbolicObstruction.IncidenceTemplate.finalFinite_infinite line 5348
theorem OAI.HyperbolicObstruction.IncidenceTemplate.finalFinite_noAction line 5352
theorem OAI.HyperbolicObstruction.IncidenceTemplate.exists_finite_infinite_noAction line 5359
Source documentation
A finite topological model whose fundamental group admits no geometric CAT(0) action, without asphericity or metric conclusions.
```
theorem exists_finite_infinite_noAction : ∃ K : FiniteComplex, ∃ x : K.Carrier,
    ConnectedSpace K.Carrier ∧ Infinite (FundamentalGroup K.Carrier x) ∧
      NoGeometricCATZeroAction.{u} (FundamentalGroup K.Carrier x) := by
…
```
Mentions: OAI.HyperbolicObstruction.FiniteComplex
lemma OAI.HyperbolicObstruction.IncidenceTemplate.finalFinite_linear line 5374
theorem OAI.HyperbolicObstruction.IncidenceTemplate.exists_finite_linear_noAction line 5390
Source documentation
A connected finite model with infinite fundamental group, linear disk filling, and no geometric CAT(0) action of its fundamental group.
```
theorem exists_finite_linear_noAction : ∃ K : FiniteComplex, ∃ x : K.Carrier, ∃ C : ℝ,
    ConnectedSpace K.Carrier ∧ Infinite (FundamentalGroup K.Carrier x) ∧
      0 ≤ C ∧ K.LinearDiskFilling C ∧
      NoGeometricCATZeroAction.{u} (FundamentalGroup K.Carrier x) := by
…
```
Mentions: OAI.HyperbolicObstruction.FiniteComplex
lemma OAI.HyperbolicObstruction.IncidenceTemplate.finalCover_higher line 5414
lemma OAI.HyperbolicObstruction.IncidenceTemplate.finalFinite_aspherical line 5439

theorem OAI.HyperbolicObstruction.IncidenceTemplate.exists_finite_aspherical_linear_noAction line 5445

Source documentation

The entire finite aspherical linear-filling no-action construction, on one model. The two metric consequences remain distinct obligations of main.

theorem exists_finite_aspherical_linear_noAction :
    ∃ K : FiniteComplex, ∃ x : K.Carrier, ∃ C : ℝ,
    ConnectedSpace K.Carrier ∧ K.Aspherical x ∧ Infinite (FundamentalGroup K.Carrier x) ∧
      0 ≤ C ∧ K.LinearDiskFilling C ∧
      NoGeometricCATZeroAction.{u} (FundamentalGroup K.Carrier x) := by
…

Mentions: OAI.HyperbolicObstruction.FiniteComplex

def OAI.HyperbolicObstruction.WordLength.Good line 5465
lemma OAI.HyperbolicObstruction.WordLength.good_nil line 5467
lemma OAI.HyperbolicObstruction.WordLength.good_append line 5468
lemma OAI.HyperbolicObstruction.WordLength.good_inverse line 5473
lemma OAI.HyperbolicObstruction.WordLength.exists_word line 5478
lemma OAI.HyperbolicObstruction.WordLength.le_length line 5492
lemma OAI.HyperbolicObstruction.WordLength.attained line 5496
lemma OAI.HyperbolicObstruction.WordLength.one line 5503
lemma OAI.HyperbolicObstruction.WordLength.eq_zero_iff line 5507
lemma OAI.HyperbolicObstruction.WordLength.mul_le line 5514
lemma OAI.HyperbolicObstruction.WordLength.inv_le line 5521
lemma OAI.HyperbolicObstruction.WordLength.inv line 5527
lemma OAI.HyperbolicObstruction.WordDistance.nonneg line 5534
lemma OAI.HyperbolicObstruction.WordDistance.self line 5535
lemma OAI.HyperbolicObstruction.WordDistance.comm line 5537
lemma OAI.HyperbolicObstruction.WordDistance.eq_zero_iff line 5540
lemma OAI.HyperbolicObstruction.WordDistance.triangle line 5542
lemma OAI.HyperbolicObstruction.WordDistance.left line 5548
def OAI.HyperbolicObstruction.WordDistance.metric line 5552
Source documentation
The canonical word metric agrees with WordDistance.
```
@[instance_reducible] def metric : MetricSpace G where
…
```
def OAI.HyperbolicObstruction.WordPictures.Cochain.value line 5570
def OAI.HyperbolicObstruction.WordPictures.Cochain.letter line 5571
def OAI.HyperbolicObstruction.WordPictures.Cochain.integral line 5572
lemma OAI.HyperbolicObstruction.WordPictures.Cochain.value_nil line 5576
lemma OAI.HyperbolicObstruction.WordPictures.Cochain.value_append line 5577
lemma OAI.HyperbolicObstruction.WordPictures.Cochain.value_cons line 5579
lemma OAI.HyperbolicObstruction.WordPictures.Cochain.value_reverse line 5581
lemma OAI.HyperbolicObstruction.WordPictures.Cochain.letter_flip line 5583
lemma OAI.HyperbolicObstruction.WordPictures.Cochain.integral_nil line 5586
lemma OAI.HyperbolicObstruction.WordPictures.Cochain.integral_cons line 5587
lemma OAI.HyperbolicObstruction.WordPictures.Cochain.integral_append line 5589
lemma OAI.HyperbolicObstruction.WordPictures.Cochain.integral_reverse line 5597
lemma OAI.HyperbolicObstruction.WordPictures.Cochain.integral_reduction line 5610
lemma OAI.HyperbolicObstruction.WordPictures.Cochain.move_bound line 5620
lemma OAI.HyperbolicObstruction.WordPictures.Cochain.homotopy_bound line 5640
structure OAI.HyperbolicObstruction.VertexPath line 5661
def OAI.HyperbolicObstruction.VertexPath.start line 5666
def OAI.HyperbolicObstruction.VertexPath.finish line 5667
def OAI.HyperbolicObstruction.VertexPath.integral line 5668
def OAI.HyperbolicObstruction.VertexPath.reverse line 5670
def OAI.HyperbolicObstruction.VertexPath.sub line 5671
def OAI.HyperbolicObstruction.VertexPath.append line 5672
lemma OAI.HyperbolicObstruction.VertexPath.reverse_length line 5674
lemma OAI.HyperbolicObstruction.VertexPath.reverse_at line 5675
lemma OAI.HyperbolicObstruction.VertexPath.reverse_start line 5676
lemma OAI.HyperbolicObstruction.VertexPath.reverse_finish line 5677
lemma OAI.HyperbolicObstruction.VertexPath.sub_length line 5678
lemma OAI.HyperbolicObstruction.VertexPath.sub_at line 5679
lemma OAI.HyperbolicObstruction.VertexPath.sub_start line 5680
lemma OAI.HyperbolicObstruction.VertexPath.sub_finish line 5681
lemma OAI.HyperbolicObstruction.VertexPath.append_length line 5683
lemma OAI.HyperbolicObstruction.VertexPath.append_at_left line 5684
lemma OAI.HyperbolicObstruction.VertexPath.append_at_right line 5686
lemma OAI.HyperbolicObstruction.VertexPath.append_start line 5691
lemma OAI.HyperbolicObstruction.VertexPath.append_finish line 5693
lemma OAI.HyperbolicObstruction.VertexPath.integral_append line 5695
lemma OAI.HyperbolicObstruction.VertexPath.integral_reverse line 5708
def OAI.HyperbolicObstruction.VertexPath.Unit line 5721
def OAI.HyperbolicObstruction.VertexPath.Quasi line 5722
def OAI.HyperbolicObstruction.VertexPath.Geodesic line 5724
lemma OAI.HyperbolicObstruction.VertexPath.unit_sub line 5726
lemma OAI.HyperbolicObstruction.VertexPath.unit_reverse line 5732
lemma OAI.HyperbolicObstruction.VertexPath.unit_append line 5737
lemma OAI.HyperbolicObstruction.VertexPath.dist_le line 5747
lemma OAI.HyperbolicObstruction.VertexPath.dist_le_abs line 5760
lemma OAI.HyperbolicObstruction.VertexPath.geodesic_of_end line 5767
lemma OAI.HyperbolicObstruction.VertexPath.geodesic_unit line 5783
lemma OAI.HyperbolicObstruction.VertexPath.geodesic_quasi line 5787
def OAI.HyperbolicObstruction.WordPictures.Cochain.path line 5798
lemma OAI.HyperbolicObstruction.WordPictures.Cochain.path_length line 5800
lemma OAI.HyperbolicObstruction.WordPictures.Cochain.path_point_zero line 5801
lemma OAI.HyperbolicObstruction.WordPictures.Cochain.path_start line 5802
lemma OAI.HyperbolicObstruction.WordPictures.Cochain.path_finish line 5803
lemma OAI.HyperbolicObstruction.WordPictures.Cochain.path_cons_succ line 5805
lemma OAI.HyperbolicObstruction.WordPictures.Cochain.path_integral line 5808
lemma OAI.HyperbolicObstruction.WordPictures.Cochain.path_unit line 5824
lemma OAI.HyperbolicObstruction.WordPictures.Cochain.edge_letter line 5841
lemma OAI.HyperbolicObstruction.WordPictures.Cochain.represent_path line 5869
lemma OAI.HyperbolicObstruction.WordPictures.Cochain.represent_good line 5893
lemma OAI.HyperbolicObstruction.WordPictures.Cochain.geodesic_exists line 5912
def OAI.HyperbolicObstruction.VertexPath.tentWeight line 5933
lemma OAI.HyperbolicObstruction.VertexPath.tentWeight_antisymm line 5936
lemma OAI.HyperbolicObstruction.VertexPath.integral_shift line 5939
lemma OAI.HyperbolicObstruction.VertexPath.quadratic_bound line 5949
def OAI.HyperbolicObstruction.CochainLinear line 5997
Source documentation
A quantitative consequence of actual linear word filling, tested by Lipschitz cochains. This property makes no geometric conclusion an assumption.
```
def CochainLinear (X : Type*) [MetricSpace X] (K : ℝ) : Prop :=
…
```
lemma OAI.HyperbolicObstruction.WordPictures.Cochain.linear_of_filling line 6008
lemma OAI.HyperbolicObstruction.VertexPath.quasi_injective line 6051
lemma OAI.HyperbolicObstruction.VertexPath.quasi_extension line 6060
lemma OAI.HyperbolicObstruction.VertexPath.tent_lipschitz line 6078
lemma OAI.HyperbolicObstruction.VertexPath.nearest line 6087
lemma OAI.HyperbolicObstruction.VertexPath.maximum_nearest line 6093
lemma OAI.HyperbolicObstruction.VertexPath.geodesic_length line 6109
lemma OAI.HyperbolicObstruction.VertexPath.geodesic_sub line 6111
lemma OAI.HyperbolicObstruction.VertexPath.quasi_reverse line 6119
lemma OAI.HyperbolicObstruction.VertexPath.integral_sub_eq line 6134
lemma OAI.HyperbolicObstruction.VertexPath.integral_sub_mono line 6139
lemma OAI.HyperbolicObstruction.VertexPath.integral_tent_zero line 6151
lemma OAI.HyperbolicObstruction.VertexPath.arithmetic_tent_sum line 6157
lemma OAI.HyperbolicObstruction.VertexPath.integral_tent_lower line 6170
Source documentation
A tent centered on a long unit path sees a quadratic amount of integral. The coordinate function is the actual Lipschitz index extension.
```
lemma integral_tent_lower (p : VertexPath X) (hp : p.Unit) (u : X→ℝ)
    (hu : ∀ i ≤ p.length, u (p.point i)=i) {R k s t : ℕ}
    (hs : s ≤ k) (ht : k+R ≤ t) (htp : t ≤ p.length) :
    (R:ℝ)^2/2 ≤ (p.sub s t).integral (tentWeight
      (fun x => max 0 ((R:ℝ)-dist (p.point k) x)) u) := by
…
```
Mentions: OAI.HyperbolicObstruction.VertexPath, OAI.HyperbolicObstruction.VertexPath.integral, OAI.HyperbolicObstruction.VertexPath.tentWeight
def OAI.HyperbolicObstruction.VertexPath.between line 6208
lemma OAI.HyperbolicObstruction.VertexPath.between_start line 6211
lemma OAI.HyperbolicObstruction.VertexPath.between_finish line 6217
lemma OAI.HyperbolicObstruction.VertexPath.between_unit line 6222
lemma OAI.HyperbolicObstruction.VertexPath.between_length_real line 6229
lemma OAI.HyperbolicObstruction.VertexPath.between_length_le line 6236
lemma OAI.HyperbolicObstruction.VertexPath.between_point line 6242

lemma OAI.HyperbolicObstruction.VertexPath.outside_connector line 6252

Source documentation

A connector of length at most R stays outside the R-tent whenever its initial vertex is 2R away, or is already on the comparison path.

lemma outside_connector
    (hgeo : ∀ x y : X, ∃ c : VertexPath X, c.start=x ∧ c.finish=y ∧ c.Geodesic)
    (q : VertexPath X) (b x : X) (R : ℝ) (hR : 0 ≤ R)
    (hq : ∀ j ≤ q.length, R ≤ dist b (q.point j))
    (hnear : ∃ j ≤ q.length, dist x (q.point j) ≤ R)
    (hfar : (∃ j ≤ q.length, x=q.point j) ∨ 2*R ≤ dist b x) :
    ∃ j ≤ q.length, ∃ c : VertexPath X,
      c.start=x ∧ c.finish=q.point j ∧ c.Unit ∧ (c.length:ℝ) ≤ R ∧
        ∀ i ≤ c.length, R ≤ dist b (c.point i) := by
…

Mentions: OAI.HyperbolicObstruction.VertexPath

lemma OAI.HyperbolicObstruction.VertexPath.end_dist_le line 6283

lemma OAI.HyperbolicObstruction.VertexPath.cochain_morse_max line 6288

Source documentation

Localized-loop proof of uniform Morse stability. The loop has length at most 56R and its tent integral at least R²/2.

lemma cochain_morse_max {K : ℝ} (hK : 0 ≤ K) (hco : CochainLinear X K)
    (hgeo : ∀ x y : X, ∃ c : VertexPath X, c.start=x ∧ c.finish=y ∧ c.Geodesic)
    (p q : VertexPath X) (hp : p.Unit) (hqp : p.Quasi 3) (hq : q.Unit) (hqq : q.Quasi 3)
    (hstart : p.start=q.start) (hfinish : p.finish=q.finish)
    {k R : ℕ} (hk : k ≤ p.length)
    (hfarq : ∀ j ≤ q.length, (R:ℝ) ≤ dist (p.point k) (q.point j))
    (hnear : ∀ i ≤ p.length, ∃ j ≤ q.length, dist (p.point i) (q.point j) ≤ R) :
    (R:ℝ) ≤ 112*K := by
…

Mentions: OAI.HyperbolicObstruction.CochainLinear, OAI.HyperbolicObstruction.VertexPath

lemma OAI.HyperbolicObstruction.VertexPath.cochain_morse line 6412
lemma OAI.HyperbolicObstruction.VertexPath.geodesic_reverse line 6424
lemma OAI.HyperbolicObstruction.VertexPath.nearest_append_quasi line 6430
Source documentation
Joining at a nearest vertex produces a 3-quasigeodesic, with no additive error. This avoids any planar-diagram or simple-boundary assumption.
```
lemma nearest_append_quasi {p q : VertexPath X} (hp : p.Geodesic) (hq : q.Geodesic)
    (he : p.finish=q.start)
    (hnear : ∀ i ≤ p.length, dist p.finish q.finish ≤ dist (p.point i) q.finish) :
    (p.append q).Quasi 3 := by
…
```
Mentions: OAI.HyperbolicObstruction.VertexPath, OAI.HyperbolicObstruction.VertexPath.Quasi
def OAI.HyperbolicObstruction.VertexPath.ThinTriangles line 6486
Source documentation
Literal vertex thin triangles.
```
def ThinTriangles (X : Type*) [MetricSpace X] (D : ℝ) : Prop :=
…
```
lemma OAI.HyperbolicObstruction.VertexPath.cochain_thin line 6492
def OAI.HyperbolicObstruction.VertexPath.product line 6540
lemma OAI.HyperbolicObstruction.VertexPath.product_nonneg line 6541
lemma OAI.HyperbolicObstruction.VertexPath.product_le_left line 6545
lemma OAI.HyperbolicObstruction.VertexPath.product_le_right line 6548
lemma OAI.HyperbolicObstruction.VertexPath.geodesic_start_dist line 6552
lemma OAI.HyperbolicObstruction.VertexPath.geodesic_finish_dist line 6556
lemma OAI.HyperbolicObstruction.VertexPath.thin_initial_close line 6561
lemma OAI.HyperbolicObstruction.VertexPath.thin_product line 6604
lemma OAI.HyperbolicObstruction.VertexPath.thin_fourpoint line 6646
lemma OAI.HyperbolicObstruction.WordPictures.wordHyperbolic_of_linear line 6667
lemma OAI.HyperbolicObstruction.IncidenceTemplate.finalFinite_hyperbolic line 6721

theorem OAI.HyperbolicObstruction.IncidenceTemplate.exists_finite_aspherical_hyperbolic_noAction line 6747

Source documentation

SAME-model complete construction and word-hyperbolicity. It deliberately omits, rather than assumes, the remaining Cartan-Hadamard/deck consequence.

theorem exists_finite_aspherical_hyperbolic_noAction :
    ∃ K : FiniteComplex, ∃ x : K.Carrier, ∃ C : ℝ,
    ConnectedSpace K.Carrier ∧ K.Aspherical x ∧ Infinite (FundamentalGroup K.Carrier x) ∧
      0 ≤ C ∧ K.LinearDiskFilling C ∧
      NoGeometricCATZeroAction.{u} (FundamentalGroup K.Carrier x) ∧
      WordHyperbolic (FundamentalGroup K.Carrier x) := by
…

Mentions: OAI.HyperbolicObstruction.FiniteComplex, OAI.HyperbolicObstruction.WordHyperbolic

lemma OAI.HyperbolicObstruction.CurvatureComparison.sinh_cosh_bound line 6767
lemma OAI.HyperbolicObstruction.CurvatureComparison.tanhOver_antitone line 6772
lemma OAI.HyperbolicObstruction.CurvatureComparison.deriv_logCoshSqrt line 6794
lemma OAI.HyperbolicObstruction.CurvatureComparison.logCoshSqrt_concave line 6801
lemma OAI.HyperbolicObstruction.CurvatureComparison.concave_balance line 6813
lemma OAI.HyperbolicObstruction.CurvatureComparison.cosh_balance line 6830
lemma OAI.HyperbolicObstruction.CurvatureComparison.cosh_triangle_comparison line 6843
lemma OAI.HyperbolicObstruction.CurvatureComparison.midpoint_nonpos line 6870
lemma OAI.HyperbolicObstruction.IsSegment.continuousOn line 6928
lemma OAI.HyperbolicObstruction.CATNegOne.midpoint_cn line 6936
lemma OAI.HyperbolicObstruction.CATNegOne.cn_of_midpoint line 6956
lemma OAI.HyperbolicObstruction.IsSegment.midpoint_dist line 6969
theorem OAI.HyperbolicObstruction.CATNegOne.catZero line 6978
Source documentation
Curvature monotonicity for the exact definitions used in the main.
```
theorem CATNegOne.catZero (h : CATNegOne X) : CATZero X := by
…
```
Mentions: OAI.HyperbolicObstruction.CATNegOne, OAI.HyperbolicObstruction.CATZero
def OAI.HyperbolicObstruction.IsGeodesic.midpoint line 7016
lemma OAI.HyperbolicObstruction.IsGeodesic.dist_left_midpoint line 7018
lemma OAI.HyperbolicObstruction.IsGeodesic.dist_midpoint_right line 7024
def OAI.HyperbolicObstruction.UniformLocalCATZero line 7034
Source documentation
A uniform ambient neighborhood lies in a CAT(0) subspace.
```
def UniformLocalCATZero (r : ℝ) : Prop :=
…
```
lemma OAI.HyperbolicObstruction.uniformLocalCATZero_of_compact line 7037
lemma OAI.HyperbolicObstruction.midpoint_eq_subtype line 7049
lemma OAI.HyperbolicObstruction.IsGeodesic.midpoint_mem_ball line 7061
lemma OAI.HyperbolicObstruction.UniformLocalCATZero.midpoint_lipschitz line 7072
lemma OAI.HyperbolicObstruction.UniformLocalCATZero.midpoint_cn line 7086
abbrev OAI.HyperbolicObstruction.FiniteMidpointFixedPoint.left line 7109
abbrev OAI.HyperbolicObstruction.FiniteMidpointFixedPoint.center line 7110
abbrev OAI.HyperbolicObstruction.FiniteMidpointFixedPoint.right line 7111
def OAI.HyperbolicObstruction.FiniteMidpointFixedPoint.weight line 7113
lemma OAI.HyperbolicObstruction.FiniteMidpointFixedPoint.weight_pos line 7115
lemma OAI.HyperbolicObstruction.FiniteMidpointFixedPoint.weight_le line 7121
lemma OAI.HyperbolicObstruction.FiniteMidpointFixedPoint.weight_neighbors line 7129

theorem OAI.HyperbolicObstruction.FiniteMidpointFixedPoint.exists_fixed line 7137

Source documentation

The compact finite Dirichlet problem. Boundary values are fixed, and all interior coordinates satisfy the ordinary one-half neighbor estimate.

theorem exists_fixed [Nonempty P] (n : ℕ) (u : P → Fin (n+2) → X)
    (hu : ∀ i, Continuous (fun p => u p i)) (hinj : Function.Injective u)
    (T : P → P) (hT : ∀ i, Continuous (fun p => u (T p) i))
    (hleft : ∀ p q, u (T p) 0=u (T q) 0)
    (hright : ∀ p q, u (T p) (Fin.last (n+1))=u (T q) (Fin.last (n+1)))
    (hmid : ∀ p q (i : Fin n),
      dist (u (T p) (center i)) (u (T q) (center i)) ≤
        (dist (u p (left i)) (u q (left i))+dist (u p (right i)) (u q (right i)))/2) :
    ∃ p, T p=p := by
…

Mentions: OAI.HyperbolicObstruction.FiniteMidpointFixedPoint.center, OAI.HyperbolicObstruction.FiniteMidpointFixedPoint.left, OAI.HyperbolicObstruction.FiniteMidpointFixedPoint.right

lemma OAI.HyperbolicObstruction.DiscreteHarmonic.maximum line 7214
lemma OAI.HyperbolicObstruction.DiscreteHarmonic.chord line 7237
def OAI.HyperbolicObstruction.LocalPolygonContinuation.Box line 7274
lemma OAI.HyperbolicObstruction.LocalPolygonContinuation.box_closed line 7278
lemma OAI.HyperbolicObstruction.LocalPolygonContinuation.box_nonempty line 7290
lemma OAI.HyperbolicObstruction.LocalPolygonContinuation.neighbors_in_ball line 7306
def OAI.HyperbolicObstruction.LocalPolygonContinuation.node line 7321
lemma OAI.HyperbolicObstruction.LocalPolygonContinuation.node_zero line 7328
lemma OAI.HyperbolicObstruction.LocalPolygonContinuation.node_last line 7330
lemma OAI.HyperbolicObstruction.LocalPolygonContinuation.node_center line 7332
lemma OAI.HyperbolicObstruction.LocalPolygonContinuation.node_mem line 7342
theorem OAI.HyperbolicObstruction.LocalPolygonContinuation.exists_stationary line 7364
Source documentation
Small endpoint perturbations have an actual midpoint-stationary polygon in the prescribed box. Compactness is used only for a genuine finite minimum.
```
theorem exists_stationary {a b : X} (ha : dist a (q 0)≤r/20)
    (hb : dist b (q (Fin.last (n+1)))≤r/20) :
    ∃ p : Fin (n+2) → X, p ∈ Box (r:=r) q a b ∧
…
```
Mentions: OAI.HyperbolicObstruction.LocalPolygonContinuation.Box
lemma OAI.HyperbolicObstruction.IsSegment.reparam line 7418
lemma OAI.HyperbolicObstruction.IsSegment.dist_from_source line 7432
lemma OAI.HyperbolicObstruction.catZero_of_segment_midpoint line 7437
def OAI.HyperbolicObstruction.RadialBusemann line 7463
Source documentation
Radial comparison for any two constant-speed geodesics with common start.
```
def RadialBusemann (X : Type*) [MetricSpace X] : Prop :=
…
```
theorem OAI.HyperbolicObstruction.catZero_of_local_radial line 7469
Source documentation
Small-scale comparison plus the constructed global radial contraction is sufficient for the literal whole-segment CAT(0) definition.
```
theorem catZero_of_local_radial (g : IsGeodesic X) (hb : RadialBusemann X)
    (hl : ∀ x : X, ∃ r : ℝ, 0<r ∧ CATZero (Metric.ball x r)) : CATZero X := by
…
```
Mentions: OAI.HyperbolicObstruction.IsGeodesic, OAI.HyperbolicObstruction.RadialBusemann, OAI.HyperbolicObstruction.CATZero
lemma OAI.HyperbolicObstruction.CurvatureComparison.local_midpoint_nonpos line 7543
lemma OAI.HyperbolicObstruction.CurvatureComparison.local_midpoint_chord line 7593
structure OAI.HyperbolicObstruction.IsLocalSegment line 7620
Source documentation
A uniformly locally constant-speed geodesic on the unit interval.
```
structure IsLocalSegment (γ : ℝ → X) (L : ℝ) : Prop where
…
```
lemma OAI.HyperbolicObstruction.IsSegment.isLocalSegment line 7626
lemma OAI.HyperbolicObstruction.UniformLocalCATZero.eq_midpoint_of_dist line 7630
lemma OAI.HyperbolicObstruction.IsLocalSegment.close_chord line 7646
lemma OAI.HyperbolicObstruction.IsLocalSegment.close_unique line 7706
lemma OAI.HyperbolicObstruction.SegmentChain.interval_cover line 7725
lemma OAI.HyperbolicObstruction.SegmentChain.interval_union line 7740
def OAI.HyperbolicObstruction.SegmentChain.cell line 7755
lemma OAI.HyperbolicObstruction.SegmentChain.cell_mem line 7756
def OAI.HyperbolicObstruction.SegmentChain.curve line 7759
lemma OAI.HyperbolicObstruction.SegmentChain.compatible line 7765
lemma OAI.HyperbolicObstruction.SegmentChain.curve_eq line 7782
lemma OAI.HyperbolicObstruction.SegmentChain.curve_continuousOn line 7790
lemma OAI.HyperbolicObstruction.SegmentChain.curve_zero line 7802
lemma OAI.HyperbolicObstruction.SegmentChain.curve_last line 7807
lemma OAI.HyperbolicObstruction.SegmentChain.curve_node line 7817
def OAI.HyperbolicObstruction.SegmentChain.unitCurve line 7826
Source documentation
The literal interpolation on the unit interval.
```
def unitCurve (t : ℝ) : X := curve hN p γ ((N:ℝ)*t)
```
Mentions: OAI.HyperbolicObstruction.SegmentChain.curve
lemma OAI.HyperbolicObstruction.SegmentChain.unitCurve_continuousOn line 7828
lemma OAI.HyperbolicObstruction.SegmentChain.unitCurve_zero line 7834
lemma OAI.HyperbolicObstruction.SegmentChain.unitCurve_one line 7835