IncidentRootObstruction.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Why an incident one-way root prevents the two-block argument

A nonzero root crossing the selected block moves its coordinate projection. If the stabilizer contains the entire root, it cannot preserve that block on any identity neighborhood. Thus a terminal strongly connected class cannot be substituted for a symmetric root block while incoming roots remain. This states the precise obstruction to that proposed reduction.

lemma OAI.DukePrimeDegree.cross_root_not_mem_blockComplement line 22
lemma OAI.DukePrimeDegree.cross_root_moves_blockProjection line 35

theorem OAI.DukePrimeDegree.not_local_block_containment_of_cross_root line 48

Source documentation

Arbitrarily small elements of an incident root already rule out local containment in the two-block group. No entropy premise is used.

theorem not_local_block_containment_of_cross_root {n : ℕ}
    (L : Subgroup (G n)) (S : Set (Fin n)) {i j : Fin n} (hij : i ≠ j)
    (hcross : ¬(i ∈ S ↔ j ∈ S))
    (hroot : ∀ t : ℝ, SpecialLinearGroup.transvection hij t ∈ L) :
    {g : L | g.val ∈ blockMatrixGroup (blockComplementSetoid S)} ∉ 𝓝 (1 : L) := by
…

Mentions: OAI.DukePrimeDegree.blockMatrixGroup, OAI.DukePrimeDegree.blockComplementSetoid