RarePriorFiniteMonitor

Abstract

The monitor begins with the first paid Read. Its only count register is Fin 376 with saturation at 375. The block is six alpha bits followed by ten beta bits; the suffix is beta alpha, beta beta alpha alpha. An independent prefix grammar establishes exact whole-word recognition. The finite block position, suffix position, accepted state and sink hold no history.

Runtime is the original FiniteFields together with the monitor and one-shot mode. Every transaction first calls the original partial finiteStep. The legal-history projection keeps original Counts and payloadReturns in the source rather than in the observer. Third-write activation follows the original marker writer and bare snapshot latch.

G alpha completes; G beta enters Gbeta. Gbeta beta completes; Gbeta alpha executes the original return and disables special operation permanently. Seeds, early phases and other legal histories use the ordinary query row. Pending permits only matching Stop, and delivered permits neither Read nor Stop. Off-permission matrix rows grant no terminal Read.

Theorem 1.1 (whole word recognition).

$\forall (w : List Letter), (scanWord monitorInitial w = . accepted \Leftrightarrow \exists n : N, 375 \leq n \land w = blocks n + + latchWord)$

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

Source. Repository-derived.

Commentary.

The prefix invariant distinguishes complete blocks, incomplete blocks, suffix positions and the sink. Acceptance is equivalent to a complete word with at least 375 blocks.

Theorem 1.2 (runtime projection).

$\forall (z : Runtime), (\forall (ops : List Operation), ((runtimeExecute z ops) . map Runtime . fields = executeFinite z . fields ops))$

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

Source. Repository-derived.

Commentary.

Projecting every partial runtime execution to FiniteFields gives the original finite execution, including failures.

Theorem 1.3 (arbitrary legal projection).

$\forall (ops : List Operation), ((Legal ops) \Rightarrow ((runtimeRun ops) . map Runtime . fields = (run ops) . map (fun c \mapsto c . source . finiteFields)))$

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

Source. Repository-derived.

Commentary.

Original native prefix reconstruction identifies the finite fields for every legal paid operation history. Source counters remain external.

Theorem 1.4 (query mode classification).

$\forall (z : Runtime), ((queryMode z = . g \Leftrightarrow z . fields . control = . fourth (. active . p) \land z . mode = . g) \land (queryMode z = . gBeta \Leftrightarrow z . fields . control = . fourth (. active . beta) \land z . mode = . gBeta) \land (queryMode z = . ordinary \Leftrightarrow \neg (z . fields . control = . fourth (. active . p) \land z . mode = . g) \land \neg (z . fields . control = . fourth (. active . beta) \land z . mode = . gBeta)))$

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

Source. Repository-derived.

Commentary.

A special query requires its matching fourth-segment phase and one-shot mode. All other finite configurations use the ordinary row.

Theorem 1.5 (original latch activation).

$\forall (n : N), ((375 \leq n) \Rightarrow (runtimeRun (reads (blocks n + + latchWord)) = some ⟨ latchedFields, . accepted, . g ⟩ \land runtimeRun (reads (blocks n + + latchWord . take 5)) = some ⟨ beforeLatchFields, . suffix 4, . watching ⟩ \land beforeLatchFields . registers . snapshot = none \land latchedFields . registers . snapshot = some ⟨ 1, 1, 1 ⟩ \land finiteStep beforeLatchFields (. read 0) = some latchedFields))$

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

Source. Repository-derived.

Commentary.

The five-letter suffix prefix has no snapshot. The sixth original Read performs the third marker write and latches the snapshot before G becomes active.

Theorem 1.6 (special transactions).

$\forall (r : Registers), (\forall (mon : Monitor), (runtimeStep ⟨⟨ . fourth (. active . p), r ⟩, mon, . g ⟩ (. read 0) = some ⟨⟨ . fourth (. pending 0), writeMarker r 30 ⟩, scan mon 0, . ordinary ⟩ \land runtimeStep ⟨⟨ . fourth (. active . p), r ⟩, mon, . g ⟩ (. read 1) = some ⟨⟨ . fourth (. active . beta), r ⟩, scan mon 1, . gBeta ⟩ \land runtimeStep ⟨⟨ . fourth (. active . beta), r ⟩, mon, . gBeta ⟩ (. read 0) = some ⟨⟨ . fourth (. active . p), r ⟩, scan mon 0, . ordinary ⟩ \land runtimeStep ⟨⟨ . fourth (. active . beta), r ⟩, mon, . gBeta ⟩ (. read 1) = some ⟨⟨ . fourth (. pending 1), writeMarker r 31 ⟩, scan mon 1, . ordinary ⟩))$

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

Source. Repository-derived.

Commentary.

The four original active transitions give the two special completions, the Gbeta continuation and the return that selects ordinary mode.

Theorem 1.7 (terminal permissions).

$\forall (r : Registers), (\forall (mon : Monitor), (\forall (m : Mode), (\forall (a b x : Letter), (runtimeStep ⟨⟨ . fourth (. pending a), r ⟩, mon, m ⟩ (. read x) = none \land (runtimeStep ⟨⟨ . fourth (. pending a), r ⟩, mon, m ⟩ (. stop b)) . map Runtime . fields = (if b = a then some ⟨ . fourth . delivered, r ⟩ else none) \land runtimeStep ⟨⟨ . fourth . delivered, r ⟩, mon, m ⟩ (. read x) = none \land runtimeStep ⟨⟨ . fourth . delivered, r ⟩, mon, m ⟩ (. stop b) = none))))$

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

Source. Repository-derived.

Commentary.

Pending admits exactly its matching Stop. Pending and delivered reject every Read; delivered also rejects every Stop.

Theorem 1.8 (exhaustive history modes).

$\forall (ops : List Operation), (\forall (z : Runtime), ((runtimeRun ops = some z) \Rightarrow ((z . mode = . g \Rightarrow \exists n, 375 \leq n \land ops = reads (blocks n + + latchWord)) \land (z . mode = . gBeta \Rightarrow \exists n, 375 \leq n \land ops = reads (blocks n + + latchWord + + [1])) \land ((\neg\exists n, 375 \leq n \land ops = reads (blocks n + + latchWord)) \Rightarrow (\neg\exists n, 375 \leq n \land ops = reads (blocks n + + latchWord + + [1])) \Rightarrow queryMode z = . ordinary))))$

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

Source. Repository-derived.

Commentary.

The history invariant restricts G and Gbeta to the recognized whole word and its single beta continuation. Every other successful history queries the ordinary row.

Theorem 1.9 (special return permanence).

$\forall (r : Registers), (\forall (mon : Monitor), (\forall (ops : List Operation), (\forall (d : Runtime), ((runtimeExecute ⟨⟨ . fourth (. active . beta), r ⟩, mon, . gBeta ⟩ (. read 0 :: ops) = some d) \Rightarrow (d . mode = . ordinary)))))$

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

Source. Repository-derived.

Commentary.

Ordinary mode is invariant under every subsequent successful transaction, including the suffix after the original Gbeta alpha return.

trureturing — Discovering truth

RarePriorFiniteMonitor

Abstract

References

Keyboard shortcuts

trureturing — Discovering truth

RarePriorFiniteMonitor

Abstract

References