Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Exact normalization of capped semantic read rules

Abstract

Exact normalization of capped semantic read rules

A source is a phase phi and a two-sided Boolean spin sequence S. At the active integer address 2e+phi, the visible reply is the XOR of S(e) and S(e+1); separator replies are zero. The hidden value uses the original integer endpoint, including the negative seam. RawRule.next depends only on the unchanged seed and the ordered acquired record. Finite nonnegative waits are separate from a terminal nonreturn.

ReadTree has integer-labelled binary read nodes and leaves labelled by an optional hidden output. Execution retains the complete ordered address/reply record. paid is its length, so repeated and separator calls remain charged. A none leaf records nonreturn at its exact depth. TotalCap bounds the uncapped extended-natural paidCount on every phase, spin sequence and seed, including exceptional paths.

Theorem 1.1 (Exact suffix execution).

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/StoppingLaw/SemanticNormalization.unfold_correct (✓ std3). ∎

Source. Repository-derived.

Commentary.

Starting at any acquired record with at most k further calls, unfolding reaches the original terminal event with precisely the appended execution record. The induction is on the remaining call budget; a further read at budget zero contradicts the cap.

Theorem 1.2 (Pointwise preservation on every actual capped path).

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/StoppingLaw/SemanticNormalization.normalization_pointwise (✓ std3). ∎

Source. Repository-derived.

Commentary.

normalize unfolds from the empty record. Completes identifies its exact original terminal record, output and paid count. Return/nonreturn indicators agree as well: a finite number of finite waits remains finite. The height bound applies to every formal branch, with no padding of earlier terminals.

Theorem 1.3 (Measurable ordinary tree selector).

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/StoppingLaw/SemanticNormalization.measurable_normalize (✓ std3). ∎

Source. Repository-derived.

Commentary.

The finite tree type is countable and carries its discrete measurable structure. Measurability follows by induction through next-event decisions at countably many records.

Theorem 1.4 (One common ordinary version for seed completion).

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/StoppingLaw/SemanticNormalization.completion_normalization_bridge (✓ std3). ∎

Source. Repository-derived.

Commentary.

CappedTrees(k) is the subtype of trees of height at most k. One measurable selector agrees for almost every seed; on that common set it preserves every source execution. This statement does not assert pointwise agreement of arbitrary completed versions at every seed.

Theorem 1.5 (Exact recovery of a bounded tree family).

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/StoppingLaw/SemanticNormalization.normalize_realize (✓ std3). ∎

Source. Repository-derived.

Commentary.

realize follows the ordered acquired record, rejecting inconsistent addresses. When the supplied tree already has height at most k, normalization recovers it exactly.

Theorem 1.6 (Ordinary selector for ambient completed events).

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/StoppingLaw/SemanticNormalization.normalization_version (✓ std3). ∎

Source. Repository-derived.

Commentary.

CompletedRule allows source-dependent ambient-null versions of the available observation field. A single ordinary seed selector agrees product-almost everywhere. Separately, completed_normalization_execution preserves each actual completed execution under its all-path cap; that pointwise execution assertion is distinct from the almost-everywhere selector identity.

The normalization construction changes neither the seed space nor the actual read clock. It is a finite semantic unfolding and does not decide divergence of arbitrary programs.

References