BlockOrbitMass.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Positive mass on a block orbit already gives the prime-degree obstruction

The finite measure is assumed invariant only under the chosen opposite root pair. Restricting it to one positive block orbit preserves those two maps. The rational commutant argument therefore rules out every proper block partition, without full invariance under the block group.

lemma OAI.DukePrimeDegree.transvection_neg_one_mem_blockMatrixGroup line 21
lemma OAI.DukePrimeDegree.latticeOrbitPoint_comap_invariant_element line 27
theorem OAI.DukePrimeDegree.partition_universal_of_root_pair_supported_on_block_orbit line 50

theorem OAI.DukePrimeDegree.partition_universal_of_positive_block_orbit_mass line 112

Source documentation

Positive mass, not full support, suffices. The root pair must belong to the same proposed block, so restriction to that orbit remains invariant.

theorem partition_universal_of_positive_block_orbit_mass {n : ℕ}
    (hn : n.Prime) (g : G n) (r : Setoid (Fin n))
    (i j : Fin n) (hij : i ≠ j) (hr : r i j)
    (μ : Measure (X n)) [IsFiniteMeasure μ]
    (hpos : μ (range (latticeOrbitPoint g (blockMatrixGroup r))) ≠ 0)
    (hinv : μ.map (fun x => rightAction x
      (Matrix.SpecialLinearGroup.transvection hij (-1 : ℝ))) = μ)
    (hopinv : μ.map (fun x => rightAction x
      (Matrix.SpecialLinearGroup.transvection hij.symm (-1 : ℝ))) = μ)
    (hgeneric : ∀ᵐ x ∂μ, ∀ v ∈ pointLattice x, v ≠ 0 → ∀ k, v k ≠ 0) :
    ∀ a b, r a b := by
…

Mentions: OAI.DukePrimeDegree.latticeOrbitPoint, OAI.DukePrimeDegree.blockMatrixGroup