BoundaryFlow.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

def OAI.KervaireFlow.antisymmetric line 42
def OAI.KervaireFlow.divergence line 55
Source documentation
Literal sum of corner phases on each boundary circle.
```
def divergence (b : D → Z) : (D → ℝ) →ₗ[ℝ] (Z → ℝ) where
…
```
lemma OAI.KervaireFlow.divergence_single line 71
def OAI.KervaireFlow.edgeFlow line 82
Source documentation
Supported on the two ends of one band, including the harmless loop case.
```
def edgeFlow (θ : Equiv.Perm D) (d : D) : D → ℝ :=
…
```
lemma OAI.KervaireFlow.edgeFlow_mem line 86
lemma OAI.KervaireFlow.divergence_edgeFlow line 101
def OAI.KervaireFlow.Adj line 106
Source documentation
Adjacency in the graph dual to the band sides, with orientations retained.
```
def Adj (b : D → Z) (θ : Equiv.Perm D) (x y : Z) : Prop :=
…
```
lemma OAI.KervaireFlow.difference_mem_range line 110

theorem OAI.KervaireFlow.exists_flow line 130

Source documentation

Any total-zero boundary phases are realized by antisymmetric phases on the paired slots of a connected diagram.

theorem exists_flow (b : D → Z) (θ : Equiv.Perm D) (hθ : ∀ d, θ (θ d) = d)
    (hconn : ∀ x y, Relation.ReflTransGen (Adj b θ) x y)
    (root : Z) (η : Z → ℝ) (hη : ∑ z, η z = 0) :
    ∃ γ : D → ℝ, (∀ d, γ (θ d) = -γ d) ∧
      ∀ z, (∑ d, if b d = z then γ d else 0) = η z := by
…

Mentions: OAI.KervaireFlow.Adj

lemma OAI.KervaireFlow.dual_connected line 155

Source documentation

Changing the disk successor to the boundary successor does not change connectivity of the dual graph.

lemma dual_connected (b : D → Z) (hb : Function.Surjective b)
    (σ θ : Equiv.Perm D) (hθ : ∀ d, θ (θ d) = d)
    (hcycle : ∀ d, b (σ (θ d)) = b d)
    (hconn : ∀ d e, Relation.ReflTransGen (fun d e => e = σ d ∨ e = θ d) d e) :
    ∀ x y, Relation.ReflTransGen (Adj b θ) x y := by
…

Mentions: OAI.KervaireFlow.Adj

def OAI.KervaireBoundary.traversalSign line 182
lemma OAI.KervaireBoundary.traversalSign_positive line 187
lemma OAI.KervaireBoundary.traversalSign_negative line 193

lemma OAI.KervaireBoundary.exists_band_mixer line 200

Source documentation

The signed band involution supplies exactly the scalar hypotheses of the full fixed-space mixing theorem.

lemma exists_band_mixer [Nonempty K] (s : I → ℤ)
    (hs : ∀ i, s i = 1 ∨ s i = -1) (hsum : (∑ i, s i) = 1 ∨ (∑ i, s i) = -1)
    (θ : Equiv.Perm (Slot I K)) (hθ : ∀ d, θ (θ d) = d)
    (hop : ∀ d, traversalSign s (θ d) = -traversalSign s d)
    (γ : Slot I K → ℝ) (hγ : ∀ d, γ (θ d) = -γ d) :
    ∃ X : Matrix.unitaryGroup K ℂ, 2 * Fintype.card K ≤
      KervaireFixed.fixedDim (mixingMatrix (I := I) (X : Matrix K K ℂ) *
…

Mentions: OAI.KervaireBoundary.traversalSign, OAI.KervaireFixed.fixedDim

lemma OAI.KervaireBoundary.S_mul_bands line 231

lemma OAI.KervaireBoundary.boundary_phase_upper line 242

Source documentation

The literal phase bound for every antisymmetric real choice of band phases.

lemma boundary_phase_upper [Nonempty I] [Nonempty K] (ρ : Equiv.Perm I) (a : I → A)
    (s : I → ℤ) (hs : ∀ i, s i = 1 ∨ s i = -1) (hsum : (∑ i, s i) = 1 ∨ (∑ i, s i) = -1)
    (θ : Equiv.Perm (Slot I K)) (hθ : ∀ d, θ (θ d) = d)
    (hop : ∀ d, traversalSign s (θ d) = -traversalSign s d)
    (γ : Slot I K → ℝ) (hγ : ∀ d, γ (θ d) = -γ d) :
    let _ := isStarNormal_of_mem_unitary (weightedShift_unitary (successor ρ * θ)
…

Mentions: OAI.KervaireBoundary.traversalSign

theorem OAI.KervaireBoundary.planar_boundary line 266