martingale_check
std.stats.martingale_check · Level L2The martingale conditions for a process X_0 … X_T (one row per time) on a finite probability space with a filtration given by partitions L (one row per time): whether L is a filtration; whether X is adapted (each X_t constant on the blocks of F_t); and the gaps E[X_{t+1} | F_t] − X_t for t < T, which are all 0 for a martingale. Integrability is automatic on a finite space. A martingale need not have independent increments, be Markov, or converge.
Signature
martingale_check(L: f64[T, n], X: f64[T, n], p: f64[n]) → f64[], f64[], f64[T−1, n]
Requires: T ≥ 2
Structure
The function as NOVA stores it: one box per input, operation and output, and arrows that carry values. A double border marks another library function this one runs — called once, or by Scan once per element; select it to open that function.
- input
- operation
- constant
- call
- output
Verification
- Signature proven by NOVA’s shape solver, for every size with T ≥ 2.
- Equal to the reference
block by block at every time, in exact arithmeticin exact rational arithmetic, on all 40 test cases. - All 575 float64 results inside the running error bound; the closest uses 44% of it.
- Interpreter and NumPy backend return bit-identical results.
- At float32 too: the 40 test cases rounded to float32, and 40 of them inside the running error bound at u = 2⁻²⁴; the closest uses 41% of it.
- correctly rounded (the float64 nearest the exact value)
- 87%
- bit-equal to the NumPy formula in float64
- 100%
- largest error, in units in the last place
- 29
Large ulp counts appear where a result is tiny next to the numbers it is computed from (after cancellation, for example), so one unit in the last place is tiny too; the absolute error is still inside the bound. Results within their own error of zero are not counted.
Identity
sha256:934c545adb4d2b1f34b3e03adfaac3a4e875c6e495c95597814f887abacd44c6The semantic hash of the graph. It changes when the program changes, and never when only its documentation does.
Control handle
- Symbol
- Ω:std.stats.martingale_check · Ω:martingale_check
- Pins
sha256:30b8f5c3f106f2fb7b3c2946136344ffaf8fbc3dc8755f395c88f934514a842ethis graph and the 3 it reaches through calls- Evidence
sha256:552ca3eac8c8a0e9212e744277eb300f845a06ad5bec59e3ebc5022d69f1da3athe hash of its verification record- Needs
- no capability: a pure function
Through NOVA’s control layer, the symbol launches this function only while the program still matches what it pins: a change to this graph, or to any graph it reaches, needs a migration first.