PrimeBlockEndpoint.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Prime-degree block rigidity

Real-span rationality of the block centralizer forces a nontrivial block partition in prime degree to be the universal partition.

def OAI.DukePrimeDegree.rationalBlockRealSpan line 20
Source documentation
The real span of the rational block centralizer in lattice coordinates.
```
def rationalBlockRealSpan {n : ℕ} (g : G n) (r : Setoid (Fin n)) :
    Submodule ℝ (Fin n → ℝ) :=
…
```
theorem OAI.DukePrimeDegree.coordinate_eq_of_mem_rationalBlockRealSpan line 26
Source documentation
If the rational block centralizer consists only of scalars, every function in its real span has equal coordinate values.
```
theorem coordinate_eq_of_mem_rationalBlockRealSpan {n : ℕ}
    (g : G n) (r : Setoid (Fin n))
    (hbot : rationalBlockStabilizer g r = ⊥)
    {v : Fin n → ℝ} (hv : v ∈ rationalBlockRealSpan g r) (i j : Fin n) :
    v i = v j := by
…
```
Mentions: OAI.DukePrimeDegree.rationalBlockStabilizer, OAI.DukePrimeDegree.rationalBlockRealSpan
theorem OAI.DukePrimeDegree.root_partition_universal_of_rational_span line 50
Source documentation
Prime dimension and real-span rationality force a nontrivial root partition to have a single block. The premise refers to the concrete intersection of the rational lattice stabilizer and block centralizer.
```
theorem root_partition_universal_of_rational_span {n : ℕ}
    (hn : n.Prime) (g : G n)
    (hzero : ∀ v ∈ rowLattice g.val, v ≠ 0 → ∀ j, v j ≠ 0)
    (r : Setoid (Fin n)) (hblock : ∃ i j, i ≠ j ∧ r i j)
    (hspan : ∀ c ∈ blockCoordinateAlgebra r, c ∈ rationalBlockRealSpan g r) :
    ∀ i j, r i j := by
…
```
Mentions: OAI.DukePrimeDegree.blockCoordinateAlgebra, OAI.DukePrimeDegree.rationalBlockRealSpan