Finite observable sleeping suffix-variance certificates

This module rewrites the observable sleeping suffix-variance oracle for finite hypothesis PMFs. Posterior integrals, relative entropy, observable quadratic variation, geometric-atom excesses, and selected boundaries are all finite sums or ordinary real expressions. A second endpoint also expands each finite-state transition kernel into its supplied PMF table.

The exact selector minimizes over the admitted finite geometric prefix. It is not a coin-betting master or a parameter-free construction. The common event allows the posterior, wake, reporting time, and selector to depend on the observed path. Its target is the posterior-averaged conditional risk encountered on the selected suffix, not future, stationary, population, or deployment risk without an additional bridge.

Finite observable suffix quantities

noncomputable def FormalSLT.StochasticDynamics.finiteTrajectoryPosteriorSuffixPredictorQuadraticVariation {ι : Type u_1} {Z : Type u_2} [Fintype ι] (score : ι → TrajectoryScore Z) (posterior : ι → ℝ) (w n : ℕ) (x : ℕ → Z) : ℝ

Finite-posterior raw prediction-residual quadratic variation on [w,n). The forward predictor still uses the complete history before each k.

Equations

• One or more equations did not get rendered due to their size.

theorem FormalSLT.StochasticDynamics.continuousTrajectoryPosteriorSuffixPredictorQuadraticVariation_toPMF {ι : Type u_1} {Z : Type u_2} [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] (score : ι → TrajectoryScore Z) {posterior : ι → ℝ} (hposterior : PACBayesKL.IsPMF posterior) (w n : ℕ) (x : ℕ → Z) : continuousTrajectoryPosteriorSuffixPredictorQuadraticVariation score hposterior.toPMF.toMeasure w n x = finiteTrajectoryPosteriorSuffixPredictorQuadraticVariation score posterior w n x

Converting a finite posterior PMF to a measure changes no raw observable suffix quadratic variation.

theorem FormalSLT.StochasticDynamics.finiteTrajectoryPosteriorConstantTiltSuffixPredictorQuadraticPenalty_eq {ι : Type u_1} {Z : Type u_2} [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] (score : ι → TrajectoryScore Z) {posterior : ι → ℝ} (hposterior : PACBayesKL.IsPMF posterior) (lam : ℝ) (w n : ℕ) (x : ℕ → Z) : finiteTrajectoryPosteriorConstantTiltSuffixPredictorQuadraticPenalty score posterior (fun (x : ℕ) => lam) w n x = AnytimeValid.forwardEmpiricalBernsteinPsi lam * finiteTrajectoryPosteriorSuffixPredictorQuadraticVariation score posterior w n x

The finite constant-tilt penalty factors as psi(lambda) times the raw finite-posterior suffix quadratic variation.

theorem FormalSLT.StochasticDynamics.finiteTrajectoryPosteriorSuffixPredictorQuadraticVariation_mem_Icc {ι : Type u_1} {Z : Type u_2} [Fintype ι] (score : ι → TrajectoryScore Z) (hscore : ∀ (h : ι) (n : ℕ) (u : ↥(Finset.Iic n) → Z) (y : Z), score h n u y ∈ Set.Icc 0 1) {posterior : ι → ℝ} (hposterior : PACBayesKL.IsPMF posterior) {w n : ℕ} (hwn : w ≤ n) (x : ℕ → Z) : finiteTrajectoryPosteriorSuffixPredictorQuadraticVariation score posterior w n x ∈ Set.Icc 0 ↑(n - w)

Unit-bounded finite scores put the raw observable suffix quadratic variation between zero and the suffix length.

noncomputable def FormalSLT.StochasticDynamics.finiteTrajectorySleepingSuffixVarianceGeometricTiltExcess {ι : Type u_1} {Z : Type u_2} [Fintype ι] (prior posterior : ι → ℝ) (score : ι → TrajectoryScore Z) (delta : ℝ) (a w n : ℕ) (x : ℕ → Z) : ℝ

Finite KL plus the wake-adjusted geometric-atom confidence charge and raw observable suffix-variance penalty.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def FormalSLT.StochasticDynamics.finiteTrajectorySleepingSuffixVarianceGeometricTiltBoundary {ι : Type u_1} {Z : Type u_2} [Fintype ι] (prior posterior : ι → ℝ) (score : ι → TrajectoryScore Z) (delta : ℝ) (a w n : ℕ) (x : ℕ → Z) : ℝ

