TauLib.Denotation.Structural

Structural theorems surfacing the deep difference between τ-Idx and standard Nat.

The Core Insight

τ-Idx (= Nat as abbreviation) is not generic Nat. It is the earned natural number system discovered as the alpha orbit O_α = {⟨α,0⟩, ⟨α,1⟩, ⟨α,2⟩, …}. Structurally it is a commutative semiring without additive inverses:

• No additive zero in the ontological sense: 0 is the empty product, not a destructive absorber. Additive inverses are only earned at Part IX via TauInt formal differences (Boundary/NumberTower.lean).

• Omega (ω) is a dynamical absorber: it absorbs ρ (the progression iterator), NOT multiplication. ω is the one-point compactification of N⁺.

• Almost all properties hold universally: no “for n ≠ 0” guards needed, except for the single locus of multiplicative cancellation.

• Cauchy-compactness: the primorial ultrametric on omega-tails induces a profinite topology with finite stabilization.

This module makes these facts explicit via precise theorems.

Registry Cross-References

• [I.P06] Arithmetic Laws — earned semiring, no ring

• [I.P07] Well-Ordering — universal, no zero exclusion

• [I.K2] Omega Fixed Point — dynamical absorber

Section 1: Earned Semiring — Not a Ring

τ-Idx forms a commutative semiring (addition, multiplication with identities 0 and 1, distributivity) but cannot be extended to a ring within the earned framework. The absence of additive inverses is structural, not a deficiency: ρ generates only positive depth values, so negative depths do not exist in τ.

Tau.Denotation.Structural.tauIdx_sum_zero_iff

source theorem Tau.Denotation.Structural.tauIdx_sum_zero_iff (n m : TauIdx) :idx_add n m = 0 ↔ n = 0 ∧ m = 0

The sum of two τ-Idx values is zero iff both are zero. This is the foundational fact: addition on τ-Idx cannot “cancel” to zero.

Tau.Denotation.Structural.tauIdx_no_additive_inverse

source **theorem Tau.Denotation.Structural.tauIdx_no_additive_inverse (n : TauIdx)

(hn : n > 0) :¬∃ (m : TauIdx), idx_add n m = 0**

No positive element has an additive inverse in τ-Idx. Ground truth: “Actual infinity (ω) without additive zero” (Book I Reference).

Tau.Denotation.Structural.tauIdx_no_ring_negation

source theorem Tau.Denotation.Structural.tauIdx_no_ring_negation :¬∃ (neg : TauIdx → TauIdx), ∀ (n : TauIdx), idx_add n (neg n) = 0

There exists no negation function on τ-Idx. This is the precise statement that τ-Idx is a semiring, not a ring. Additive inverses are first earned at Part IX via TauInt formal differences.

Section 2: The Positive Core — N⁺ is Closed

N⁺ = {n : τ-Idx | n > 0} is closed under all four earned arithmetic operations. This means the positive elements form an autonomous sub-structure: arithmetic never “falls” into zero unless it starts there.

Tau.Denotation.Structural.tauIdx_pos_closed_add

source **theorem Tau.Denotation.Structural.tauIdx_pos_closed_add (n m : TauIdx)

(hn : n > 0) :idx_add n m > 0**

Addition with a positive argument always yields a positive result.

Tau.Denotation.Structural.tauIdx_pos_closed_mul

source **theorem Tau.Denotation.Structural.tauIdx_pos_closed_mul (n m : TauIdx)

(hn : n > 0)

(hm : m > 0) :idx_mul n m > 0**

Multiplication of two positive values is positive (no zero divisors in N⁺).

Tau.Denotation.Structural.tauIdx_pos_closed_exp

source **theorem Tau.Denotation.Structural.tauIdx_pos_closed_exp (n : TauIdx)

(hn : n > 0)

(m : TauIdx) :idx_exp n m > 0**

Exponentiation with positive base is always positive.

Tau.Denotation.Structural.tauIdx_succ_always_pos

