LiftedBasis.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.HyperbolicObstruction.ConeSkeleton.MacroCell line 18
Source documentation
One (unoriented) elementary top triangle per actual macro edge. The finite vertex numbering only chooses signs; it does not identify different edges.
```
abbrev MacroCell := {e : Sym2 MacroGraph.Vertex // e ∈ MacroGraph.graph.edgeSet}
```
Mentions: OAI.HyperbolicObstruction.MacroGraph.Vertex
def OAI.HyperbolicObstruction.ConeSkeleton.macroCell line 20
lemma OAI.HyperbolicObstruction.ConeSkeleton.macroCell_symm line 21
def OAI.HyperbolicObstruction.ConeSkeleton.macroOrientation line 25
lemma OAI.HyperbolicObstruction.ConeSkeleton.macroOrientation_symm line 29
abbrev OAI.HyperbolicObstruction.ConeSkeleton.LiftedCellularChain line 46
Source documentation
Integral chains with independent coordinates for every deck translate of an elementary top triangle, fan triangle, square, or six-cell. No topological realization or equation on these chains is part of the definition.
```
abbrev LiftedCellularChain := (G × ((Top n w × MacroCell) ⊕ FrozenCell n w d)) →₀ ℤ
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.Top, OAI.HyperbolicObstruction.ConeSkeleton.MacroCell, OAI.HyperbolicObstruction.ConeSkeleton.FrozenCell
def OAI.HyperbolicObstruction.ConeSkeleton.liftedTopBasis line 48
lemma OAI.HyperbolicObstruction.ConeSkeleton.liftedTopBasis_symm line 52
def OAI.HyperbolicObstruction.ConeSkeleton.liftedFrozenBasis line 56
def OAI.HyperbolicObstruction.ConeSkeleton.integralLiftedTarget line 63
def OAI.HyperbolicObstruction.ConeSkeleton.integralLiftedFrozenTarget line 66
theorem OAI.HyperbolicObstruction.ConeSkeleton.uniform_integral_lifted_chain_zero line 71
Source documentation
The entire signed integral lifted cell vector vanishes, not just a scalar augmentation.
```
theorem uniform_integral_lifted_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

theorem OAI.HyperbolicObstruction.ConeSkeleton.finalDiagramStage_integral_chain_zero line 90

Source documentation

The same final sampled arrays have the integral lifted-chain conclusion, with no additional event or a posteriori choice of presentation.

theorem finalDiagramStage_integral_chain_zero (m : ℕ)
    (G : Type) [Group G]
    (voltage : Dart (finalDiagramStage m).size (finalDiagramStage m).master → G)
    (hv : ∀ e, voltage (rev (finalDiagramStage m).size (finalDiagramStage m).master e) = (voltage e)⁻¹)
    (hcell : ∀ a : Cell (finalDiagramStage m).size (finalDiagramStage m).master (finalDiagramStage m).six,
      (List.ofFn (fun i => voltage (side (finalDiagramStage m).size (finalDiagramStage m).master
        (finalDiagramStage m).six a i))).prod = 1)
    (P : WalkPicture.{0} (integralLiftedTarget (finalDiagramStage m).size (finalDiagramStage m).master
      (finalDiagramStage m).six G voltage hv hcell))
    (hm : P.FrozenMapped (integralLiftedFrozenTarget (finalDiagramStage m).size (finalDiagramStage m).master
      (finalDiagramStage m).six G voltage hv hcell)) : P.chain = 0 :=
…

Mentions: OAI.HyperbolicObstruction.ConeSkeleton.Dart, OAI.HyperbolicObstruction.ConeSkeleton.size, OAI.HyperbolicObstruction.ConeSkeleton.rev, OAI.HyperbolicObstruction.ConeSkeleton.Cell, OAI.HyperbolicObstruction.ConeSkeleton.side, OAI.HyperbolicObstruction.ConeSkeleton.integralLiftedTarget, OAI.HyperbolicObstruction.ConeSkeleton.integralLiftedFrozenTarget