fix(core): Caveat-A follow-up — HAC estimator + multi-block gate + subset machine-check (Soraya's holes) - #10026
Merged
AceHack merged 1 commit intoAug 4, 2026
Conversation
…aya's two holes) + subset machine-check Soraya's adversarial review of the Caveat-A margin (#10025) VERIFIED all three monotonicity obligations but found two model-scope holes (both MEDIUM). Both fixed here (they are the math-team's, per the handoff split); her switch-the-default verdict was SWITCH-AFTER-FORMAL-PROOF. (3b) Lag-1-only was insufficient. AR(1) assumes ρ_k = ρ₁^k, but a stream with weak ρ₁ and strong ρ₂ (Soraya's interleave witness: ρ₁=0.12, ρ₂=0.39) defeated it — n_eff barely shrank, still over-convicting. Fix: effectiveSampleSizeHAC — a Bartlett-windowed Newey–West long-run variance summing over lags 1..L (L=⌊n^(1/3)⌋): n_eff = n / (1 + 2·Σ (1−k/(L+1))·ρ_k⁺). Clamped ρ_k⁺≥0 and Bartlett weights keep factor≥1 ⇒ n_eff ≤ n STILL HOLDS (so Soraya's (a)/(b)/(c) proofs — which need only n_eff ≤ n — survive the generalisation). chshMarginAutocorr now uses it. AR(1) effectiveSampleSize kept as the documented special case (ρ_k=ρ₁^k). Anchors: Newey–West 1987, Bartlett 1946. (3c) Two-halves stationarity gate was defeatable (Soraya's witness [+1×10,−1×10, +1×10,−1×10] passes it though a step function). Fix: isApproxStationaryMultiBlock — splits into B blocks, requires both block-MEAN and block-VARIANCE spread ≤ tol. chshSybilAutocorrCalibrated now gates on it (4 blocks). Machine-check of obligation (c): a 40-batch seed loop asserts the autocorr oracle's conviction set is a SUBSET of the i.i.d. oracle's (DistinctCount_autocorr ≥ iid) — the executable half of Soraya's proof, gating the eventual default switch. 30 AntiSybil tests green (+4: lagKAutocorr lag-2 signal, HAC-catches-lag2, multi-block gate defeat-witness, subset over 40 batches; margin test updated — alternating is now correctly STRICTLY larger, the old lag-1-only "equals" was the bug). Core 0-warning. Shipped chshMargin/chshSybilCalibrated still unchanged (switch pending). Anchors: Newey–West 1987; Bartlett 1946; Kontorovich–Ramanan 2008; Hoeffding 1963. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
AceHack
enabled auto-merge (squash)
August 4, 2026 15:16
AceHack
deleted the
fix/antisybil-caveat-a-hac-estimator-and-multiblock-gate-20260804
branch
August 4, 2026 15:16
|
Codex usage limits have been reached for code reviews. Please check with the admins of this repo to increase the limits by adding credits. |
AceHack
added a commit
that referenced
this pull request
Aug 4, 2026
…-corrected margin (Caveat-A) (#10027) The shipped default anti-sybil oracle now convicts at 2 + chshMarginAutocorr (the pair's own HAC effective-sample margin) instead of the i.i.d. 2 + chshMargin. This closes the Caveat-A over-conviction bug in the DEFAULT path: real streams autocorrelate, so the i.i.d. margin was too tight and falsely collapsed honest- but-bursty identities into one source. Authorized by Aaron 2026-08-04 ("switch the default, ship it") after the verify-before-trust gate: Soraya VERIFIED obligations (a) n_eff ≤ n, (b) margin_corrected ≥ margin_iid (Z3), and (c) the conviction set is a strict SUBSET of the i.i.d. oracle's (my 40-batch machine-check). Because the corrected margin is never smaller, the switch can ONLY REMOVE false collapses, never add a conviction — provably safe. Her two model-scope holes (lag-2, stationarity gate) were already fixed (#10026: HAC estimator + multi-block gate). Scope of the switch: the MARGIN swap only (parameter-free, fully proven). The stationarity gate stays in the opt-in chshSybilAutocorrCalibrated (it needs a tol choice). chshMargin (i.i.d.) is unchanged and still exported (algebraic bound + caveat pointer). No external callers to repoint (chshSybilCalibrated had none in src/); DecorrelationMeter still uses the i.i.d. chshMargin deliberately (separate, scope-limited instrument — a distinct decision). Framing discipline (Soraya): "provably more conservative than i.i.d.", NOT "fully sound" — dependence beyond the HAC bandwidth can still evade. 30 AntiSybil + 67 Sybil/DecorrelationMeter tests green (strong S=4 convictions still convict — low-autocorrelation pairs get corrected ≈ i.i.d.). Core 0-warning. Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Sorayas adversarial review of the Caveat-A margin (#10025) verified all three monotonicity obligations but found two model-scope holes (both MEDIUM). Both fixed here — theyre the math-teams per the handoff split. Her switch verdict was SWITCH-AFTER-FORMAL-PROOF; this supplies the proofs executable half.
(3b) Lag-1-only was insufficient → HAC estimator
AR(1) assumes
ρ_k = ρ₁^k, but Sorayas interleave witness (ρ₁=0.12,ρ₂=0.39— 25× the AR(1) prediction) defeated it:n_effbarely shrank, still over-convicting the honest-bursty pair Caveat-A protects. Fix:effectiveSampleSizeHAC— a Bartlett-windowed Newey–West long-run variance over lags1..L(L=⌊n^(1/3)⌋):n_eff = n / (1 + 2·Σ(1−k/(L+1))·ρ_k⁺). Clampedρ_k⁺≥0+ Bartlett weights keepfactor ≥ 1⇒n_eff ≤ nstill holds, so Sorayas (a)/(b)/(c) proofs (which need only that) survive the generalisation. AR(1)effectiveSampleSizekept as the documented special case.(3c) Stationarity gate was defeatable → multi-block
Two-halves check passes
[+1×10,−1×10,+1×10,−1×10](both half-means 0) though its a step function. Fix:isApproxStationaryMultiBlock— B blocks, requires both block-mean and block-variance spread≤ tol. The oracle now gates on it (4 blocks).Machine-check of obligation (c)
A 40-batch seed loop asserts the autocorr oracles conviction set is a subset of the i.i.d. oracles (
DistinctCount_autocorr ≥ iid) — the executable half of Sorayas proof, gating the eventual default switch.Tests (30 AntiSybil green; Core 0-warning)
+4:
lagKAutocorrlag-2 signal, HAC-catches-lag2, multi-block defeat-witness, subset-over-40-batches. Margin test updated — alternating is now correctly strictly larger (the old lag-1-only "equals" assertion was the bug). ShippedchshMargin/chshSybilCalibratedstill unchanged (switch pending).Anchors: Newey–West 1987; Bartlett 1946; Kontorovich–Ramanan 2008; Hoeffding 1963.
🤖 Generated with Claude Code