source theorem Tau.Denotation.Structural.tauIdx_succ_always_pos (n : TauIdx) :idx_add n 1 > 0

Every successor is positive: n + 1 > 0 always holds. No guard needed — this is universal over τ-Idx.

Section 3: Zero as Non-Participant

Zero in τ-Idx is vacuous, not destructive. It is the unique degenerate element: it absorbs multiplication and has no prime factorization. But its degeneracy is passive — it doesn’t participate in the generative dynamics of ρ.

Tau.Denotation.Structural.tauIdx_zero_not_prime

source theorem Tau.Denotation.Structural.tauIdx_zero_not_prime :¬Coordinates.idx_prime 0

Zero is not a prime: it has no prime factorization.

Tau.Denotation.Structural.tauIdx_zero_not_succ

source theorem Tau.Denotation.Structural.tauIdx_zero_not_succ :¬∃ (k : TauIdx), idx_add k 1 = 0

Zero is not a successor: no element of τ-Idx maps to zero under ρ (addition). This reflects that the alpha orbit generates only positive depths.

Tau.Denotation.Structural.tauIdx_integral_domain

source theorem Tau.Denotation.Structural.tauIdx_integral_domain (n m : TauIdx) :idx_mul n m = 0 ↔ n = 0 ∨ m = 0

Integral domain property: the product of two τ-Idx values is zero iff at least one factor is zero. Equivalently: positive × positive = positive. There is no “annihilation” except through the vacuous zero.

Tau.Denotation.Structural.tauIdx_zero_unique_mul_absorber

source **theorem Tau.Denotation.Structural.tauIdx_zero_unique_mul_absorber (a : TauIdx)

(h : ∀ (n : TauIdx), idx_mul a n = a) :a = 0**

Zero is the unique multiplicative absorber: if a * n = a for all n, then a = 0. This rules out any “phantom absorber” in τ-Idx.

Tau.Denotation.Structural.tauIdx_zero_vacuous_divisor

source theorem Tau.Denotation.Structural.tauIdx_zero_vacuous_divisor (a : TauIdx) :Coordinates.idx_divides a 0

Zero is divisible by everything (vacuously): every a divides 0. This is a restatement of idx_divides_zero for emphasis: divisibility into zero is trivial, not informative.

Section 4: Universal vs. Guarded — The Single Failure Locus

The dramatic structural fact of τ-Idx: almost every algebraic property holds universally (no “for n ≠ 0” guard). The single exception is multiplicative cancellation, which fails exactly at zero.

In ring theory, “for a ≠ 0” qualifications appear everywhere. In τ-Idx:

• Addition: fully cancellative, universal (Theorem 13)

• Multiplication: cancellative ↔ n > 0 (Theorem 16)

• Divisibility: reflexive, transitive, antisymmetric — all universal

• Well-ordering: universal, no qualification needed

Tau.Denotation.Structural.tauIdx_add_left_cancel

source **theorem Tau.Denotation.Structural.tauIdx_add_left_cancel (n a b : TauIdx)

(h : idx_add n a = idx_add n b) :a = b**

Addition is left-cancellative: NO guard needed. This is universal — it holds for ALL n, including n = 0.

Tau.Denotation.Structural.tauIdx_add_right_cancel

source **theorem Tau.Denotation.Structural.tauIdx_add_right_cancel (a b n : TauIdx)

(h : idx_add a n = idx_add b n) :a = b**

Addition is right-cancellative: NO guard needed.

Tau.Denotation.Structural.tauIdx_mul_cancel_fails_at_zero

source theorem Tau.Denotation.Structural.tauIdx_mul_cancel_fails_at_zero :idx_mul 0 1 = idx_mul 0 2

The single failure: multiplicative cancellation breaks at zero. 0 × 1 = 0 × 2 but 1 ≠ 2.

Tau.Denotation.Structural.tauIdx_mul_cancel_exactly_pos