Finite posterior empirical suffix risk plus one observable geometric-atom excess.

Equations

• One or more equations did not get rendered due to their size.

theorem FormalSLT.StochasticDynamics.continuousTrajectorySleepingSuffixVarianceGeometricTiltExcess_toPMF {ι : Type u_1} {Z : Type u_2} [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] {prior posterior : ι → ℝ} (hprior : PACBayesKL.IsFullSupportPMF prior) (hposterior : PACBayesKL.IsPMF posterior) (score : ι → TrajectoryScore Z) (delta : ℝ) (a w n : ℕ) (x : ℕ → Z) : continuousTrajectorySleepingSuffixVarianceGeometricTiltExcess ⋯.toPMF.toMeasure hposterior.toPMF.toMeasure score delta a w n x = finiteTrajectorySleepingSuffixVarianceGeometricTiltExcess prior posterior score delta a w n x

A continuous-measure geometric excess is exactly the finite expression under a full-support finite prior.

theorem FormalSLT.StochasticDynamics.continuousTrajectorySleepingSuffixVarianceGeometricTiltBoundary_toPMF {ι : Type u_1} {Z : Type u_2} [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] {prior posterior : ι → ℝ} (hprior : PACBayesKL.IsFullSupportPMF prior) (hposterior : PACBayesKL.IsPMF posterior) (score : ι → TrajectoryScore Z) (delta : ℝ) (a w n : ℕ) (x : ℕ → Z) : continuousTrajectorySleepingSuffixVarianceGeometricTiltBoundary ⋯.toPMF.toMeasure hposterior.toPMF.toMeasure score delta a w n x = finiteTrajectorySleepingSuffixVarianceGeometricTiltBoundary prior posterior score delta a w n x

A continuous-measure geometric boundary is exactly the finite expression under finite prior and posterior PMFs.

Exact finite-prefix selector

def FormalSLT.StochasticDynamics.finiteTrajectorySleepingSuffixVarianceMaxIndex (w n : ℕ) : ℕ

Largest geometric atom admitted by the suffix length.

Equations

• FormalSLT.StochasticDynamics.finiteTrajectorySleepingSuffixVarianceMaxIndex w n = FormalSLT.StochasticDynamics.continuousTrajectorySleepingSuffixVarianceMaxIndex w n

noncomputable def FormalSLT.StochasticDynamics.finiteTrajectorySleepingSuffixVarianceFinitePrefixArgmin {ι : Type u_1} {Z : Type u_2} [Fintype ι] (prior posterior : ι → ℝ) (score : ι → TrajectoryScore Z) (delta : ℝ) (w n : ℕ) (x : ℕ → Z) : ℕ

Exact minimizer of the finite observable excess over the admitted geometric prefix.

Equations

• FormalSLT.StochasticDynamics.finiteTrajectorySleepingSuffixVarianceFinitePrefixArgmin prior posterior score delta w n x = Classical.choose ⋯

theorem FormalSLT.StochasticDynamics.finiteTrajectorySleepingSuffixVarianceFinitePrefixArgmin_mem {ι : Type u_1} {Z : Type u_2} [Fintype ι] (prior posterior : ι → ℝ) (score : ι → TrajectoryScore Z) (delta : ℝ) (w n : ℕ) (x : ℕ → Z) : finiteTrajectorySleepingSuffixVarianceFinitePrefixArgmin prior posterior score delta w n x ∈ Finset.range (finiteTrajectorySleepingSuffixVarianceMaxIndex w n + 1)

The finite selector belongs to the admitted geometric prefix.

theorem FormalSLT.StochasticDynamics.finiteTrajectorySleepingSuffixVarianceFinitePrefixArgmin_le {ι : Type u_1} {Z : Type u_2} [Fintype ι] (prior posterior : ι → ℝ) (score : ι → TrajectoryScore Z) (delta : ℝ) (w n : ℕ) (x : ℕ → Z) {a : ℕ} (ha : a ∈ Finset.range (finiteTrajectorySleepingSuffixVarianceMaxIndex w n + 1)) : finiteTrajectorySleepingSuffixVarianceGeometricTiltExcess prior posterior score delta (finiteTrajectorySleepingSuffixVarianceFinitePrefixArgmin prior posterior score delta w n x) w n x ≤ finiteTrajectorySleepingSuffixVarianceGeometricTiltExcess prior posterior score delta a w n x

