Registry · Proposition III.P22 tau-effective formalized

III.P22 — CRT Witness Decomposition

Witness space at primorial depth k factors: W(x, Prim(k)) ≅ ∏ W(x, p_i). Each prime contributes independent 1D search. CRT guarantees reconstruction. Product of costs becomes sum of costs.

Book III Part 9 Ch. 57

Dependency Graph

Depends on (2)

Depended on by (3)

Lean Formalization

Module: TauLib.BookIII.Computation.WitnessSearch

Symbol: crt_witness_check