Verification corpus

Generated 2026-07-31T00:20:11+00:00 · every figure on this page is read from the artifacts at generation time, never typed

Tommy Ferreira · tommy@vcb-ai.online

Evidence tiers

Verification log

from verify_math1.py — tier badges applied to the raw output

HOW TO READ THIS LOG — the green checks are NOT all the same kind of green.
  [WITNESS  n=k]  SymPy proved the identity at FIXED arity k. Not the general case.
  [EMPIRICAL   ]  checked over a finite sweep of parameters. Not a proof.
  plain PASS    a numeric claim reproduced to the stated precision.
  Hypothesis      falsification search, 200 draws. NOT a proof of the universal.
  The GENERAL statements are kernel-checked in lean-proofs/ (28 theorems,
  axiom-audited, no sorryAx) — list derived from source, not typed:
     weighted_residuals_sum_zero  weighted_sse_decomp  wmean_minimises
     power_at_indifference_lt_alpha  no_calibrated_powered_threshold  no_sample_size_escapes
     discrimination_survives_calibration  calibrated_test_is_still_useful  corrWeight_zero
     corrWeight_one  bStar_zero  bStar_minimises
     b2_optimal_iff_matches_bStar  binomTail_nonneg  binomTail_antitone_k
     binom_power_at_indifference_lt_alpha  binom_no_sample_size_escapes  binomTail_of_lt
     binomTail_top  binomTail_top_monotone  tail_le_of_rate_le
     calibrated_below_boundary  succ_mul_choose  choose_mul_eq
     choose_mul  choose_mul'  CG_empty_is_degenerate
     article_swap_is_CR_failure
  Reading a WITNESS as a general proof is the stratified-instrument defect this
  package exists to catch. See MATH2.md Appendix 2 R4 and Appendix 3 W4.


==============================================================================
SECTION 1 — LegalOne PAS stability (Eq 1-5)
==============================================================================
  Eq 3 raw        :  TrSigma*eta**2*lambda_max/2 + eta**2*g2*lambda_max/2 - eta*g2
  doc's split     :  descent=-eta*g2*(-eta*lambda_max/2 + 1)   noise=TrSigma*eta**2*lambda_max/2
  PASS Eq 3 descent+noise split is algebraically exact
  PASS Eq: stability window eta < 2/lambda_max   solve gives eta < 2/lambda_max
  PASS noise term convex in eta (d2/deta2 > 0)   d2/deta2 = TrSigma*lambda_max
  PASS Eq 5: exp(5) ~ 148   exp(5)=148.4132
  PASS Eq 5: alpha->1 relaxes EXACTLY to equilibrium w1   P(anchor|a=1)=0.200000
         alpha:  0.00 -> P(anchor)=0.9738   0.50 -> 0.7528   1.00 -> 0.2000
  NEW  Doc says alpha->0 'collapses onto the anchor'. It reaches 97.38%, not 100%.
         Bounded by w1*e^5/(w1*e^5+1-w1). To exceed 99% at w1=0.2 needs lambda>=6.0.

==============================================================================
SECTION 2 — LegalOne token-level baseline (Eq 6-14)
==============================================================================
  WITNESS Eq 13: cross term collapses to 0  [WITNESS n=5; general = Lean weighted_residuals_sum_zero]   cross = 0
  WITNESS Eq 14: Var1 = Var2 + N(b2-b1)^2  [WITNESS n=5; general proof = Lean weighted_sse_decomp]   residual = 0
  PASS b2 is the stationary point of the weighted SSE

  --- the assumption the proof rests on, made explicit ---
  Doc asserts:  Var(ghat) proportional to  sum_i L_i (R_i - b)^2
  But minimising a weighted SSE by its own weighted mean is a tautology.
  ALL content lives in that proportionality. Deriving it:
     ghat = (1/N) sum_i sum_j s_ij (R_i - b),   E[s_ij] = 0
     Cov(s_ij, s_ik) = sigma^2 rho I  for j != k   (within-sequence rho)
     Var(sum_j s_ij) = sigma^2 [ L_i + rho L_i (L_i - 1) ] =: sigma^2 W_i(rho)
  PASS rho=0  =>  b*(rho) == b2 (length-weighted)
  PASS rho=1  =>  b*(rho) == length-SQUARED weighted mean
  NEW  Eq 14's CONCLUSION holds only in the rho=0 limit.
         Algebra exact; applicability is not. Optimal baseline drifts L_i -> L_i^2 as rho grows.

  crossover: L_i^2 term dominates when rho > 1/(L_i - 1)
      L=  100  rho* = 0.01010  (1.010%)
      L=  500  rho* = 0.00200  (0.200%)
      L= 1000  rho* = 0.00100  (0.100%)
      L= 4000  rho* = 0.00025  (0.025%)

  worked example  L=[200.0, 400.0, 800.0, 4000.0]  R=[0.9, 0.5, 0.4, 0.1]
      b1 (unweighted) = 0.4750
      b2 (length-wt)  = 0.2037      doc's recommendation
      rho=0        b*=0.2037   |b*-b2|=0.0000
      rho=0.0001   b*=0.1831   |b*-b2|=0.0206
      rho=0.00025  b*=0.1658   |b*-b2|=0.0379
      rho=0.001    b*=0.1381   |b*-b2|=0.0656
      rho=0.01     b*=0.1198   |b*-b2|=0.0839
      rho=1        b*=0.1171   |b*-b2|=0.0866
  NEW  For 4000-token traces the crossover is rho~0.00025.
         Consecutive CoT tokens share the whole prefix; rho is nowhere near that small, so reasoning-model RL never occupies the regime where b2 is optimal.

==============================================================================
SECTION 3 — TESSY objective decomposition (Eq 1-5)
==============================================================================
  Eq 1-2 are a definitional split of a sum over token positions:
      L = sum_i KL_i  =  sum_{i in Cap} KL_i  +  sum_{i in Sty} KL_i
  PASS Eq 2 split is valid iff T_Cap and T_Sty partition the positions   disjoint + exhaustive => sum splits. No content beyond additivity.
  NEW  TESSY carries NO convergence proof and none is claimed.
         Eq 3 states a GOAL (per-token sourcing); Eq 4-5 give a span-level approximation to it. The gap between them is unquantified in the paper: boundary predictors B_S,B_T are imperfect classifiers, so L_Sty is only approximately pre-satisfied. No bound is given on the residual.

