RarePriorGeneratedLaw

Abstract

RarePriorGeneratedLaw

The decoder accepts only Runtime and the fixed installed service semantics. A marked trajectory records the same deterministic runtime update and selected threshold. Complete infinite-path restart, event-block deletion, and terminal branches establish the configuration residual law. Original history conditioning uses the published source/private product law and a deterministic actual row. No interpreter budget or broad COMPLETE membership is asserted here.

Theorem 1.1 (terminal path invariance).

$\forall (z : Runtime), ((\exists b, z . fields . control = . fourth (. pending b)) \lor z . fields . control = . fourth . delivered) \Rightarrow \forall (p q : Nat \Rightarrow Marked), renderPath z p = renderPath z q$

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

Source. Repository-derived.

Commentary.

The statement retains the complete original telescope and conditions.

Theorem 1.2 (terminal Dirac law).

$\forall (z : Runtime), ((\exists b, z . fields . control = . fourth (. pending b)) \lor z . fields . control = . fourth . delivered) \Rightarrow decoder z = Measure . dirac (renderPath z (fun_{\mapsto} (z, 0)))$

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

Source. Repository-derived.

Commentary.

The statement retains the complete original telescope and conditions.

Theorem 1.3 (fields measurable).

$\forall (f : FiniteFields), (Measurable (fieldsTranscript f))$

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

Source. Repository-derived.

Commentary.

The statement retains the complete original telescope and conditions.

Theorem 1.4 (conditioned read path).

$\forall (z : Runtime), (\forall (x : Letter), ((ProbabilityTheory . cond (pathLaw z) {p ∣ p 0 = (z, x)}) . map (fun p n \mapsto p (n + 1)) = pathLaw (readAdvance z x)))$

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

Source. Repository-derived.

Commentary.

The statement retains the complete original telescope and conditions.

Theorem 1.5 (first measurable).

$Measurable firstOperation$

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

Source. Repository-derived.

Commentary.

The statement retains the complete original telescope and conditions.

Theorem 1.6 (generated read compatibility).

$\forall (z : Runtime), ((\forall x, finiteOperation z . fields x = some (. read x)) \Rightarrow ((\forall x, \exists d, runtimeStep z (. read x) = some d) \Rightarrow (\forall (x : Letter), ((decoder z) {t ∣ firstOperation t = some (. read x)} = (bernoulliMeasure (0 : Letter) 1 (emissionParameter z)) {x} \land (ProbabilityTheory . cond (decoder z) {t ∣ firstOperation t = some (. read x)}) . map deleteBlock = decoder (readAdvance z x)))))$

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

Source. Repository-derived.

Commentary.

The statement retains the complete original telescope and conditions.

Theorem 1.7 (configuration compatibility).

$\forall (z : Runtime), (((\forall b, z . fields . control \neq = . fourth (. pending b)) \Rightarrow z . fields . control \neq = . fourth . delivered \Rightarrow \forall x : Letter, (decoder z) {t ∣ firstOperation t = some (. read x)} = (bernoulliMeasure (0 : Letter) 1 (emissionParameter z)) {x} \land (ProbabilityTheory . cond (decoder z) {t ∣ firstOperation t = some (. read x)}) . map deleteBlock = decoder (readAdvance z x)) \land (\forall b : Letter, z . fields . control = . fourth (. pending b) \Rightarrow (decoder z) {t ∣ firstOperation t = some (. stop b)} = 1 \land (ProbabilityTheory . cond (decoder z) {t ∣ firstOperation t = some (. stop b)}) . map deleteBlock = decoder ((runtimeStep z (. stop b)) . getD z)) \land (z . fields . control = . fourth . delivered \Rightarrow decoder z = Measure . dirac (renderPath z (fun anonymous_{anonymous} \mapsto (z, 0))) \land (decoder z) {t ∣ firstOperation t = none} = 1 \land \forall (p : Nat \Rightarrow Marked) (n : Nat), renderPath z p (n + 1) = none))$

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

Source. Repository-derived.

Commentary.

The statement retains the complete original telescope and conditions.

Theorem 1.8 (generated full law).

$\forall (z : Runtime), (IsProbabilityMeasure (decoder z) \land 0 < (emissionParameter z : Real) \land (emissionParameter z : Real) < 1 \land returnedAlphaMass (selectedThreshold z) = (emissionParameter z : Real) \land (\forall (n : Nat) (w : Fin (n + 1) \Rightarrow Marked), ((pathLaw z) . map fun p (i : Fin (n + 1)) \mapsto p i . val) {w} = markedInitial z {w 0} * product i : Fin n, markedKernel (w i . castSucc) {w i . succ}) \land (\forall (p : Nat \Rightarrow Marked), (p 0) .1 = z \Rightarrow (\forall n, (p (n + 1)) .1 = readAdvance (p n) .1 (p n) .2) \Rightarrow (\forall n, (p n) .1 = readFold z (fun k \mapsto (p k) .2) n) \land \forall c : AcquiredNativeState, c . source . finiteFields = z . fields \Rightarrow renderPath z p = fullTranscript c (fun k \mapsto (p k) .2)) \land (AE p law pathLaw z, (p 0) .1 = z \land \forall n, (p (n + 1)) .1 = readAdvance (p n) .1 (p n) .2))$

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

Source. Repository-derived.

Commentary.

The statement retains the complete original telescope and conditions.

Theorem 1.9 (history marginal compatibility).

$\forall (mu : PMF NativeConditionalControl . DepthLaw . Depth), (\forall (h : List Operation), (\forall (c : AcquiredNativeState), (\forall (hc : run h = some c), ((ProbabilityTheory . cond (NativeObserverJointLaw . actualLaw actualObserver mu h . length) (NativeConditionalControl . DepthLaw . nativeEvent h c setProduct Set . univ)) . map (Prod . map (fun t : NativeConditionalControl . DepthLaw . Depth \times Stream \mapsto (t .1, rawTail t .2 (readLetters h) . length)) id) = (NativeConditionalControl . DepthLaw . jointLaw (NativeConditionalControl . DepthLaw . posterior mu h c hc)) . prod (NativeObserverJointLaw . row actualObserver h) . toMeasure \land \exists z : Runtime, runtimeRun h = some z \land z . fields = c . source . finiteFields \land NativeObserverJointLaw . row actualObserver h = PMF . pure z \land historyGenerated h = decoder z \land \forall (op : Operation) (d : AcquiredNativeState), nativeStep c op = some d \Rightarrow NativeObserverJointLaw . row actualObserver (h + + [op]) = actualUpdate op z \land (ProbabilityTheory . cond (historyGenerated h) {t ∣ firstOperation t = some op}) . map deleteBlock = historyGenerated (h + + [op])))))$

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

Source. Repository-derived.

Commentary.

The statement retains the complete original telescope and conditions.

References