The finite selector has no larger excess than any admitted atom.

noncomputable def FormalSLT.StochasticDynamics.finiteTrajectorySleepingSuffixVarianceSelectedExcess {ι : Type u_1} {Z : Type u_2} [Fintype ι] (prior posterior : ι → ℝ) (score : ι → TrajectoryScore Z) (delta : ℝ) (w n : ℕ) (x : ℕ → Z) : ℝ

Observable finite excess chosen by the exact finite-prefix selector.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def FormalSLT.StochasticDynamics.finiteTrajectorySleepingSuffixVarianceSelectedBoundary {ι : Type u_1} {Z : Type u_2} [Fintype ι] (prior posterior : ι → ℝ) (score : ι → TrajectoryScore Z) (delta : ℝ) (w n : ℕ) (x : ℕ → Z) : ℝ

Finite ordinary-risk endpoint chosen by the exact finite-prefix selector.

Equations

• One or more equations did not get rendered due to their size.

theorem FormalSLT.StochasticDynamics.finiteTrajectorySleepingSuffixVarianceSelectedBoundary_le {ι : Type u_1} {Z : Type u_2} [Fintype ι] (prior posterior : ι → ℝ) (score : ι → TrajectoryScore Z) (delta : ℝ) (w n : ℕ) (x : ℕ → Z) {a : ℕ} (ha : a ∈ Finset.range (finiteTrajectorySleepingSuffixVarianceMaxIndex w n + 1)) : finiteTrajectorySleepingSuffixVarianceSelectedBoundary prior posterior score delta w n x ≤ finiteTrajectorySleepingSuffixVarianceGeometricTiltBoundary prior posterior score delta a w n x

The selected finite boundary is no larger than every admitted geometric atom boundary.

theorem FormalSLT.StochasticDynamics.continuousTrajectorySleepingSuffixVarianceSelectedExcess_toPMF {ι : Type u_1} {Z : Type u_2} [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] {prior posterior : ι → ℝ} (hprior : PACBayesKL.IsFullSupportPMF prior) (hposterior : PACBayesKL.IsPMF posterior) (score : ι → TrajectoryScore Z) (delta : ℝ) (w n : ℕ) (x : ℕ → Z) : continuousTrajectorySleepingSuffixVarianceSelectedExcess ⋯.toPMF.toMeasure hposterior.toPMF.toMeasure score delta w n x = finiteTrajectorySleepingSuffixVarianceSelectedExcess prior posterior score delta w n x

The continuous and finite exact selectors may choose different minimizing indices, but their selected excess values agree.

theorem FormalSLT.StochasticDynamics.continuousTrajectorySleepingSuffixVarianceSelectedBoundary_toPMF {ι : Type u_1} {Z : Type u_2} [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] {prior posterior : ι → ℝ} (hprior : PACBayesKL.IsFullSupportPMF prior) (hposterior : PACBayesKL.IsPMF posterior) (score : ι → TrajectoryScore Z) (delta : ℝ) (w n : ℕ) (x : ℕ → Z) : continuousTrajectorySleepingSuffixVarianceSelectedBoundary ⋯.toPMF.toMeasure hposterior.toPMF.toMeasure score delta w n x = finiteTrajectorySleepingSuffixVarianceSelectedBoundary prior posterior score delta w n x

The continuous selected endpoint is exactly the finite selected endpoint.

Finite dyadic envelope

noncomputable def FormalSLT.StochasticDynamics.finiteTrajectorySleepingSuffixVarianceGrowingPrefixComplexity {ι : Type u_1} [Fintype ι] (prior posterior : ι → ℝ) (delta : ℝ) (w n : ℕ) : ℝ

Largest-prefix finite KL complexity at wake-adjusted confidence.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def FormalSLT.StochasticDynamics.finiteTrajectorySleepingSuffixVarianceLILEnvelope {ι : Type u_1} {Z : Type u_2} [Fintype ι] (prior posterior : ι → ℝ) (score : ι → TrajectoryScore Z) (delta : ℝ) (w n : ℕ) (x : ℕ → Z) : ℝ

