StationaryHistorySlotGraph
Abstract
Original single-collision slot conditions extract actual marked parent and child histories.
Theorem 1.1 (The actual unique single collision).
Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Algorithms/StationaryHistorySlotGraph.single_collision_rows (✓ std3). ∎
Source. Repository-derived.
Commentary.
When J=s=1, exactly one actual target has two binary parents. Their two distinct source rows each supply two child digits in a three-digit target, so they intersect. The whole incoming surplus is spent at that shared slot w. Every other slot has at most one incoming edge. The actual resolving-row count is one, selecting v.
Theorem 1.2 (Actual histories from unmarked slot conditions).
Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Algorithms/StationaryHistorySlotGraph.prescribed_of_single_collision (✓ std3). ∎
Source. Repository-derived.
Commentary.
Prescribed contains actual binary parents A,B, a binary history H and unary history K on w, and their unary children H1,K1 on v. In the displayed formula Ha and Ka denote H1 and K1. UnmarkedShape is the following fully quantified source condition: the unique collision slot is producing, differs from the pure resolving slot, every nonbinary history on the collision slot is a singleton, and every history on the resolving slot is a singleton. J=Xi=1 gives total history surplus two, so these two doubled rows exhaust all repeated histories. The selected binary source rows and actual outgoing edges determine the marked parent and child relationships. Their literal waits agree on each common source row, their physical supports are disjoint, and resolving children have different actual digits. The producing history may itself be one of A,B; neither acyclicity nor a different producing target is required.