95. A fully rational dependent-data reference experiment
On this page · Permalink · Source line 3828
Both the continuous uniform measure \(du/2\) and the following five-node measure satisfy the moment assumptions:
The reference experiment uses the five-node measure, not rounded observations from the continuous model. At each step, the conditional probability of a node is its reference weight times \(p_{a,b}(u\mid s)\). Exact rational probabilities are sampled by integer draws. The learner receives only the node sequence, the measure and the declared model. The true parameters are present only in the separate generator and verification code.
Matching four moments does not identify the two observation laws. The continuous model gives the set of five nodes probability zero, while the discrete model gives it probability one. Their single-observation total variation is therefore one. The continuous theorems and the exact discrete reference calculation are deliberately distinguished.
For a path of \(n\) transitions, use two scalar regressions,
The noise scales follow from response ranges \([-1,1]\) and \([-1/2,1]\). The prior parameter bounds are \(|a|,|b|\leq1\). Each regression uses ridge one and failure probability \(1/40\), giving a total failure budget \(1/20\) for both parameters at every time.
Proposition 84: Exact rational outer confidence intervals
Write \(V=1+\sum\phi_t^2\) and \(\widehat\theta=\sum\phi_tY_t/V\). Let \(k=\lceil\log_2 V\rceil\) and \(h=\lceil\log_2(1/\delta)\rceil\). A rational upper enclosure of
is an upper bound on Proposition 81's scalar radius. Rounding the lower interval endpoint downward and the upper endpoint upward, then intersecting with \([-1,1]\), preserves its conditional coverage. Both intervals cover their true parameters simultaneously at every time with probability at least \(19/20\).
Read proof · Recorded Lean scope · Visual guide: A confidence set can meet an exact certificate · Permalink · Source line 3854
Proof
The positive exponential series gives \(e^{7/10}>1+7/10+(7/10)^2/2+(7/10)^3/6+(7/10)^4/24>2\). Hence \(\log 2<7/10\), so \(\log V+2\log(1/\delta)\leq(7/10)(k+2h)\). Divide the scalar regression bound by \(\sqrt V\). For a nonnegative rational \(x\), the smallest integer \(j\) with \((j/10^{12})^2\geq x\) supplies a rational upper square-root enclosure. Integer square root and an exact final comparison compute it. Outward rounding only enlarges the interval. Intersecting with a true prior constraint preserves coverage. Apply the two-regression union bound on their time-uniform events. \(\square\)
All counts, sums, radius enclosures and interval endpoints in this experiment are rational. No floating-point logarithm is trusted in the confidence arithmetic. An exact replay verifies the arithmetic and the declared protocol. It does not authenticate the observations, prove that a physical process satisfies the model, or measure the procedure's coverage from one pseudorandom run.
95.1 Executed result
On this page · Permalink · Source line 3866
The seeded reference path uses \(a=2/5\), \(b=1/5\) and initial observation zero. It was first run to 65,536 transitions and then extended along the same seeded path to 262,144. Time-uniform coverage permits that extension without spending another time-selection budget. This is not a new independent coverage experiment.
At the final checkpoint, outward-rounded intervals are
Every member of this rectangle has density at least
The rounded fitted center is \((409/1000,203/1000)\). It lies inside the rectangle. No reset or other coefficient correction is applied.
At earlier recorded checkpoints the sufficient density-floor test withheld a whole-box certificate. Its first successful recorded checkpoint was 32,768 transitions, with floor \(1/100\). This is not a claim that 32,768 is the smallest possible sample size, or even the first passing individual step. Only the declared checkpoints were evaluated. A withheld whole-box certificate does not declare the nominal fit or true process invalid.