==============================================================================
SECTION 4 — CG-DPO metric, graph semantics, corruption axes (Eq 1-7)
==============================================================================
  toy graph: 7 statutes, 4 decisions, 6 edges

  corruption     cited        CP  CR  CT   axis zeroed
  (none)         LRA_187       1   1   1   ['-']
  hallucination  LRA_9999      0   0   1   ['CP', 'CR']
  law_swap       CRIM_625      1   0   1   ['CR']
  article_swap   LRA_189       1   0   1   ['CR']
  anachronism    LRA_188       1   0   0   ['CR', 'CT']
  PASS article_swap gives CP=1, CR=0  => it is a RELEVANCE failure   confirms the doc's correction of the paper's own label
  PASS anachronism gives CT=0 (repealed before context date)
  PASS Eq 5: CP is a multiplicative gate (CP=0 zeroes the term)

  --- degenerate solution ---
      perfect answer     CG=1.000  CQ=1.000
      one fabrication    CG=0.667  CQ=0.667
      CITES NOTHING      CG=1.000  CQ=1.000
  PASS Eq 1 convention CG=1 on empty set makes a SILENT model score perfectly   identical score for perfect and for zero citations
  NEW  CG has the same suppression-vs-competence defect as a trap-only probe.
         'Deleted the instrument' is indistinguishable from 'used it correctly' because the metric punishes commission and never omission. Same structural hole the two-arm temporal probe was built to close.

  FIX — pair CG with citation recall against C*(x):
      answer                 CG  recall     F1
      perfect             1.000   1.000  1.000
      one fabrication     0.667   1.000  0.800
      half-cited          1.000   0.500  0.667
      CITES NOTHING       1.000   0.000  0.000
  PASS F1 against C* correctly scores the silent model 0

==============================================================================
SECTION 5 — Addendum: binomial bounds, majority vote, power
==============================================================================
  5.1  the corrected closed forms
      n= 50   floor 0.05^(1/n) = 94.1845%    ceiling 1-0.05^(1/n) = 5.8155%
      n= 58   floor 0.05^(1/n) = 94.9661%    ceiling 1-0.05^(1/n) = 5.0339%
      n= 59   floor 0.05^(1/n) = 95.0492%    ceiling 1-0.05^(1/n) = 4.9508%
      n= 60   floor 0.05^(1/n) = 95.1297%    ceiling 1-0.05^(1/n) = 4.8703%
      n=200   floor 0.05^(1/n) = 98.5133%    ceiling 1-0.05^(1/n) = 1.4867%
  PASS 0.05^(1/50) = 94.18%  (success-rate floor, 0 failures)
  PASS 1 - 0.05^(1/50) = 5.82%  (failure-rate ceiling)
  PASS closed form == exact Clopper-Pearson at k=n
  PASS void slack 0/60 -> 4.87%   got 4.8703%
  PASS void slack 0/59 -> 4.95%   got 4.9508%
  PASS void slack 0/58 -> 5.03%   got 5.0339%
  PASS exact CP lower bound 49/50 -> 90.86%   got 90.8602%
  PASS exact CP lower bound 48/50 -> 87.94%   got 87.9386%
  PASS exact CP lower bound 47/50 -> 85.22%   got 85.2163%
  PASS exact CP lower bound 46/50 -> 82.62%   got 82.6209%

  5.2  majority-of-5 understatement
             q       P(maj)    ratio   1/(10q^2)
        30.00%   16.308000%      1.8         1.1
        20.00%    5.792000%      3.5         2.5
        10.00%    0.856000%     11.7        10.0
         5.00%    0.115813%     43.2        40.0
         2.00%    0.007762%    257.7       250.0
         1.00%    0.000985%   1015.2      1000.0
  PASS q=5% -> 0.12% observed, 43x understatement
  PASS q=2% -> ~257x understatement
  NEW  Closed form for the understatement: ratio -> 1/(10 q^2) as q->0.
         QUADRATIC in rarity — the rarer the real defect, the worse the suppression.

      majority-of-k: does MORE voting help?
        k=1: P(fire|q=5%)= 5.000000%   understatement      1.0x
        k=3: P(fire|q=5%)= 0.725000%   understatement      6.9x
        k=5: P(fire|q=5%)= 0.115813%   understatement     43.2x
        k=7: P(fire|q=5%)= 0.019358%   understatement    258.3x
        k=9: P(fire|q=5%)= 0.003322%   understatement   1505.0x
  NEW  More samples makes under-detection WORSE, monotonically.
         majority-of-k understates by ~q^-(k-1)/2. Going 3->5->7 multiplies the blindness. A vote is the wrong aggregator for a rare-defect hunt.

  5.3  power, and the indifference-point tautology
      N2=7 at n=60 (calibrated to m0=5%):
        power at m=5%:   2.97%   <- false-fire rate
        power at m=15%:  81.52%   doc claims 81.5%
        power at m=20%:  96.92%   doc claims 96.9%
  PASS power(60, N=7, m=0.15) = 81.5%
  PASS power(60, N=7, m=0.20) = 96.9%

      THE TAUTOLOGY: N := min{k : LB(k,n) > m0}  =>  power(m0) < alpha
           n    N     LB(N)   power@m0   < 5% ?
          30    9   16.633%     2.778%   YES
          60   15   16.086%     2.913%   YES
         100   22   15.389%     3.928%   YES
         200   39   15.005%     4.980%   YES
         500   89   15.033%     4.784%   YES
        2000  327   15.002%     4.975%   YES
  EMPIRICAL power at indifference < alpha  [EMPIRICAL over 6 n; general = Lean no_sample_size_escapes]   no sample size escapes; it is not a sample-size problem

      resolving the apparent contradiction with the beam analysis:
        n= 60 N=15:  m0=15% -> power  2.91%    m=N/n=25.0% -> power 54.94%
        n=200 N=39:  m0=15% -> power  4.98%    m=N/n=19.5% -> power 52.83%
  PASS both analyses correct — different points   MATH1.md is right about m0; the beam analysis is right about N/n
  NEW  MATH1.md conflates two thresholds in one paragraph.
         It quotes N2=7 (calibrated to m0=5%) then discusses 'the indifference point (say 15%)', whose threshold is N=15. Both statements are true; the prose slides between them without flagging the change.

