Verification Block
Exact Symbolic Checks
These checks use SymPy to simplify the theorem, conditional-risk remainder, and rank-1 monitoring identities exactly.
sympy
Pass
Poincaré / Wirtinger sharpness
The first cosine eigenfunction attains equality in the time-domain bound.
\[\bar r = \frac{1}{T}\int_0^T \cos\!\left(\frac{\pi t}{T}\right) dt = 0\]
\[\mathrm{Var}_U(r(U)) = \frac{1}{T}\int_0^T \cos^2\!\left(\frac{\pi t}{T}\right) dt = \frac{1}{2}\]
\[\frac{T}{\pi^2}\int_0^T (r'(t))^2 dt = \frac{1}{2}\]
- Used r(t) = cos(pi t / T), the first zero-mean eigenfunction on [0, T].
- Verified the temporal mean is exactly zero.
- Verified Var_U(r(U)) and (T / pi^2) int_0^T (r'(t))^2 dt simplify to the same closed form.
| Metric | Value |
|---|
| mean | 0 |
| variance | 1/2 |
| rhs | 1/2 |
| gap | 0 |
sympy
Pass
Jacobian-velocity theorem on a deterministic path
For X_t = t, g = f, and f(x) = cos(pi x / T), the theorem is exact with beta = 1.
\[X_t = t,\qquad \dot X_t = 1,\qquad f(x) = g(x) = \cos\!\left(\frac{\pi x}{T}\right)\]
\[J_f(X_t)\dot X_t = -\frac{\pi}{T}\sin\!\left(\frac{\pi t}{T}\right)\]
\[\mathrm{Var}_U(r(U)) = \frac{T}{\pi^2}\int_0^T \left\|J_f(X_t)\dot X_t\right\|^2 dt = \frac{1}{2}\]
- The deployment path is deterministic, so the expectation operators collapse exactly.
- Because g = f, Assumption A3 holds with beta = 1 and |grad g dot Xdot| = |J_f Xdot|.
- The Jacobian-velocity right-hand side equals the exact volatility from the lemma-sharp example.
| Metric | Value |
|---|
| variance | 1/2 |
| jv rhs | 1/2 |
| gap | 0 |
sympy
Pass
Composition case in Remark A3
Directional derivatives of g = h o f factor exactly into h'(f) and the score Jacobian term.
\[g(x) = h(f(x)),\qquad h(z) = \arctan(z)\]
\[\nabla g(x)\cdot v = h'(f(x))\, \nabla f(x)\cdot v\]
- Used a nontrivial smooth score field f(x1, x2) = x1^2 + x1 x2 + sin(x2).
- Used h(z) = atan(z), so g(x1, x2) = atan(f(x1, x2)).
- Simplified grad g dot v - h'(f) grad f dot v to zero exactly.
sympy
Pass
Conditional-risk remainder identity
The conditional cross-entropy derivative splits exactly into a score-mediated term and the remainder used in Proposition 1.
\[g(x)=\log(1+e^{f(x)})-\eta(x)f(x)\]
\[g'(x)=(\sigma(f(x))-\eta(x))f'(x)-\eta'(x)f(x)\]
\[2\beta^2\gamma^2+2q^2-(\beta\gamma+q)^2=(\beta\gamma-q)^2\ge 0\]
- Wrote binary conditional risk as softplus(f(x)) - eta(x) f(x).
- Verified its derivative equals (sigma(f)-eta) f' - eta' f exactly.
- Verified the separated bound because 2 beta^2 gamma^2 + 2 q^2 - (beta gamma + q)^2 = (beta gamma - q)^2 >= 0.
| Metric | Value |
|---|
| decomposition gap | 0 |
| separated square gap | 0 |
sympy
Pass
Rank-1 hazard-score bookkeeping
The pointwise algebra behind Proposition 2 is exact; the expectation form follows by averaging these identities.
\[\frac{\Delta \mu_t}{\Delta} = a v + r u,\qquad v_t = c v + s u,\qquad v^\top u = 0\]
\[s_t^2 = \left\|\frac{\Delta \mu_t}{\Delta}\right\|^2 = |a|^2 + |r|^2\]
\[\|J_f v_t\|^2 = c^2\|J_f v\|^2 + s^2\|J_f u\|^2 + 2cs\langle J_f v, J_f u\rangle\]
- Worked in an orthonormal basis with v = e1, u = e2, Delta mu / Delta = (a, r), and a generic 2 x 2 Jacobian matrix.
- Verified s_t^2 = |a|^2 + |r|^2 from the orthogonal block-drift decomposition.
- Verified the directional energy splits into aligned, orthogonal, and overlap terms with coefficients c^2, s^2, and 2cs.
| Metric | Value |
|---|
| s sq gap | 0 |
| g gap | 0 |
| h gap | 0 |
sympy + dense numeric sweep
Pass
Bernoulli cross-entropy derivative bound
The soft-target Bernoulli cross-entropy derivative is sigma(z) - q, so its magnitude never exceeds 1.
\[h(z) = -q \log \sigma(z) - (1-q)\log(1-\sigma(z))\]
\[h'(z) = \sigma(z) - q,\qquad |h'(z)| \le 1 \text{ for } q \in [0,1]\]
- Differentiated the scalar loss h(z) = -q log sigma(z) - (1-q) log(1-sigma(z)) exactly.
- Verified the closed form h'(z) = sigma(z) - q symbolically.
- Checked the beta = 1 bound over a dense grid in z and q.
| Metric | Value |
|---|
| identity gap | 0 |
| max abs derivative on grid | 0.999994 |