Finite observable dyadic square-root envelope for the exact selector. Its iterated-logarithm interpretation still requires controlled posterior KL and wake cost relative to the suffix length.

Equations

• One or more equations did not get rendered due to their size.

theorem FormalSLT.StochasticDynamics.continuousTrajectorySleepingSuffixVarianceLILEnvelope_toPMF {ι : Type u_1} {Z : Type u_2} [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] {prior posterior : ι → ℝ} (hprior : PACBayesKL.IsFullSupportPMF prior) (hposterior : PACBayesKL.IsPMF posterior) (score : ι → TrajectoryScore Z) (delta : ℝ) (w n : ℕ) (x : ℕ → Z) : continuousTrajectorySleepingSuffixVarianceLILEnvelope ⋯.toPMF.toMeasure hposterior.toPMF.toMeasure score delta w n x = finiteTrajectorySleepingSuffixVarianceLILEnvelope prior posterior score delta w n x

The continuous dyadic envelope is exactly the finite expression.

theorem FormalSLT.StochasticDynamics.finiteTrajectorySleepingSuffixVarianceSelectedExcess_le_LILEnvelope {ι : Type u_1} {Z : Type u_2} [Fintype ι] {prior posterior : ι → ℝ} (hprior : PACBayesKL.IsFullSupportPMF prior) (hposterior : PACBayesKL.IsPMF posterior) (score : ι → TrajectoryScore Z) (hscore : ∀ (h : ι) (n : ℕ) (u : ↥(Finset.Iic n) → Z) (y : Z), score h n u y ∈ Set.Icc 0 1) {delta : ℝ} (hdelta : 0 < delta) (hdelta1 : delta ≤ 1) {w n : ℕ} (hsuffix : 4 ≤ n - w) (x : ℕ → Z) : finiteTrajectorySleepingSuffixVarianceSelectedExcess prior posterior score delta w n x ≤ finiteTrajectorySleepingSuffixVarianceLILEnvelope prior posterior score delta w n x

The finite exact selector is bounded by the finite observable dyadic envelope.

theorem FormalSLT.StochasticDynamics.finiteTrajectorySleepingSuffixVarianceSelectedBoundary_le_LILEnvelope {ι : Type u_1} {Z : Type u_2} [Fintype ι] {prior posterior : ι → ℝ} (hprior : PACBayesKL.IsFullSupportPMF prior) (hposterior : PACBayesKL.IsPMF posterior) (score : ι → TrajectoryScore Z) (hscore : ∀ (h : ι) (n : ℕ) (u : ↥(Finset.Iic n) → Z) (y : Z), score h n u y ∈ Set.Icc 0 1) {delta : ℝ} (hdelta : 0 < delta) (hdelta1 : delta ≤ 1) {w n : ℕ} (hsuffix : 4 ≤ n - w) (x : ℕ → Z) : finiteTrajectorySleepingSuffixVarianceSelectedBoundary prior posterior score delta w n x ≤ finiteTrajectoryPosteriorEmpiricalPrequentialSuffixRisk score posterior w n x + finiteTrajectorySleepingSuffixVarianceLILEnvelope prior posterior score delta w n x

The finite selected boundary is bounded by finite empirical suffix risk plus the finite observable dyadic envelope.

Common finite events