==============================================================================
SUMMARY
==============================================================================
  checkable claims verified : 32
  claims failed             : 0
  new findings              : 8

  Every numerical and algebraic claim in MATH1.md is CORRECT.
  The corrections are to SCOPE and EXPOSITION, not to arithmetic:
    - Eq 14 is exact algebra but optimal only at rho=0, a regime
      long-CoT RL never occupies
    - CG=1 on the empty set makes a silent model score perfectly
    - majority voting suppresses rare defects quadratically, and
      more voters is worse
    - the N2=7 / N=15 slide in section 5

Property tests

HYPOTHESIS 200 randomised draws per theorem. A bounded search finding nothing is evidence, not proof.

test_math1_properties.py::test_eq14_variance_decomposition PASSED        [  8%]
test_math1_properties.py::test_eq14_var2_is_minimal PASSED               [ 16%]
test_math1_properties.py::test_optimal_baseline_interpolates PASSED      [ 25%]
test_math1_properties.py::test_zero_failure_closed_form PASSED           [ 33%]
test_math1_properties.py::test_floor_and_ceiling_are_complements PASSED  [ 41%]
test_math1_properties.py::test_power_at_indifference_bounded_by_alpha PASSED [ 50%]
test_math1_properties.py::test_power_monotone_in_true_rate PASSED        [ 58%]
test_math1_properties.py::test_majority5_always_understates PASSED       [ 66%]
test_math1_properties.py::test_majority5_asymptote PASSED                [ 75%]
test_math1_properties.py::test_more_samples_worse_understatement PASSED  [ 83%]
test_math1_properties.py::test_cg_empty_is_degenerate PASSED             [ 91%]
test_math1_properties.py::test_cp_is_multiplicative_gate PASSED          [100%]

============================= 12 passed in 32.17s ==============================

Lean — declarations

LEAN derived from lean-proofs/LeanProofs/Basic.lean, not typed

Lean — axiom audit

A green build is not a hole-free proof. #print axioms on every declaration is the difference.

MATH2 — findings and welds

MATH2 — what survives verification, and what changes

Companion to MATH1.md. Every claim in that document was put through SymPy (symbolic algebra), SciPy + mpmath (exact binomial tails at 40 digits), Hypothesis (200 randomised counterexample searches per theorem), NetworkX (an actual citation graph), and Lean 4 + Mathlib (two theorems machine-checked to the kernel, axiom-audited for holes).

Reproduce with:

python3 verify_math1.py                              # 32 checks, exit 0
python3 -m pytest test_math1_properties.py -q        # 12 property tests
cd lean-proofs && lake build && lake env lean axioms.lean

Verdict: 32 checkable claims verified, 0 failed. MATH1.md's arithmetic and algebra are correct throughout, including the self-corrected 0.05^(1/n) formula. The eight findings below are corrections to scope and exposition — cases where a true statement is load-bearing for a conclusion it does not actually support.

The document's closing thesis — every proof separates signal from noise, then suppresses the noise without biasing the signal — survives. Three of the eight findings are instances of the same failure one level up: a mechanism that suppresses noise so hard it suppresses the signal too.

The one finding that changes a recommendation

F1. Eq 14 is exact algebra, and optimal in a regime long-CoT RL never occupies

The decomposition is verified in Lean, no holes:

theorem weighted_sse_decomp (s : Finset ι) (L R : ι → ℝ) (b : ℝ)
    (hN : ∑ i ∈ s, L i ≠ 0) :
    ∑ i ∈ s, L i * (R i - b) ^ 2
      = (∑ i ∈ s, L i * (R i - wmean s L R) ^ 2)
        + (∑ i ∈ s, L i) * (wmean s L R - b) ^ 2

Exact for any weights, any rewards, no distributional assumption. MATH1.md is right that it is "pure algebra on the definition of a weighted mean."

But that is also the problem. Minimising a weighted SSE by its own weighted mean is a tautology. All the content sits in the asserted proportionality

Var(ĝ)  ∝  Σᵢ Lᵢ (Rᵢ − b)²

which MATH1.md states without derivation. Deriving it exposes the assumption. With ĝ = (1/N) Σᵢ Σⱼ s_ij (Rᵢ − b) and E[s_ij] = 0 (the score identity of Eq 8–11), let ρ be the within-sequence correlation of score vectors, Cov(s_ij, s_ik) = σ²ρI for j ≠ k:

Var(Σⱼ s_ij)  =  σ² [ Lᵢ + ρ Lᵢ(Lᵢ − 1) ]  =:  σ² Wᵢ(ρ)
Var(ĝ | R)    =  (σ²/N²) Σᵢ Wᵢ(ρ) (Rᵢ − b)²

so the variance-minimising baseline is b*(ρ) = Σ Wᵢ Rᵢ / Σ Wᵢ. Verified symbolically:

The crossover is at ρ ≈ 1/(Lᵢ − 1), because the Lᵢ² term overtakes the Lᵢ term exactly there:

L =  100   ->  ρ* = 0.0101   (1.01%)
L =  500   ->  ρ* = 0.0020   (0.20%)
L = 1000   ->  ρ* = 0.0010   (0.10%)
L = 4000   ->  ρ* = 0.00025  (0.025%)

For a 4000-token reasoning trace the crossover is one fortieth of one percent. Consecutive tokens in a chain of thought are conditioned on the entire shared prefix; ρ is nowhere near that small. Worked example (L = [200, 400, 800, 4000], R = [0.9, 0.5, 0.4, 0.1]):

