TauLib · API Book III

TauLib.BookIII.Spectral.CRT

TauLib.BookIII.Spectral.CRT

CRT Decomposition Theorem at spectral level, Reconstruction Functor, and Independence of Prime-Level Actions.

Registry Cross-References

  • [III.T10] CRT Decomposition Theorem – crt_spectral_check

  • [III.D20] Reconstruction Functor – reconstruction_functor_check

  • [III.P05] Independence of Prime-Level Actions – prime_independence_check

Mathematical Content

III.T10 (CRT Decomposition): τ-native Chinese Remainder Theorem: ℤ/Prim(k)ℤ ≅ ∏ᵢ₌₁ᵏ ℤ/pᵢℤ proved constructively without signed arithmetic. CRT = algebraic Euler product.

III.D20 (Reconstruction Functor): CRT defines a functor R_k from ∏(ℤ/pᵢℤ-Mod) to ℤ/Prim(k)ℤ-Mod. This functor is an equivalence.

III.P05 (Prime Independence): Prime-level actions T^(i) on ℤ/pᵢℤ are independent. CRT guarantees unique reassembly.

Tau.BookIII.Spectral.crt_spectral_check

source def Tau.BookIII.Spectral.crt_spectral_check (bound db : Denotation.TauIdx) :Bool

[III.T10] CRT spectral decomposition at enriched level. Verifies that crt_decompose ∘ crt_reconstruct = id at each primorial level, enriched by tower coherence. Equations

  • Tau.BookIII.Spectral.crt_spectral_check bound db = Tau.BookIII.Spectral.crt_spectral_check.go bound db 0 1 ((bound + 1) * (db + 1)) Instances For

Tau.BookIII.Spectral.crt_spectral_check.go

source@[irreducible]

**def Tau.BookIII.Spectral.crt_spectral_check.go (bound db : Denotation.TauIdx)

(x k fuel : ℕ) :Bool**

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookIII.Spectral.crt_add_check

source def Tau.BookIII.Spectral.crt_add_check (bound db : Denotation.TauIdx) :Bool

[III.T10] CRT ring homomorphism: addition is preserved. Equations

  • Tau.BookIII.Spectral.crt_add_check bound db = Tau.BookIII.Spectral.crt_add_check.go bound db 0 0 1 ((bound + 1) * (bound + 1) * (db + 1)) Instances For

Tau.BookIII.Spectral.crt_add_check.go

source@[irreducible]

**def Tau.BookIII.Spectral.crt_add_check.go (bound db : Denotation.TauIdx)

(x y k fuel : ℕ) :Bool**

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookIII.Spectral.crt_add_check.go_components

source@[irreducible]

**def Tau.BookIII.Spectral.crt_add_check.go_components (rx ry rsum : List Denotation.TauIdx)

(i k : ℕ) :Bool**

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookIII.Spectral.crt_mul_check

source def Tau.BookIII.Spectral.crt_mul_check (bound db : Denotation.TauIdx) :Bool

[III.T10] CRT ring homomorphism: multiplication is preserved. Equations

  • Tau.BookIII.Spectral.crt_mul_check bound db = Tau.BookIII.Spectral.crt_mul_check.go bound db 0 0 1 ((bound + 1) * (bound + 1) * (db + 1)) Instances For

Tau.BookIII.Spectral.crt_mul_check.go

source@[irreducible]

**def Tau.BookIII.Spectral.crt_mul_check.go (bound db : Denotation.TauIdx)

(x y k fuel : ℕ) :Bool**

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookIII.Spectral.crt_mul_check.go_mul_components

source@[irreducible]

**def Tau.BookIII.Spectral.crt_mul_check.go_mul_components (rx ry rprod : List Denotation.TauIdx)

(i k : ℕ) :Bool**

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookIII.Spectral.reconstruction_functor_check

source def Tau.BookIII.Spectral.reconstruction_functor_check (bound db : Denotation.TauIdx) :Bool

[III.D20] Reconstruction functor R_k: given residues, reconstruct the unique element mod Prim(k). Checks that R_k is inverse to S_k (the restriction/decomposition functor). Equations

  • Tau.BookIII.Spectral.reconstruction_functor_check bound db = Tau.BookIII.Spectral.reconstruction_functor_check.go bound db 0 1 ((bound + 1) * (db + 1)) Instances For

