Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Finite exterior fields and the full posterior guard

Abstract

Finite exterior fields and the full posterior guard

Definition 1.1 (The erased-center finite exterior).

Lean statement: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/ErasedExteriorFiltration.window

Formalization. D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/ErasedExteriorFiltration.window (✓ std3).

Source. Repository-derived.

Commentary.

window(r,z) is the pair of original chronological Boolean blocks from -r through -1 and from one through r. The center coordinate is absent.

Definition 1.2 (The finite observation field).

Lean statement: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/ErasedExteriorFiltration.field

Formalization. D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/ErasedExteriorFiltration.field (✓ std3).

Source. Repository-derived.

Commentary.

field(r) is the sigma-algebra generated by window(r).

Definition 1.3 (One increasing exterior filtration).

Lean statement: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/ErasedExteriorFiltration.information

Formalization. D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/ErasedExteriorFiltration.information (✓ std3).

Source. Repository-derived.

Commentary.

information is the natural-indexed filtration of field(r) inside the original visible process field. The transition from r+1 to r deletes one outer coordinate on each side.

Theorem 1.4 (The full exterior is generated by these windows).

Lean statement: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/ErasedExteriorFiltration.full_field

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

Source. Repository-derived.

Commentary.

The supremum over all natural radii of field(r) equals the field generated by the pair of entire retained half-lines exterior. Both inclusions are proved through the actual original coordinate maps.

Definition 1.5 (The native finite exterior posterior).

Lean statement: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/ErasedExteriorFiltration.finiteMean

Formalization. D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/ErasedExteriorFiltration.finiteMean (✓ std3).

Source. Repository-derived.

Commentary.

For every finite stationary marked presentation theta, finiteMean(theta,r) is the native regular conditional probability of X0=true given window(r), evaluated at the actual observed pair, under visibleLaw(theta).

Theorem 1.6 (Actual full erasure excludes a uniform strict guard).

Lean statement: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/ErasedExteriorFiltration.no_uniform_exterior_guard

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

Source. Repository-derived.

Commentary.

For any finite stationary marked presentation whose actual full exterior posterior equals X0 almost surely, every event G of positive actual visible probability, epsilon>0 and starting radius r0, it is impossible that the native finiteMean(theta,r) belongs to [epsilon,1-epsilon] almost surely on G for every r>=r0. The proof uses the exact generated full field, the native conditional-distribution/conditional-expectation identity and almost-sure martingale convergence on that same measure.

References