RegularRootSymmetry.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Finite regular entropy tests and prime-degree rigidity

The finite regular entropy identities balance incoming and outgoing root coefficients. This makes the invariant-root relation symmetric, yielding Haar classification in prime degree when regular entropy is positive.

def OAI.DukePrimeDegree.CanonicalRegularEntropyTests line 23
Source documentation
The finite family of entropy identities used by the prime-degree application. Both time directions are retained explicitly.
```
def CanonicalRegularEntropyTests (d : ℕ) (μ : Measure (X (d + 1)))
    [IsProbabilityMeasure μ] : Prop :=
…
```

theorem OAI.DukePrimeDegree.canonicalRootCoefficient_symmetric_of_balance line 41

Source documentation

Balance of mean root information yields equality of opposite coefficients, using root invariance and the root commutator.

theorem canonicalRootCoefficient_symmetric_of_balance (hd : 2 < d + 1)
    (hbalance : ∀ i, ∑ j, canonicalRootCoefficient d μ i j =
      ∑ j, canonicalRootCoefficient d μ j i) :
    ∀ i j, canonicalRootCoefficient d μ i j = canonicalRootCoefficient d μ j i := by
…

Mentions: OAI.DukePrimeDegree.canonicalRootCoefficient

theorem OAI.DukePrimeDegree.rootInvarianceRelation_symmetric_of_coefficient_balance line 67
Source documentation
The actual full-root invariance relation is symmetric under balance of the actual mean coefficients. No finite-orbit hypothesis is needed.
```
theorem rootInvarianceRelation_symmetric_of_coefficient_balance (hd : 2 < d + 1)
    (hbalance : ∀ i, ∑ j, canonicalRootCoefficient d μ i j =
      ∑ j, canonicalRootCoefficient d μ j i) :
    Std.Symm (rootInvarianceRelation μ) := by
…
```
Mentions: OAI.DukePrimeDegree.canonicalRootCoefficient
theorem OAI.DukePrimeDegree.rootInvarianceRelation_symmetric_of_regular_tests line 91
Source documentation
Time reversal of only the displayed finite regular entropy tests supplies the coefficient balance required for actual root symmetry.
```
theorem rootInvarianceRelation_symmetric_of_regular_tests (hd : 2 < d + 1)
    (htests : CanonicalRegularEntropyTests d μ) :
    Std.Symm (rootInvarianceRelation μ) := by
…
```
Mentions: OAI.DukePrimeDegree.CanonicalRegularEntropyTests

theorem OAI.DukePrimeDegree.isHaar_of_prime_regular_entropy_tests line 101

Source documentation

Finite regular entropy identities and positive regular entropy give Haar probability.

theorem isHaar_of_prime_regular_entropy_tests
    (hprime : (d + 1).Prime) (hd : 2 < d + 1)
    (htests : CanonicalRegularEntropyTests d μ)
    (hpos : 0 < measureEntropy μ (fun x => rightAction x
      (diagonalOneParameter (regularDiagonalWeights d) (regularDiagonalWeights_sum d) 1))) :
    IsHaarProbability μ := by
…

Mentions: OAI.DukePrimeDegree.CanonicalRegularEntropyTests

theorem OAI.DukePrimeDegree.eklPrimeInput_of_regular_entropy_tests line 117
Source documentation
Finite regular entropy identities for diagonal-ergodic probabilities imply the prime-degree rigidity criterion.
```
theorem eklPrimeInput_of_regular_entropy_tests (d : ℕ)
    (htests : ∀ (μ : Measure (X (d + 1))) (hμ : IsProbabilityMeasure μ),
      ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d + 1)) μ →
        @CanonicalRegularEntropyTests d μ hμ) :
    EKLPrimeInput d := by
…
```
Mentions: OAI.DukePrimeDegree.CanonicalRegularEntropyTests, OAI.DukePrimeDegree.EKLPrimeInput