Charged installation and unary event addressing

Abstract

RarePriorLiteralController.TransfersAddress

Installation and address execution charge the image, retained snapshot and active controls together. The unary key and frame offset select a bit of the installed original event row; the proofs preserve concurrent context through each literal instruction cut.

Theorem 1.1 (Charged literal installation and frame transfer).

$$\forall (s:\mathrm{TransferSnapshot}),((\mathrm{Function}.\mathrm{Injective}(\mathrm{transferCode}))\wedge (((\forall (q:\mathrm{TransferSnapshot}),(\mathrm{programImage}).\mathrm{length}+(\mathrm{motorStaticImage}).\mathrm{length}+(\mathrm{transferCode}(q)).\mathrm{length}<\mathrm{literalTransferBound})\wedge (((\forall (\mathrm{ticks}:\mathbb{N}),((((\mathrm{literalInstallStep}{)}^{[\mathrm{ticks}]}\mathrm{literalInstallStart}(s)).\mathrm{base}=(s).\mathrm{base})\wedge (((((\mathrm{literalInstallStep}{)}^{[\mathrm{ticks}]}\mathrm{literalInstallStart}(s)).\mathrm{header}=(s).\mathrm{header})\wedge (((((\mathrm{literalInstallStep}{)}^{[\mathrm{ticks}]}\mathrm{literalInstallStart}(s)).\mathrm{frame}=(s).\mathrm{frame})\wedge (((\exists (m:\mathbb{N}),\mathrm{HeadControl}(((\mathrm{literalInstallStep}{)}^{[\mathrm{ticks}]}\mathrm{literalInstallStart}(s)).\mathrm{installation},m))\wedge ((((((\mathrm{literalInstallStep}{)}^{[\mathrm{ticks}]}\mathrm{literalInstallStart}(s)).\mathrm{installation}).\mathrm{pc}\ne \mathrm{MotorPC}.\mathrm{fault})\wedge ((((\mathrm{literalInstallStep}{)}^{[\mathrm{ticks}]}\mathrm{literalInstallStart}(s)).\mathrm{installation}).\mathrm{pc}\ne \mathrm{MotorPC}.\mathrm{halt}\to \mathrm{motorRank}((\mathrm{literalInstallStep}((\mathrm{literalInstallStep}{)}^{[\mathrm{ticks}]}\mathrm{literalInstallStart}(s))).\mathrm{installation})<\mathrm{motorRank}(((\mathrm{literalInstallStep}{)}^{[\mathrm{ticks}]}\mathrm{literalInstallStart}(s)).\mathrm{installation}))))))))))))\wedge (((\forall (m:\mathbb{N}),\forall (\mathrm{hm}:m\le \mathrm{programWidth}),\forall (r:\mathbb{N}),((\mathrm{literalInstallStep}{)}^{[\mathrm{motorTime}(m)+r]}\mathrm{literalInstallStart}(s)).\mathrm{installation}=\mathrm{motorRun}(\mathrm{programTape},\mathrm{motorCheckpoint}(\mathrm{programTape},m,\mathrm{hm}),r))\wedge ((((((\mathrm{literalInstallStep}{)}^{[\mathrm{motorTime}(\mathrm{programWidth})]}\mathrm{literalInstallStart}(s)).\mathrm{installation}).\mathrm{tape}=\mathrm{programTape})\wedge (((\forall (\mathrm{slot}:\mathrm{Fin}(6)),\mathrm{motorTrace}(\mathrm{literalInstalledFrameROM}((\mathrm{literalInstallStep}{)}^{[\mathrm{motorTime}(\mathrm{programWidth})]}\mathrm{literalInstallStart}(s),\mathrm{slot}),\mathrm{motorEntry}(\mathrm{frameWidth}),\mathrm{motorTime}(\mathrm{frameWidth}))=\mathrm{bitCode}(\mathrm{frameCodec}(\mathrm{eventROM}(((((s).\mathrm{base}).\mathrm{retained}).\mathrm{pre}).\mathrm{fields},(((s).\mathrm{base}).\mathrm{retained}).\mathrm{operation},\mathrm{slot}))))\wedge (\mathrm{literalStreamedBlock}(((((s).\mathrm{base}).\mathrm{retained}).\mathrm{pre}).\mathrm{fields},(((s).\mathrm{base}).\mathrm{retained}).\mathrm{operation})=\mathrm{eventBlock}(((((s).\mathrm{base}).\mathrm{retained}).\mathrm{pre}).\mathrm{fields},(((s).\mathrm{base}).\mathrm{retained}).\mathrm{operation})))))))))))))$$

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorLiteralController/TransfersAddress.charged_literal_transfers (✓ std3). ∎

Source. Repository-derived.

Commentary.

The full attachment code is injective and bounded at every value. Every install cut preserves concurrent context, has a valid encoded head, excludes fault and decreases a deterministic rank. Paused installation matches exact motor checkpoints, the installed tape is the actual program image and selected row traces reproduce the original eventBlock.

