arXiv:2608.04228 · v4
Topological Computational Paths: Presentation Invariance and Observable Quotients
摘要
A computational path records the steps used to establish an equality. Topologies on computational equality witnesses can depend on the chosen generators and execution schedule, even when their algebraic and homotopical meanings agree. We study continuous presentations of finite computational paths whose declared rewrites are realized by endpoint-fixed homotopies. We compare a topology retaining the full signed trace with an observable topology recording endpoints, length, and exact path realization. Continuous finite-word interpretations that are inverse up to scoped rewriting preserve trace-sensitive quotient arrows and their final composable-pair spaces. Observable quotients behave differently. Over a point with a nonempty primitive alphabet, we classify their topology: it records length parity when all named relations preserve parity, and is otherwise indiscrete. Adjoining a conservative abbreviation can therefore turn a discrete two-element quotient into an indiscrete space, even though ordinary multiplication remains continuous. A circle presentation also gives nonhomeomorphic quotients under binary and equal-slot timing. Geometric completeness alone does not identify the trace-sensitive and observable topologies. Multiplication is continuous on the quotient of composable representatives. We characterize when this topology agrees with the ordinary pullback topology and give an open-projection criterion. Universal presentations recover classical fundamental-groupoid topology. Normal forms, primitive interchange, and a Cayley covering prove completeness for circle, torus, product, and rose presentations. A literal-word correspondence relates the semantics to the reflexivity, symmetry, and transitivity fragment of equality derivations. Selected results are formalized in Lean, with the realization models and proof coverage stated explicitly.
作者备注：34 pages, 10 figures. Substantially revised and retitled; expanded presentation-invariance results, observable-quotient counterexamples, and geometric completeness examples; clarified formalization scope. Lean artifact: https://github.com/Arthur742Ramos/TopologicalComputationalPaths