PrimeSingleBlockHaar.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Prime-degree Haar rigidity from a nontrivial invariant-root partition

The canonical component is genuinely ergodic for its chosen root block. The shearing argument constructs a positive-mass block orbit, and the rational stabilizer argument forces that block to be the full coordinate set. The root partition is supplied explicitly here: producing its symmetry and nontriviality from positive entropy is the separate entropy step, not a hidden homogeneous-orbit hypothesis.

theorem OAI.DukePrimeDegree.singleBlock_eq_univ_of_generic_local_stabilizer line 29

theorem OAI.DukePrimeDegree.isHaar_of_prime_nontrivial_root_partition line 65

Source documentation

The orbit-existence conclusion is proved inside the argument. The only remaining dynamical premise is the actual equivalence relation of invariant roots with at least one nontrivial class.

theorem isHaar_of_prime_nontrivial_root_partition
    (d : ℕ) (hprime : (d + 1).Prime)
    (μ : Measure (X (d + 1))) [IsProbabilityMeasure μ]
    [ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d + 1)) μ]
    (r : Setoid (Fin (d + 1)))
    (hr : ∀ i j, r i j ↔ rootInvarianceRelation μ i j)
    (hnontrivial : ∃ k l, k ≠ l ∧ r k l) :
    IsHaarProbability μ := by
…

theorem OAI.DukePrimeDegree.isHaar_of_prime_symmetric_invariant_roots line 120

Source documentation

The geometric application requires symmetry of the actual root invariance relation. Reflexivity and transitivity are already proved from the concrete root group identities.

theorem isHaar_of_prime_symmetric_invariant_roots
    (d : ℕ) (hprime : (d + 1).Prime)
    (μ : Measure (X (d + 1))) [IsProbabilityMeasure μ]
    [ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d + 1)) μ]
    (hsymm : Std.Symm (rootInvarianceRelation μ))
    (hroot : ∃ i j, i ≠ j ∧ rootInvarianceRelation μ i j) :
    IsHaarProbability μ := by
…

theorem OAI.DukePrimeDegree.eklPrimeInput_of_root_symmetry line 139
Source documentation
Symmetry of the invariant-root relation, together with the existence of a nontrivial invariant root from positive entropy, gives prime-degree Haar rigidity.
```
theorem eklPrimeInput_of_root_symmetry (d : ℕ)
    (hsymm : ∀ (μ : Measure (X (d + 1))), IsProbabilityMeasure μ →
      ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d + 1)) μ →
        Std.Symm (rootInvarianceRelation μ)) :
    EKLPrimeInput d := by
…
```
Mentions: OAI.DukePrimeDegree.EKLPrimeInput