From Relational Distinguishability to the Recurrence of Ticks: A Lean 4–Certified Construction

Reconstructions derive quantum theory from operational principles about states, measurements and probabilities. This paper asks what relational distinguishability alone forces before these exist, answering with a machine-checked construction: one admitted unit of distinguishability forces a recurring tick. Its one axiom: existence is relational distinguishability; every later object is generated from it, each numeral a theorem, no parameter is free. Persistence, that the unit remain re-identifiable as the same unit, is a forced standing requirement generated before any runtime succession of actual occurrences exists. Four theorems follow. A persistent closed history must differ from its reversal, forcing three channels. Their transfers generate a discrete internal geometry with residual share Ω = 1 − 𝜋/(3 √ 2). Handed to each owner, that share is carried without erasure while its unresolved account cannot terminate, so its tick recurs with no input of time or scheduling; the residual reaching its threshold posts an escapement, the complete closure that re-identifies it. The process has a fixed direction: records are retained, irrationality makes the residual recover the history, no reverse step licensed. Under interfaces proposed in two appendices, the derived counting structure reproduces, without probabilities, two reconstructions’ counts: quantum theory’s degrees of freedom at dimension three and its elementary system’s parameters. Physical measurement may be available in subsequent work, so long as the construction is specified for its application and quantities are read as dimensionless relations to one chosen standard candle; if that identification fails, the theory as a physical theory fails as a whole.