theorem FormalSLT.StochasticDynamics.exists_finiteTrajectorySleepingSuffixVarianceOracle_event {ι : Type u_1} {Z : Type u_2} [Fintype ι] [Fintype Z] [MeasurableSpace Z] [MeasurableSingletonClass Z] (K : (n : ℕ) → ProbabilityTheory.Kernel (↥(Finset.Iic n) → Z) Z) [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (K n)] (x0 : Z) (score : ι → TrajectoryScore Z) (hscore : ∀ (h : ι) (n : ℕ) (u : ↥(Finset.Iic n) → Z) (y : Z), score h n u y ∈ Set.Icc 0 1) {prior : ι → ℝ} (hprior : PACBayesKL.IsFullSupportPMF prior) {delta : ℝ} (hdelta : 0 < delta) (hdelta1 : delta ≤ 1) (posterior : (ℕ → Z) → ℕ → ι → ℝ) (hposterior : ∀ (x : ℕ → Z) (n : ℕ), PACBayesKL.IsPMF (posterior x n)) (wake : (ℕ → Z) → ℕ → ℕ) : ∃ (goodEvent : Set (ℕ → Z)), (trajectoryMeasure K x0).real goodEventᶜ ≤ delta ∧ ∀ x ∈ goodEvent, ∀ (n : ℕ), 4 ≤ n - wake x n → have rho := posterior x n; have w := wake x n; have selected := finiteTrajectorySleepingSuffixVarianceFinitePrefixArgmin prior rho score delta w n x; selected ∈ Finset.range (finiteTrajectorySleepingSuffixVarianceMaxIndex w n + 1) ∧ finiteTrajectoryPosteriorAverageConditionalSuffixRisk K score rho w n x < finiteTrajectorySleepingSuffixVarianceSelectedBoundary prior rho score delta w n x ∧ finiteTrajectorySleepingSuffixVarianceSelectedExcess prior rho score delta w n x ≤ finiteTrajectorySleepingSuffixVarianceLILEnvelope prior rho score delta w n x ∧ finiteTrajectorySleepingSuffixVarianceSelectedBoundary prior rho score delta w n x ≤ finiteTrajectoryPosteriorEmpiricalPrequentialSuffixRisk score rho w n x + finiteTrajectorySleepingSuffixVarianceLILEnvelope prior rho score delta w n x

One event supports the exact finite-PMF suffix-variance selector for every path-selected posterior, wake, and reporting time.

theorem FormalSLT.StochasticDynamics.exists_finitePMFTrajectorySleepingSuffixVarianceOracle_event {ι : Type u_1} {Z : Type u_2} [Fintype ι] [Fintype Z] [MeasurableSpace Z] [MeasurableSingletonClass Z] (P : (n : ℕ) → (↥(Finset.Iic n) → Z) → Z → ℝ) (hP : ∀ (n : ℕ) (u : ↥(Finset.Iic n) → Z), PACBayesKL.IsPMF (P n u)) (x0 : Z) (score : ι → TrajectoryScore Z) (hscore : ∀ (h : ι) (n : ℕ) (u : ↥(Finset.Iic n) → Z) (y : Z), score h n u y ∈ Set.Icc 0 1) {prior : ι → ℝ} (hprior : PACBayesKL.IsFullSupportPMF prior) {delta : ℝ} (hdelta : 0 < delta) (hdelta1 : delta ≤ 1) (posterior : (ℕ → Z) → ℕ → ι → ℝ) (hposterior : ∀ (x : ℕ → Z) (n : ℕ), PACBayesKL.IsPMF (posterior x n)) (wake : (ℕ → Z) → ℕ → ℕ) : ∃ (goodEvent : Set (ℕ → Z)), (trajectoryMeasure (finiteTrajectoryKernel P hP) x0).real goodEventᶜ ≤ delta ∧ ∀ x ∈ goodEvent, ∀ (n : ℕ), 4 ≤ n - wake x n → have rho := posterior x n; have w := wake x n; have selected := finiteTrajectorySleepingSuffixVarianceFinitePrefixArgmin prior rho score delta w n x; selected ∈ Finset.range (finiteTrajectorySleepingSuffixVarianceMaxIndex w n + 1) ∧ finitePMFTrajectoryPosteriorAverageConditionalSuffixRisk P score rho w n x < finiteTrajectorySleepingSuffixVarianceSelectedBoundary prior rho score delta w n x ∧ finiteTrajectorySleepingSuffixVarianceSelectedExcess prior rho score delta w n x ≤ finiteTrajectorySleepingSuffixVarianceLILEnvelope prior rho score delta w n x ∧ finiteTrajectorySleepingSuffixVarianceSelectedBoundary prior rho score delta w n x ≤ finiteTrajectoryPosteriorEmpiricalPrequentialSuffixRisk score rho w n x + finiteTrajectorySleepingSuffixVarianceLILEnvelope prior rho score delta w n x

Fully finite specialization: posterior quantities and every conditional transition risk are explicit finite sums.