RarePriorResidentCode

Abstract

RarePriorResidentCode

Explicit mixed-radix codecs encode NativeControl, Registers, ThirdSnapshot, FiniteFields, the saturating monitor and one-shot mode. Their runtime has 793800 times 6023 times 4 addresses. A second explicit codec encodes the threshold tag, PC, bit position, candidate and output. Native dictionaries store every runtime-operation key and its original partial successor; service dictionaries store every service-bit key and microstep successor. A third resident dictionary initializes the threshold tag from the original finite query mode, using high for G, low for Gbeta and ordinary otherwise.

Resident code includes all three addressed key and payload tapes, the instruction records, and the saturation, threshold, acceptance and bit-width constants. The interpreter scans key bits sequentially and copies payload bits sequentially. Its row address, bit cursor, accumulator, PC and equality flag have fixed finite bounds. At the selected row, the exact copied payload implements the original runtimeStep or fair-bit microStep. The execution iteration count belongs to the correctness proof and is absent from runtime state.

The complete snapshot serializes ready and synthetic-copy runtimes, service state, current operation, 32 bounded output scratch cells, cursor, PC, table/source/destination addresses, bit position, matching flag and workspace. Fixed-width blocks make this encoding injective. B0 is one fixed witness greater than resident-code length plus complete snapshot width, with B0 at least one; it is independent of prior, horizon and rare mass. All scanner states fit the same snapshot fields. The scratch is a finite output workspace; full-record rendering is supplied separately.

Theorem 1.1 (Unary block width).

$$\forall (n:\mathbb{N}),\forall (x:\mathrm{Fin}n),(\mathrm{bitCode}x).\mathrm{length}=n$$

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorResidentCode.bit_code_length (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every finite address has the same fixed unary block width, including zero. The serial scanner controller uses this supplier to charge its complete local state.

Theorem 1.2 (Unary block recovery).

$$\forall (n:\mathbb{N}),\mathrm{Function}.\mathrm{Injective}(\mathrm{fun}x:\mathrm{Fin}n\mapsto \mathrm{bitCode}x)$$

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorResidentCode.bit_code_injective (✓ std3). ∎

Source. Repository-derived.

Commentary.

The unary block retains every finite address. The serial controller consumes this supplier in its complete local-state encoding.

Theorem 1.3 (charged snapshot bound).

$$\forall (s:\mathrm{MicroSnapshot}),((\mathrm{snapshotCode}s).\mathrm{length}=\mathrm{snapshotWidth}\wedge \mathrm{residentCode}.\mathrm{length}+(\mathrm{snapshotCode}s).\mathrm{length}<B0\wedge 1\le B0)$$

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorResidentCode.charged_snapshot_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

Each serialized field has fixed width. The budget is one plus resident width plus snapshot width and charges every stored tape and snapshot bit.

Theorem 1.4 (complete snapshot encoding).

$$\mathrm{Function}.\mathrm{Injective}\mathrm{snapshotCode}$$

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorResidentCode.complete_snapshot_encoding (✓ std3). ∎

Source. Repository-derived.

Commentary.

Fixed-width block boundaries recover every scalar field. Sequential recovery of the output blocks recovers the entire bounded output store.

Theorem 1.5 (bounded scanner correct).

$$\forall (kn:\mathbb{N}),(\forall (\mathrm{table}:\mathrm{Fin}k\Rightarrow \mathrm{Fin}n),(\forall (a:\mathrm{Fin}k),(\mathrm{scannerResult}(\mathrm{scannerTicks}\mathrm{table}(a.\mathrm{val}\ast (k+1)+k+1+n+1)(\mathrm{scannerEntry}a))=\mathrm{some}(\mathrm{table}a))))$$

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorResidentCode.bounded_scanner_correct (✓ std3). ∎

Source. Repository-derived.

Commentary.

The scanner skips unmatched key rows, reaches the queried row and copies its unary payload bit by bit into the bounded accumulator.

Theorem 1.6 (installed bounded program).

$$\forall (z:\mathrm{Runtime}),(\forall (\mathrm{op}:\mathrm{Operation}),(\forall (s:\mathrm{Service}),(\forall (b:\mathrm{Letter}),(\forall (\mathrm{base}:\mathrm{MicroSnapshot}),(\mathrm{nativeProgram}z\mathrm{op}=\mathrm{runtimeStep}z\mathrm{op}\wedge \mathrm{serviceProgram}sb=\mathrm{some}(\mathrm{microStep}sb)\wedge \mathrm{initializationProgram}z=\mathrm{some}(\mathrm{entry}(\mathrm{selectedThreshold}z))\wedge (\forall (kn:\mathbb{N})(\mathrm{hk}:k\le \mathrm{runtimeSize}\ast 4)(\mathrm{hn}:n\le \mathrm{runtimeSize}+1)(q:\mathrm{Scanner}kn),\mathrm{residentCode}.\mathrm{length}+(\mathrm{snapshotCode}(\mathrm{scannerSnapshot}\mathrm{base}q\mathrm{hk}\mathrm{hn})).\mathrm{length}<B0)\wedge (\forall (kn:\mathbb{N})(\mathrm{hk}:k\le \mathrm{runtimeSize}\ast 4)(\mathrm{hn}:n\le \mathrm{runtimeSize}+1),\mathrm{Function}.\mathrm{Injective}(\mathrm{fun}q:\mathrm{Scanner}kn\mapsto \mathrm{snapshotCode}(\mathrm{scannerSnapshot}\mathrm{base}q\mathrm{hk}\mathrm{hn})))\wedge (\forall (r:\mathrm{Registers})(\mathrm{mon}:\mathrm{Monitor})(m:\mathrm{Mode})(abx:\mathrm{Letter}),\mathrm{runtimeStep}⟨⟨.\mathrm{fourth}(.\mathrm{pending}a),r⟩,\mathrm{mon},m⟩(.\mathrm{read}x)=\mathrm{none}\wedge (\mathrm{runtimeStep}⟨⟨.\mathrm{fourth}(.\mathrm{pending}a),r⟩,\mathrm{mon},m⟩(.\mathrm{stop}b)).\mathrm{map}\mathrm{Runtime}.\mathrm{fields}=(\mathrm{if}b=a\mathrm{then}\mathrm{some}⟨.\mathrm{fourth}.\mathrm{delivered},r⟩\mathrm{else}\mathrm{none})\wedge \mathrm{runtimeStep}⟨⟨.\mathrm{fourth}.\mathrm{delivered},r⟩,\mathrm{mon},m⟩(.\mathrm{read}x)=\mathrm{none}\wedge \mathrm{runtimeStep}⟨⟨.\mathrm{fourth}.\mathrm{delivered},r⟩,\mathrm{mon},m⟩(.\mathrm{stop}b)=\mathrm{none}))))))$$

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorResidentCode.installed_bounded_program (✓ std3). ∎

Source. Repository-derived.

Commentary.

The three proved resident row relations implement original runtime updates, service microsteps and mode-based service initialization. Every scanner state has an injective charged snapshot encoding, and terminal permissions remain original.

References

• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorResidentCode.bit_code_injective
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorResidentCode.bit_code_length
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorResidentCode.bounded_scanner_correct
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorResidentCode.charged_snapshot_bound
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorResidentCode.complete_snapshot_encoding
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorResidentCode.installed_bounded_program
• Dependency: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorFairBitService