Abstract

We prove a rail-dependent exponential lower bound on the number of normal-form- distinguishable proof states under persistent commutator defects, even after quotienting by canonicalization. We model a proof attempt as a trajectory in a proof-state space under a fixed rail (admissible move classes, a deterministic readout map ρR implementing a representative policy, and explicit resource bounds). Local proof moves are generally path-dependent (non-commutative). We encode this path-dependence as an indicator-valued proof curvature and propose a rail-relative horizon mechanism: beyond a curvature barrier, termination becomes obstructed within the rail, while provable approximants may persist. The resulting internal indistinguishability between “a proof exists but is unreachable under the rail” and “no admissible proof exists under the rail” is identified as proof-horizon behavior. Our main quantitative statement is a rail-dependent lower bound: if curvature occurs with density ε > 0 and the readout merging rate αR is finite, then for any δ > 0 and all sufficiently large k we have NR(k) ≥ exp((ε log 2 − αR − δ)k) (in particular when ε log 2 > αR).