TauLib · API Book I

TauLib.BookI.Denotation.Arithmetic

TauLib.Denotation.Arithmetic

Earned arithmetic: addition, multiplication, exponentiation, and tetration derived from the iterator ρ.

Registry Cross-References

  • [I.D10] Index Addition — idx_add, idx_add_eq_nat_add

  • [I.D11] Index Multiplication — idx_mul, idx_mul_eq_nat_mul

  • [I.D12] Index Exponentiation — idx_exp, idx_exp_eq_nat_pow

  • [I.D13] Index Tetration — idx_tetration

  • [I.P05] Arithmetic Injectivity — idx_add_injective, idx_mul_injective, idx_exp_injective

  • [I.P06] Arithmetic Laws — idx_add_comm, idx_add_assoc, idx_mul_comm, etc.

Ground Truth Sources

  • chunk_0057_M000678: Multiplication as stride iteration of ρ

  • chunk_0060_M000698: UR-ITER requirement, arithmetic from ρ without algebraic substrate

  • chunk_0052_M000622: Binary operators derived, not primitive

Mathematical Content

The key insight: arithmetic is NOT imported but earned from ρ iteration.

  • Addition: n + m = depth of ρᵐ(⟨α, n⟩)

  • Multiplication: n × m = iterated addition

  • Exponentiation: n ^ m = iterated multiplication

  • Tetration: ⁿm = iterated exponentiation

The “bridge lemmas” prove each coincides with the Nat operation.

Tau.Denotation.idx_add

source def Tau.Denotation.idx_add (n m : TauIdx) :TauIdx

[I.D10] Index addition: the depth after m applications of ρ to ⟨α, n⟩. This earns addition from the iterator. Equations

  • Tau.Denotation.idx_add n m = (Tau.Orbit.iter_rho m (Tau.Denotation.toAlphaOrbit n)).depth Instances For

Tau.Denotation.idx_add_eq_nat_add

source theorem Tau.Denotation.idx_add_eq_nat_add (n m : TauIdx) :idx_add n m = n + m

Bridge lemma: idx_add coincides with Nat.add.

Tau.Denotation.idx_mul

source def Tau.Denotation.idx_mul (n m : TauIdx) :TauIdx

[I.D11] Index multiplication: iterated addition. Equations

  • Tau.Denotation.idx_mul n 0 = 0
  • Tau.Denotation.idx_mul n (Nat.succ m_2) = Tau.Denotation.idx_add (Tau.Denotation.idx_mul n m_2) n Instances For

Tau.Denotation.idx_mul_eq_nat_mul

source theorem Tau.Denotation.idx_mul_eq_nat_mul (n m : TauIdx) :idx_mul n m = n * m

Bridge lemma: idx_mul coincides with Nat.mul.

Tau.Denotation.idx_exp

source def Tau.Denotation.idx_exp (n m : TauIdx) :TauIdx

[I.D12] Index exponentiation: iterated multiplication. Equations

  • Tau.Denotation.idx_exp n 0 = 1
  • Tau.Denotation.idx_exp n (Nat.succ m_2) = Tau.Denotation.idx_mul (Tau.Denotation.idx_exp n m_2) n Instances For

Tau.Denotation.idx_exp_eq_nat_pow

source theorem Tau.Denotation.idx_exp_eq_nat_pow (n m : TauIdx) :idx_exp n m = n ^ m

Bridge lemma: idx_exp coincides with Nat.pow.

Tau.Denotation.idx_tetration

source def Tau.Denotation.idx_tetration (n m : TauIdx) :TauIdx

[I.D13] Index tetration: iterated exponentiation (right-associative tower). ⁿm means n^(n^(n^…)) with m copies of n. Equations

  • Tau.Denotation.idx_tetration n 0 = 1
  • Tau.Denotation.idx_tetration n (Nat.succ m_2) = Tau.Denotation.idx_exp n (Tau.Denotation.idx_tetration n m_2) Instances For

Tau.Denotation.idx_tetration_eq

source theorem Tau.Denotation.idx_tetration_eq (n m : TauIdx) :idx_tetration n m = Orbit.tetration n m

Bridge lemma: idx_tetration matches the Nat tetration from Ladder.

Tau.Denotation.ladderOp_add_eq_idx

source theorem Tau.Denotation.ladderOp_add_eq_idx (n m : TauIdx) :Orbit.ladderOp Orbit.LadderLevel.add_level n m = idx_add n m

ladderOp at add_level coincides with earned idx_add.

Tau.Denotation.ladderOp_mul_eq_idx