b₁ (unweighted)   0.4750
b₂ (length-wt)    0.2037     <- the document's recommendation
b*(ρ=0.0001)      0.1831
b*(ρ=0.001)       0.1381
b*(ρ=1)           0.1171

b* has moved further from b₂ (0.087) than b₂ moved from b₁ (0.271 → the gap the proof was written to close is 0.271, and the residual gap is a third of it again). And it saturates almost immediately — by ρ = 0.01 it is within 0.003 of its ρ = 1 limit.

Change: keep Eq 14 as the exact identity it is, but state its hypothesis. b₂ is variance-optimal iff per-token score vectors are uncorrelated within a sequence. For long-CoT RL, estimate ρ and use Wᵢ(ρ); the length-weighted mean is the ρ = 0 corner of a one-parameter family, not the answer.

Findings that change how a measurement is read

F2. Majority-of-k suppresses rare defects quadratically, and more voters is worse

MATH1.md gives the mechanism and two data points (43× at q = 5%, ~256× at q = 2%). Both verified exactly (43.2×, 257.7×). Two additions.

A closed form. As q → 0, P(Bin(5,q) ≥ 3) ≈ 10q³, so the understatement ratio is

q / P(majority fires)  →  1 / (10 q²)

within 7.3% at q = 5%, 3.0% at q = 2%, 1.5% at q = 1%. The understatement is quadratic in the rarity of the defect — precisely the wrong direction, as the rarer and more dangerous the failure, the blinder the gate.

Generalising to majority-of-k reverses the intuition. For k = 2m+1, P(fire) ≈ C(k, m+1) q^(m+1), so the understatement grows like q^(−m):

q = 5%     k=1      1.0×
           k=3      6.9×
           k=5     43.2×
           k=7    258.3×
           k=9   1505.0×

Change: more samples in a majority vote makes under-detection worse, monotonically. A vote is the wrong aggregator for a rare-defect hunt. If a vote is used as an action gate, the per-sample rate must be reported alongside it — and it is the per-sample rate, not the vote, that describes what a user experiences from a single-shot product.

F3. CG = 1 on the empty set makes a silent model score perfectly

Built as an actual networkx.DiGraph with statute nodes, decision nodes, and citation edges. The Eq 1 convention gives:

answer              CG      CQ
perfect            1.000   1.000
one fabrication    0.667   0.667
CITES NOTHING      1.000   1.000     <- identical to perfect

MATH1.md reads the convention as "conservative in the safe direction (refusal is never a false positive here)." True as far as it goes, and it is fine for a pure hallucination metric. But CG is used in the paper as a quality score across five systems, and as a quality score it cannot distinguish a well-grounded answer from a model that has stopped citing altogether.

This is structurally identical to the trap-only temporal probe: deleted the instrument is indistinguishable from used it correctly, because the metric punishes commission and never omission. The fix is the same as the two-arm design — pair it with recall against the citations a correct answer should make, C*(x):

answer                 CG   recall     F1
perfect             1.000    1.000   1.000
one fabrication     0.667    1.000   0.800
half-cited          1.000    0.500   0.667
CITES NOTHING       1.000    0.000   0.000    <- now correctly zero

