import FormalSLT.StochasticDynamics.TrajectoryForwardBesselPACBayesOracle /-! # Informative countable-tilt trajectory empirical-Bernstein receipt This checker instantiates the all-time trajectory endpoint on a genuinely prefix-dependent Boolean process. A fixed two-rule catalog contains a static predictor and an online last-label predictor. The observed first transition selects a point posterior, so both posterior branches occur on positive-mass supported cylinders and the selected posterior pays `KL = log 2`. At confidence `1 - 1/160`, the online branch has positive Bessel variance `1/512`. Its checked selected boundary lies in `(0.2738, 0.2744)`, while the same path at time `2048` selects the next countable atom and has boundary in `(0.1432, 0.1434)`. The latter is strictly smaller. Claim boundary: the predictor catalog is fixed before observing data, though one catalog member is prefix-adaptive. The countable theorem confidence- allocates over singleton atom events; it does not construct a master selected e-process. -/ open Finset MeasureTheory ProbabilityTheory open FormalSLT.AnytimeValid FormalSLT.PACBayesKL open FormalSLT.PACBayes.ForwardBesselPACBayesCountable open FormalSLT.PACBayes.ForwardBesselPACBayesOracle open scoped ENNReal NNReal namespace FormalSLT.Examples.CheckTrajectoryEmpiricalBernsteinPACBayesCountableInformative open FormalSLT.StochasticDynamics noncomputable section set_option maxRecDepth 10000 set_option maxHeartbeats 1000000 def oneThenZero (k : ℕ) : ℝ := if k = 0 then 1 else 0 local instance (p : Prop) : Decidable p := Classical.propDecidable p def firstMonitoredState (n : ℕ) (u : (i : Finset.Iic n) → Bool) : Bool := if h : 1 ≤ n then u ⟨1, Finset.mem_Iic.mpr h⟩ else false def informativeNextState (n : ℕ) (u : (i : Finset.Iic n) → Bool) : Bool := if firstMonitoredState n u then u ⟨n, Finset.mem_Iic.mpr le_rfl⟩ else !(u ⟨n, Finset.mem_Iic.mpr le_rfl⟩) def informativeDynamicPMF (n : ℕ) (u : (i : Finset.Iic n) → Bool) : PMF Bool := PMF.ofFintype (fun y ↦ if n = 0 then if y then ((3 / 4 : NNReal) : ENNReal) else ((1 / 4 : NNReal) : ENNReal) else if y = informativeNextState n u then 1 else 0) (by by_cases hn : n = 0 · have hsumNN : (3 / 4 : NNReal) + 1 / 4 = 1 := by norm_num have hsum : ((3 / 4 : NNReal) : ENNReal) + ((1 / 4 : NNReal) : ENNReal) = 1 := by rw [← ENNReal.coe_add, hsumNN] rfl simpa [hn, Fintype.sum_bool] using hsum · cases hnext : informativeNextState n u <;> simp [hn]) def informativeDynamicKernel (n : ℕ) : Kernel ((i : Finset.Iic n) → Bool) Bool := Kernel.ofFunOfCountable fun u ↦ (informativeDynamicPMF n u).toMeasure instance informativeDynamicKernel.instIsMarkovKernel (n : ℕ) : IsMarkovKernel (informativeDynamicKernel n) := ⟨fun u ↦ by change IsProbabilityMeasure (informativeDynamicPMF n u).toMeasure infer_instance⟩ def persistentTruePath (n : ℕ) : Bool := decide (0 < n) def firstFalseThenAlternatingPath (n : ℕ) : Bool := decide (0 < n ∧ Even n) /-- At time two, two reachable histories have the same initial and current state but induce opposite next-step laws through their first monitored state. -/ theorem informativeDynamicKernel_history_witness : persistentTruePath 2 = firstFalseThenAlternatingPath 2 ∧ informativeDynamicPMF 2 (Preorder.frestrictLe 2 persistentTruePath) true = 1 ∧ informativeDynamicPMF 2 (Preorder.frestrictLe 2 firstFalseThenAlternatingPath) true = 0 := by norm_num [persistentTruePath, firstFalseThenAlternatingPath, informativeDynamicPMF, informativeNextState, firstMonitoredState, PMF.ofFintype_apply, Preorder.frestrictLe_apply] def informativeScore (i : Bool) : FormalSLT.StochasticDynamics.TrajectoryScore Bool := fun n u y ↦ if i then if n = 0 then (if y then 1 else 0) else if y = u ⟨n, Finset.mem_Iic.mpr le_rfl⟩ then 0 else 1 else if y then 1 else 0 theorem informativeScore_mem_Icc : ∀ i n u y, informativeScore i n u y ∈ Set.Icc (0 : ℝ) 1 := by intro i n u y fin_cases i <;> simp [informativeScore] <;> split_ifs <;> norm_num /-- The online rule changes its prediction with the observed prefix, while the static rule does not. Both displayed prefixes lead to the same next label. -/ theorem informativeScore_online_update_witness : informativeScore true 1 (Preorder.frestrictLe 1 persistentTruePath) true = 0 ∧ informativeScore true 1 (Preorder.frestrictLe 1 firstFalseThenAlternatingPath) true = 1 ∧ informativeScore false 1 (Preorder.frestrictLe 1 persistentTruePath) true = 1 ∧ informativeScore false 1 (Preorder.frestrictLe 1 firstFalseThenAlternatingPath) true = 1 := by norm_num [informativeScore, persistentTruePath, firstFalseThenAlternatingPath, Preorder.frestrictLe_apply] def transitionViolationScore : FormalSLT.StochasticDynamics.TrajectoryScore Bool := fun n u y ↦ if 1 ≤ n then if y = informativeNextState n u then 0 else 1 else 0 theorem transitionViolationScore_mem_Icc : ∀ n u y, transitionViolationScore n u y ∈ Set.Icc (0 : ℝ) 1 := by intro n u y simp [transitionViolationScore] split_ifs <;> norm_num theorem transitionViolation_conditionalRisk_eq_zero (n : ℕ) (hn : 1 ≤ n) (x : ℕ → Bool) : FormalSLT.StochasticDynamics.conditionalTrajectoryRisk informativeDynamicKernel transitionViolationScore n x = 0 := by unfold FormalSLT.StochasticDynamics.conditionalTrajectoryRisk informativeDynamicKernel change ∫ y, transitionViolationScore n (Preorder.frestrictLe n x) y ∂(informativeDynamicPMF n (Preorder.frestrictLe n x)).toMeasure = 0 rw [PMF.integral_eq_sum, Fintype.sum_bool] have hn0 : n ≠ 0 := Nat.ne_of_gt hn cases hnext : informativeNextState n (Preorder.frestrictLe n x) <;> simp [transitionViolationScore, informativeDynamicPMF, hn, hn0, hnext] def informativePathMeasure : Measure (ℕ → Bool) := FormalSLT.StochasticDynamics.trajectoryMeasure informativeDynamicKernel false instance informativePathMeasure.instIsProbabilityMeasure : IsProbabilityMeasure informativePathMeasure := by unfold informativePathMeasure infer_instance theorem transitionViolation_observed_ae_zero (n : ℕ) (hn : 1 ≤ n) : FormalSLT.StochasticDynamics.observedTrajectoryScore transitionViolationScore n =ᵐ[informativePathMeasure] 0 := by have hcond := FormalSLT.StochasticDynamics.observedTrajectoryScore_condExp informativeDynamicKernel false transitionViolationScore transitionViolationScore_mem_Icc n have hcond0 : informativePathMeasure[ FormalSLT.StochasticDynamics.observedTrajectoryScore transitionViolationScore n | Filtration.piLE (X := fun _ : ℕ ↦ Bool) n] =ᵐ[informativePathMeasure] (0 : (ℕ → Bool) → ℝ) := by refine hcond.trans (Filter.Eventually.of_forall fun x ↦ ?_) exact transitionViolation_conditionalRisk_eq_zero n hn x have hcondIntegral : ∫ x, informativePathMeasure[ FormalSLT.StochasticDynamics.observedTrajectoryScore transitionViolationScore n | Filtration.piLE (X := fun _ : ℕ ↦ Bool) n] x ∂informativePathMeasure = 0 := by simpa using integral_congr_ae hcond0 have hintegral : ∫ x, FormalSLT.StochasticDynamics.observedTrajectoryScore transitionViolationScore n x ∂informativePathMeasure = 0 := by rw [← integral_condExp ((Filtration.piLE (X := fun _ : ℕ ↦ Bool)).le n)] exact hcondIntegral exact (integral_eq_zero_iff_of_nonneg (fun x ↦ (FormalSLT.StochasticDynamics.observedTrajectoryScore_mem_Icc transitionViolationScore_mem_Icc n x).1) (FormalSLT.StochasticDynamics.integrable_observedTrajectoryScore (κ := informativeDynamicKernel) (x0 := false) (score := transitionViolationScore) transitionViolationScore_mem_Icc n)).1 hintegral theorem informative_recurrence_ae (n : ℕ) (hn : 1 ≤ n) : ∀ᵐ x ∂informativePathMeasure, x (n + 1) = informativeNextState n (Preorder.frestrictLe n x) := by filter_upwards [transitionViolation_observed_ae_zero n hn] with x hx unfold FormalSLT.StochasticDynamics.observedTrajectoryScore at hx simp [transitionViolationScore, hn] at hx exact hx def informativeSupportEvent : Set (ℕ → Bool) := {x | ∀ n, 1 ≤ n → x (n + 1) = informativeNextState n (Preorder.frestrictLe n x)} theorem informativeSupportEvent_ae : ∀ᵐ x ∂informativePathMeasure, x ∈ informativeSupportEvent := by change ∀ᵐ x ∂informativePathMeasure, ∀ n, 1 ≤ n → x (n + 1) = informativeNextState n (Preorder.frestrictLe n x) rw [ae_all_iff] intro n by_cases hn : 1 ≤ n · exact (informative_recurrence_ae n hn).mono fun x hx _ ↦ hx · exact Filter.Eventually.of_forall fun _ hx ↦ (hn hx).elim def firstTrueEvent : Set (ℕ → Bool) := {x | x 1 = true} theorem informativePathMeasure_firstTrueEvent : informativePathMeasure firstTrueEvent = (3 : ENNReal) / 4 := by let u0 : (i : Finset.Iic 0) → Bool := fun _ ↦ false have hmap := FormalSLT.StochasticDynamics.map_trajectory_next informativeDynamicKernel 0 u0 have happly : Measure.map (fun x : ℕ → Bool ↦ x 1) informativePathMeasure = informativeDynamicKernel 0 u0 := by simpa [informativePathMeasure, FormalSLT.StochasticDynamics.trajectoryMeasure, u0] using hmap calc informativePathMeasure firstTrueEvent = (Measure.map (fun x : ℕ → Bool ↦ x 1) informativePathMeasure) {true} := by rw [Measure.map_apply (measurable_pi_apply 1) (MeasurableSet.singleton true)] rfl _ = informativeDynamicKernel 0 u0 {true} := by rw [happly] _ = (3 : ENNReal) / 4 := by change (informativeDynamicPMF 0 u0).toMeasure {true} = _ rw [(informativeDynamicPMF 0 u0).toMeasure_apply_singleton true (MeasurableSet.singleton true)] norm_num [informativeDynamicPMF, PMF.ofFintype_apply] def informativeCylinder : Set (ℕ → Bool) := informativeSupportEvent ∩ firstTrueEvent theorem informativePathMeasure_informativeCylinder : informativePathMeasure informativeCylinder = (3 : ENNReal) / 4 := by rw [informativeCylinder, Measure.measure_inter_eq_of_ae informativeSupportEvent_ae, informativePathMeasure_firstTrueEvent] theorem path_eq_true_of_mem_informativeCylinder {x : ℕ → Bool} (hx : x ∈ informativeCylinder) {n : ℕ} (hn : 1 ≤ n) : x n = true := by have hx1 : x 1 = true := by simpa [informativeCylinder, firstTrueEvent] using hx.2 induction n, hn using Nat.le_induction with | base => exact hx1 | succ n hn ih => have hrec := hx.1 n hn rw [hrec] simp [informativeNextState, firstMonitoredState, hn, Preorder.frestrictLe_apply, hx1, ih] def uniformPrior (_i : Bool) : ℝ := 1 / 2 theorem uniformPrior_isFullSupportPMF : IsFullSupportPMF uniformPrior := by refine ⟨⟨?_, ?_⟩, ?_⟩ · intro i fin_cases i <;> norm_num [uniformPrior] · norm_num [uniformPrior, Fintype.sum_bool] · intro i fin_cases i <;> norm_num [uniformPrior] def pointPosterior (selected i : Bool) : ℝ := if i = selected then 1 else 0 theorem pointPosterior_isPMF (selected : Bool) : IsPMF (pointPosterior selected) := by refine ⟨?_, ?_⟩ · intro i fin_cases selected <;> fin_cases i <;> norm_num [pointPosterior] · fin_cases selected <;> norm_num [pointPosterior, Fintype.sum_bool] /-- `true` selects the online last-label predictor; `false` selects the static false predictor. -/ def selectedPosterior (x : ℕ → Bool) (_n : ℕ) : Bool → ℝ := pointPosterior (x 1) theorem selectedPosterior_isPMF (x : ℕ → Bool) (n : ℕ) : IsPMF (selectedPosterior x n) := pointPosterior_isPMF _ theorem selectedPosterior_explicit_branches : selectedPosterior persistentTruePath 512 = pointPosterior true ∧ selectedPosterior firstFalseThenAlternatingPath 512 = pointPosterior false := by constructor <;> rfl theorem pointPosterior_kl_eq_log_two (selected : Bool) : klDiv (pointPosterior selected) uniformPrior = Real.log 2 := by fin_cases selected <;> simp [klDiv, pointPosterior, uniformPrior] theorem selectedPosterior_kl_eq_log_two (x : ℕ → Bool) (n : ℕ) : klDiv (selectedPosterior x n) uniformPrior = Real.log 2 := pointPosterior_kl_eq_log_two _ theorem selectedPosterior_kl_pos (x : ℕ → Bool) (n : ℕ) : 0 < klDiv (selectedPosterior x n) uniformPrior := by rw [selectedPosterior_kl_eq_log_two] exact Real.log_pos (by norm_num) theorem observed_onlineScore_eq_oneThenZero_of_mem {x : ℕ → Bool} (hx : x ∈ informativeCylinder) (k : ℕ) : FormalSLT.StochasticDynamics.observedTrajectoryScore (informativeScore true) k x = oneThenZero k := by have hx1 : x 1 = true := by simpa [informativeCylinder, firstTrueEvent] using hx.2 by_cases hk : k = 0 · subst k simp [FormalSLT.StochasticDynamics.observedTrajectoryScore, informativeScore, oneThenZero, hx1] · have hk1 : 1 ≤ k := Nat.one_le_iff_ne_zero.mpr hk have hkTrue := path_eq_true_of_mem_informativeCylinder hx hk1 have hksTrue := path_eq_true_of_mem_informativeCylinder hx (by omega : 1 ≤ k + 1) simp [FormalSLT.StochasticDynamics.observedTrajectoryScore, informativeScore, oneThenZero, hk, Preorder.frestrictLe_apply, hkTrue, hksTrue] theorem selected_empiricalRisk_eq_one_512_of_mem {x : ℕ → Bool} (hx : x ∈ informativeCylinder) : FormalSLT.StochasticDynamics.trajectoryPosteriorEmpiricalPrequentialRisk informativeScore (selectedPosterior x 512) 512 x = (1 : ℝ) / 512 := by have hposterior : selectedPosterior x 512 = pointPosterior true := by unfold selectedPosterior have hx1 : x 1 = true := by simpa [informativeCylinder, firstTrueEvent] using hx.2 rw [hx1] rw [hposterior] unfold FormalSLT.StochasticDynamics.trajectoryPosteriorEmpiricalPrequentialRisk posteriorAverage FormalSLT.StochasticDynamics.trajectoryEmpiricalPrequentialRisk runningMean runningSum rw [Fintype.sum_bool] simp only [pointPosterior, Bool.false_eq_true, if_false, zero_mul, if_true, one_mul] have hsum : ∑ k ∈ Finset.range 512, FormalSLT.StochasticDynamics.observedTrajectoryScore (informativeScore true) k x = 1 := by calc _ = ∑ k ∈ Finset.range 512, oneThenZero k := by apply Finset.sum_congr rfl intro k _ exact observed_onlineScore_eq_oneThenZero_of_mem hx k _ = 1 := by norm_num [oneThenZero, Finset.sum_range_succ] rw [hsum] norm_num theorem online_forwardBesselQ_512_eq_of_mem {x : ℕ → Bool} (hx : x ∈ informativeCylinder) : forwardBesselQ (fun k ↦ FormalSLT.StochasticDynamics.observedTrajectoryScore (informativeScore true) k x) 512 = (511 : ℝ) / 512 := by have hmean : forwardPrefixMean (fun k ↦ FormalSLT.StochasticDynamics.observedTrajectoryScore (informativeScore true) k x) 512 = forwardPrefixMean oneThenZero 512 := by unfold forwardPrefixMean congr 1 apply Finset.sum_congr rfl intro k _ exact observed_onlineScore_eq_oneThenZero_of_mem hx k unfold forwardBesselQ rw [hmean] calc (∑ i ∈ Finset.range 512, (FormalSLT.StochasticDynamics.observedTrajectoryScore (informativeScore true) i x - forwardPrefixMean oneThenZero 512) ^ 2) = ∑ i ∈ Finset.range 512, (oneThenZero i - forwardPrefixMean oneThenZero 512) ^ 2 := by apply Finset.sum_congr rfl intro i _ rw [observed_onlineScore_eq_oneThenZero_of_mem hx i] _ = (511 : ℝ) / 512 := by norm_num [forwardPrefixMean, oneThenZero, Finset.sum_range_succ] theorem online_besselVariance_eq_one_512_of_mem {x : ℕ → Bool} (hx : x ∈ informativeCylinder) : FormalSLT.Statistics.ClassicalEstimation.sampleVarianceBessel (fun i : Fin 512 ↦ FormalSLT.StochasticDynamics.observedTrajectoryScore (informativeScore true) i x) = (1 : ℝ) / 512 := by have h := forwardBesselQ_eq_card_sub_one_mul_sampleVarianceBessel (fun k ↦ FormalSLT.StochasticDynamics.observedTrajectoryScore (informativeScore true) k x) (n := 512) (by norm_num) rw [online_forwardBesselQ_512_eq_of_mem hx] at h norm_num at h ⊢ linarith theorem online_besselVariance_mem_Ioo_of_mem {x : ℕ → Bool} (hx : x ∈ informativeCylinder) : FormalSLT.Statistics.ClassicalEstimation.sampleVarianceBessel (fun i : Fin 512 ↦ FormalSLT.StochasticDynamics.observedTrajectoryScore (informativeScore true) i x) ∈ Set.Ioo (0 : ℝ) (1 / 4) := by rw [online_besselVariance_eq_one_512_of_mem hx] norm_num theorem online_hybridPenalty_512_eq_of_mem {x : ℕ → Bool} (hx : x ∈ informativeCylinder) : forwardHybridBesselPenalty (fun k ↦ FormalSLT.StochasticDynamics.observedTrajectoryScore (informativeScore true) k x) 512 = (2045 : ℝ) / 1024 := by unfold forwardHybridBesselPenalty rw [online_forwardBesselQ_512_eq_of_mem hx] norm_num [harmonic] theorem selected_posteriorHybridPenalty_512_eq_of_mem {x : ℕ → Bool} (hx : x ∈ informativeCylinder) : FormalSLT.StochasticDynamics.trajectoryPosteriorHybridBesselPenalty (selectedPosterior x 512) informativeScore 512 x = (2045 : ℝ) / 1024 := by have hposterior : selectedPosterior x 512 = pointPosterior true := by unfold selectedPosterior have hx1 : x 1 = true := by simpa [informativeCylinder, firstTrueEvent] using hx.2 rw [hx1] rw [hposterior] unfold FormalSLT.StochasticDynamics.trajectoryPosteriorHybridBesselPenalty posteriorAverage rw [Fintype.sum_bool] simp only [pointPosterior, Bool.false_eq_true, if_false, zero_mul, if_true, one_mul, add_zero] exact online_hybridPenalty_512_eq_of_mem hx theorem online_forwardBesselQ_2048_eq_of_mem {x : ℕ → Bool} (hx : x ∈ informativeCylinder) : forwardBesselQ (fun k ↦ FormalSLT.StochasticDynamics.observedTrajectoryScore (informativeScore true) k x) 2048 = (2047 : ℝ) / 2048 := by have hmean : forwardPrefixMean (fun k ↦ FormalSLT.StochasticDynamics.observedTrajectoryScore (informativeScore true) k x) 2048 = forwardPrefixMean oneThenZero 2048 := by unfold forwardPrefixMean congr 1 apply Finset.sum_congr rfl intro k _ exact observed_onlineScore_eq_oneThenZero_of_mem hx k unfold forwardBesselQ rw [hmean] calc (∑ i ∈ Finset.range 2048, (FormalSLT.StochasticDynamics.observedTrajectoryScore (informativeScore true) i x - forwardPrefixMean oneThenZero 2048) ^ 2) = ∑ i ∈ Finset.range 2048, (oneThenZero i - forwardPrefixMean oneThenZero 2048) ^ 2 := by apply Finset.sum_congr rfl intro i _ rw [observed_onlineScore_eq_oneThenZero_of_mem hx i] _ = (2047 : ℝ) / 2048 := by norm_num [forwardPrefixMean, oneThenZero, Finset.sum_range_succ] theorem online_hybridPenalty_2048_eq_of_mem {x : ℕ → Bool} (hx : x ∈ informativeCylinder) : forwardHybridBesselPenalty (fun k ↦ FormalSLT.StochasticDynamics.observedTrajectoryScore (informativeScore true) k x) 2048 = (8189 : ℝ) / 4096 := by unfold forwardHybridBesselPenalty rw [online_forwardBesselQ_2048_eq_of_mem hx] norm_num [harmonic] theorem selected_posteriorHybridPenalty_2048_eq_of_mem {x : ℕ → Bool} (hx : x ∈ informativeCylinder) : FormalSLT.StochasticDynamics.trajectoryPosteriorHybridBesselPenalty (selectedPosterior x 2048) informativeScore 2048 x = (8189 : ℝ) / 4096 := by have hposterior : selectedPosterior x 2048 = pointPosterior true := by unfold selectedPosterior have hx1 : x 1 = true := by simpa [informativeCylinder, firstTrueEvent] using hx.2 rw [hx1] rw [hposterior] unfold FormalSLT.StochasticDynamics.trajectoryPosteriorHybridBesselPenalty posteriorAverage rw [Fintype.sum_bool] simp only [pointPosterior, Bool.false_eq_true, if_false, zero_mul, if_true, one_mul, add_zero] exact online_hybridPenalty_2048_eq_of_mem hx def highConfidenceBoundary (n : ℕ) (x : ℕ → Bool) : ℝ := FormalSLT.StochasticDynamics.trajectoryCountableEmpiricalBernsteinPACBayesBoundary uniformPrior informativeScore (selectedPosterior x n) (1 / 160) (geometricForwardTiltIndex n) n x theorem selected_tilt_index_512 : geometricForwardTiltIndex 512 = 3 := by norm_num [geometricForwardTiltIndex, Nat.log] theorem selected_tilt_index_2048 : geometricForwardTiltIndex 2048 = 4 := by norm_num [geometricForwardTiltIndex, Nat.log] theorem selected_tilt_weight_3 : polynomialForwardTiltWeight 3 = (1 : ℝ) / 20 := by norm_num [polynomialForwardTiltWeight, FormalSLT.PACBayes.InfiniteEmpiricalBernsteinStitch.reverseDyadicEpochWeight] theorem selected_tilt_weight_4 : polynomialForwardTiltWeight 4 = (1 : ℝ) / 30 := by norm_num [polynomialForwardTiltWeight, FormalSLT.PACBayes.InfiniteEmpiricalBernsteinStitch.reverseDyadicEpochWeight] theorem selected_tilt_log_cost_512 : Real.log (1 / (((1 : ℝ) / 160) * polynomialForwardTiltWeight 3)) = 7 * Real.log 2 + 2 * Real.log 5 := by rw [selected_tilt_weight_3] norm_num have hlog3200 : Real.log 3200 = 7 * Real.log 2 + 2 * Real.log 5 := by calc Real.log 3200 = Real.log ((2 : ℝ) ^ 7 * 5 ^ 2) := by norm_num _ = Real.log ((2 : ℝ) ^ 7) + Real.log ((5 : ℝ) ^ 2) := by rw [Real.log_mul (by positivity) (by positivity)] _ = 7 * Real.log 2 + 2 * Real.log 5 := by rw [Real.log_pow, Real.log_pow] norm_num exact hlog3200 theorem selected_tilt_log_cost_2048 : Real.log (1 / (((1 : ℝ) / 160) * polynomialForwardTiltWeight 4)) = 6 * Real.log 2 + Real.log 3 + 2 * Real.log 5 := by rw [selected_tilt_weight_4] norm_num have hlog4800 : Real.log 4800 = 6 * Real.log 2 + Real.log 3 + 2 * Real.log 5 := by calc Real.log 4800 = Real.log (((2 : ℝ) ^ 6 * 3) * 5 ^ 2) := by norm_num _ = Real.log ((2 : ℝ) ^ 6 * 3) + Real.log ((5 : ℝ) ^ 2) := by rw [Real.log_mul (by positivity) (by positivity)] _ = (Real.log ((2 : ℝ) ^ 6) + Real.log 3) + Real.log ((5 : ℝ) ^ 2) := by rw [Real.log_mul (by positivity) (by norm_num)] _ = 6 * Real.log 2 + Real.log 3 + 2 * Real.log 5 := by rw [Real.log_pow, Real.log_pow] ring exact hlog4800 theorem highConfidenceBoundary_512_eq_of_mem {x : ℕ → Bool} (hx : x ∈ informativeCylinder) : highConfidenceBoundary 512 x = (8 * Real.log 2 + 2 * Real.log 5 + forwardEmpiricalBernsteinPsi (1 / 16) * (2045 / 1024)) / 32 := by unfold highConfidenceBoundary rw [selected_tilt_index_512, FormalSLT.StochasticDynamics.trajectoryCountableEmpiricalBernsteinPACBayesBoundary_eq_explicit uniformPrior informativeScore (selectedPosterior x 512) (by norm_num) 3 512 x, selectedPosterior_kl_eq_log_two, selected_posteriorHybridPenalty_512_eq_of_mem hx] norm_num [geometricForwardTilt] rw [show Real.log 3200 = 7 * Real.log 2 + 2 * Real.log 5 by calc Real.log 3200 = Real.log ((2 : ℝ) ^ 7 * 5 ^ 2) := by norm_num _ = Real.log ((2 : ℝ) ^ 7) + Real.log ((5 : ℝ) ^ 2) := by rw [Real.log_mul (by positivity) (by positivity)] _ = 7 * Real.log 2 + 2 * Real.log 5 := by rw [Real.log_pow, Real.log_pow] norm_num] ring theorem highConfidenceBoundary_2048_eq_of_mem {x : ℕ → Bool} (hx : x ∈ informativeCylinder) : highConfidenceBoundary 2048 x = (7 * Real.log 2 + Real.log 3 + 2 * Real.log 5 + forwardEmpiricalBernsteinPsi (1 / 32) * (8189 / 4096)) / 64 := by unfold highConfidenceBoundary rw [selected_tilt_index_2048, FormalSLT.StochasticDynamics.trajectoryCountableEmpiricalBernsteinPACBayesBoundary_eq_explicit uniformPrior informativeScore (selectedPosterior x 2048) (by norm_num) 4 2048 x, selectedPosterior_kl_eq_log_two, selected_posteriorHybridPenalty_2048_eq_of_mem hx] norm_num [geometricForwardTilt] rw [show Real.log 4800 = 6 * Real.log 2 + Real.log 3 + 2 * Real.log 5 by calc Real.log 4800 = Real.log (((2 : ℝ) ^ 6 * 3) * 5 ^ 2) := by norm_num _ = Real.log ((2 : ℝ) ^ 6 * 3) + Real.log ((5 : ℝ) ^ 2) := by rw [Real.log_mul (by positivity) (by positivity)] _ = (Real.log ((2 : ℝ) ^ 6) + Real.log 3) + Real.log ((5 : ℝ) ^ 2) := by rw [Real.log_mul (by positivity) (by norm_num)] _ = 6 * Real.log 2 + Real.log 3 + 2 * Real.log 5 := by rw [Real.log_pow, Real.log_pow] ring] ring theorem highConfidenceBoundary_512_enclosure {x : ℕ → Bool} (hx : x ∈ informativeCylinder) : (2738 : ℝ) / 10000 < highConfidenceBoundary 512 x ∧ highConfidenceBoundary 512 x < (2744 : ℝ) / 10000 := by rw [highConfidenceBoundary_512_eq_of_mem hx] have hpsi0 := forwardEmpiricalBernsteinPsi_nonneg (by norm_num : (0 : ℝ) ≤ 1 / 16) (by norm_num : (1 : ℝ) / 16 < 1) have hpsi := forwardEmpiricalBernsteinPsi_le_two_mul_sq (by norm_num : (1 : ℝ) / 16 ≤ 1 / 2) constructor <;> nlinarith [Real.log_two_gt_d9, Real.log_five_gt_d9, Real.log_two_lt_d9, Real.log_five_lt_d9] theorem highConfidenceBoundary_2048_enclosure {x : ℕ → Bool} (hx : x ∈ informativeCylinder) : (1432 : ℝ) / 10000 < highConfidenceBoundary 2048 x ∧ highConfidenceBoundary 2048 x < (1434 : ℝ) / 10000 := by rw [highConfidenceBoundary_2048_eq_of_mem hx] have hpsi0 := forwardEmpiricalBernsteinPsi_nonneg (by norm_num : (0 : ℝ) ≤ 1 / 32) (by norm_num : (1 : ℝ) / 32 < 1) have hpsi := forwardEmpiricalBernsteinPsi_le_two_mul_sq (by norm_num : (1 : ℝ) / 32 ≤ 1 / 2) constructor <;> nlinarith [Real.log_two_gt_d9, Real.log_three_gt_d9, Real.log_five_gt_d9, Real.log_two_lt_d9, Real.log_three_lt_d9, Real.log_five_lt_d9] theorem highConfidenceBoundary_2048_lt_512_of_mem {x : ℕ → Bool} (hx : x ∈ informativeCylinder) : highConfidenceBoundary 2048 x < highConfidenceBoundary 512 x := by have hsmall := (highConfidenceBoundary_2048_enclosure hx).2 have hlarge := (highConfidenceBoundary_512_enclosure hx).1 linarith theorem highConfidence_rhs_512_lt_seven_twenty_fifths_of_mem {x : ℕ → Bool} (hx : x ∈ informativeCylinder) : FormalSLT.StochasticDynamics.trajectoryPosteriorEmpiricalPrequentialRisk informativeScore (selectedPosterior x 512) 512 x + highConfidenceBoundary 512 x < (7 : ℝ) / 25 := by rw [selected_empiricalRisk_eq_one_512_of_mem hx] have hboundary := (highConfidenceBoundary_512_enclosure hx).2 linarith def informativeExceptionalEvent : Set (ℕ → Bool) := FormalSLT.StochasticDynamics.trajectoryCountableEmpiricalBernsteinPACBayesExceptionalEvent informativeDynamicKernel uniformPrior informativeScore (1 / 160) theorem informativeExceptionalEvent_mass_le_delta : informativePathMeasure.real informativeExceptionalEvent ≤ (1 : ℝ) / 160 := by simpa [informativePathMeasure, informativeExceptionalEvent] using (FormalSLT.StochasticDynamics.trajectoryCountableEmpiricalBernsteinPACBayesExceptionalEvent_mass_le (K := informativeDynamicKernel) false (score := informativeScore) informativeScore_mem_Icc uniformPrior_isFullSupportPMF (delta := (1 / 160 : ℝ)) (by norm_num)) theorem informativeCylinder_real_mass : informativePathMeasure.real informativeCylinder = (3 : ℝ) / 4 := by rw [measureReal_def, informativePathMeasure_informativeCylinder] norm_num theorem informative_goodCylinderPath_exists : ∃ x : ℕ → Bool, x ∈ informativeCylinder ∧ x ∉ informativeExceptionalEvent := by by_contra h have hsubset : informativeCylinder ⊆ informativeExceptionalEvent := by intro x hx by_contra hgood exact h ⟨x, hx, hgood⟩ have hmono : informativePathMeasure.real informativeCylinder ≤ informativePathMeasure.real informativeExceptionalEvent := measureReal_mono hsubset rw [informativeCylinder_real_mass] at hmono have hbad := informativeExceptionalEvent_mass_le_delta linarith def firstFalseEvent : Set (ℕ → Bool) := {x | x 1 = false} theorem informativePathMeasure_firstFalseEvent : informativePathMeasure firstFalseEvent = (1 : ENNReal) / 4 := by let u0 : (i : Finset.Iic 0) → Bool := fun _ ↦ false have hmap := FormalSLT.StochasticDynamics.map_trajectory_next informativeDynamicKernel 0 u0 have happly : Measure.map (fun x : ℕ → Bool ↦ x 1) informativePathMeasure = informativeDynamicKernel 0 u0 := by simpa [informativePathMeasure, FormalSLT.StochasticDynamics.trajectoryMeasure, u0] using hmap calc informativePathMeasure firstFalseEvent = (Measure.map (fun x : ℕ → Bool ↦ x 1) informativePathMeasure) {false} := by rw [Measure.map_apply (measurable_pi_apply 1) (MeasurableSet.singleton false)] rfl _ = informativeDynamicKernel 0 u0 {false} := by rw [happly] _ = (1 : ENNReal) / 4 := by change (informativeDynamicPMF 0 u0).toMeasure {false} = _ rw [(informativeDynamicPMF 0 u0).toMeasure_apply_singleton false (MeasurableSet.singleton false)] norm_num [informativeDynamicPMF, PMF.ofFintype_apply] def alternateCylinder : Set (ℕ → Bool) := informativeSupportEvent ∩ firstFalseEvent theorem alternateCylinder_real_mass : informativePathMeasure.real alternateCylinder = (1 : ℝ) / 4 := by have hmeasure : informativePathMeasure alternateCylinder = (1 : ENNReal) / 4 := by rw [alternateCylinder, Measure.measure_inter_eq_of_ae informativeSupportEvent_ae, informativePathMeasure_firstFalseEvent] rw [measureReal_def, hmeasure] norm_num theorem alternate_goodCylinderPath_exists : ∃ x : ℕ → Bool, x ∈ alternateCylinder ∧ x ∉ informativeExceptionalEvent := by by_contra h have hsubset : alternateCylinder ⊆ informativeExceptionalEvent := by intro x hx by_contra hgood exact h ⟨x, hx, hgood⟩ have hmono : informativePathMeasure.real alternateCylinder ≤ informativePathMeasure.real informativeExceptionalEvent := measureReal_mono hsubset rw [alternateCylinder_real_mass] at hmono have hbad := informativeExceptionalEvent_mass_le_delta linarith theorem selector_branches_on_positive_mass_good_cylinders : (∃ x : ℕ → Bool, x ∈ informativeCylinder ∧ x ∉ informativeExceptionalEvent ∧ selectedPosterior x 512 = pointPosterior true) ∧ (∃ x : ℕ → Bool, x ∈ alternateCylinder ∧ x ∉ informativeExceptionalEvent ∧ selectedPosterior x 512 = pointPosterior false) := by constructor · obtain ⟨x, hx, hgood⟩ := informative_goodCylinderPath_exists refine ⟨x, hx, hgood, ?_⟩ unfold selectedPosterior have hx1 : x 1 = true := by simpa [informativeCylinder, firstTrueEvent] using hx.2 rw [hx1] · obtain ⟨x, hx, hgood⟩ := alternate_goodCylinderPath_exists refine ⟨x, hx, hgood, ?_⟩ unfold selectedPosterior have hx1 : x 1 = false := by simpa [alternateCylinder, firstFalseEvent] using hx.2 rw [hx1] theorem informative_allTime_vanishing_capstone : ∃ goodEvent : Set (ℕ → Bool), informativePathMeasure.real goodEventᶜ ≤ (1 : ℝ) / 160 ∧ (∀ x ∈ goodEvent, ∀ n : ℕ, 2 ≤ n → FormalSLT.StochasticDynamics.trajectoryPosteriorAverageConditionalRisk informativeDynamicKernel informativeScore (selectedPosterior x n) n x < FormalSLT.StochasticDynamics.trajectoryPosteriorEmpiricalPrequentialRisk informativeScore (selectedPosterior x n) n x + FormalSLT.StochasticDynamics.trajectoryCountableEmpiricalBernsteinPACBayesBoundary uniformPrior informativeScore (selectedPosterior x n) (1 / 160) (geometricForwardTiltIndex n) n x) ∧ (∀ x ∈ goodEvent, Filter.Tendsto (fun n ↦ FormalSLT.StochasticDynamics.trajectoryCountableEmpiricalBernsteinPACBayesBoundary uniformPrior informativeScore (selectedPosterior x n) (1 / 160) (geometricForwardTiltIndex n) n x) Filter.atTop (nhds 0)) := by simpa [informativePathMeasure] using (FormalSLT.StochasticDynamics.exists_trajectoryCountableEmpiricalBernsteinPACBayes_allTime_vanishing_event (K := informativeDynamicKernel) false (score := informativeScore) informativeScore_mem_Icc uniformPrior_isFullSupportPMF (delta := (1 / 160 : ℝ)) (by norm_num) (by norm_num) selectedPosterior selectedPosterior_isPMF) theorem selected_risk_bound_of_not_mem {x : ℕ → Bool} (hx : x ∉ informativeExceptionalEvent) : FormalSLT.StochasticDynamics.trajectoryPosteriorAverageConditionalRisk informativeDynamicKernel informativeScore (selectedPosterior x 512) 512 x < FormalSLT.StochasticDynamics.trajectoryPosteriorEmpiricalPrequentialRisk informativeScore (selectedPosterior x 512) 512 x + highConfidenceBoundary 512 x := by have hbound := FormalSLT.StochasticDynamics.trajectoryCountableEmpiricalBernsteinPACBayes_allPosteriors_of_not_mem informativeDynamicKernel (score := informativeScore) informativeScore_mem_Icc uniformPrior_isFullSupportPMF (delta := (1 / 160 : ℝ)) (by norm_num) (by simpa [informativeExceptionalEvent] using hx) (geometricForwardTiltIndex 512) (selectedPosterior x 512) (selectedPosterior_isPMF x 512) 512 (by norm_num) simpa [highConfidenceBoundary] using hbound theorem informative_nonvacuous_receipt : ∃ x : ℕ → Bool, x ∈ informativeCylinder ∧ x ∉ informativeExceptionalEvent ∧ selectedPosterior x 512 = pointPosterior true ∧ klDiv (selectedPosterior x 512) uniformPrior = Real.log 2 ∧ 0 < klDiv (selectedPosterior x 512) uniformPrior ∧ FormalSLT.Statistics.ClassicalEstimation.sampleVarianceBessel (fun i : Fin 512 ↦ FormalSLT.StochasticDynamics.observedTrajectoryScore (informativeScore true) i x) = (1 : ℝ) / 512 ∧ FormalSLT.Statistics.ClassicalEstimation.sampleVarianceBessel (fun i : Fin 512 ↦ FormalSLT.StochasticDynamics.observedTrajectoryScore (informativeScore true) i x) ∈ Set.Ioo (0 : ℝ) (1 / 4) ∧ geometricForwardTiltIndex 512 = 3 ∧ Real.log (1 / (((1 : ℝ) / 160) * polynomialForwardTiltWeight 3)) = 7 * Real.log 2 + 2 * Real.log 5 ∧ geometricForwardTiltIndex 2048 = 4 ∧ Real.log (1 / (((1 : ℝ) / 160) * polynomialForwardTiltWeight 4)) = 6 * Real.log 2 + Real.log 3 + 2 * Real.log 5 ∧ FormalSLT.StochasticDynamics.trajectoryPosteriorAverageConditionalRisk informativeDynamicKernel informativeScore (selectedPosterior x 512) 512 x < FormalSLT.StochasticDynamics.trajectoryPosteriorEmpiricalPrequentialRisk informativeScore (selectedPosterior x 512) 512 x + highConfidenceBoundary 512 x ∧ FormalSLT.StochasticDynamics.trajectoryPosteriorEmpiricalPrequentialRisk informativeScore (selectedPosterior x 512) 512 x + highConfidenceBoundary 512 x < (7 : ℝ) / 25 ∧ (2738 : ℝ) / 10000 < highConfidenceBoundary 512 x ∧ highConfidenceBoundary 512 x < (2744 : ℝ) / 10000 ∧ (1432 : ℝ) / 10000 < highConfidenceBoundary 2048 x ∧ highConfidenceBoundary 2048 x < (1434 : ℝ) / 10000 ∧ highConfidenceBoundary 2048 x < highConfidenceBoundary 512 x := by obtain ⟨x, hx, hgood⟩ := informative_goodCylinderPath_exists refine ⟨x, hx, hgood, ?_, selectedPosterior_kl_eq_log_two x 512, selectedPosterior_kl_pos x 512, online_besselVariance_eq_one_512_of_mem hx, online_besselVariance_mem_Ioo_of_mem hx, selected_tilt_index_512, selected_tilt_log_cost_512, selected_tilt_index_2048, selected_tilt_log_cost_2048, selected_risk_bound_of_not_mem hgood, highConfidence_rhs_512_lt_seven_twenty_fifths_of_mem hx, (highConfidenceBoundary_512_enclosure hx).1, (highConfidenceBoundary_512_enclosure hx).2, (highConfidenceBoundary_2048_enclosure hx).1, (highConfidenceBoundary_2048_enclosure hx).2, highConfidenceBoundary_2048_lt_512_of_mem hx⟩ unfold selectedPosterior have hx1 : x 1 = true := by simpa [informativeCylinder, firstTrueEvent] using hx.2 rw [hx1] /-! ## Observable growing-prefix oracle receipt -/ /-- Exact trajectory boundary after minimizing over the geometric prefix available at reporting time `n`. -/ def observableOracleBoundary (n : ℕ) (x : ℕ → Bool) : ℝ := trajectoryGrowingPrefixForwardBesselPACBayesBoundary uniformPrior informativeScore (selectedPosterior x n) (1 / 160) n x /-- The observable oracle retains the previously audited all-time atom as a candidate, so its exact boundary can only improve on that boundary. -/ theorem observableOracleBoundary_le_highConfidenceBoundary (n : ℕ) (x : ℕ → Bool) : observableOracleBoundary n x ≤ highConfidenceBoundary n x := by apply trajectoryGrowingPrefixForwardBesselPACBayesBoundary_le_atom simp [growingPrefixForwardBesselPACBayesMaxIndex] /-- On every path outside the allocated exceptional event, the ordinary posterior-averaged conditional trajectory risk is controlled by empirical prequential risk plus the exact post-data oracle boundary. -/ theorem observableOracle_risk_bound_of_not_mem {x : ℕ → Bool} (hx : x ∉ informativeExceptionalEvent) : trajectoryPosteriorAverageConditionalRisk informativeDynamicKernel informativeScore (selectedPosterior x 512) 512 x < trajectoryPosteriorEmpiricalPrequentialRisk informativeScore (selectedPosterior x 512) 512 x + observableOracleBoundary 512 x := by have hbound := trajectoryCountableEmpiricalBernsteinPACBayes_allPosteriors_of_not_mem informativeDynamicKernel (score := informativeScore) informativeScore_mem_Icc uniformPrior_isFullSupportPMF (delta := (1 / 160 : ℝ)) (by norm_num) (by simpa [informativeExceptionalEvent] using hx) (trajectoryGrowingPrefixForwardBesselPACBayesArgmin uniformPrior informativeScore (selectedPosterior x 512) (1 / 160) 512 x) (selectedPosterior x 512) (selectedPosterior_isPMF x 512) 512 (by norm_num) simpa [observableOracleBoundary, trajectoryGrowingPrefixForwardBesselPACBayesBoundary] using hbound /-- The exact selected boundary is controlled by the explicit observable variance-adaptive envelope on the same path. -/ theorem observableOracleBoundary_512_le_LILEnvelope (x : ℕ → Bool) : observableOracleBoundary 512 x ≤ trajectoryGrowingPrefixForwardBesselPACBayesLILEnvelope uniformPrior informativeScore (selectedPosterior x 512) (1 / 160) 512 x := by exact trajectoryGrowingPrefixForwardBesselPACBayesBoundary_le_LILEnvelope uniformPrior_isFullSupportPMF (selectedPosterior_isPMF x 512) informativeScore_mem_Icc (by norm_num) (by norm_num) (by norm_num) x /-- At the two audited reporting times, exact post-data minimization preserves the previous strict numerical upper bounds without evaluating the classical argmin witness. -/ theorem observableOracleBoundary_numeric_receipt {x : ℕ → Bool} (hx : x ∈ informativeCylinder) : observableOracleBoundary 512 x < (2744 : ℝ) / 10000 ∧ observableOracleBoundary 2048 x < (1434 : ℝ) / 10000 := by constructor · exact (observableOracleBoundary_le_highConfidenceBoundary 512 x).trans_lt (highConfidenceBoundary_512_enclosure hx).2 · exact (observableOracleBoundary_le_highConfidenceBoundary 2048 x).trans_lt (highConfidenceBoundary_2048_enclosure hx).2 /-- The complete empirical-plus-oracle right-hand side remains strictly below `7/25` on the audited positive-mass cylinder. -/ theorem observableOracle_rhs_512_lt_seven_twenty_fifths_of_mem {x : ℕ → Bool} (hx : x ∈ informativeCylinder) : trajectoryPosteriorEmpiricalPrequentialRisk informativeScore (selectedPosterior x 512) 512 x + observableOracleBoundary 512 x < (7 : ℝ) / 25 := by have horacle := observableOracleBoundary_le_highConfidenceBoundary 512 x have hold := highConfidence_rhs_512_lt_seven_twenty_fifths_of_mem hx linarith /-- Replayable end-to-end receipt: a positive-mass supported trajectory lies outside the allocated exceptional event, its path-selected posterior has the ordinary conditional-risk guarantee, and the exact post-data tilt oracle is both nonvacuous and bounded by the observable LIL-order envelope. -/ theorem informative_observableOracle_receipt : ∃ x : ℕ → Bool, x ∈ informativeCylinder ∧ x ∉ informativeExceptionalEvent ∧ selectedPosterior x 512 = pointPosterior true ∧ trajectoryPosteriorAverageConditionalRisk informativeDynamicKernel informativeScore (selectedPosterior x 512) 512 x < trajectoryPosteriorEmpiricalPrequentialRisk informativeScore (selectedPosterior x 512) 512 x + observableOracleBoundary 512 x ∧ observableOracleBoundary 512 x < (2744 : ℝ) / 10000 ∧ observableOracleBoundary 2048 x < (1434 : ℝ) / 10000 ∧ trajectoryPosteriorEmpiricalPrequentialRisk informativeScore (selectedPosterior x 512) 512 x + observableOracleBoundary 512 x < (7 : ℝ) / 25 ∧ observableOracleBoundary 512 x ≤ trajectoryGrowingPrefixForwardBesselPACBayesLILEnvelope uniformPrior informativeScore (selectedPosterior x 512) (1 / 160) 512 x := by obtain ⟨x, hx, hgood⟩ := informative_goodCylinderPath_exists have hposterior : selectedPosterior x 512 = pointPosterior true := by unfold selectedPosterior have hx1 : x 1 = true := by simpa [informativeCylinder, firstTrueEvent] using hx.2 rw [hx1] exact ⟨x, hx, hgood, hposterior, observableOracle_risk_bound_of_not_mem hgood, (observableOracleBoundary_numeric_receipt hx).1, (observableOracleBoundary_numeric_receipt hx).2, observableOracle_rhs_512_lt_seven_twenty_fifths_of_mem hx, observableOracleBoundary_512_le_LILEnvelope x⟩ /-! Public endpoint and complete local axiom receipt. -/ #check trajectoryCountableEmpiricalBernsteinPACBayes_allPosteriors_of_not_mem #check exists_trajectoryCountableEmpiricalBernsteinPACBayes_allTime_vanishing_event #check informativeDynamicKernel_history_witness #check informativeScore_online_update_witness #check selectedPosterior_explicit_branches #check selector_branches_on_positive_mass_good_cylinders #check informative_allTime_vanishing_capstone #check informative_nonvacuous_receipt #check trajectoryGrowingPrefixForwardBesselPACBayesArgmin #check trajectoryGrowingPrefixForwardBesselPACBayesBoundary #check trajectoryGrowingPrefixForwardBesselPACBayesLILEnvelope #check trajectoryGrowingPrefixForwardBesselPACBayesArgmin_mem #check trajectoryGrowingPrefixForwardBesselPACBayesBoundary_le_atom #check trajectoryGrowingPrefixForwardBesselPACBayesBoundary_le_LILEnvelope #check trajectoryGrowingPrefixForwardBesselPACBayesBoundary_le_allTimeRate #check trajectoryGrowingPrefixForwardBesselPACBayesBoundary_tendsto_zero #check exists_trajectoryGrowingPrefixForwardBesselPACBayesOracle_event #check informative_observableOracle_receipt #print axioms informativeDynamicKernel_history_witness #print axioms informativeScore_mem_Icc #print axioms informativeScore_online_update_witness #print axioms transitionViolationScore_mem_Icc #print axioms transitionViolation_conditionalRisk_eq_zero #print axioms transitionViolation_observed_ae_zero #print axioms informative_recurrence_ae #print axioms informativeSupportEvent_ae #print axioms informativePathMeasure_firstTrueEvent #print axioms informativePathMeasure_informativeCylinder #print axioms path_eq_true_of_mem_informativeCylinder #print axioms uniformPrior_isFullSupportPMF #print axioms pointPosterior_isPMF #print axioms selectedPosterior_isPMF #print axioms selectedPosterior_explicit_branches #print axioms pointPosterior_kl_eq_log_two #print axioms selectedPosterior_kl_eq_log_two #print axioms selectedPosterior_kl_pos #print axioms observed_onlineScore_eq_oneThenZero_of_mem #print axioms selected_empiricalRisk_eq_one_512_of_mem #print axioms online_forwardBesselQ_512_eq_of_mem #print axioms online_besselVariance_eq_one_512_of_mem #print axioms online_besselVariance_mem_Ioo_of_mem #print axioms online_hybridPenalty_512_eq_of_mem #print axioms selected_posteriorHybridPenalty_512_eq_of_mem #print axioms online_forwardBesselQ_2048_eq_of_mem #print axioms online_hybridPenalty_2048_eq_of_mem #print axioms selected_posteriorHybridPenalty_2048_eq_of_mem #print axioms selected_tilt_index_512 #print axioms selected_tilt_index_2048 #print axioms selected_tilt_weight_3 #print axioms selected_tilt_weight_4 #print axioms selected_tilt_log_cost_512 #print axioms selected_tilt_log_cost_2048 #print axioms highConfidenceBoundary_512_eq_of_mem #print axioms highConfidenceBoundary_2048_eq_of_mem #print axioms highConfidenceBoundary_512_enclosure #print axioms highConfidenceBoundary_2048_enclosure #print axioms highConfidenceBoundary_2048_lt_512_of_mem #print axioms highConfidence_rhs_512_lt_seven_twenty_fifths_of_mem #print axioms informativeExceptionalEvent_mass_le_delta #print axioms informativeCylinder_real_mass #print axioms informative_goodCylinderPath_exists #print axioms informativePathMeasure_firstFalseEvent #print axioms alternateCylinder_real_mass #print axioms alternate_goodCylinderPath_exists #print axioms selector_branches_on_positive_mass_good_cylinders #print axioms informative_allTime_vanishing_capstone #print axioms selected_risk_bound_of_not_mem #print axioms informative_nonvacuous_receipt #print axioms trajectoryGrowingPrefixForwardBesselPACBayesArgmin_mem #print axioms trajectoryGrowingPrefixForwardBesselPACBayesBoundary_le_atom #print axioms trajectoryGrowingPrefixForwardBesselPACBayesBoundary_le_LILEnvelope #print axioms trajectoryGrowingPrefixForwardBesselPACBayesBoundary_le_allTimeRate #print axioms trajectoryGrowingPrefixForwardBesselPACBayesBoundary_tendsto_zero #print axioms exists_trajectoryGrowingPrefixForwardBesselPACBayesOracle_event #print axioms observableOracleBoundary_le_highConfidenceBoundary #print axioms observableOracle_risk_bound_of_not_mem #print axioms observableOracleBoundary_512_le_LILEnvelope #print axioms observableOracleBoundary_numeric_receipt #print axioms observableOracle_rhs_512_lt_seven_twenty_fifths_of_mem #print axioms informative_observableOracle_receipt end end FormalSLT.Examples.CheckTrajectoryEmpiricalBernsteinPACBayesCountableInformative