Theorem 1.2 (Paid unary address and installed bit).

$$\forall (s:\mathrm{TransferSnapshot}),((\mathrm{Function}.\mathrm{Injective}(\mathrm{addressCode}))\wedge (((\forall (q:\mathrm{AddressState}),(\mathrm{programImage}).\mathrm{length}+(\mathrm{addressStaticImage}).\mathrm{length}+(\mathrm{addressCode}(q)).\mathrm{length}<\mathrm{literalAddressBound})\wedge (((\forall (a:\mathrm{Fin}(\mathrm{frameKeyWidth})),\forall (i:\mathrm{Fin}(\mathrm{frameWidth})),\forall (n:\mathbb{N}),(((\mathrm{addressRun}(\mathrm{addressEntry}(s,a,i),n)).\mathrm{outer}=s)\wedge ((((\mathrm{addressRun}(\mathrm{addressEntry}(s,a,i),n)).\mathrm{key}=(\mathrm{addressEntry}(s,a,i)).\mathrm{key})\wedge ((((\mathrm{addressRun}(\mathrm{addressEntry}(s,a,i),n)).\mathrm{offset}=(\mathrm{addressEntry}(s,a,i)).\mathrm{offset})\wedge (((((\mathrm{addressRun}(\mathrm{addressEntry}(s,a,i),n)).\mathrm{control}).\mathrm{pc}\ne \mathrm{AddressPC}.\mathrm{fault})\wedge (((\mathrm{addressRun}(\mathrm{addressEntry}(s,a,i),n)).\mathrm{control}).\mathrm{pc}\ne \mathrm{AddressPC}.\mathrm{returned}\to \mathrm{addressRank}(\mathrm{addressStep}(\mathrm{addressRun}(\mathrm{addressEntry}(s,a,i),n)))<\mathrm{addressRank}(\mathrm{addressRun}(\mathrm{addressEntry}(s,a,i),n)))))))))))\wedge (((\forall (a:\mathrm{Fin}(\mathrm{frameKeyWidth})),\forall (i:\mathrm{Fin}(\mathrm{frameWidth})),\exists (\mathrm{ticks}:\mathbb{N}),\exists (q:\mathrm{AddressState}),((\mathrm{addressRun}(\mathrm{addressEntry}(s,a,i),\mathrm{ticks})=q)\wedge (((((q).\mathrm{control}).\mathrm{pc}=\mathrm{AddressPC}.\mathrm{returned})\wedge ((((q).\mathrm{outer}=s)\wedge ((((((q).\mathrm{head}).\mathrm{probe}).\mathrm{val}=(\mathrm{addressIndex}(a,i)).\mathrm{val})\wedge (((((q).\mathrm{control}).\mathrm{latch}=((s).\mathrm{installation}).\mathrm{tape}\mathrm{addressIndex}(a,i))\wedge (\mathrm{ticks}\le \mathrm{addressTimeBound})))))))))))\wedge (\forall (\mathrm{slot}:\mathrm{Fin}(6)),\forall (i:\mathrm{Fin}(\mathrm{frameWidth})),\exists (\mathrm{ticks}:\mathbb{N}),\exists (q:\mathrm{AddressState}),((\mathrm{addressRun}(\mathrm{addressEntry}((\mathrm{literalInstallStep}{)}^{[\mathrm{motorTime}(\mathrm{programWidth})]}\mathrm{literalInstallStart}(s),\mathrm{frameKey}(s,\mathrm{slot}),i),\mathrm{ticks})=q)\wedge (((((q).\mathrm{control}).\mathrm{pc}=\mathrm{AddressPC}.\mathrm{returned})\wedge (((q).\mathrm{control}).\mathrm{latch}=\mathrm{frameTape}(\mathrm{eventROM}(((((s).\mathrm{base}).\mathrm{retained}).\mathrm{pre}).\mathrm{fields},(((s).\mathrm{base}).\mathrm{retained}).\mathrm{operation},\mathrm{slot}))i))))))))))))$$

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorLiteralController/TransfersAddress.charged_address_execution (✓ std3). ∎

Source. Repository-derived.

Commentary.

The complete address-state code is injective and fits a fixed image-plus-state bound at every value. Every cut preserves the outer snapshot and raw input tapes, excludes fault and decreases an external deterministic rank until return. For every finite unary key and offset, the actual carry and branch run returns the selected installed bit, and proved literal installation identifies each selected event-frame bit with the original eventROM.

References

• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorLiteralController/TransfersAddress.charged_address_execution
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorLiteralController/TransfersAddress.charged_literal_transfers
• Dependency: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/NativeFullResidual
• Dependency: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorLiteralController/EncodedHead
• Dependency: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorResidentCode
• Dependency: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorSerialExecution