Native post-clock inverse
Abstract
Exact rational post-clock fields recover every finite legal native addressed word.
Source is the original Boolean free magma: true is alpha and false is beta. Material coordinates include each beta’s separate left marker. The original guarded Call runner promotes alpha at p or splits beta at p into the literal branch (beta,alpha). Promotion adds only pL. Splitting retains the old pL and adds only pLL and pR. The current endpoint consists of the term and a rational function on its explicitly listed finite material support.
For positive rational a and c, clock(a,c,t) is a times the identity plus c times the unit native material adjacency. Its determinant is assumed nonzero on every actual term reached by a finite legal word. Encoding starts at the earned alpha field 1, and each successful letter performs actual zero inclusion followed by Tick on the new term. Replay is partial exactly through the original logical guard; no Reset, Add or extra Tick appears in this recurrence.
Theorem 1.1 (Complete reached-image inverse).
Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/OriginalVector/NativePostClockInverse.postclock_inverse (✓ std3). ∎
Source. Repository-derived.
Commentary.
For every finite successful addressed word, including the empty word, encoding exists on its actual final term and every material coordinate is strictly positive. Decode of that endpoint returns exactly that word. Decode followed by replay returns the input endpoint on the reached image, and equal encoded endpoints force equal words. At every further enabled event, the local predecessor returns exactly the original endpoint and event; its material size is strictly smaller.
Untick computes the rational reciprocal of the finite determinant times the adjugate, then multiplies the full finite field. It uses finite rational arithmetic. The zeros after Untick are exactly the last fresh support: a singleton pL for promotion or the pair pLL,pR for splitting. These signatures distinguish both the kind and the address. The current local subtree is tested against the literal replacement before selection. Collapse replaces beta by alpha or (beta,alpha) by beta and restricts the unticked field, retaining all old coordinates. Each fresh coordinate has an old neighbor, so the positive edge coefficient makes it positive after Tick; at old coordinates the positive diagonal suffices.
DecodeFuel uses the current material size as fuel. Each actual reverse step strictly reduces that size, and the empty origin returns the empty list. The runtime inputs are only the current native term, its full finite rational field, and a,c. Histories occur in correctness proofs and are absent from predecessor selection and decoder inputs. There is no off-image recognition assertion. The pre-clock construction and the common-source inverse outside this reached image are separate questions.