source theorem Tau.Denotation.ladderOp_mul_eq_idx (n m : TauIdx) :Orbit.ladderOp Orbit.LadderLevel.mul_level n m = idx_mul n m

ladderOp at mul_level coincides with earned idx_mul.

Tau.Denotation.ladderOp_exp_eq_idx

source theorem Tau.Denotation.ladderOp_exp_eq_idx (n m : TauIdx) :Orbit.ladderOp Orbit.LadderLevel.exp_level n m = idx_exp n m

ladderOp at exp_level coincides with earned idx_exp.

Tau.Denotation.ladderOp_tet_eq_idx

source theorem Tau.Denotation.ladderOp_tet_eq_idx (n m : TauIdx) :Orbit.ladderOp Orbit.LadderLevel.tet_level n m = idx_tetration n m

ladderOp at tet_level coincides with earned idx_tetration.

Tau.Denotation.fold_chain

source theorem Tau.Denotation.fold_chain :(∀ (n m : TauIdx), idx_add n m = (Orbit.iter_rho m (toAlphaOrbit n)).depth) ∧ (∀ (n m : TauIdx), idx_mul n (m + 1) = idx_add (idx_mul n m) n) ∧ (∀ (n m : TauIdx), idx_exp n (m + 1) = idx_mul (idx_exp n m) n) ∧ ∀ (n m : TauIdx), idx_tetration n (m + 1) = idx_exp n (idx_tetration n m)

The Fold Chain Principle: each arithmetic level is obtained by structural recursion on the previous level. Ground truth: chunk_0060 (UR-ITER), chunk_0057 (counting = time).

Tau.Denotation.idx_add_comm

source theorem Tau.Denotation.idx_add_comm (n m : TauIdx) :idx_add n m = idx_add m n

Addition is commutative.

Tau.Denotation.idx_add_assoc

source theorem Tau.Denotation.idx_add_assoc (a b c : TauIdx) :idx_add (idx_add a b) c = idx_add a (idx_add b c)

Addition is associative.

Tau.Denotation.idx_add_zero

source theorem Tau.Denotation.idx_add_zero (n : TauIdx) :idx_add n 0 = n

Addition has identity 0.

Tau.Denotation.idx_zero_add

source theorem Tau.Denotation.idx_zero_add (n : TauIdx) :idx_add 0 n = n

Zero is a left identity for addition.

Tau.Denotation.idx_mul_comm

source theorem Tau.Denotation.idx_mul_comm (n m : TauIdx) :idx_mul n m = idx_mul m n

Multiplication is commutative.

Tau.Denotation.idx_mul_assoc

source theorem Tau.Denotation.idx_mul_assoc (a b c : TauIdx) :idx_mul (idx_mul a b) c = idx_mul a (idx_mul b c)

Multiplication is associative.

Tau.Denotation.idx_mul_one

source theorem Tau.Denotation.idx_mul_one (n : TauIdx) :idx_mul n 1 = n

Multiplication has identity 1.

Tau.Denotation.idx_one_mul

source theorem Tau.Denotation.idx_one_mul (n : TauIdx) :idx_mul 1 n = n

One is a left identity for multiplication.

Tau.Denotation.idx_mul_zero

source theorem Tau.Denotation.idx_mul_zero (n : TauIdx) :idx_mul n 0 = 0

Multiplication has absorbing element 0.

Tau.Denotation.idx_distrib

source theorem Tau.Denotation.idx_distrib (a b c : TauIdx) :idx_mul a (idx_add b c) = idx_add (idx_mul a b) (idx_mul a c)

Distributivity: a × (b + c) = a × b + a × c.

Tau.Denotation.idx_add_injective

source theorem Tau.Denotation.idx_add_injective (n : TauIdx) :Function.Injective (idx_add n)

[I.P05] Addition is injective in the second argument.

Tau.Denotation.idx_mul_injective

source **theorem Tau.Denotation.idx_mul_injective (n : TauIdx)

(hn : n > 0) :Function.Injective (idx_mul n)**

Multiplication by n > 0 is injective in the second argument.

Tau.Denotation.idx_exp_injective

source **theorem Tau.Denotation.idx_exp_injective (n : TauIdx)

(hn : n ≥ 2) :Function.Injective (idx_exp n)**

Exponentiation with base ≥ 2 is injective in the exponent.

Tau.Denotation.idx_exp_non_comm

source theorem Tau.Denotation.idx_exp_non_comm :¬∀ (n m : TauIdx), idx_exp n m = idx_exp m n

Exponentiation is not commutative (counterexample: 2^3 ≠ 3^2).