Tau.BookIII.Spectral.reconstruction_functor_check.go

source@[irreducible]

**def Tau.BookIII.Spectral.reconstruction_functor_check.go (bound db : Denotation.TauIdx)

(x k fuel : ℕ) :Bool**

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookIII.Spectral.reconstruction_tower_check

source def Tau.BookIII.Spectral.reconstruction_tower_check (bound db : Denotation.TauIdx) :Bool

[III.D20] Reconstruction functor respects tower: R_{k+1} projects to R_k under reduce. Equations

  • Tau.BookIII.Spectral.reconstruction_tower_check bound db = Tau.BookIII.Spectral.reconstruction_tower_check.go bound db 0 1 ((bound + 1) * (db + 1)) Instances For

Tau.BookIII.Spectral.reconstruction_tower_check.go

source@[irreducible]

**def Tau.BookIII.Spectral.reconstruction_tower_check.go (bound db : Denotation.TauIdx)

(x k fuel : ℕ) :Bool**

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookIII.Spectral.prime_independence_check

source def Tau.BookIII.Spectral.prime_independence_check (bound db : Denotation.TauIdx) :Bool

[III.P05] Prime-level independence: modifying one residue does not affect others. The CRT structure guarantees orthogonality. Equations

  • Tau.BookIII.Spectral.prime_independence_check bound db = Tau.BookIII.Spectral.prime_independence_check.go bound db 0 1 0 ((bound + 1) * (db + 1) * (db + 1)) Instances For

Tau.BookIII.Spectral.prime_independence_check.go

source@[irreducible]

**def Tau.BookIII.Spectral.prime_independence_check.go (bound db : Denotation.TauIdx)

(x k i fuel : ℕ) :Bool**

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookIII.Spectral.prime_independence_check.check_off_diag

source@[irreducible]

**def Tau.BookIII.Spectral.prime_independence_check.check_off_diag (residues : List Denotation.TauIdx)

(i j k : ℕ) :Bool**

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookIII.Spectral.crt_spectral_20_4

source theorem Tau.BookIII.Spectral.crt_spectral_20_4 :crt_spectral_check 20 4 = true

Tau.BookIII.Spectral.crt_add_10_3

source theorem Tau.BookIII.Spectral.crt_add_10_3 :crt_add_check 10 3 = true

Tau.BookIII.Spectral.crt_mul_10_3

source theorem Tau.BookIII.Spectral.crt_mul_10_3 :crt_mul_check 10 3 = true

Tau.BookIII.Spectral.reconstruction_20_4

source theorem Tau.BookIII.Spectral.reconstruction_20_4 :reconstruction_functor_check 20 4 = true

Tau.BookIII.Spectral.reconstruction_tower_20_4

source theorem Tau.BookIII.Spectral.reconstruction_tower_20_4 :reconstruction_tower_check 20 4 = true

Tau.BookIII.Spectral.prime_independence_5_4

source theorem Tau.BookIII.Spectral.prime_independence_5_4 :prime_independence_check 5 4 = true

Tau.BookIII.Spectral.crt_roundtrip_42

source theorem Tau.BookIII.Spectral.crt_roundtrip_42 :Polarity.crt_reconstruct (Polarity.crt_decompose 42 3) 3 = Polarity.reduce 42 3

[III.T10] Structural: CRT round-trip at depth 3 for x = 42.

Tau.BookIII.Spectral.crt_decompose_42

source theorem Tau.BookIII.Spectral.crt_decompose_42 :Polarity.crt_decompose 42 3 = [0, 0, 2]

[III.T10] Structural: CRT decomposes 42 mod 30 = 12 into (12 mod 2, 12 mod 3, 12 mod 5) = (0, 0, 2).

Tau.BookIII.Spectral.crt_basis_0_3

source theorem Tau.BookIII.Spectral.crt_basis_0_3 :Polarity.crt_decompose (Polarity.crt_basis 3 0) 3 = [1, 0, 0]

[III.P05] Structural: CRT basis element 0 at depth 3 has residue 1 mod 2, 0 mod 3, 0 mod 5.