TauLib.BookII.Topology.Invariant

Topology uniqueness: the profinite topology is the unique compact Hausdorff topology compatible with CRT reductions.

Registry Cross-References

• [II.T10] Topology Uniqueness — topology_unique_check

Mathematical Content

The cylinder topology is the initial (coarsest) topology making all CRT reduction maps π_k : τ³ → ℤ/M_kℤ continuous.

Theorem (II.T10): This is the UNIQUE topology on τ³ satisfying: (a) CRT continuity: all π_k continuous (b) Hausdorff separation (c) Compactness

Proof: Any compact Hausdorff topology containing the initial topology equals it (continuous bijection from compact to Hausdorff is homeomorphism).

Consequence: topology is earned (invariant of denotation), not chosen.

Tau.BookII.Topology.crt_continuous_check

source def Tau.BookII.Topology.crt_continuous_check (k bound : Denotation.TauIdx) :Bool

CRT reduction maps preserve cylinder structure: if y ∈ C_k(x), then π_l(y) ∈ C_l(π_l(x)) for all l ≤ k. This is the cylinder-theoretic definition of continuity. Equations

• Tau.BookII.Topology.crt_continuous_check k bound = Tau.BookII.Topology.crt_continuous_check.go k bound 2 2 ((bound + 1) * (bound + 1)) Instances For

Tau.BookII.Topology.crt_continuous_check.check_lower

source@[irreducible]

def Tau.BookII.Topology.crt_continuous_check.check_lower (x y k l fuel_l : Nat) :Bool

Check all lower stages preserve agreement. Equations

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

Tau.BookII.Topology.crt_continuous_check.go

source@[irreducible]

**def Tau.BookII.Topology.crt_continuous_check.go (k bound : Denotation.TauIdx)

(x y fuel : Nat) :Bool**

Equations

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

Tau.BookII.Topology.topology_unique_check

source def Tau.BookII.Topology.topology_unique_check (bound db : Denotation.TauIdx) :Bool

[II.T10] Topology uniqueness verification. The cylinder topology satisfies all three conditions: (a) CRT continuous, (b) Hausdorff, (c) compact. Any topology satisfying all three must equal the cylinder topology. Equations

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

Tau.BookII.Topology.reduction_compatible_check

source def Tau.BookII.Topology.reduction_compatible_check (bound : Denotation.TauIdx) :Bool

The reduction maps form a compatible family: reduce(reduce(x, l), k) = reduce(x, k) for k ≤ l. This is the defining property of an inverse system. Equations

• Tau.BookII.Topology.reduction_compatible_check bound = Tau.BookII.Topology.reduction_compatible_check.go bound 1 1 2 ((bound + 1) * 5 * 5) Instances For

Tau.BookII.Topology.reduction_compatible_check.go

source@[irreducible]

**def Tau.BookII.Topology.reduction_compatible_check.go (bound : Denotation.TauIdx)

(k l x fuel : Nat) :Bool**

Equations

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

Tau.BookII.Topology.crt_cont_k1

source theorem Tau.BookII.Topology.crt_cont_k1 :crt_continuous_check 1 20 = true

Tau.BookII.Topology.crt_cont_k2

source theorem Tau.BookII.Topology.crt_cont_k2 :crt_continuous_check 2 20 = true

Tau.BookII.Topology.topo_unique

source theorem Tau.BookII.Topology.topo_unique :topology_unique_check 12 5 = true

Tau.BookII.Topology.red_compat

source theorem Tau.BookII.Topology.red_compat :reduction_compatible_check 30 = true