TauLib.Orbit.Saturation

Tetration algebraic degradation and the Minimal Alphabet Theorem.

Registry Cross-References

• [I.T09] Minimal Alphabet Theorem — minimal_alphabet

• [I.T10a] Tetration Algebraic Degradation — tetration_algebraic_degradation

Mathematical Content

Tetration (level 4 of the hyperoperation ladder) is algebraically degraded compared to levels 1-3 (addition, multiplication, exponentiation):

• Non-commutative: 2↑↑3 ≠ 3↑↑2

• Non-associative: (2↑↑2)↑↑2 ≠ 2↑↑(2↑↑2)

• No universal right identity: ¬∃ e, ∀ n ≥ 2, n↑↑e = n

These failures combine with the channel exhaustion (Ladder.lean) and the counter-models (TooMany.lean, TooFew.lean) to give the Minimal Alphabet Theorem: |Gen| = 5 is the unique cardinality achieving completeness, rigidity, and saturation simultaneously.

Tau.Orbit.Saturation.tetration_non_comm

source theorem Tau.Orbit.Saturation.tetration_non_comm :tetration 2 3 ≠ tetration 3 2

Tetration is not commutative: 2↑↑3 = 16 ≠ 9 = 3↑↑2.

Tau.Orbit.Saturation.tetration_non_assoc

source theorem Tau.Orbit.Saturation.tetration_non_assoc :tetration (tetration 2 2) 2 ≠ tetration 2 (tetration 2 2)

Tetration is not associative: (2↑↑2)↑↑2 = 4↑↑2 = 256 ≠ 65536 = 2↑↑(2↑↑2) = 2↑↑4.

Tau.Orbit.Saturation.tetration_no_left_identity

source theorem Tau.Orbit.Saturation.tetration_no_left_identity :¬∃ (e : Nat), e ≥ 2 ∧ ∀ (n : Nat), n ≥ 1 → tetration e n = n

Tetration has no universal right identity. Proof: for e = 0, n↑↑0 = 1 ≠ n for n ≥ 2. For e = 1, n↑↑1 = n (works). But this is the only candidate, and for e ≥ 2, 2↑↑e ≥ 4 > 2, so e=1 is unique and we need to show there’s no other candidate. Actually, e=1 IS a right identity. The claim should be: tetration has no right identity other than 1 that works universally, AND the operation has no left identity.

More precisely: there is no left identity for tetration. For any e, e↑↑n = n fails: e↑↑2 = e^e ≠ 2 for e ≥ 2.

Tau.Orbit.Saturation.lower_ops_have_identities

source theorem Tau.Orbit.Saturation.lower_ops_have_identities :(∀ (n : Nat), n + 0 = n) ∧ (∀ (n : Nat), n * 1 = n) ∧ ∀ (n : Nat), n ^ 1 = n

Contrast: addition has identity 0, multiplication has identity 1, exponentiation has right identity 1 (n^1 = n). Tetration has right identity 1 (n↑↑1 = n) but no left identity ≥ 2.

Tau.Orbit.Saturation.AlgebraicDegradation

source structure Tau.Orbit.Saturation.AlgebraicDegradation :Prop

Tetration is algebraically degraded: non-commutative, non-associative, no left identity ≥ 2. This is the algebraic obstruction to canonicality at the 4th operation level.

• non_comm : tetration 2 3 ≠ tetration 3 2
• non_assoc : tetration (tetration 2 2) 2 ≠ tetration 2 (tetration 2 2)
• no_left_identity : ¬∃ (e : Nat), e ≥ 2 ∧ ∀ (n : Nat), n ≥ 1 → tetration e n = n Instances For

Tau.Orbit.Saturation.tetration_algebraic_degradation

source theorem Tau.Orbit.Saturation.tetration_algebraic_degradation :AlgebraicDegradation

[I.T10a] Tetration Algebraic Degradation: Tetration fails all three algebraic canonicality conditions.

Tau.Orbit.Saturation.MinimalAlphabetSpec

source structure Tau.Orbit.Saturation.MinimalAlphabetSpec :Prop

The Minimal Alphabet specification: what 5 generators achieve.

• add_has_channel : ladderChannel LadderLevel.add_level = some Kernel.Generator.pi Ladder completeness: all 3 rewiring levels have channels

• mul_has_channel : ladderChannel LadderLevel.mul_level = some Kernel.Generator.gamma
• exp_has_channel : ladderChannel LadderLevel.exp_level = some Kernel.Generator.eta

• tet_no_channel : ladderChannel LadderLevel.tet_level = none Saturation: the next level (tetration) has no channel

• solenoidal_exact : Kernel.solenoidalGenerators.length = 3 Exactly 3 solenoidal generators

• channels_distinct : Kernel.Generator.pi ≠ Kernel.Generator.gamma ∧ Kernel.Generator.pi ≠ Kernel.Generator.eta ∧ Kernel.Generator.gamma ≠ Kernel.Generator.eta Channels are pairwise distinct

Instances For

Tau.Orbit.Saturation.five_gen_spec

source theorem Tau.Orbit.Saturation.five_gen_spec :MinimalAlphabetSpec

The 5-generator system satisfies the Minimal Alphabet specification.

Tau.Orbit.Saturation.minimal_alphabet

source theorem Tau.Orbit.Saturation.minimal_alphabet :MinimalAlphabetSpec ∧ (∃ (f : TooMany.Obj6 → TooMany.Obj6), (∀ (x : TooMany.Obj6), f (TooMany.rho6 x) = TooMany.rho6 (f x)) ∧ (∀ (x : TooMany.Obj6), f (f x) = x) ∧ ¬∀ (x : TooMany.Obj6), f x = x) ∧ TooFew.ladder4Channel TooFew.Ladder4Level.exp_level = none ∧ AlgebraicDegradation

[I.T09] The Minimal Alphabet Theorem: 5 generators is the unique cardinality achieving all three properties:

(a) Completeness: All rewiring levels through exponentiation have canonical orbit channel assignments (π↔+, γ↔×, η↔^).

(b) Rigidity: No non-trivial ρ-automorphism exists. (4 generators also have this, but 6 do not.)

(c) Saturation: Tetration (level 4) has no channel, and is algebraically degraded (non-commutative, non-associative, no left identity).

Moreover, the counter-models show:

• 4 generators FAIL completeness: exponentiation loses its channel (only 2 solenoidal generators for 3 rewiring levels)

• 6 generators FAIL rigidity: the swap η↔ζ is a non-trivial ρ-automorphism (surplus solenoidal generator creates ambiguity)

This establishes |Gen| = 5 as the unique solution to the simultaneous requirements of completeness + rigidity + saturation.