OAI/NumberTheory/DukePrimeDegree/Entropy/LowEntropyInvariant.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Unconditional low-entropy root invariance

For the integer-lattice quotient, a nontrivial distinguished root leaf and atomic companion leaves force invariance under the distinguished root subgroup. All support, recurrence, and shearing steps are proved. This is the low-entropy alternative in EKL (2006), Theorem 2.3, specialized to the quotient used by the prime-degree packet theorem.

  1. theorem OAI.DukePrimeDegree.root_invariant_of_atomic_companion_leaves line 21