source theorem Tau.Denotation.Structural.tauIdx_mul_cancel_exactly_pos (n : TauIdx) :(∀ (a b : TauIdx), idx_mul n a = idx_mul n b → a = b) ↔ n > 0

The characterization theorem: multiplicative cancellation holds for n if and only if n > 0. This makes the single zero-sensitive locus maximally explicit.

Read as: “zero is the unique obstruction to multiplicative cancellation in τ-Idx.”

Section 5: Omega as Dynamical Absorber

Omega (ω) is the one-point compactification of the positive naturals N⁺. It absorbs the dynamical iterator ρ (fixed point by K2), but it does NOT absorb algebraic operations (multiplication). This is the τ-analog of ∞ in N⁺ ∪ {∞}: omega is a topological/dynamical limit, not an algebraic zero.

Key contrast with standard Nat: Nat has 0 as algebraic absorber (0 × n = 0). τ has ω as dynamical absorber (ρ(ω) = ω). These are structurally orthogonal.

Tau.Denotation.Structural.omega_rho_absorber

source theorem Tau.Denotation.Structural.omega_rho_absorber (d : Nat) :Kernel.rho { seed := Kernel.Generator.omega, depth := d } = { seed := Kernel.Generator.omega, depth := d }

Omega absorbs ρ: the beacon is a fixed point of the progression iterator. Restatement of K2 for emphasis in the structural context.

Tau.Denotation.Structural.omega_unique_fixed_seed

source theorem Tau.Denotation.Structural.omega_unique_fixed_seed (x : Kernel.TauObj) :Kernel.rho x = x ↔ x.seed = Kernel.Generator.omega

Omega is the UNIQUE fixed seed of ρ: an object x satisfies ρ(x) = x if and only if x lives in the omega fiber. This characterizes omega as the sole dynamical absorber.

Tau.Denotation.Structural.alpha_orbit_no_fixed_point

source theorem Tau.Denotation.Structural.alpha_orbit_no_fixed_point (n : TauIdx) :Kernel.rho (toAlphaOrbit n) ≠ toAlphaOrbit n

The alpha orbit has no fixed points of ρ: every TauIdx element strictly advances under ρ. The orbit is genuinely progressive.

Tau.Denotation.Structural.alpha_orbit_strictly_monotone

source **theorem Tau.Denotation.Structural.alpha_orbit_strictly_monotone (n m : TauIdx)

(h : n < m) :(toAlphaOrbit n).depth < (toAlphaOrbit m).depth**

The alpha orbit is strictly monotone in depth: higher orbit index means strictly greater depth. There is no “stalling” in the orbit.

Section 6: Finite Stabilization & Compactness

The primorial ultrametric on omega-tails induces a profinite topology on the completion space. The key property is finite stabilization: at each primorial level M_k, two omega-tails either agree or disagree — and agreement propagates downward through the reduction maps.

This gives τ-Idx its Cauchy-compact character: every Compatible sequence stabilizes at each finite level, making the completion (the space of all compatible omega-tails) compact. This is the τ-analog of Ẑ (profinite integers).

Tau.Denotation.Structural.ultra_dist_self

source theorem Tau.Denotation.Structural.ultra_dist_self (n d : TauIdx) :Polarity.ultra_dist (Polarity.mk_omega_tail n d) (Polarity.mk_omega_tail n d) = 0

The ultrametric distance of an omega-tail to itself is zero. This is the identity-of-indiscernibles axiom for the earned ultrametric.

Tau.Denotation.Structural.congruent_tails_agree

source **theorem Tau.Denotation.Structural.congruent_tails_agree (n m d k : TauIdx)

(hk1 : 1 ≤ k)

(hkd : k ≤ d)

(hmod : n % Polarity.primorial k = m % Polarity.primorial k) :(Polarity.mk_omega_tail n d).get (k - 1) = (Polarity.mk_omega_tail m d).get (k - 1)**

Finite stabilization: two numbers congruent modulo M_k produce omega-tails that agree at level k. This is the mechanism behind Cauchy-compactness: agreement at level k is determined by a finite check.