Change: never report CG alone as groundedness or quality. As hallucination-precision — which is what CG structurally is (the paper's §4.1: "CG is structurally identical to precision in information retrieval") — the empty convention is correct on its own terms: a model citing nothing has committed zero precision violations, and vacuous truth is the right precision value. The lie appears only on promotion. A CG of 0.873 read as groundedness is compatible with a system that cites almost nothing.

F4. MATH1.md conflates two thresholds in the power argument

Section 5 quotes N₂ = 7 at n = 60 and its powers (81.5% at m = 0.15, 96.9% at m = 0.20 — both verified exactly), then discusses "the indifference point (say 15%)" and the threshold "defined as the smallest integer whose lower bound exceeds 15%."

Those are different thresholds. N₂ = 7 is calibrated to m₀ = 5%; the threshold calibrated to m₀ = 15% is N = 15:

m₀ = 5%    ->  N =  7   LB = 5.61%    power@m₀ = 2.97%
m₀ = 15%   ->  N = 15   LB = 16.09%   power@m₀ = 2.91%

Both statements are individually true. The paragraph slides between them without flagging the change, which makes the tautology look like it applies to the arm with 81.5% power.

This also resolves the apparent contradiction with the beam-search analysis, which asserts P(reject) ≈ 0.5 at the boundary. Both are right, about different points:

n=60, N=15:   m₀ = 15%     -> power  2.91%   (MATH1.md's point)
              m = N/n = 25% -> power 54.94%   (the beam analysis's point)

m₀ is the indifference point; N/n is where the MLE equals the threshold. Neither analysis is wrong.

The tautology, generalised and machine-checked

MATH1.md argues the abstention-arm impossibility through Clopper–Pearson duality and binomial tails. None of that is needed, and removing it makes the result stronger. Machine-checked in Lean:

def Calibrated (T : ℕ → ℝ) (α : ℝ) (N : ℕ) : Prop := T N < α
def PowerAtIndifference (T : ℕ → ℝ) (N : ℕ) : ℝ := T N

theorem power_at_indifference_lt_alpha
    (T : ℕ → ℝ) (α : ℝ) (N : ℕ) (h : Calibrated T α N) :
    PowerAtIndifference T N < α := h

T is the only probabilistic object and nothing requires it to be binomial, monotone, or even a measure. "Power at m₀" and "type-I error at m₀" are the same number — the probability of firing when the truth is m₀ — so calibration at m₀ is the statement that this number is below α.

The lifted form is what actually kills the design:

theorem no_sample_size_escapes
    (T : ℕ → ℕ → ℝ) (α : ℝ) (N : ℕ → ℕ)
    (hcal : ∀ n, Calibrated (T n) α (N n)) :
    ∀ n, PowerAtIndifference (T n) (N n) < α

This is strictly stronger than MATH1.md's "at n=200 you get 5.0%, at n=60 you get 2.9%" — which are datapoints consistent with a trend — because it proves no n helps, for the reason that n never enters the argument at all. Numerically confirmed to n = 2000, where power is still 4.975%.

Axiom audit (all six theorems): [propext, Classical.choice, Quot.sound]. No sorryAx, no holes.

Minor

F5. Eq 5's softmax does not collapse fully onto the anchor. At α → 0 with λ = 5, w₁ = 0.2, the anchor share is w₁e⁵/(w₁e⁵ + 1 − w₁) = 97.38%, not 100%. Exceeding 99% at that w₁ needs λ ≥ 6.0. "Almost nothing but familiar data" is a fair description of 97.4%; the mechanism just is not a hard switch. The α → 1 relaxation to the equilibrium mixture is exact — verified to machine precision.

F6. Eq 2's split is valid only if the partition is exhaustive. L = L_Cap + L_Sty requires T_Cap and T_Sty to be disjoint and to cover every token position. Tokens that are neither — formatting, tool-call syntax, whitespace — fall outside both and are silently dropped from the objective.

F7. TESSY's Eq 3 → Eq 4–5 gap is unquantified. Eq 3 states a per-token sourcing goal; Eq 4–5 realise it at span granularity via imperfect boundary classifiers B_S, B_T. So L_Sty is only approximately pre-satisfied, and the paper gives no bound on the residual. This is not an error — TESSY claims a construction, not a theorem — but the construction's central promise ("L_Sty vanishes by design") holds only to classifier accuracy.

F8. The article_swap correction is confirmed on a real graph. MATH1.md's correction of the paper's own label is right: article_swap yields CP = 1, CR = 0, so it is a relevance failure, not a precision failure, by the paper's own Eq 2–3.

Summary

The through-line MATH1.md identified holds, and extends to its own subject matter. F1, F2 and F3 are all the same shape: a noise-suppression mechanism that suppresses the signal along with it. b₂ removes length bias and, at realistic ρ, introduces a larger one. Majority voting removes sampler noise and removes the defect. CG = 1 on empty removes false hallucination flags and removes the ability to detect silence.

Separating signal from noise is only half the discipline. The other half is checking what the separator took with it.

Appendix — response to the meta-audit (F5–F8)

Three findings in the meta-audit target this document and its Lean file, not MATH1.md. Two hold, one does not, and one is about a table that is not mine. Checked rather than accepted.

F5 — HOLDS, and is the sharpest finding in the set

Theorem 2's substance lives in the defs — the proof is := h; the Clopper–Pearson duality is the translation layer, not the theorem. Honest about depth; overstated in comment.

Correct on both counts. power_at_indifference_lt_alpha has proof := h: it unfolds two definitions with the same body and closes. The only genuinely mathematical step — the duality LB_α(N,n) > m₀ ↔ P_{m₀}(X ≥ N) < α — sits in a docstring and the kernel never sees it.

And the overstatement is mine: MATH2.md said removing the binomial machinery "makes the result stronger." It makes it more general while moving the content out of the proof and into the framing. Those are different things, and conflating them is the same species of defect as a number wearing the wrong formula.

Fixed by adding the part that is not definitional. The impossibility is strictly local to m₀, and saying so requires a construction:

structure TailFamily where
  T : ℝ → ℕ → ℝ
  mono : ∀ k, Monotone fun m => T m k

theorem discrimination_survives_calibration
    (α ε m₀ : ℝ) (hα : 0 < α) (hε : 0 < ε) :
    ∃ F : TailFamily, ∃ N : ℕ,
      Calibrated (F.T m₀) α N ∧
      ∀ m₁ > m₀, 1 - ε ≤ PowerAtIndifference (F.T m₁) N

This has a witness, not an unfold. It says the design loses exactly one blind spot — the boundary itself — and retains near-perfect discrimination against every strictly worse rate. Which is why the substantive arm keeps its trigger (2.97% at m=5%, 81.5% at m=15%) and only the abstention arm loses one. Eight theorems now; axiom audit still [propext, Classical.choice, Quot.sound].

F8 — DOES NOT HOLD. Checked exhaustively.

The 87.94% defect reappears in the Lean comment: m = N/n substituted for m₀.

Grepped every occurrence. In Basic.lean, all eleven mentions of m0 refer to the population boundary and none to N/n. In MATH2.md, N/n appears exactly twice, both explicitly distinguishing it:

  m = N/n = 25% -> power 54.94%   (the beam analysis's point)
  `m₀` is the indifference point; `N/n` is where the MLE equals the threshold.

And verify_math1.py:280–283 evaluates both points in one assertion precisely to hold them apart. The substitution is not present. Recording this as a rejected finding with evidence, because accepting a criticism that does not hold is its own failure mode — and one that is easy to fall into when the criticism is flattering to accept.

F6 — holds, but about the meta-audit's own table

The dropped Gate and Coupling cells for the PAS row are the invention, so for the record:

The gate is the window; the coupling is the plasticity coefficient. Everything else in PAS is bookkeeping around those two.

F7 — holds, and my closing line over-unifies

The first three results are exact algebraic decompositions — Pythagorean in weighted L², or additive splits of a sum. The Addendum is frequentist coverage: statements about tail probabilities under a null. Same epistemology (separate what you control from what you do not), genuinely different mathematics. "Identical reflex" is true of the habit and false of the algebra, and the closing paragraph should not have let the second ride on the first.

Net

Appendix 2 — meta-audit round 2 (R1–R6). Two verified against source, three self-corrections.

R1 and R6 make claims about the source papers. Both were checked against the papers themselves, not accepted. Both hold, and R1 makes F1 substantially sharper than MATH2 stated it.

R1 — VERIFIED against LegalOne. F1 is an internal critique, not a hypothetical.

MATH2 said F1 "changes a recommendation" and left the recommendation anonymous. It is not anonymous. From RESEARCH/LEGALONE-2602.00642:

line 284: "we employ the DAPO algorithm as the unified optimization backbone, complemented by a novel token-level baseline designed to minimize variance" line 294: "we extend the context length to 16k tokens" line 296: "The context length is set to 32k tokens"

So LegalOne deploys b₂ inside DAPO on RL tasks at 16k–32k context. Putting those lengths through MATH2's own crossover ρ* ≈ 1/(L−1):

L = 16,000   ->  ρ* = 0.0000625   (0.0063%)
L = 32,000   ->  ρ* = 0.0000313   (0.0031%)

Three thousandths of one percent. F1 is therefore not "b₂ may be suboptimal in some hypothetical long-CoT setting" — it is the paper whose proof MATH1 was faithfully explaining violates that proof's own hypothesis in its own RL stage, by three to four orders of magnitude. MATH2 derived the knife and set it down without noting where it was already lodged. Corrected here.

R6 — VERIFIED against TESSY. F7's "no bound" was too strong.

TESSY Table 3 (paper line 699) does measure the boundary-predictor sensitivity:

Exactly the figures R6 cited. So the span-approximation residual is not unbounded — it is empirically bounded at ~2.5 OJBench points across a 200× swing in predictor training data, and TESSY notes 100K is "over-provisioned."

F7 should read: no theoretical bound; an empirical sensitivity is in Table 3.

And "sensitivity" is the load-bearing word — 2.53 is a slope, not a height. Table 3 measures how much the residual grows when the boundary classifier degrades (500 vs 100K training samples). It does not measure the residual's absolute magnitude at the 100K operating point against a perfect per-token oracle. Reading 2.53 as "the residual is about 2.5 points" would be the level-versus-slope confusion — the same defect in a new font, and the reason this wording must not be "corrected" to bound by a later reader.

Worth flagging that this correction makes the audited paper look better, which is precisely the class of finding a biased auditor suppresses.

R2 — HOLDS. F3's summary line commits F3's own defect.

MATH2's body is precise: CG = 1 on ∅ is "fine for a pure hallucination metric," and the defect is the paper's reuse of CG as a quality score. The summary line — "never report CG alone" — over-suppresses.

As a precision measure the empty convention is correct: a model that cites nothing has committed zero precision violations, and vacuous truth is the right answer, exactly as a trap-only probe is the right answer for commission alone. It becomes a lie only when CG is promoted to groundedness.

Corrected: never report CG alone as groundedness or quality; as hallucination-precision the empty convention is legitimate and CG-alone stands.

The lapse is the exact shape F3 describes — a true statement (the convention is precision-correct) silently load-bearing for a conclusion it does not support (so CG is a fine quality score) — committed one level up, in a headline. The discipline caught its own author at the margin.

R3 — HOLDS, and it is the sharpest of the six. F3's fix presupposes the

absent oracle.

verify_math1.py §4 demonstrates the F1-score fix, and the silent model correctly scores 0. But look at how the script obtains C*:

Cstar = {"x_autounfair": {"LRA_187", "EEA_6"}}     # HARD-CODED

The gold citation set is supplied by hand for the toy. In the real CG-DPO setting C*(x) is precisely the object the graph-only design was built to avoid needing — the entire premise is that the graph is the oracle and there is no per-query gold citation list. So MATH2's clean F1 = 0 on the silent model rests on an oracle production does not possess.

The fix is still right; its feasibility rides on an oracle that must be checked for rather than assumed. The best available proxy is the graph's own CR component — citations that semantically similar decisions actually made, which the paper already computes:

Corrected fix: report CG alongside CR-aggregated recall, not C* recall.

Structurally identical to the two-arm temporal probe, which only worked because we happened to hold as_at metadata. The toy possessed its oracle by construction; the deployment does not.

R4 — HOLDS, and it is the audit-of-the-verification the package needed.

The green checks are not all the same kind of green, and reading them as one is the original sin in a new font. The verification is stratified three ways:

So the n=5 PASS is not the general proof; the Lean theorem is. Same for the tautology: verify §5.3 and test_power_at_indifference_bounded_by_alpha are empirical over many (n, m₀); power_at_indifference_lt_alpha and no_sample_size_escapes are the general statements.

Read the verification as stratified. Nothing in it is wrong; the labels just have to say which layer certified what. Recorded in MATH1-VERIFICATION.md header.

R5 — noted. F4 corrects the beam-search analysis as well as MATH1.

Both attached "indifference point" to different rates; the shared error was the label, and the label was the load-bearing word.

The near-miss, worth keeping

The audit reports nearly manufacturing a ninth finding — believing MATH2 had dropped the leading coefficient C(k, m+1) from F2's asymptotic, then finding it in MATH2's own sentence. Reported as caught rather than suppressed.

That is the right disposition and it matches the standard set in POST-TRAINING-STATUS.md for cluster E: a verified silence is a result, and an audit that presents only its surviving findings has laundered its own false positives. Same reason F8 was rejected with grep evidence rather than quietly accepted.

Net, round 2

Zero findings reversed. Four documents now carry corrections traceable to a verified check or a rejected finding with evidence: MATH1, MATH2, the beam-search analysis, and the source papers themselves.

Appendix 3 — five welds. All checkable claims verified against source.

Precision improvements, no reversals. Section numbers and figures checked in the papers, not accepted from the audit.

W1 — F1: the assumption's address and the violation's address are different

Verified against LEGALONE-2602.00642 section structure:

§4.2   TOKEN-LEVEL BASELINE OPTIMIZATION
§4.2.1   MOTIVATION AND DEFINITION      <- the proportionality is asserted HERE,
                                            with within-sequence rho left implicit
§2.2.5   TRAINING DETAILS               <- 32K context window
§4.1     (RL task suite)                 <- Legal Document Generation at 32K tokens

The violated hypothesis is not in Eq 12–14's algebra — that is exact, and both MATH1 and the Lean theorem confirm it. It is one step earlier, in the assertion Var(ĝ) ∝ Σ Lᵢ(R−b)².

locus of the unstated rho=0 assumption   §4.2.1
locus of the violation                   §2.2.5 (32K window), §4.1 (32K RL task)
crossover at L=32,000                    rho* ~ 3e-5   (0.0031%)

Appendix 2's R1 aimed the pointer at "§4.2" generally. This separates the two addresses, which matters because a reader going to §4.2 to find a broken proof will not find one — the proof is fine; the sentence before it is the problem.

W2 — F3 summary: keep the word precision in the clause

Applied in place at MATH2 line 175. Verified — CG-DPO §4.1 line 99, verbatim:

"CG is structurally identical to precision in information retrieval"

So the corrected clause has to name what CG is, or the next reader re-derives why the empty convention is legitimate on its own terms. Done.

W3 — F3 fix: CR-aggregated recall inherits the SAME coverage gap

The proxy is computable from the graph alone — recall against ∪_{d ∈ similar(x)} citations(d) — needing no per-query gold list, and it scores the silent model 0 for the same reason the toy C* did (recall against any non-empty reference is 0 for an empty citation set).

But the caveat must travel with it, by the same denominator discipline applied to the metric itself. CR-aggregated recall is bounded by the same graph that bounds CG, so the coverage gap rides along. Verified — CG-DPO §7.1 line 470:

"32 (59%) exist in the legislation database but are absent from the citation graph — the cited article is real, but courts rarely cite it directly (graph coverage gap)."

and §5.3 line 284: "CG thus provides a lower bound on citation accuracy, with the bound tightening as G grows."

So both CG and the recall proxy are lower bounds on the same graph. 59% of flagged hallucinations in the paper's own audit were coverage gaps, not fabrications. Carry that with the fix; a proxy that inherits its reference's blind spots inherits its error rate too.

W4 — F4: the stratification needs a guarantee-type column

Three tiers were enumerated; the kind of guarantee each provides was implied and not stated. Stating it:

The distinction that matters: "Hypothesis passed" ≠ "theorem proved." A falsification search that finds nothing is evidence, and it is the same witness-as-proof error one tier up if read as certainty. Axiom audit confirms the Lean tier rests on propext, Classical.choice, Quot.sound and nothing smuggled.

W5 — F7: 2.53 is a slope, not a height

Applied in place. Table 3 measures the residual's sensitivity to classifier degradation, not its magnitude at the operating point. Recorded so a later reader does not "correct" sensitivity to bound.

Ledger, closed

Nineteen findings, zero reversals, one rejection with evidence, one reported near-miss. Every correction traces to a verified check or to a rejected finding with the evidence attached.

The one open item, stated exactly

ρ = the within-sequence correlation of score vectors ∇log π(a_ij) inside LegalOne's 32K-token RL sequences.

What is closed: if ρ > 3×10⁻⁵ at L=32,000, b₂ is the wrong baseline. That threshold is proven — Lean for the identity, SymPy for b*(ρ), and the crossover is arithmetic.

What is open: whether the inequality holds, and by how much. That is not "is the math wrong" — the math is closed. It is "how large is the consequence of applying it outside its regime," and the magnitude is |b* − b₂| at the true ρ, which the worked example placed near 0.087 at ρ=1 but which could be larger or smaller in LegalOne's actual run.

Settling it requires per-token gradient statistics from inside someone else's training loop. No SymPy witness, no Hypothesis search, no Lean proof, and no verify run observes that. The apparatus says exactly where to look and refuses to say what is there.

Appendix 4 — REVERSAL. §5's impossibility was a category error.

This withdraws a finding. MATH1.md §5 and MATH2.md's treatment of it both presented "power at the indifference point is locked to alpha" as a structural impossibility that killed the abstention arm's trigger. The arithmetic was right and the interpretation was wrong.

The error

If a trigger is calibrated so that firing implies the one-sided 95% lower bound clears m0, then m0 is the null boundary. Firing there is Type-I error by construction, and bounding it at alpha is correct size control — the thing you want. Calling that bound a "power ceiling" treats m0 as an effect to be detected, but power is defined on the alternative space, m > m0.

So the theorem power_at_indifference_lt_alpha is true, trivially, and says only that a calibrated test controls its size. It is not an impossibility.

What the real defect was

The spec named one rate as both the null boundary and the detection target:

(a) fire only when the 95% LB clears 15%   -> 15% in the NULL
(b) reliably fire when the truth is 15%    -> 15% in the ALTERNATIVE

Unsatisfiable because a single rate cannot be both — a specification bug, not a property of one-sided tests.

The correction, measured

OLD (null = target = 15%)     N=15   power@15% = 2.91%   -> "impossible"
NEW (null 5%, target 15%)     N= 7   size @5%  =  2.97%   controlled
                                     power@15% = 81.52%
                                     power@20% = 96.92%

Trigger reinstated at N = 7 of 60. On firing it proves the rate exceeds 5%, not 15%. What a test proves is set by the null; what it detects is set by power.

Corrections to this file

• Appendix 2 R5 and the §2 framing throughout: the tautology is real but unremarkable, and does not support the conclusion drawn from it.
• Lean rename required: PowerAtIndifference T N := T N labels the category error. The object is right; rename to RejectionProbAtBoundary.
• discrimination_survives_calibration survives and is promoted — it is the formal statement of the 81.52% @ 15% row, i.e. that a calibrated test does discriminate rates above its boundary. That was written as a consolation and is now the main result of §2.

What is untouched

F2, majority-of-k suppression, is independent — no hypothesis test appears in it. Confirmed monotone worse in k at every q.

One further error found while checking: the two mechanisms compound. The majority vote runs per item; the binomial trigger runs on the count of failing items. A defect suppressed to 0.12% per item never produces enough failing items for the trigger to fire. MATH2 treated the levels as separable. k=3 reduces first-level suppression 43x -> 6.9x and relieves the second.

For the record

19 findings held · 1 REVERSED · 1 rejected with evidence · 1 reported near-miss

Every other correction came from checking our own work. This one needed someone outside the loop who knew the statistics well enough to see that a bounded rejection probability at the null boundary is the test working, not failing. The audit-of-the-audit found the audit's own framing defect exactly once, and it took an external statistician to find it — which is the honest limit of self-review.

MATH1 — source derivations

L(θ_{t+1}) − L(θ_t)
  ≈ ∇L(θ_t)·Δ  +  ½ Δᵀ H(θ_t) Δ                 [Taylor, H = ∇²L the Hessian]
  = −η_t ∇L(θ_t)ᵀ g̃_t  +  (η_t²/2) g̃_tᵀ H(θ_t) g̃_t

E[L(θ_{t+1}) − L(θ_t)]  ≤  −η_t |∇L(θ_t)|²  +  (η_t² λ_max(H)/2) · E[|g̃_t|²]

E[|g̃_t|²] = |E[g̃_t]|² + Tr(Σ_t) = |∇L(θ_t)|² + Tr(Σ_t)

E[ΔL] ≤ −η_t|∇L|² + (η_t²λ_max/2)|∇L|² + (η_t²λ_max/2)Tr(Σ_t)
      = −η_t|∇L|² · [ 1 − (η_t λ_max(H)/2) ]   +   (η_t² λ_max(H)/2) · Tr(Σ_t)
        \_________________ descent term ______________/     \____ noise term ____/

η_t  <  2 / λ_max(H)                              [the stability window]

ΔL_val ≈ −η_max · ⟨∇L_val, g_train⟩   +   (η_max²/2) · g_trainᵀ H_val g_train
          \______ alignment term ______/       \________ curvature term ________/

                  w_i · exp( λ · 𝟙_{i=1} · (1 − α(t)) )
P(B_i | t)  =  ────────────────────────────────────────────
                  Σ_j  w_j · exp( λ · 𝟙_{j=1} · (1 − α(t)) )

b1 = (1/n) Σ_i R_i                       [mean over samples]
b2 = (Σ_i Σ_j r_{i,j}) / N  =  (Σ_i L_i R_i) / (Σ_i L_i)     [mean over tokens, N = Σ_i L_i]

g = E_{τ ~ π_θ} [ Σ_t  ∇_θ log π_θ(a_t | s_t) · ( R(τ) − b ) ]

E[ ∇log π(a_t|s_t) · b ]  =  E_{h_t}[  E_{a_t ~ π}[ ∇log π(a_t|s_t) · b  |  h_t ]  ]

= E_{h_t}[  b ·  E_{a_t ~ π}[ ∇log π(a_t|s_t) ]  ]

E_{a_t ~ π}[ ∇log π(a_t|s_t) ]  =  ∫ π(a|s) · (∇π(a|s)/π(a|s)) da  =  ∫ ∇π(a|s) da
                                =  ∇ ∫ π(a|s) da  =  ∇(1)  =  0

Σ_i L_i (R_i − b1)²  =  Σ_i L_i ( (R_i − b2) + (b2 − b1) )²
  =  Σ_i L_i (R_i − b2)²                    [ = Var2 ]
   + Σ_i L_i (b2 − b1)²
   + 2 (b2 − b1) Σ_i L_i (R_i − b2)         [ the cross term ]

2(b2 − b1) · [ Σ_i L_i R_i  −  b2 Σ_i L_i ]  =  2(b2 − b1) · [ b2·N  −  b2·N ]  =  0

Var1  =  Var2  +  (b2 − b1)² · Σ_i L_i  =  Var2  +  N·(b2 − b1)²
        \_Var(b1)_/  \_Var(b2)_/            \____ variance gap ≥ 0 ____/

L(M_S) = Σ_i  E[ KL( P_D(y_i)  ‖  P_{M_S}(y_i) ) ]

L(M_S) = L_Cap(M_S) + L_Sty(M_S)
L_Cap = Σ_{i ∈ T_Cap} E[KL(...)],    L_Sty = Σ_{i ∈ T_Sty} E[KL(...)]

y_i  ~  P_{M_T}(·)   if i ∈ T_Cap      [teacher writes the reasoning]
y_i  ~  P_{M_S}(·)   if i ∈ T_Sty      [student writes the connective tissue]

s^i = M_S( x, [s¹,t¹,…,s^{i−1},t^{i−1}] )
t^i = M_T( x, [s¹,t¹,…,s^{i−1},t^{i−1}, s^i] )

s^i = s̃^i_{< B_S(s̃^i)},     t^i = t̃^i_{< B_T(t̃^i)}

CG(r, G) = |{ c ∈ C(r) : c ∈ G }| / |C(r)|,      with CG = 1 if C(r) = ∅

CP(c, G)        = 1 if c ∈ V_n(G) else 0                 [precision / existence]
CR(c, x, G)     = 1 if ∃ d ∈ similar(x) : (d,c) ∈ E else 0   [relevance]
CT(c, t)        = 1 if valid_at(c, t) else 0             [temporality]

CQ(r, G, x, t) = (1/|C(r)|) Σ_{c ∈ C(r)}  CP(c) · ½[ CR(c,x,G) + CT(c,t) ]

(x, y_w, y_l) = ( prompt(d),  text(d, c),  text(d, σ(c)) )
                  query       preferred     rejected

L_DPO(θ) = − E_{(x,y_w,y_l)} [ log σ( β·log(p_θ(y_w|x)/p_ref(y_w|x))
                                     − β·log(p_θ(y_l|x)/p_ref(y_l|x)) ) ]

success-rate lower bound (0 failures)  =  s_L  =  0.05^(1/n)

success-rate floor  (sensitivity LB, 0 failures)  =  0.05^(1/n)        → 94.18% at n=50
failure-rate ceiling (miss-rate UB,  0 failures)  =  1 − 0.05^(1/n)    →  5.82% at n=50

P(majority says error | q) = Σ_{j=3}^{5} C(5,j) q^j (1−q)^{5−j}

power(m) = P( Binomial(eff_n, m) ≥ N2 ) = 1 − Σ_{j=0}^{N2−1} C(eff_n, j) m^j (1−m)^{eff_n−j}

Reproduce

cd /home/hybridwolf/Documents/TINMAN/Math
bash ci.sh                       # all layers + cross-layer agreement
python3 verify_math1.py          # 32 claims
python3 -m pytest test_math1_properties.py -q
cd lean-proofs && lake build && lake env lean axioms.lean
python3 worksheet_gen.py         # next-cycle checklist
python3 report_gen.py            # this page