fix(core): Caveat-A — autocorrelation-corrected CHSH margin (AntiSybil over-conviction) - #10025
Merged
AceHack merged 1 commit intoAug 4, 2026
Conversation
…l over-conviction on bursty streams) AntiSybil.chshMargin ε=sqrt(32·ln(1/δ)/n) is a Hoeffding bound assuming per-round-independent λ. Real commit/message streams autocorrelate (author bursts, topic runs) ⇒ effective sample size n_eff < n ⇒ the TRUE margin is larger ⇒ the shipped margin is OPTIMISTIC and over-convicts (falsely collapses honest- but-autocorrelated identities into one source). Soraya's Caveat-(a), routed via the math-team handoff (2026-08-02). Model chosen (the math-team decision the handoff assigns; Soraya's candidate #1): the AR(1) effective-sample correction, soundness-biased. - lag1Autocorr: ρ₁ of the round-ordered ±1 outcome-product series. - effectiveSampleSize n ρ₁ = n·(1−ρ₁⁺)/(1+ρ₁⁺), ρ₁⁺=clamp ρ₁ to [0,0.999]. n_eff ≤ n always, equality iff ρ₁ ≤ 0 (Soraya's monotonicity obligation). Negative autocorrelation gets NO optimistic bonus (conservative). - chshMarginAutocorr: substitute n_eff for n in ε — equals chshMargin on i.i.d. (ρ₁≤0), strictly larger on positively-autocorrelated products. - isApproxStationary: candidate #2 gate — a non-stationary window downgrades to non-convicting (never evidence). - chshSybilAutocorrCalibrated: the sound oracle — conviction at 2 + marginAutocorr + the stationarity downgrade. STRICTLY more conservative than chshSybilCalibrated (margin_corrected ≥ margin_iid, gate only removes) ⇒ can only drop FALSE collapses. SCOPE SPLIT respected: this is the model + estimator (math-team). Concentration CORRECTNESS (n_eff ≤ n eq. iff ρ₁=0; margin_corrected ≥ margin_iid; band ordering) is Soraya's to prove formally (Z3/FsCheck) — routing to her next. The shipped chshMargin / chshSybilCalibrated are UNCHANGED (opt-in sound path + caveat pointer in the docstring); switching the default is gated on Soraya's formal sign-off (security verify-before-trust). 6 property tests (28 AntiSybil green): lag1Autocorr signs, effectiveSampleSize monotonicity + clamp, marginAutocorr ≥ iid always / strictly-larger-on-autocorr / equals-on-alternating, stationarity gate, oracle subset-conservatism. Core 0-warning. Anchors: Hoeffding 1963; Newey–West 1987 (HAC); Kontorovich–Ramanan 2008 (mixing concentration); Pironio et al. 2010. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
AceHack
enabled auto-merge (squash)
August 4, 2026 15:01
|
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
deleted the
fix/antisybil-chsh-margin-autocorrelation-caveat-a-20260804
branch
August 4, 2026 15:01
AceHack
added a commit
that referenced
this pull request
Aug 4, 2026
…aya's two holes) + subset machine-check (#10026) 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>
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.
Fixes Sorayas Caveat-(a) (routed via the 2026-08-02 math-team handoff):
AntiSybil.chshMarginis a Hoeffding bound assuming per-round-independent λ, but real commit/message streams autocorrelate (author bursts, topic runs) ⇒ effective sample sizen_eff < n⇒ the true margin is larger ⇒ the shipped margin is optimistic and over-convicts (falsely collapses honest-but-autocorrelated identities into one source).Model chosen (the math-team decision the handoff assigns — Sorayas candidate #1)
The AR(1) effective-sample correction, soundness-biased:
lag1Autocorr— ρ₁ of the round-ordered ±1 outcome-product series.effectiveSampleSize n ρ₁ = n·(1−ρ₁⁺)/(1+ρ₁⁺),ρ₁⁺ = clamp ρ₁ to [0, 0.999].n_eff ≤ nalways, equality iffρ₁ ≤ 0. Negative autocorrelation gets no optimistic bonus.chshMarginAutocorr— substitutesn_effforn; equalschshMarginon i.i.d., strictly larger on positively-autocorrelated products.isApproxStationary— candidate Round 26 — rename tail, §18 memory clarification, three dispatches #2 gate: a non-stationary window downgrades to non-convicting.chshSybilAutocorrCalibrated— the sound oracle (2 + marginAutocorr+ stationarity downgrade). Strictly more conservative thanchshSybilCalibrated— can only drop FALSE collapses, never add.Scope split respected
This is the model + estimator (math-team). Concentration correctness (the monotonicity obligations) is Sorayas to prove formally (Z3/FsCheck) — routing to her now. The shipped
chshMargin/chshSybilCalibratedare unchanged (opt-in sound path + a caveat pointer in the docstring); switching the default is gated on Sorayas formal sign-off (security verify-before-trust).Tests (28 AntiSybil green; Core 0-warning)
6 property tests:
lag1Autocorrsigns,effectiveSampleSizemonotonicity + clamp,chshMarginAutocorr≥ iid always / strictly-larger-on-autocorr / equals-on-alternating, stationarity gate, oracle subset-conservatism.Does not touch the algebraic bounds (2, 2√2, 4) — only the finite-sample margin around them. Anchors: Hoeffding 1963; Newey–West 1987; Kontorovich–Ramanan 2008; Pironio et al. 2010.
🤖 Generated with Claude Code