Formalization: Parametric Rates for Stationary Policy Evaluation with Binary Hidden States
The complete Lean development behind this paper — every definition, lemma, and theorem of its module, including helpers the paper text never cites. Identifiers link within this page, into the Causalean library, or out to the official Mathlib docs.
CausalSmith.Stat.STAT_PomdpBinaryhiddenRate_Research.Basic 68 declarations The paper-local carrier for a finite partially observed Markov decision process, its observable-data decision problem, and the partial-history importance-weighted estimators.
Fixed-binary POMDP minimax model
The paper-local carrier for a finite partially observed Markov decision process, its observable-data decision problem, and the partial-history importance-weighted estimators. Causalean's generic real-valued minimax API is reused, while the dependent-trajectory model is defined locally because the substrate contains no POMDP experiment at this abstraction level.
A memoryless policy on the finite observed-state alphabet.
CausalSmith.Stat.PomdpBinaryhiddenRate.Policy · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:30 The finite observed/latent joint-state alphabet.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.JointState · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:34 The observed alphabet of this fixed-binary paper.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.BinaryObservedState · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:37 The hidden alphabet of this fixed-binary paper.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.BinaryHiddenState · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:41 The four-state product used by the paper's model class.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.BinaryJointState · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:45 Memoryless policies on the paper's binary observed alphabet.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.BinaryPolicy · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:49 One reward and successor-state block emitted by the POMDP kernel.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.Step · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:53 A length-T trajectory has T+1 states and T action/reward pairs.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.FullTrajectory · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:56 The observable trajectory, with latent and terminal states removed.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.ObsView · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:61 Raw ingredients of one trajectory experiment.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.RawPomdpExperiment · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:65 The binary experiment carrier used by every class member and testing law.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.BinaryPomdpExperiment · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:76 For the M input, this supplies the inst Is Probability Measure Full Trajectory Law instance.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.instIsProbabilityMeasureFullTrajectoryLaw · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:80 The joint state at a path coordinate, including the terminal coordinate.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.stateAt · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:88 The current state at epoch t.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.curState · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:92 The successor state at epoch t, including the final transition.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.nextState · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:98 The observed action at epoch t.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.actionAt · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:103 The observed real reward at epoch t.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.rewardAt · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:107 Projection from the full trajectory to exactly the information observed by an estimator.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.obsProj · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:111 The observed trajectory law.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.obsLaw · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:115 Embed an index strictly before t into the epoch index set.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.prefixIndex · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:120 State-and-epoch history strictly before t, together with the current state.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.StateHistoryView · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:123 A state-history view with the current action adjoined.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.ActionHistoryView · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:127 State-and-epoch history strictly before t, together with the current state.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.histStateView · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:131 The state history with the current action adjoined.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.histActionPair · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:137 The conditioning view for the reward-transition kernel identity.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.histView · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:141 The kernel conditioning view with (Y_t,S_{t+1}) adjoined.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.histNextPair · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:145 Read the observed current state from the state-history view.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.currentObsState · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:149 Read (S_t,A_t) from the kernel-conditioning view.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.currentStateAction · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:153 The time-homogeneous reward-transition kernel as a Mathlib kernel.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.kernelOfK · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:158 The behavior action kernel.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.behaviourKernel · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:163 the measurable current State Action assertion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.measurable_currentStateAction · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:169 the measurable current Obs State assertion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.measurable_currentObsState · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:175 A finite vector is a probability vector.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.ProbabilityVector · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:181 A policy is pointwise a probability vector on the binary action set.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.PolicyVector · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:185 The joint-state transition matrix induced by a memoryless policy.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.policyKernel · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:189 Stationarity of a finite probability vector for a transition matrix.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.IsStationary · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:195 A totalized stationary law, equal to a stationary probability vector whenever one exists.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.stationaryLaw · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:199 The selected stationary law satisfies the stationarity equations whenever a witness exists. the h condition. the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.stationaryLaw_isStationary_of_exists · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:205 Half the finite ℓ1 norm, the discrete total-variation norm.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.tvNorm · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:211 Apply a finite row kernel to a signed row vector.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.applyKernel · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:215 Target-policy conditional mean reward at a joint state.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.rewardRegression · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:220 The derived contraction factor.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.mixingAlpha · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:226 The derived policy-overlap factor.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.policyFactor · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:230 The time-homogeneous reward/successor law, with rewards supported on [0,1].
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.PomdpKernelLaw · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:236 Conditional action randomization through the observed state.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.SequentialIgnorability · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:247 The trajectory starts in the behavior stationary law.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.StationaryStart · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:257 The target policy is a probability policy dominated by L times behavior.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.PolicyOverlap · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:264 Behavior-induced joint-state kernel contracts probability vectors.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.BehaviorContraction · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:270 Target-induced joint-state kernel contracts probability vectors.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.TargetContraction · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:278 The six-condition binary observed/hidden POMDP class.
Definition (Lean source)
@realizes X(Fin 2 observed alphabet) @realizes H(Fin 2 hidden alphabet) @realizes Xt(binary observed coordinate) @realizes Ht(binary hidden coordinate)
CausalSmith.Stat.PomdpBinaryhiddenRate.BinaryPomdpClass · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:286 Stationary target-policy expected reward.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.targetValue · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:301 The likelihood ratio with zero-cell convention.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.ratio · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:306 The score at zero-based epoch t; valid in statements when k ≤ t.val.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.score · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:311 Population score expectation at a specified eligible epoch.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.populationMoment · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:319 Seven empirical intervention moments use epochs 7 through T.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.empiricalMoment · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:326 A four-state matrix.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.FourMatrix · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:333 Finite Dobrushin coefficient: maximal row total-variation distance.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.dobrushin · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:336 Transient characteristic factor, dividing by the stationary root.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.transientPoly · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:341 Product of two transient characteristic factors.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.pairPoly · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:346 Seven-moment modulus factor.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.stabilityFactor · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:351 Variance constant for the seven scores.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.varianceFactor · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:356 The overlap radius in the cardinality-uniform comparator.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.overlapRadius · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:368 The exponent in the cardinality-uniform comparator.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.rateExponent · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:372 Hidden alphabet used by the comparator reset construction at depth Q T.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.ComparatorHiddenAlphabet · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:381 The cited reset-depth family at the same logarithmic depth witnesses the fixed-radius two-point lower bound.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.ComparatorResetLowerWitness · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:386 The cited cardinality-uniform comparator. CausalSmith (2026), Latent Stationary Overlap and Minimax Off-Policy Evaluation in Finite POMDPs, main minimax theorem and reset-chain lower-bound construction, handle CausalSmithLatentOverlap2026. This is a cited input.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.CardinalityUniformComparator · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:405 The handle is the problem of constructing a cost-certified algorithm in an explicit arithmetic or bit-complexity and precision model. Start from the 3×3 Hankel matrix of m̂_(i+j+1)−m̂_(i+j); adapt over recurrence ranks 0–3; constrain transient roots to |z|≤α; return a stable four-state scalar realization with globally certified seven-moment objective gap at most T⁻¹, uniformly on rank-deficient strata and without a positive singular-value margin. The exhaustive grid has a finite candidate list of size O(T^19) for fixed t0, but no runtime or arithmetic-operation bound for fitting and selection is asserted.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.polynomialTimeHandle · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:428 The frozen open question, recorded as a nonassertive string.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.polynomialTimeAttainmentQuestion · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Basic.lean:441 CausalSmith.Stat.STAT_PomdpBinaryhiddenRate_Research.Constructions 43 declarations The exhaustive rational grid, observable-data minimax functional, and finite four-state testing family are defined from the binary POMDP carrier.
Finite grid and positive testing constructions
The exhaustive rational grid, observable-data minimax functional, and finite four-state testing family are defined from the binary POMDP carrier.
Grid resolution in the estimator construction.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.gridSize · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:22 Unfiltered finite tuple carrying an initial law, four transition rows, and rewards.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.GridCode · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:27 A simplex grid row is a nonnegative integer tuple summing to M.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.IsGridRow · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:32 Enumerate just the four-coordinate simplex rows.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.simplexGrid · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:36 Enumerate four simplex rows as a transition matrix.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.gridMatrixRows · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:41 Cartesian enumeration before the Dobrushin filter.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.gridCandidateUniverse · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:50 The grid code's initial distribution.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.gridNu · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:58 The grid code's stochastic matrix before the stability filter.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.gridR · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:62 The grid code's reward vector.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.gridReward · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:66 The stable transition matrix is mixed with the uniform reset kernel.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.stabilizedGridMatrix · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:70 A four-point version of the Dobrushin coefficient for grid rows.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.gridDobrushin · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:76 The finite candidate set, before fitting observable moments.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.gridCandidates · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:81 Seven-moment worst residual of a stable candidate.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.gridObjective · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:88 A base-M+1 code supplies a fixed lexicographic tie break.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.gridLexCode · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:97 Select a minimum-residual candidate, then the least grid code among ties.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.selectGridCode · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:105 Finite stable-grid estimator selected by seven observable moments.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.stableGridEstimator · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:120 Raw procedures see only policies and the observed trajectory.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.RawEstimator · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:129 Bounded measurable observable estimators; clipping to [0,1] is loss reducing.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.ObservableEstimator · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:132 A fixed binary model index carries exactly the six law conditions.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.ModelIndex · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:138 Observed-data squared risk at a binary POMDP law.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.observedRisk · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:143 Observable-data minimax squared risk over the fixed binary class.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.minimaxRisk · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:153 Perturbation amplitude for the two testing laws.
CausalSmith.Stat.PomdpBinaryhiddenRate.vT · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:159 On the theorem's positive-horizon domain, the testing amplitude has the paper's range. Under the listed formal conditions, the stated conclusion holds.
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.vT_mem_Ioc · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:162 Positive Bernoulli probability for a reward under hidden state h.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingRewardProb · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:178 Hidden-state successor probability controlled by the action.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingHiddenProb · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:182 Observed-state emission probability given the successor hidden state.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingEmission · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:186 The successor hidden-state and emission factors form a probability row. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingStepMass_sum · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:191 The stationary initialization weights sum to one. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingInitialMass_sum · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:201 The two conditional reward masses sum to one. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingRewardMass_sum · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:208 Summing a complete action, reward, and successor block gives unit mass. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingOneStepMass_sum · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:214 A normalized successor law at each epoch and the stationary initial law give a normalized sequence of joint states. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingStateMass_sum · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:229 The successor-state mass after averaging over a fair action.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingNextStateMass · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:255 For the testing construction, the conditional next-state mass function sums to one. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingNextStateMass_sum · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:261 Summing a reward and action block leaves the successor-state mass. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingStepMarginal_sum · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:272 The positive four-state testing reward/successor kernel.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingKernel · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:293 A finite testing trajectory with Boolean rewards.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.TestingPath · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:304 Embed a Boolean-reward path into the real-reward trajectory carrier.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.decodeTestingPath · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:308 Product mass of one path under the testing kernel and fair behavior policy.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingPathWeight · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:312 Every atom of the finite testing law has nonnegative mass. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingPathWeight_nonneg · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:324 The explicit finite path coefficients sum to one. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingPathWeight_sum · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:353 The finite mixture of path Dirac laws for the testing experiment.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingTrajectoryLaw · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:384 Normalization of the explicit finite testing trajectory law. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingTrajectoryLaw_isProbability · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:390 Testing experiment with equal fair policies and the explicit finite trajectory law.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingExperiment · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Constructions.lean:405 CausalSmith.Stat.STAT_PomdpBinaryhiddenRate_Research.Helpers.ComplexOscillation 6 declarations Real TV duality applied to rotated real parts controls the diameter of complex functions.
Complex oscillation contraction
Real TV duality applied to rotated real parts controls the diameter of complex functions. This yields the transient eigenvalue bound without an eigenbasis.
Every pair of rows is within the Dobrushin TV coefficient. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.row_tv_le_dobrushin · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/ComplexOscillation.lean:21 A stochastic Dobrushin contraction contracts complex diameters in one step. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.dobrushin_complex_diameter_contraction · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/ComplexOscillation.lean:33 A stochastic matrix fixes complex constant vectors. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.stochastic_complex_constant · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/ComplexOscillation.lean:55 A nonstationary complex eigenvector cannot be constant. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.stochastic_complex_eigenvector_nonconstant · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/ComplexOscillation.lean:64 Nonconstant modes of a stochastic matrix lie in its Dobrushin disk. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.dobrushin_complex_eigenvector_norm_le · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/ComplexOscillation.lean:87 Every characteristic root other than one obeys the Dobrushin bound. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.dobrushin_complex_charpoly_root_norm_le · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/ComplexOscillation.lean:105 CausalSmith.Stat.STAT_PomdpBinaryhiddenRate_Research.Helpers.EmpiricalMoments 12 declarations Each retained score is square-integrable and has the same intervention mean.
Unbiased observable empirical moments
Each retained score is square-integrable and has the same intervention mean. Averaging the T−6 retained epochs therefore gives an unbiased observable moment.
Projection to observed coordinates satisfies the measurability conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.binary_obsProj_measurable · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/EmpiricalMoments.lean:21 The observed law inherits probability mass one from the trajectory law. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.binary_obsLaw_isProbability · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/EmpiricalMoments.lean:28 Policy overlap and bounded rewards make every observable score square-integrable. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.binary_score_memLp_two · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/EmpiricalMoments.lean:34 The mean of an eligible score, computed using only its observed-data law, equals the target-policy matrix-power moment. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.integral_observable_score_eq_matrixMoment · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/EmpiricalMoments.lean:45 The average over epochs seven through T is unbiased for each of the seven intervention moments; its normalization uses exactly T−6 summands. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.empiricalMoment_unbiased · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/EmpiricalMoments.lean:59 The score variance inherits the second-moment bound in the intervention lemma. This controls the diagonal term in equation (8). Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.observable_score_variance_le · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/EmpiricalMoments.lean:94 Without a separation assumption, nonnegativity of the variances of the sum and difference controls covariance by the common score variance bound. This is the short-lag bound in equation (8). Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.observable_score_covariance_le · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/EmpiricalMoments.lean:110 The separated-window covariance estimate also holds under the observed law used by the estimator, by measurable projection of the full trajectory. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.observable_score_covariance_le_separated · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/EmpiricalMoments.lean:133 Finite averaging preserves the scores' square integrability. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.empiricalMoment_memLp_two · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/EmpiricalMoments.lean:149 The unbiased empirical squared error is exactly the normalized finite covariance sum, before bounding short and separated lags in equation (8). Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.empiricalMoment_mse_eq_covariance_sum · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/EmpiricalMoments.lean:157 The square of the maximum of seven absolute errors is bounded by their sum of squares, pointwise, as used in equation (9). the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.seven_error_max_sq_le_sum · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/EmpiricalMoments.lean:181 Integrating the maximum error costs at most the sum of the seven empirical mean-squared errors; no independence between the seven moments is needed. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.empiricalMoment_max_mse_le_sum · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/EmpiricalMoments.lean:190 CausalSmith.Stat.STAT_PomdpBinaryhiddenRate_Research.Helpers.EmpiricalVariance 6 declarations Short lags cost at most six score second moments per epoch; separated lags are summed through the geometric mixing tail.
Finite lag summation for the seven empirical moments
Short lags cost at most six score second moments per epoch; separated lags are summed through the geometric mixing tail. This proves equations (8) and (9).
For a finite collection of nonnegative powers whose distinct exponents all lie below a horizon, the selected power sum is at most the complete geometric sum up to that horizon. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.binary_sum_pow_image_le_range · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/EmpiricalVariance.lean:18 A finite geometric sum with a nonnegative ratio strictly below one is bounded by the reciprocal of one minus that ratio. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.binary_geom_partial_le_inv · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/EmpiricalVariance.lean:34 For a symmetric pairwise quantity on a finite ordered sample, the sum of its absolute values equals the diagonal contribution plus twice the strictly upper-triangular contribution. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.binary_sum_abs_symmetric_eq_diag_add_two_upper · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/EmpiricalVariance.lean:47 The sum over future retained scores has at most k short lags and a geometrically summable separated tail. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.binary_sum_abs_covariance_future_le · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/EmpiricalVariance.lean:97 Equation (8): each unbiased empirical moment has mean-squared error at most V divided by the number of retained epochs. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.empiricalMoment_mse_le_varianceFactor · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/EmpiricalVariance.lean:184 Equation (9): taking the maximum of seven errors costs only a factor seven. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.empiricalMoment_max_mse_le_varianceFactor · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/EmpiricalVariance.lean:264 CausalSmith.Stat.STAT_PomdpBinaryhiddenRate_Research.Helpers.GridAdmissibility 14 declarations The finite candidate set contains a reset kernel.
Admissibility of the finite stable-grid estimator
The finite candidate set contains a reset kernel. Its selected matrix is stochastic, its stationary reward is bounded, and selection is measurable because it depends on finitely many measurable comparisons.
Every enumerated candidate has simplex transition rows. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.gridCandidates_row · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/GridAdmissibility.lean:21 A point-mass row repeated four times supplies a grid candidate. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.gridCandidates_nonempty · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/GridAdmissibility.lean:36 Both stages of minimization retain membership in the candidate set. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.selectGridCode_mem · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/GridAdmissibility.lean:59 Positive-resolution simplex grid rows decode to a stochastic matrix. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.gridR_stochastic · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/GridAdmissibility.lean:74 Mixing a stochastic grid matrix with a positive reset gives a stationary law. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.stabilizedGridMatrix_stationary · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/GridAdmissibility.lean:87 Every selected candidate has a stationary reward between zero and one. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.stableGridEstimator_range · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/GridAdmissibility.lean:126 A fixed-window score satisfies the measurability conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.score_measurable · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/GridAdmissibility.lean:158 Each empirical moment satisfies the measurability conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.empiricalMoment_measurable · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/GridAdmissibility.lean:171 The seven-moment maximum discrepancy satisfies the measurability conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.gridObjective_measurable · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/GridAdmissibility.lean:178 Choosing a minimum depends only on the pairwise order of the objectives. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.grid_min_choose_congr · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/GridAdmissibility.lean:192 The selected code is constant whenever all objective comparisons agree. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.selectGridCode_order_congr · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/GridAdmissibility.lean:209 Finite measurable comparisons give a selected code satisfying the measurability conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.selectGridCode_measurable · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/GridAdmissibility.lean:250 Composing the selected code with its stationary reward satisfies the measurability conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.stableGridEstimator_measurable · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/GridAdmissibility.lean:283 The finite-grid construction gives a unit-interval-valued measurable procedure for every supplied pair of policies in the theorem's regime. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.stableGridEstimator_admissible · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/GridAdmissibility.lean:293 CausalSmith.Stat.STAT_PomdpBinaryhiddenRate_Research.Helpers.GridApprox 4 declarations Round the four-state initial distribution, transition rows, and reward vector onto the rational simplex grid and mix with the uniform reset kernel.
Finite stable-grid approximation
Round the four-state initial distribution, transition rows, and reward vector onto the rational simplex grid and mix with the uniform reset kernel.
Simplex rounding supplies an enumerated stable candidate with the telescoping error. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.grid_candidate_moment_approximation · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/GridApprox.lean:23 A finite relabeling preserves matrix-power moments. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.matrix_moment_relabel · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/GridApprox.lean:92 Relabeling a finite state space preserves contraction of probability vectors. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.contractsL1_relabel · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/GridApprox.lean:110 A stable grid candidate approximates all seven target-policy moments. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.grid_approximation · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/GridApprox.lean:140 CausalSmith.Stat.STAT_PomdpBinaryhiddenRate_Research.Helpers.GridFit 4 declarations Lexicographic tie breaking preserves the minimum empirical residual.
Error transfer for the finite stable-grid fit
Lexicographic tie breaking preserves the minimum empirical residual. A candidate that approximates the seven population moments then bounds the selected fit's population discrepancy by twice the sampling error plus the grid error.
The scalar moment represented by a decoded stable grid candidate.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.gridCodeMoment · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/GridFit.lean:20 The lexicographic tie break selects a candidate with minimum empirical residual. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.selectGridCode_objective_le · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/GridFit.lean:26 An approximating candidate transfers the empirical maximum error to the selected realization's population moments. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.selected_grid_moment_error · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/GridFit.lean:46 Equation (15) of the upper-bound proof: the actual selected candidate fits all seven target-policy moments within twice their sampling error plus T⁻¹. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.selected_grid_intervention_moment_error · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/GridFit.lean:84 CausalSmith.Stat.STAT_PomdpBinaryhiddenRate_Research.Helpers.GridRounding 2 declarations Floor the first three simplex coordinates and assign their discarded mass to the fourth coordinate.
Four-state simplex rounding
Floor the first three simplex coordinates and assign their discarded mass to the fourth coordinate. The decoded row has total-variation error at most 3/M.
Flooring a unit-interval reward gives a grid coordinate with error at most 1/M. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.reward_grid_rounding · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/GridRounding.lean:18 Rounding three coordinates down and using a residual fourth coordinate preserves the simplex, with total-variation error at most 3/M. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.simplex_grid_rounding · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/GridRounding.lean:40 CausalSmith.Stat.STAT_PomdpBinaryhiddenRate_Research.Helpers.GridStability 4 declarations Row-wise rounding preserves the Dobrushin filter.
Stability and error of rounded grid kernels
Row-wise rounding preserves the Dobrushin filter. Mixing with the uniform kernel enforces contraction and costs at most 6/(alpha M) in row TV.
Contraction of probability vectors bounds every pair of point-mass rows. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.contractsL1_gridDobrushin · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/GridStability.lean:19 TV obeys the triangle inequality between finite row vectors. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.row_tv_triangle · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/GridStability.lean:51 Row-wise TV approximation perturbs the Dobrushin coefficient by twice its error. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.gridDobrushin_perturbation · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/GridStability.lean:60 Uniform-reset stabilization preserves stochasticity and has the required row error. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.stabilizedGridMatrix_row_error · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/GridStability.lean:83 CausalSmith.Stat.STAT_PomdpBinaryhiddenRate_Research.Helpers.GridValue 4 declarations Relabeling the four grid coordinates puts the selected realization on the joint-state carrier.
Stationary value transfer for the selected grid
Relabeling the four grid coordinates puts the selected realization on the joint-state carrier. The pair-polynomial modulus then gives equation (16).
The initial coordinates of an admissible positive-resolution code sum to one. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.gridNu_probability · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/GridValue.lean:18 The candidate filter and reset mixture enforce the specified contraction radius. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.stabilizedGridMatrix_dobrushin_le · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/GridValue.lean:35 Relabeling the grid coordinates allows direct use of the joint-state value modulus. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.grid_value_modulus · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/GridValue.lean:67 Equation (16): the selected stationary value inherits twice the empirical moment error. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.stableGridEstimator_value_error · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/GridValue.lean:125 CausalSmith.Stat.STAT_PomdpBinaryhiddenRate_Research.Helpers.InterventionMoments 8 declarations The action-weighted short-history scores identify target-policy transition moments.
Observable intervention moments
The action-weighted short-history scores identify target-policy transition moments. Their second moments and separated-window covariances are controlled by policy overlap and behavior contraction.
Matrix power of a four-state kernel, using matrix multiplication.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.fourMatrixPower · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/InterventionMoments.lean:24 This result establishes the stated mathematical relation for the construction under consideration. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.fourMatrixPower_zero · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/InterventionMoments.lean:27 Covariance of two observable score windows under the full trajectory law.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.scoreCovariance · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/InterventionMoments.lean:33 Likelihood peeling and backward Markov contraction control separated score windows. The unit reward support gives oscillation one, rather than the signed-reward constant two. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.scoreCovariance_le_separated · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/InterventionMoments.lean:40 Each state coordinate integrates against the stationary behavior law. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.integral_binary_curState_eq_stationary · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/InterventionMoments.lean:124 Iterating the Markov operator agrees with multiplying by matrix powers. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.binary_markovOperatorIter_eq_mulVec · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/InterventionMoments.lean:217 The seven observable scores have the intervention identity, bounded second moments, and geometric covariance decay for separated windows. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.observable_intervention_moments · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/InterventionMoments.lean:233 The zero-lag intervention identity under the four conditions used in the coincident-policy reduction. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.observable_intervention_moment_zero · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/InterventionMoments.lean:283 CausalSmith.Stat.STAT_PomdpBinaryhiddenRate_Research.Helpers.ModelRegularity 4 declarations Probability policies give stochastic transition rows and unit-range reward regressions.
Binary POMDP kernel regularity
Probability policies give stochastic transition rows and unit-range reward regressions. Contracted target kernels have stationary probability laws.
Probability target policies preserve the unit range of kernel rewards. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.rewardRegression_unit · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/ModelRegularity.lean:18 Unit-range kernel rewards and probability policies keep the target value in [0,1]. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.targetValue_mem_unitInterval · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/ModelRegularity.lean:59 A probability reward-successor kernel and a probability policy induce stochastic rows. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.policyKernel_stochastic_of_kernelLaw · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/ModelRegularity.lean:82 The contracted target kernel has the selected stationary probability law. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.targetStationary_of_class · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/ModelRegularity.lean:114 CausalSmith.Stat.STAT_PomdpBinaryhiddenRate_Research.Helpers.PairPolynomial 30 declarations The four-state transient characteristic factors yield an exact stationary-value identity and a uniform seven-moment modulus under Dobrushin contraction, including complex and defective transient modes.
Seven-moment pair-polynomial stability
The four-state transient characteristic factors yield an exact stationary-value identity and a uniform seven-moment modulus under Dobrushin contraction, including complex and defective transient modes.
The moment of a row vector, transition matrix, and reward vector.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.matrixMoment · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/PairPolynomial.lean:22 The stationary value of a finite reward vector.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.matrixValue · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/PairPolynomial.lean:27 Stationarity is preserved by every matrix power. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.stationary_vecMul_pow · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/PairPolynomial.lean:31 Left evaluation of a polynomial against a stationary law evaluates at one. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.stationary_vecMul_aeval · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/PairPolynomial.lean:40 The constant right vector witnesses the stationary characteristic root. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.stochastic_charpoly_isRoot_one · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/PairPolynomial.lean:52 Exact characteristic factorization, independent of diagonalizability. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.stochastic_charpoly_factor · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/PairPolynomial.lean:65 Cayley–Hamilton puts the transient polynomial's image in the fixed space. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.transientPoly_aeval_annihilated · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/PairPolynomial.lean:72 Polynomial matrix evaluation is the corresponding finite moment sum. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.matrixMoment_polynomial_sum · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/PairPolynomial.lean:79 Centering at the midpoint gives TV duality for any bounded real vector. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.probability_mean_tv_interval · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/PairPolynomial.lean:93 Dobrushin contraction below one leaves only constant right fixed vectors. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.dobrushin_fixedVector_constant · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/PairPolynomial.lean:122 Stationarity rules out a nonzero constant in the image of the shifted operator. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.stationary_shift_constant_eq_zero · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/PairPolynomial.lean:155 No nontrivial Jordan chain can end in the eigenspace at one. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.dobrushin_shift_sq_kernel · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/PairPolynomial.lean:167 Every positive power of the shifted operator has the same kernel. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.dobrushin_shift_pow_kernel · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/PairPolynomial.lean:182 The entire generalized eigenspace at one is the line of constant vectors. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.dobrushin_maxGenEigenspace_one · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/PairPolynomial.lean:198 Strict Dobrushin contraction makes the stationary characteristic root simple. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.dobrushin_charpoly_rootMultiplicity_one · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/PairPolynomial.lean:225 Algebraic simplicity makes the transient characteristic factor nonzero at one. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.transientPoly_eval_one_ne_zero · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/PairPolynomial.lean:239 The pair polynomial has a nonzero denominator at the stationary root. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.pairPoly_eval_one_ne_zero · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/PairPolynomial.lean:257 The transient polynomial is exactly the stationary rank-one projection. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.transientPoly_aeval_projection · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/PairPolynomial.lean:269 A stochastic matrix's transient characteristic factor is monic. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.transientPoly_monic · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/PairPolynomial.lean:297 The four-state transient characteristic factor has degree three. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.transientPoly_natDegree_three · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/PairPolynomial.lean:305 The product of stochastic transient factors is monic. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.pairPoly_monic · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/PairPolynomial.lean:314 The pair factor has exactly six roots counted with algebraic multiplicity. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.pairPoly_natDegree_six · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/PairPolynomial.lean:321 Transient roots exclude one and inherit the complex Dobrushin disk bound. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.transientPoly_complex_root_norm_le · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/PairPolynomial.lean:330 Every root of the pair factor belongs to one of its two transient factors. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.pairPoly_complex_roots_norm_le · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/PairPolynomial.lean:351 The pair factor has degree at most six on the four-state carrier. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.pairPoly_natDegree_lt_seven · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/PairPolynomial.lean:367 Multiplying by any other polynomial preserves the stationary projection. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.transientPoly_mul_aeval_projection · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/PairPolynomial.lean:380 Averaging the projection by any initial law gives the stationary value. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.polynomial_projection_value · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/PairPolynomial.lean:398 The exact seven-moment identity follows without choosing an eigenbasis. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.pairPolynomial_value_identity · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/PairPolynomial.lean:410 The exact identity transfers moment error with the actual polynomial coefficient ratio. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.pairPolynomial_value_coefficient_modulus · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/PairPolynomial.lean:437 Exact pair-polynomial identity and seven-moment modulus, including defective and complex transient modes. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.pairPolynomial_value_modulus · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/PairPolynomial.lean:478 CausalSmith.Stat.STAT_PomdpBinaryhiddenRate_Research.Helpers.PairPolynomialBounds 4 declarations Coefficient and evaluation bounds for a monic degree-six polynomial whose complex roots lie in a disk of radius less than one, counted with algebraic multiplicity.
Root-based polynomial stability estimates
Coefficient and evaluation bounds for a monic degree-six polynomial whose complex roots lie in a disk of radius less than one, counted with algebraic multiplicity.
Bounded complex roots control the sum of the seven real coefficients. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.degreeSix_coeff_sum_le_of_roots_le · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/PairPolynomialBounds.lean:19 A root disk below one gives a lower bound on a product of distances to one. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.roots_distance_prod_lower · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/PairPolynomialBounds.lean:37 The degree-six monic factor is bounded away from zero at one. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.degreeSix_eval_one_lower_of_roots_le · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/PairPolynomialBounds.lean:54 The two root estimates yield the sharp seven-coefficient stability ratio. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.degreeSix_coefficient_ratio_le_of_roots_le · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/PairPolynomialBounds.lean:68 CausalSmith.Stat.STAT_PomdpBinaryhiddenRate_Research.Helpers.ScoreMoments 7 declarations Kernel reward support gives almost-sure unit rewards.
Likelihood-weighted score moments
Kernel reward support gives almost-sure unit rewards. The finite-history likelihood cancellation bounds first and second score moments, even when behavior action cells vanish. These bounds do not require stationarity.
The kernel reward support transfers to every sampled reward coordinate. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.pomdp_reward_mem_Icc_ae · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/ScoreMoments.lean:20 Bounded kernel rewards are integrable under the trajectory probability law. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.pomdp_reward_integrable · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/ScoreMoments.lean:41 View the same trajectory experiment in the general finite POMDP carrier.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.finitePomdpView · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/ScoreMoments.lean:50 The general finite-history law conditions follow from the binary law conditions; the stronger kernel reward support supplies its reward premise. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.finitePomdpView_laws · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/ScoreMoments.lean:57 The observed score has the same definition in the general finite-history carrier. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.score_eq_phiwScore · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/ScoreMoments.lean:77 Likelihood cancellation bounds the absolute first moment by one. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.score_abs_first_moment_le_one · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/ScoreMoments.lean:84 Squaring a score costs one overlap factor per action, since the other likelihood-ratio product integrates to one under sequential randomization. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.score_second_moment_le · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/ScoreMoments.lean:104 CausalSmith.Stat.STAT_PomdpBinaryhiddenRate_Research.Helpers.TestingFamily 1 declarations Assemble the positive testing pair and its observed-data divergence bound.
Testing-family membership and separation
Assemble the positive testing pair and its observed-data divergence bound.
Both testing laws satisfy all six model conditions, have exact target separation, and are close after projection to observed data. Their policies coincide and their stationary joint-state laws coincide. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingFamily_membership · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingFamily.lean:18 CausalSmith.Stat.STAT_PomdpBinaryhiddenRate_Research.Helpers.TestingFamilyBasics 5 declarations History factorization, class membership, and positivity of the testing laws.
Testing family membership
History factorization, class membership, and positivity of the testing laws.
The finite path weights realize the conditional reward/transition law, fair-action assignment, and stationary initial state. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingExperiment_historyConditions · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingFamilyBasics.lean:16 The explicit testing laws meet the remaining overlap and contraction conditions once their finite-history factorization is established. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingExperiment_class_of_history · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingFamilyBasics.lean:79 Every testing path has strictly positive mass throughout the perturbation range. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingPathWeight_pos · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingFamilyBasics.lean:101 The testing laws have common finite support, hence every alternative is absolutely continuous with respect to every other admissible alternative. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingTrajectoryLaw_absolutelyContinuous · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingFamilyBasics.lean:131 Finite support and common positive path masses give finite KL divergence, which remains finite after projection to the observed trajectory. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingObservedLaw_klDiv_ne_top · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingFamilyBasics.lean:150 CausalSmith.Stat.STAT_PomdpBinaryhiddenRate_Research.Helpers.TestingFamilyCore 15 declarations The fair-policy binary-hidden family gives two stationary models separated in target value while their observed trajectory laws have small KL divergence.
Positive four-state testing family
The fair-policy binary-hidden family gives two stationary models separated in target value while their observed trajectory laws have small KL divergence.
The positive perturbation lies in the probability range. Under the listed formal conditions, the stated conclusion holds.
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.vT_bound · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingFamilyCore.lean:19 The negative perturbation lies in the probability range. Under the listed formal conditions, the stated conclusion holds.
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.neg_vT_bound · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingFamilyCore.lean:25 The fair coincident policies of either testing experiment satisfy target overlap for every nonnegative log-overlap radius. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingExperiment_policyOverlap · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingFamilyCore.lean:30 Both testing reward probabilities stay uniformly away from zero and one. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingRewardProb_mem_Icc · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingFamilyCore.lean:52 The explicit Bernoulli reward and successor-state kernel has unit mass. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingKernel_probability · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingFamilyCore.lean:60 Every atom of the testing kernel has reward zero or one. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingKernel_rewardSupport · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingFamilyCore.lean:100 Averaging the testing transition over the fair action gives the same row at every current state, independently of the reward perturbation. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingExperiment_policyKernel_eq · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingFamilyCore.lean:109 The common transition row is a stationary probability vector. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingExperiment_stationary · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingFamilyCore.lean:127 The selected stationary law of a testing experiment is its common transition row. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingExperiment_stationaryLaw_eq · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingFamilyCore.lean:149 The common transition row contracts every pair of state distributions. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingExperiment_contraction · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingFamilyCore.lean:171 Integrating the reward coordinate of a testing kernel recovers its Bernoulli parameter. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingKernel_reward_integral · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingFamilyCore.lean:202 The testing reward regression depends only on the current hidden state. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingExperiment_rewardRegression_eq · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingFamilyCore.lean:229 Every stationary testing experiment has target value one half plus its perturbation. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingExperiment_targetValue_eq · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingFamilyCore.lean:238 A stationary on-policy law obeys every occupancy-ratio bound above one. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.coincidentPolicy_occupancy_bound · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingFamilyCore.lean:255 Summing every continuation of a fixed initial state recovers its initial mass. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingPathWeight_initial_sum · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingFamilyCore.lean:266 CausalSmith.Stat.STAT_PomdpBinaryhiddenRate_Research.Helpers.TestingHistoryEncoding 18 declarations The explicit testing weights are the chronological finite-model construction.
Finite encoding of the binary testing paths
The explicit testing weights are the chronological finite-model construction. Transporting its history factorizations gives the required conditional laws.
The testing reward and successor mass on a two-symbol reward alphabet.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingFiniteWeight · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingHistoryEncoding.lean:21 All finite reward-transition weights are nonnegative in the testing range. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingFiniteWeight_nonneg · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingHistoryEncoding.lean:29 The finite reward-transition weights have unit total mass. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingFiniteWeight_sum · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingHistoryEncoding.lean:40 The finite PMF version of the joint testing kernel.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingFiniteKernel · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingHistoryEncoding.lean:48 Normalization preserves the explicit finite testing kernel weights. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingFiniteKernel_apply · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingHistoryEncoding.lean:53 The stationary initialization as a finite PMF.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingFiniteInit · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingHistoryEncoding.lean:61 The initialization PMF preserves the displayed stationary masses. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingFiniteInit_apply · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingHistoryEncoding.lean:66 The fair action PMF.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingFairPMF · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingHistoryEncoding.lean:76 Each action has probability one half. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingFairPMF_apply · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingHistoryEncoding.lean:81 A chronological finite reward model for the testing experiment.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingFiniteModel · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingHistoryEncoding.lean:89 Changing the reward alphabet between two finite symbols and Booleans.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingFinitePathEquiv · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingHistoryEncoding.lean:104 The chronological finite weight is exactly the displayed testing weight. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingFinitePathWeight_eq · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingHistoryEncoding.lean:111 The finite path PMF has the explicit testing path masses. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingFiniteModel_law_apply · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingHistoryEncoding.lean:132 Decoding the finite kernel recovers the real-reward testing kernel. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingFiniteModel_kernel_eq · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingHistoryEncoding.lean:145 Decoding the finite path law recovers the displayed testing trajectory law. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingFiniteModel_law_eq · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingHistoryEncoding.lean:167 The decoded finite model has the fair behavior policy. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingFiniteModel_policy_eq · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingHistoryEncoding.lean:186 The testing joint kernel is the conditional law given the complete action history. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingExperiment_kernelHistory · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingHistoryEncoding.lean:195 The fair behavior policy is the conditional action law given the complete state history. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingExperiment_actionHistory · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingHistoryEncoding.lean:215 CausalSmith.Stat.STAT_PomdpBinaryhiddenRate_Research.Helpers.TestingKL 12 declarations Cancel the common state and action factors and sum the conditional Bernoulli reward divergences before projecting the finite path law to observed data.
Quantitative divergence of the testing pair
Cancel the common state and action factors and sum the conditional Bernoulli reward divergences before projecting the finite path law to observed data.
Independent finite factors with common masses and bounded one-factor entropy have a product entropy bounded by the sum of their budgets. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testing_product_entropy_le · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingKL.lean:20 One fair-action epoch mass, with a Boolean reward.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingKLStep · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingKL.lean:80 Every single-epoch testing mass is positive. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingKLStep_pos · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingKL.lean:89 Reward and action marginalization leaves the common next-state mass. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingKLStep_sum · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingKL.lean:103 The common transition factors cancel from the one-epoch KL contribution. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingKLStep_entropy_le · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingKL.lean:109 Canceling the common initial mass and adding epoch budgets bounds the complete-data finite path entropy. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingPath_entropy_le · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingKL.lean:160 Keep the finite Boolean path carrier before decoding to real rewards.
Definition (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingFinitePathLaw · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingKL.lean:223 The finite path law assigns its displayed weight to each singleton. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingFinitePathLaw_mass · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingKL.lean:228 The finite path measure is normalized throughout the perturbation range. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingFinitePathLaw_probability · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingKL.lean:236 Strictly positive finite path weights give common support. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingFinitePathLaw_ac · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingKL.lean:247 Decoding the finite path measure gives the declared full trajectory law. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingFinitePathLaw_map · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingKL.lean:262 Each reward contributes its Bernoulli divergence; data processing then bounds the observed-law divergence without assumptions on history identities. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingObservedLaw_klDiv_le · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/Helpers/TestingKL.lean:282 CausalSmith.Stat.STAT_PomdpBinaryhiddenRate_Research.TCoincidentPolicyReduction 12 declarations When target and behavior policies agree, intervention moments reduce to the on-policy stationary reward mean and the empirical mean has parametric risk.
Coincident-policy reduction
When target and behavior policies agree, intervention moments reduce to the on-policy stationary reward mean and the empirical mean has parametric risk.
Coincident policies induce the same transition matrix and selected stationary law. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.coincidentPolicy_kernel_stationary · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/TCoincidentPolicyReduction.lean:19 An action drawn from the behavior policy has positive behavior mass almost surely. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.sequentialIgnorability_supported_action · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/TCoincidentPolicyReduction.lean:27 At coincident policies the zero-lag importance score equals the reward, including when the behavior policy has zero cells. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.coincidentPolicy_score_zero_ae · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/TCoincidentPolicyReduction.lean:51 The stationary reward mean is the causal target when policies coincide. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.coincidentPolicy_reward_mean · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/TCoincidentPolicyReduction.lean:74 The observed sample mean is unbiased at coincident policies. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.coincidentPolicy_sampleMean_unbiased · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/TCoincidentPolicyReduction.lean:87 Coincident policies supply overlap radius zero and the same contraction for both kernels. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.coincidentPolicy_binaryClass · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/TCoincidentPolicyReduction.lean:103 Separated rewards have the geometric covariance bound at coincident policies. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.coincidentPolicy_reward_covariance · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/TCoincidentPolicyReduction.lean:117 A finite geometric tail is bounded by the infinite-series value. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.finiteGeometric_sum_le · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/TCoincidentPolicyReduction.lean:141 An injectively indexed subset of a geometric tail satisfies the same bound. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.finiteGeometric_sum_image_le · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/TCoincidentPolicyReduction.lean:150 A symmetric covariance row with unit diagonal and geometric off-diagonal bounds has total mass at most one plus two geometric tails. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.geometricCovariance_row_sum_le · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/TCoincidentPolicyReduction.lean:167 Expanding the covariance sum gives the stated parametric on-policy risk bound. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.coincidentPolicy_sampleMean_mse · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/TCoincidentPolicyReduction.lean:232 For positive mixing time, a nonempty horizon, the POMDP kernel law, sequential ignorability, stationary start, behavior contraction, and coincident policies, the on-policy identity, unbiased sample mean, and variance bound hold.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.coincidentPolicy_reduction · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/TCoincidentPolicyReduction.lean:291 CausalSmith.Stat.STAT_PomdpBinaryhiddenRate_Research.TExhaustiveGridComplexity 6 declarations The finite simplex grid has a stars-and-bars count.
Candidate count of the exhaustive grid
The finite simplex grid has a stars-and-bars count. Its candidate-list cardinality has degree-nineteen growth for fixed mixing scale.
Stars and bars for the four-coordinate grid. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.simplexGrid_card · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/TExhaustiveGridComplexity.lean:19 Four independently selected simplex rows form the matrix grid. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.gridMatrixRows_card · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/TExhaustiveGridComplexity.lean:58 An unfiltered code consists of an initial row, four matrix rows, and rewards. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.gridCandidateUniverse_card · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/TExhaustiveGridComplexity.lean:73 The exact count is bounded by a degree-nineteen monomial. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.gridCandidateUniverse_growth · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/TExhaustiveGridComplexity.lean:92 The ceiling resolution grows linearly with the trajectory length. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.gridSize_linear_bound · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/TExhaustiveGridComplexity.lean:105 For positive mixing time, the stars-and-bars grid size, exact unfiltered candidate count, and degree-nineteen candidate-list growth hold for fixed t0. No fitting or selection cost is assigned.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.exhaustiveGrid_candidate_count · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/TExhaustiveGridComplexity.lean:120 CausalSmith.Stat.STAT_PomdpBinaryhiddenRate_Research.TFixedBinaryMinimax 6 declarations The seven-moment upper bound and positive four-state testing pair give a uniform parametric minimax rate.
Fixed-binary POMDP minimax rate
The seven-moment upper bound and positive four-state testing pair give a uniform parametric minimax rate. The cited cardinality-uniform comparator is an explicit input only to the contrast with growing hidden cardinality.
A squared risk dominates the squared threshold times its error probability. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.sqRisk_ge_error_probability · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/TFixedBinaryMinimax.lean:22 A measurable estimator taking values in the unit interval has integrable square loss. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.bounded_estimator_sqError_integrable · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/TFixedBinaryMinimax.lean:56 The finite-KL testing pair forces a squared-risk lower bound for each observable estimator. Under the listed formal conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.testingPair_observedRisk_lower · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/TFixedBinaryMinimax.lean:76 Every admissible observable estimator has squared risk between zero and one. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.observedRisk_unit_bounds · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/TFixedBinaryMinimax.lean:153 For positive mixing time, positive overlap exponent, a fixed overlap constant, and the cited comparator, the reset construction has logarithmic depth and eventually needs more than two hidden states.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.comparator_reset_depth_growth · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/TFixedBinaryMinimax.lean:184 For positive mixing time, nonnegative overlap exponent, the stated horizon range, and the cited comparator, the exact fixed-binary minimax rate, transferable testing pair, and asymptotic separation hold.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.fixedBinary_minimax · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/TFixedBinaryMinimax.lean:212 CausalSmith.Stat.STAT_PomdpBinaryhiddenRate_Research.TStableGridUpper 1 declarations The finite observed-data grid estimator attains a uniform parametric mean-squared-error bound over the six-condition binary POMDP class.
Fixed-binary stable-grid upper bound
The finite observed-data grid estimator attains a uniform parametric mean-squared-error bound over the six-condition binary POMDP class.
For positive mixing time, nonnegative overlap exponent, and the stated horizon range, the seven-moment stable-grid estimator satisfies the uniform mean-squared-error bound.
Formal statement
Proof (Lean source)
CausalSmith.Stat.PomdpBinaryhiddenRate.stableGrid_upper · CausalSmith/Stat/STAT_PomdpBinaryhiddenRate_Research/TStableGridUpper.lean:20