NativeControlConjugacy
Abstract
NativeControlConjugacy
The native interpreter carries a complete control, an update epoch, one actual Source, and an appended chronological Event list. A control equivalence changes only the complete control. mapOp preserves localStep, the entire Read literal and reply continuation, applyRho, and the fixed Stop payload. reindex decodes an installed control through the inverse equivalence and applies this instruction map. mapConfig leaves the epoch, actual source and full log untouched.
advance is nativeStep on an optional configuration and keeps none absorbing. Its n-fold iteration counts n chronological actions, including all root Reads. Remaining means that an actual finite Run reaches its first Stop after exactly n actions. The interpreter is deterministic: two terminating runs from the same control, epoch and actual source have the same event list and payload.
CostModel assigns a cost to each complete address, each raw Read response and the constant Update acknowledgement. Its five coordinates are primitive calls, Reads, Updates, address costs and response costs. Each Read contributes one primitive and one Read; each Update contributes one primitive and one Update. localStep contributes zero to these five primitive coordinates while remaining in the event trace. In a program with zero internal actions, remaining actions and remaining primitives agree. No absolute application-specific bill is asserted.
Theorem 1.1 (Exact native conjugacy).
Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/NativeControlConjugacy.native_control_conjugacy (✓ std3). ∎
Source. Repository-derived.
Commentary.
Induction on the actual finite Run preserves every event and the Stop payload. A separate one-step calculation preserves the source successor and appended event. Equal-step iteration gives exact finite prefixes, including empty reachability fibers. The inverse control equivalence supplies both implications. NativeSerialDepth.run_unique compares any two terminating runs from the same control, epoch and source. Applying that result after inverse run transport gives equality of the chronological traces and fixed halt payloads, and hence equality of all five charged coordinates even when the two traces are supplied independently.