validation: replace bias-SE sample-count staircase with measured exact-proof budget

Problem

The original defect was a sample-count staircase around exact bias-standard-error arithmetic. Current Draft source removes that staircase from the O(n) proof path: public validation_core::bias_standard_error attempts the checked neutral-zero O(n) proof for every n >= 3 with exactly represented finite residuals. Only the O(n²) pairwise comparison/reference remains capped at n <= 16; above sixteen, O(n) proof refusal delegates to the established bias implementation without quadratic scratch. Reusable generalized/static psychometric arithmetic remains fast-mlsirm-owned.

Current #488 authority

#488 remains Draft/open/mergeable on prerequisite #492@794ba9e6dda9f043aa499920fdf609b81b075d7e. Current exact head is 520df488fd86ba48008af8ee5a2e112b4587fc22; protected release authority remains main@a243f18da4a4ca8a8d068c39922537f1f8ed6ad0.

docs/research/validation-bias-dispersion-positivity-bound.md owns the exact-real theorem for every admitted general translated path n >= 3: canonical translation gives exact zero and a maximum normalized magnitude x with 1 <= |x| < 2, so D = n Σy² - (Σy)² = Σ_{i<j}(y_i-y_j)² >= n x²/2 >= n/2. This does not yet prove the implemented floating result positive because square rounding, both compensated sums, sample-count conversion, n*Q, and the final FMA must be bounded together.

The square-root correction-exhaustion and target-width obligations remain closed. Current admission has a repository-owned strict <3 adjacent-binary64 seed-distance theorem and exactly three exact corrections; production validation_core is explicitly 64-bit pointer-width.

Resource admission is not metric cardinality

docs/research/validation-bias-production-resource-admission.md is repository-owned and current exact head 520df488... keeps the Analysis Run and Validation Evidence contracts separate.

analysis_engine owns MAX_EVIDENCE_UNITS = 100_000 and rejects larger AnalysisCorpus values. But analysis_engine currently has no validation_core dependency, and AnalysisEvidenceUnit carries evidence identity, event time, availability time, and membership count rather than a truth/recovered numerical pair. There is no current typed/versioned contract that proves either (a) every supported product bias_standard_error call came through AnalysisCorpus or (b) one admitted evidence unit corresponds to one bias-SE metric pair.

Therefore an evidence-unit cap is not presently a bound on bias-SE sample count n. A future buyer path must state and enforce the evidence-to-metric cardinality mapping before MAX_EVIDENCE_UNITS can participate in a numerical/resource proof. The value 100_000 must not be copied into validation_core, treated as a public-library domain restriction, or used to delete numerical refusals.

The known helper false-zero witness remains source-domain reachable at n=2^54 = 18,014,398,509,481,984, with minimum-subnormal q=2^-1074 and M=2^-1021. The normalized SE is 2^-54; exact restoration is q/2, which ties to represented zero. The guard is scientifically real.

For scale only, 2^54 is about 1.8014398509481984e11 times 100_000; that ratio is not admission evidence because evidence count is not yet metric count. Independently, materializing only the two public f64 slices requires 2^58 = 288,230,376,151,711,744 bytes = 256 PiB, before working storage. This shows why a giant allocation is not realistic acceptance while preserving source-domain reachability.

The owner-correct next step is to establish/version the supported buyer call path and its cardinality contract. Only then may a product-side translated-dispersion forward-error proof use a finite metric-population bound while the public numerical library keeps its actual domain and fail-closed safety.

Exact-head evidence

520df488... is documentation-only relative to 3b5d07b2e438edef9c529317d9dd09bd53451a92; the compare contains only docs/research/validation-bias-production-resource-admission.md.

Fresh exact-head workflows are terminal:

Documentation Quality 34573224170: GREEN.
Bias SE Exact-Proof Budget 34573224257: GREEN.
Rust Foundation 34573224268: RED only in Production line and branch coverage job 103179819615.
Live PostgreSQL 103179819441: GREEN.
Rust format/lint/test/rustdoc/dependency policy 103179819679: GREEN.
Repository/Python contracts + SBOM/provenance 103179819783: GREEN.

Fresh immutable exact-head artifacts:

line artifact 10188730908, GitHub Actions archive digest sha256:f6c560819690274ad205baf77ec46089835d5563e7bbcb3d2f941fb532e63ff0;
branch artifact 10188776666, archive digest sha256:34006fb155957e34a86385cd9975340fa24bdb1950874c07e9d001e0070a1088.

The current LCOV has exactly the same 42,005 source/line DA keys as predecessor 3b5d07b... and the same two zero-count records, bias.rs:69 and bias.rs:592. With documentation-only delta and unchanged authored-line classifier inputs, the current authored-source authority remains 12,344/12,346.

The current branch artifact has the same unique source-site set and the same arm-covered/arm-missing status as the predecessor. The checked-in unique-site/per-arm-max fold remains 4,450/4,452; only two TRUE outcomes are missing: bias.rs (68,8)-(68,29) with folded counts (0,12) and (591,8)-(591,35) with (0,32). Raw LLVM/instrumented totals are not the product denominator.

Exact-head CodeRabbit review was retried after the earlier transient rate limit and completed on 520df488... with no findings in the requested resource/cardinality scope. The review independently confirmed that the change is documentation-only, keeps analysis_engine::MAX_EVIDENCE_UNITS distinct from bias-SE sample cardinality, preserves the n=2^54 source-domain witness as a resource-extreme example rather than a realistic fixture, and leaves dispersion_numerator <= 0.0 unresolved pending implementation-matched floating analysis or a compact caller-valid counterexample. This review does not establish numerical/scientific acceptance. Formal submitted reviews remain historical COMMENTED, and current unresolved inline review threads are zero; there is still no qualifying current-head approval.

Remaining obligations

Helper false-zero refusal (bias.rs:68-69): source-domain reachable but resource-extreme. Preserve it. Close product acceptance through an owner-correct bounded representation/resource/cardinality contract rather than giant allocation, source rewriting, suppression, or an arbitrary library cutoff.
General translated dispersion_numerator <= 0.0 (bias.rs:591-592): exact-real margin is D >= n/2; floating positivity still requires an implementation-matched absolute forward-error proof over the actual admitted metric-population domain or a compact caller-valid represented-input counterexample.

The isolated n=2,047 candidate/fallback measurements remain characterization only: candidate p95 23,306 ns, max RSS 2,176 kB, zero pair-record scratch; fallback p95 15,385,815 ns, max RSS 100,152 kB, 2,094,081 pair records / 100,515,888 bytes explicit scratch. They are not buyer-facing HTTP p95 guarantees.

This issue remains open. Acceptance still requires 100% owned authored line+branch coverage without suppression, deterministic/reference/refusal/permutation evidence, bounded resource evidence over the explicit supported product path and metric-cardinality contract, code-current TRACEABILITY/product-gap authority, qualifying current-head review, normal #492 prerequisite landing, and immutable release/recovery evidence. No force push, destructive rebase, self-approval, gate weakening, mutable dependency, skip/xfail, denominator trick, copied production arithmetic as an acceptance oracle, or fabricated evidence.

#491 characterization은 #488 exact head cd0f9a7b7710fc7965588017a71286bd6cdc96a5까지 전진했습니다. Production bias_standard_error admission은 n=4..=16 그대로입니다.

기존 c70210e331ec096c90a42bec9de7d619bd51fe26가 checked O(n) u128 path를 pair reference의 strict sufficient subset으로 고정한 뒤, 이번 slice에서는 남아 있던 실제 hybrid measurement shape을 구현했습니다.

c6b237e0bb1388cccd7bcb71a0df5cbf837a07c5: crates/validation_core/examples/bias_se_exact_proof_budget.rs에 O(n) sufficient fast path -> buffered O(n²) pair fallback을 추가했습니다. Compact fixtures는 linear path를 사용해야 하고, D=2^58 boundary에서 n=64는 linear admit, n=65는 checked-intermediate refusal 후 pair fallback을 사용해야 합니다. 모든 경우 timing 전에 restored exact pair numerator equality를 검사합니다.
CSV는 이제 geometry와 used_pairwise_fallback을 기록합니다. 따라서 n=65라는 sample count만 보고 fallback을 추정하지 않고 실제 expensive path 실행 여부를 evidence로 남깁니다. Buffered fallback의 Vec<Option<(u128,i32)>> capacity/scratch payload도 같은 row에서 관측됩니다.
457654593391d09f4e3dc551ce75dc856ad1964f → c077b30a37900dd40ea994d1c3bba2195bbfea83 → df8f46b8e39142f2d7218e2ce4ad515aa0c67072 → cd0f9a7b7710fc7965588017a71286bd6cdc96a5: CHANGELOG, research/TRACEABILITY, TEST_STRATEGY, OPERABILITY를 hybrid measurement contract에 맞췄습니다.
docs(ddd): restore queue authority and bounded-context ownership #435 docs/product-technical-gap-baseline.md도 d8d63aec5654ca810d19267d0e9ee514c6bae83f까지 갱신해 fix(validation): preserve representable recovery metrics #488 current head와 hybrid observability를 승계했습니다.

현재 실행 환경에는 Rust toolchain이 없어 release-mode raw CSV를 만들지 않았습니다. #488 exact-head Rust Foundation/Documentation/Security/SAST/CodeQL도 아직 queued/pending이고 Rust jobs는 runner 미배정입니다. 따라서 CPU p95, allocator/RSS, buyer-path p95 <= 20 ms, wider-integer reference 비교, exact-head GREEN을 주장하지 않습니다.

다음 production decision은 현 harness를 실제 recorded CPU/OS/Rust toolchain에서 release mode로 실행해 admitting/refusing geometry 양쪽의 raw CSV와 RSS를 확보하고 wider-reference를 비교한 뒤 내려야 합니다. 2,047, 4,095, 208,064, 또는 n=17 자체는 production budget이 아닙니다.

Exact-head evidence advanced after the all-count independent-oracle push. Predecessor eae187fcfc98e77a126907a06c7917fef90a5e2f completed Rust Foundation run 34044332463: Live PostgreSQL integration passed, while production coverage exposed two independent #![deny(missing_docs)] failures (bias_standard_error_exact_residual_mean_roundoff_contract.rs and wilson_sample_count_rounding_contract.rs). The repository/Python cron assertion remains the separate #492 foundation contract, and the Rust lane stopped at cargo fmt --all -- --check before clippy/nextest/rustdoc/deny.

Repair 9634c5b97209f01b14041dd730b953d1325698af adds scientific crate-level contracts to both failing tests without suppression, skip/xfail, fixture changes, or coverage-denominator changes. The first records the represented three-observation case where pre-rounding the exact residual mean changes the correctly rounded binary64 SE; the second records exact u64 Wilson count provenance above 2^53, including all-covered uncertainty immediately below one.

Pinned Rust 1.98.0 Rustfmt Evidence 34044330266 for eae187fc... is terminal success. Artifact 9993018483, digest sha256:795ead178971f0f660a90070c49d8304c9d4651401c29a44ff8fff1dde522350, contains a 34-file canonical formatter patch/manifest. This corrects older predecessor counts of 36/37/38 files. The formatter delta is not committed yet and is not same-head GREEN.

Current #488 head is 9634c5b97209f01b14041dd730b953d1325698af, still Draft/mergeable on protected main@a243f18da4a4ca8a8d068c39922537f1f8ed6ad0; its new Rust Foundation/Docs/Semgrep/Security/CodeQL runs were queued at the post-repair sweep. Production admission remains n=4..=16; this repair does not authorize n>16.

Fresh scientific-admission status (2026-09-08): #488 is currently at exact head 5ae4751bca0a4657bcd80a258023bec374750176 on foundation prerequisite #492@794ba9e6dda9f043aa499920fdf609b81b075d7e. The reusable arithmetic boundary remains unchanged: production bias_standard_error admits n=4..=16 through neutral_zero_linear → pairwise_reference → generic_fallback; n>16 remains characterization-only. The independent exact witness remains [-2^53, 0, 1, 2^53], P = 2^109 + 3, public result bits 0x432a20bd700c2c3e.

Current-head #488 Rust quality, Live PostgreSQL, and repository-contract/Python coverage jobs are terminal GREEN. Owned production line/branch coverage is still running, so no fresh denominator or completion claim is recorded here; the older branch-coverage counters in this issue are historical rather than current-head evidence.

The foundation owner path is now .github#1929 → TEPP#492 → TEPP#488, not the older #490 dependency note. .github#1929 records that machine-principal admission has been repaired; the remaining canonical owner gap is unchanged-head terminal CodeQL receipt publication, including the cross-repository status-publication 403 path. #492 also still lacks a qualifying independent APPROVED review. Do not widen #488 production admission or treat characterization evidence as activation evidence until #492 is normally protected-merged and #488 has exact-head scientific/coverage evidence.

#488 exact lineage advanced to 9b9caf7651f04c9f68d02c6b75284869c207bda0 with a public fallback-boundary regression. Predecessor ee69f806... proved the Monte Carlo redundant-precondition repair causally: branch diagnostics are now 2,279 sites / 4,558 arms / 4,445 covered / 113 uncovered, distributed bias.rs 79, numeric.rs 20, bias_se.rs 8, coverage.rs 6; monte_carlo.rs is no longer in the uncovered set.

The new regression exercises a valid bounded-proof refusal without changing production admission: truth=[0;4], recovered [f64::MAX,-f64::MAX,1,-1]. Neutral-zero exact proof refuses on dyadic coefficient range, pairwise reference refuses when f64::MAX - (-f64::MAX) is non-finite, and generic fallback must retain the finite correctly rounded SE 0x7fda20bd700c2c3d; a permutation is pinned to the same bits. This is route-boundary evidence for the existing neutral_zero_linear → pairwise_reference → generic_fallback contract, not evidence to widen n>16.

Current-head Rust Foundation 34236222037 and Documentation Quality 34236221952 require fresh terminal evidence before any subsequent coverage classification or resource-budget conclusion.

Current-head evidence for #488@9b9caf7651f04c9f68d02c6b75284869c207bda0 is now terminal. Rust 1.98 quality, Live PostgreSQL, repository/Python line+branch coverage, and Documentation Quality are GREEN; Production line+branch coverage remains RED.

The public pair-distance overflow/fallback regression was causal. Exact branch coverage moved from predecessor ee69f806... 4,445/4,558 covered (113 uncovered) to 4,447/4,558 covered (111 uncovered) with the source-site count unchanged at 2,279. bias_se.rs moved 8 → 7 uncovered arms and bias.rs 79 → 78; numeric.rs 20 and coverage.rs 6 are unchanged. Specifically, bias_se.rs (304,16)-(304,39) moved (0,16) → (1,16), proving the non-finite pair-distance refusal executes, and bias.rs (80,12)-(80,28) moved (0,1) → (2,1), proving the generic scaled fallback executes. Validation-core raw zero-count LCOV rows also moved 54 → 53 solely through bias.rs 29 → 28.

This strengthens the existing route-boundary evidence but does not alter the #491 resource-budget decision: production admission remains n=4..=16, and n>16 remains characterization-only until measured release-mode CPU/allocator/RSS plus full exact-head acceptance justify a contract change.

#491 current characterization/activation boundary remains unchanged: production bias_standard_error is still n=4..=16, n>16 remains characterization-only, and #488 remains stacked on #492@794ba9e6dda9f043aa499920fdf609b81b075d7e.

Fresh coverage-driven repair has advanced #488 to exact head 2ad6b829db3e48e8157c83cecc3b971903b685de. The new source change removes only the exact-count Wilson midpoint tie branch from all_covered_wilson_lower_from_exact_sample_count after proving that equality is impossible for the represented-input domain: an exactly representable integer sample count has an odd part of at most 53 bits, while a normal adjacent-binary64 midpoint has a reduced odd numerator wider than 53 bits; because z² is dyadic, exact quotient-midpoint equality would require that midpoint numerator to divide the integer sample count. The subnormal midpoint case would require z² outside finite binary64 range. Strict residual_magnitude > midpoint_residual remains the only adjacent-step condition.

This is a proof-driven branch removal, not activation evidence and not a coverage workaround. Wilson formulas, denominator reduction, sample admission, thresholds, exclusions, route order, fail-closed behavior and coverage denominator are unchanged. Current-head Documentation Quality 34255050965 is GREEN; Rust Foundation 34255050985 is non-terminal at this observation, so predecessor Rust/coverage results do not transfer. Do not widen n>16 until exact-current-head scientific/coverage/security gates plus the measured release-mode CPU/allocator/RSS budget and prerequisite #492 owner path are terminal.

2026-09-09 current-head correction for #488 lineage:

9318a3857af4cd7590cc185beda23605483b9555 is now accepted for the low-term-translation fallback witness. Branch artifact 10088400466 (sha256:52b643166823a221f7eec8965aa51675603ef09c61ceb3c3b6a031bccae4066a) folds under checked-in unique-source semantics to 4,459/4,532, 73 missing arms, all in bias.rs; (632,16)-(632,36) is (5,2), down from the prior false-count zero.
2585a75b7dd314800fc39c163e7b7e41316044d7 added a scientifically valid three-level inexact-product regression, and its Rust quality/test/PostgreSQL lanes are GREEN. It is not a causal coverage repair: branch artifact 10089189373 (sha256:a0de899993e7053ff2cef77d67511782b1774b5cd81432abd5eb27c9631cd28d) remains 4,459/4,532, 73 missing. RCA: translated [-0.1,0,0.1] makes the preceding first-square predicate true, so the || chain short-circuits before missing coordinate (296,12)-(296,71).
Current fix(validation): preserve representable recovery metrics #488 exact head is 4eb13061903d19fc489562cfbc436c0f3166cc0e, still on #492@794ba9e6dda9f043aa499920fdf609b81b075d7e. The witness is corrected to represented residuals [-1/32,0,0.1]: the first square is exact, the later 0.1² is inexact, so the missing later predicate must actually be evaluated. Independent represented-input SE rounds to 0x3fa4444444444445; permutation invariance remains required. Exact-head CI is queued, so no GREEN or coverage-reduction claim is made yet.

This does not change the #491 policy: n>16 remains characterization-only, there is no sample-count admission widening, and reusable generalized arithmetic remains fast-mlsirm-owned.

2026-09-09 current evidence update: 14e00e0f030c408e6313a4a057c1c1c28401f4c0 is now verified causal, not merely a candidate. Rust Foundation 34332623624 kept repository/Python contracts, Rust fmt/Clippy/no-retry nextest/doctest/rustdoc/dependency policy, and Live PostgreSQL GREEN; only authored production coverage remained RED. Branch artifact 10096663588 (sha256:ac71ac5d44cb4519ac7a0062ffc786396db96b7882e90102ccf71e108b4d2f54) max-folds to 4,465/4,530 covered arms, 65 missing, all in crates/validation_core/src/bias.rs, a four-arm reduction from f8c866e2... at 69 missing. Line artifact 10096605497 is sha256:8bb33a0a2c1eaf140b634f865af4606cc259d3236150dece08c5a7530f4ea2b1.

No n>16 admission inference is permitted from that coverage improvement. Current #488 head is ordinary fast-forward cb8e45d33a9d847d49a546cb42c4fb5281ce5225, still stacked on #492@794ba9e6dda9f043aa499920fdf609b81b075d7e. It adds a separate public n=3 regression for a reachable exact-three-level refusal: residuals [-m,0,m], m=1.25×2^511, keep each product and the square sum finite/exact while the direct square_sum - cross_product radicand overflows. The general translated path must preserve finite m/sqrt(3) and return bits 0x5fd7181116f43fe3, with permutation invariance. Current-head Documentation Quality 34338626145 and Rust Foundation 34338626129 are running; predecessor GREEN does not transfer. This remains coverage/scientific evidence work only, not sample-count widening or a release claim.

Scientific correction on #488: current exact head is 1a580a22452b18e582468b0cc4d8f8eed6504c39, still on #492@794ba9e6dda9f043aa499920fdf609b81b075d7e. The preceding public n=3 RED was not just coverage exercise. Rust Foundation 34338626129 ran 1,680 tests and the only test failure was the new radicand-overflow contract: generic fallback returned 0x5fd7181116f43fe4, one ULP above the exact represented-input target m/sqrt(3) = 0x5fd7181116f43fe3 for m=1.25×2^511.

The causal repair admits exact represented residuals for n=3..=16 to the existing exact neutral-zero/pair-distance rational-midpoint proof; n=2 stays on its cheaper identity and subtraction-roundoff cases still fail closed to bias.rs. This changes the lower exact-route boundary only. It does not provide evidence for n>16, does not alter #491’s upper-bound characterization policy, and does not move generalized arithmetic ownership from fast-mlsirm. Current Documentation Quality 34339491349 is GREEN; Rust Foundation 34339491514 is running, so the repair is not yet claimed GREEN.

#488 exact-head proof frontier update

At #488@4af3205bba376930d682b356701d79889bef87f7, branch artifact 10124083878 leaves 29 unique-source uncovered arms, all in crates/validation_core/src/bias.rs. The next source-order repair is the normalized-radicand finiteness predicate (320,8)-(320,40), not an additional synthetic coverage witness.

normalized_three_level_standard_error receives two distinct nonzero finite offsets from its sole production caller. Its exact leading-binade power-of-two scale is positive and finite, so each nonzero normalized magnitude is <2; normalized squares and cross-product are finite with magnitude <4; after the retained square-sum roundoff proof, the square sum is finite <8. Thus the radicand subtraction has magnitude <12 and cannot produce a non-finite value. The !normalized_radicand.is_finite() arm is structurally unreachable and should be removed while preserving the immediately following subtraction_roundoff(...) refusal.

The normalized cross-product FMA predicate (302,12)-(302,89) is explicitly not promoted to an unreachable-state finding: subnormal FMA-residual behavior still needs a complete proof. Any future n>16 activation remains separate and still requires measured release-mode CPU/allocator/RSS evidence rather than extrapolating this coverage repair.

#488 advanced to exact head 870248b54ceaea833e6c008de7c752f467614d16 by removing the source-order impossible normalized-radicand finiteness guard while retaining the exact subtraction-roundoff proof. The proof is bounded by the normalized three-level path itself: admitted normalized magnitudes are <2, admitted exact square/cross-product magnitudes are <4, admitted exact square sum is finite <8, hence square_sum - cross_product cannot be NaN/Inf and has magnitude <12.

This is separate from the unresolved n>16 budget question: no sample-count admission changed. Documentation Quality 34410155982 is GREEN; Rust Foundation 34410155960 is still queued, so no new coverage count is claimed until the exact-head artifact exists. Keep #491 open and characterization-only.

#488 exact head c52d7058eb0d9499b936bcc86108c8860888338b closes the previously unresolved normalized cross-product FMA refusal with a real public n=3 witness; no n>16 admission changed. Documentation Quality 34410872962 is GREEN. Rust Foundation 34410872788 has GREEN repository/Python+SBOM/provenance, Live PostgreSQL, fmt, Clippy, no-retry tests, doctests, rustdoc, and dependency policy; it is RED only at owned-production 100% line/branch coverage.

Immutable branch artifact 10127356920 (sha256:e459c985ee41e8e4c06c10c1028b15d40e430364c918bdb6a39b153de430e32f) folds to 4,457/4,484, 27 uncovered arms, versus predecessor 870248b... at 4,456/4,484, 28 uncovered. Target (302,12)-(302,89) moves from (true=0,false=8) to (true=2,false=8), so the regression is causal rather than test-only churn. Keep #491 characterization-only; this result does not justify widening the bounded exact-proof count.

2026-09-10 exact-proof coverage update

#488 is now c9c9ff0e2f9375d1d664807869bfddce9b2a3dfe on unchanged #492@794ba9e6dda9f043aa499920fdf609b81b075d7e.

Predecessor c52d7058eb0d9499b936bcc86108c8860888338b has immutable branch artifact 10127356920 (sha256:e459c985ee41e8e4c06c10c1028b15d40e430364c918bdb6a39b153de430e32f), which folds under checked-in unique-source max semantics to 4,457/4,484, 27 uncovered arms, all in crates/validation_core/src/bias.rs. Raw three-level radicand-roundoff coordinate (395,8)-(395,72) was (true=0,false=6).

Intermediate witness 6fdb68f2f36857e577e38188f8b62103479134a6 used directly represented residuals [0,2^26,-(2^26-1)]. Source-order inspection showed the public bias_se neutral-zero proof could admit that integer geometry before the bias.rs fallback. Immutable branch artifact 10127927356 (sha256:a7e36d378b8e3a63fec849e9b9618930cb2421e440c53a6bfddea716602e0c8d) confirms the prediction: 4,457/4,484, 27 missing, target still (true=0,false=6). This witness is explicitly falsified as a coverage repair.

Current c9c9ff0e... routes causally with recovered=[1,1,1], truth=[0,-A,+B], A=2^26·2^-80=2^-54, B=(2^26-1)·2^-80. Direct subtraction rounds every residual high part to 1.0 while error-free low terms retain [0,+A,-B]; this forces the bounded bias_se route to refuse and sends the low-term geometry through bias.rs. Raw squares/cross-product/square-sum remain exact; the exact radicand coefficient 13,510,798,680,784,897 is odd and above 2^53, so the raw radicand subtraction-roundoff predicate must refuse exact admission. The represented fallback result is pinned at 0x3c8279a74340fe34, plus permutation invariance.

Exact-head Documentation Quality 34413059482 is GREEN. Rust Foundation 34413059718 is terminal RED only at owned-production authored coverage; repository/Python contracts + SBOM/provenance, fmt, Clippy, no-retry tests, doctests, rustdoc/dependency policy, and Live PostgreSQL are GREEN. Line artifact 10128050213 (sha256:0ece6b49ef8f82a3493773b1fd2957335e51b36580fc0c31a5a2f6beb6482ab5) executes the target refusal body twice. Branch artifact 10128093062 (sha256:3c2fde46707f6fc2be2f3853dcf1517dd6217b451b68aa8f952a6a3657d80e91) folds to 4,458/4,484, 26 missing, all in bias.rs; (395,8)-(395,72) is now (true=2,false=6). Thus this public witness causally reduces missing coverage 27→26 without altering the n=3..=16 admission budget, production arithmetic, route order, or coverage denominator.

The n>16 decision remains a separate measured CPU/allocator/RSS resource-budget question. No activation or staircase change is implied by this coverage repair.

Current #488 authority advanced to exact head 3fc135d655e187db29f455b4fc995a2e3fa6df7a with one production-only hunk in crates/validation_core/src/bias.rs. Rust Foundation 34475019413 is terminal RED only at authored production line/branch coverage; format, Clippy, no-retry tests, doctests, warning-free rustdoc, dependency/license/advisory/source policy, repository/Python contracts+SBOM/provenance, and Live PostgreSQL are GREEN. Documentation Quality 34475019449 is GREEN.

Immutable branch artifact 10151231184 (sha256:94b74195aa2067e94d96c0e71423d78e4b4578fbf12f3b9ab233e1b165c002c5) folds under the checked-in crates/*/src/* unique-source/max rule to 4,450/4,454 covered arms, 4 missing. Predecessor e9447e4... was 4,452/4,458, 6 missing, so the source-invariant repair is denominator-honest 6 -> 4: it removed the impossible general-translated non-finite-restoration arm and the impossible normalized_standard_error == 0 arm while retaining the reachable final scale-restoration false-zero refusal. Line artifact 10151175066 (sha256:6a0b7141f17363785fc97403efe33b4104af4d60d7258c3751810a0b825e1e6e) still has six authored misses: bias.rs 69/109/595 and bias_se.rs 247/272/288.

The four remaining branch arms are now exactly: bias.rs (68,8)-(68,29) true, (106,8)-(106,34) false, (153,12)-(153,44) true, and (594,8)-(594,35) true. Treat them independently. In particular, this coverage repair does not change the n=3..=16 exact-proof budget or provide evidence for n>16; that remains characterization-only and still requires release-mode CPU/allocator/RSS evidence plus deterministic/refusal/permutation proof before activation.

#488 exact-head authority advanced to c577372a2f66cca7096bf6434b8c28df201d2189 after removing only the overflow-normalized scaled_standard_error non-finite result guard that is impossible on its n>=3 production call surface. Documentation Quality 34480829308 is GREEN. Rust Foundation 34480829408 is RED only on owned-production authored line/branch 100% enforcement; repository/Python+SBOM/provenance, Live PostgreSQL, fmt, Clippy, no-retry tests, doctests, rustdoc and dependency policy are GREEN.

Immutable branch artifact 10153649925 (sha256:622c8d2ead67c25894683509de6e509064f0b72c4e896f9670aa9251040e8e61) folds to 4,449/4,452, 3 missing arms, down denominator-honestly from predecessor 3fc135d... at 4 missing. Line artifact 10153584662 (sha256:e9c4c4925969b009da108c79f64c8ec1585ad4518a2f3277c1d7d15061b9fdd8) folds to 41,972/41,977, with only bias.rs:69,590 and bias_se.rs:247,272,288 uncovered.

This does not widen exact-proof admission. n=3..=16 remains the bounded represented-input path, n=2 its direct identity, and n>16 remains characterization-only. Before any widened production budget, retain the issue's release-mode CPU/allocator/RSS, compiler/hardware/build flags, deterministic/refusal/permutation evidence, owner-boundary, exact-head 100% coverage/security/docs and independent-review requirements. The remaining branch arms are helper false-zero, two-level target-width portability, and general translated nonpositive-dispersion; none is evidence for a larger sample-count budget.

#491 resource evidence advanced on #488 exact head f5c1d2ea2f666332562a5c48c49c494bf56e37bb, without widening production admission.

A new release-mode characterization workflow first exposed a provenance RED: run 34501215127 used GitHub's synthetic PR merge SHA 512fe0dffc34e655b8e48984702e397ecefc01fb, so artifact 10161944265 is rejected as exact-head evidence despite mechanical success. Repair f5c1d2ea... now binds checkout, verification, metadata and artifact naming to ${{ github.event.pull_request.head.sha || github.sha }} and fails if git rev-parse HEAD differs.

Exact-head run 34501459910 / job 102952998288 is GREEN. Artifact 10162024540 (sha256:61e64246ab1a9ab40a24b9228e790f207bdbed54a6097c56d6439ea50656a681) records Linux x86_64 / 64-bit, Rust 1.98.0 (rustc 88d9e12ae, LLVM 22.1.8), AMD EPYC 7763, 4 logical CPUs / 2 cores and the checked-in default 25 timing samples.

Candidate hybrid_narrow_wide_pair p95/scratch evidence: n=16 131ns/0B; n=64 411ns/0B; n=256 1,503ns/0B; n=1,024 5,861ns/0B; n=2,047 11,652ns/0B. At the odd n=65 refusal geometry it uses the wide product at 812ns/0B, while the narrow hybrid falls to the buffered pair route at 6,532ns with 2,080 records / 99,840B. At compact n=2,047 the buffered quadratic comparator is 26,278,488ns with 2,094,081 records / 100,515,888B and the two-pass quadratic comparator is 21,456,149ns.

Whole-process max RSS is 124,800kB, but it is not candidate RSS because that same process intentionally executes the ~100.5MB buffered comparator. Treat this artifact as release CPU plus exact algorithmic scratch-shape evidence only. The next resource slice should isolate candidate/fallback process RSS or allocator behavior while preserving the existing measurement sample count and geometry set.

Production remains n=3..=16 exact represented-input admission (n=2 direct identity); n>16 is still characterization-only. The evidence does not establish scientific activation, HTTP buyer-path p95, current-head 100% coverage, or independent approval. Current-head Documentation Quality is GREEN; Rust Foundation is being reacquired after the CI-only evidence repair. The prior source-head frontier remains three real bias.rs branch guards plus the separate bias_se.rs four-correction exhaustion line until a current-head artifact verifies otherwise.

Exact-head resource slice is now implemented on #488 a68055f108fc30b9b56348e8a5381ab436c813b3 without changing production admission. Bias SE Exact-Proof Budget run 34506253098 / job 102969057929 is terminal GREEN and exact-head-bound; immutable artifact 10163932916 has digest sha256:c04be3bb134fc22e780d9551329bb037f2985710ac6f52b2a86d6645b7f68760.

The new bias_se_resource_isolation harness runs the candidate and current fallback in separate release processes on the same deterministic odd-dyadic n=2047, diameter=2^58+1 geometry and checks the exact pair-square result. It retains the checked-in 25 timing samples. Current artifact records:

candidate narrow_wide_candidate: p95 23,306 ns, max RSS 2,176 kB, 0 pair-record scratch, used_wide_product=true;
fallback narrow_pair_fallback: p95 15,385,815 ns, max RSS 100,152 kB, 2,094,081 pair records / 100,515,888 scratch bytes, used_pairwise_fallback=true.

This closes the earlier evidence-attribution defect: candidate and fallback RSS are now isolated per process instead of inferred from the mixed comparison process. It is resource characterization only—not an independent scientific oracle, not buyer-path HTTP p95, and not permission to activate n>16. Production n=3..=16 remains unchanged. The remaining activation obligations stay deterministic/refusal/permutation evidence, applicable buyer-path latency, exact-head 100% authored production coverage, independent review, #492/CO released-owner prerequisites, and code-current TRACEABILITY/gap authority. Rust Foundation 34506253181 is still executing on the same head; repository/Python+SBOM/provenance are already GREEN, rustfmt and Clippy are GREEN, while no terminal coverage/merge-readiness claim is made yet.

Exact-head termination review result superseding the pending-review sentence in the issue body: CodeRabbit completed the focused review of a68055f108fc30b9b56348e8a5381ab436c813b3 / bias_se.rs:307. It found the exact square comparison direction, adjacent-neighbor monotonicity, midpoint ties-to-even, and lower/upper representability exits sound, but found one actionable limitation in the proposed invariant: monotonicity over the finite positive binary64 set is not a usable resource/DoS bound. The actual seed ((numerator as f64)/(denominator as f64)).sqrt()*unit still needs a complete small-ULP error bound covering u128→f64 numerator rounding, division, sqrt, power-of-two scaling, normal/subnormal transitions, and maximum-finite behavior. Therefore keep the fixed four-pass fail-closed None; do not replace it with an unbounded loop and do not return an unverified final candidate. This leaves the verified branch frontier unchanged at 3 missing bias.rs arms and keeps n>16 characterization-only.

Standards/reference trace for the remaining bias_se.rs:307 proof obligation (current docs rechecked 2026-09-11 KST): Rust’s Reference specifies integer→float casts as the closest float with roundTiesToEven; f64 is binary64; current Rust 1.98.1 f64::sqrt documentation guarantees the rounded infinite-precision result and identifies IEEE squareRoot; IEEE 754-2019 remains the active floating-point standard. Primary/current references: https://doc.rust-lang.org/stable/reference/expressions/operator-expr.html#numeric-cast ; https://doc.rust-lang.org/std/primitive.f64.html#method.sqrt ; https://standards.ieee.org/ieee/754/6210/ .

These references narrow, but do not complete, the missing seed-distance proof. The proof must compose the exact caller-domain numerator/denominator bounds with (1) u128→binary64 ties-to-even conversion error, (2) binary64 division rounding, (3) correctly rounded sqrt, and (4) exact-or-boundary-aware power-of-two scaling, then translate the resulting relative/absolute error into a maximum adjacent-binary64 distance to the exact rounding interval. Treat normal/subnormal binade crossings and the maximum-finite boundary separately. Until that derivation yields a small finite correction bound no larger than the implemented cap (or justifies a different bounded algorithm), line 307 remains a legitimate bounded-resource fail-closed path.

bias_se.rs:307 bounded-termination investigation advanced on exact #488@a68055f108fc30b9b56348e8a5381ab436c813b3; this does not change production admission or the current 3-arm coverage authority.

Primary Rust contracts now close the previously implicit seed-rounding premises: integer→float cast is nearest/ties-to-even (Rust Reference numeric cast), primitive f64 division/multiplication use IEEE roundTiesToEven, and f64::sqrt is the rounded infinite-precision IEEE squareRoot result. With u=2^-53, current admission 1<=N<=u128::MAX, 1<=D<=2^53 makes D as f64 exact and keeps N/D normal. For pre-restoration seed c = RN(sqrt(RN(RN(N)/D))) and exact y=sqrt(N/D), the composed bound is

(1-u)^2 <= c/y <= (1+u)^2, so |c/y - 1| <= 2u + u^2.

A three-adjacent-value miss in any normal binade requires at least 2.5 local half/whole spacings from the exact target's rounding interval; even at a power-of-two boundary the smaller predecessor spacing leaves a >2u relative separation. In a subnormal restoration, the propagated pre-scale error below MIN_POSITIVE is <~1 minimum-subnormal quantum and the final exact-power-of-two multiplication rounding contributes <=0.5 quantum, still excluding a three-value miss. Zero/∞ threshold crossings are already conservative None exits. This suggests the correctly rounded finite result is at most two adjacent values from the seed, so at most two neighbor_is_closer moves are required and the third decision pass must terminate.

I requested a focused CodeRabbit falsification review on #488 covering power-of-two boundaries, normal/subnormal transition, half-min-subnormal zero, MAX/∞ threshold, and u128::MAX cast binades before treating this as accepted proof. Do not replace the current cap with an unbounded loop or return an unverified exhausted candidate. A production refactor should only follow if that independent review accepts the complete boundary argument and should encode the finite correction budget explicitly.

Primary references: Rust Reference, numeric casts https://doc.rust-lang.org/reference/expressions/operator-expr.html#numeric-cast ; Rust f64 primitive-operation rounding and sqrt precision https://doc.rust-lang.org/std/primitive.f64.html .

Current reference-evidence authority for #491 is now #488 exact head 01ca3088b4a4bc514a441c4ab8ca4430219ab9e9.

A public fallback characterization contract was added at crates/validation_core/tests/bias_large_sample_reference_characterization_contract.rs without changing production routing or the n=3..=16 exact-proof admission ceiling. For one zero residual plus 2,046 identical residuals (n=2,047), it fixes the exact two-level identity SE(mean)=|gap|/2047: gap=f64::from_bits(0x4330_0000_0000_0001)=2^52+1 must produce bits 0x4280_0200_4008_0101 for zero-anchor positions 0 / 1,023 / 2,046, with repeated calls checking bitwise determinism. A minimum-subnormal gap=2^-1074 specimen requires InvalidInput at the same anchor positions, preserving false-zero refusal.

Exact-head Documentation Quality and Bias SE Exact-Proof Budget are GREEN. Rust Foundation is GREEN for rustfmt, Clippy, no-retry tests, doctests, warning-free rustdoc, dependency/license/advisory policy, repository/Python contracts+SBOM/provenance, and Live PostgreSQL; it remains RED only because owned-production line/branch coverage has not reached 100%. Current immutable coverage artifacts are line 10167422485 / sha256:b9043630f0dd6e87b35bb2d8fd296e20593b551b72d9ac767b2146a4b70fc107 and branch 10167481107 / sha256:10b3ef144a15c6e2e998a6cdb21dc3f0709fe4d8760f30ee622a4e7da298e2b8. Proof-budget artifact 10167332804 is sha256:eb274cedd6b3b40d4a558755af900e42a0f4869b754252faf0d37be645f25acc.

Focused CodeRabbit review on the exact head independently confirmed the literal, rational result and nearest bits, permutation specimens, false-zero refusal, and that n=2,047 still delegates to the established fallback. This closes part of the deterministic/reference/refusal/permutation evidence gap for one two-level large-sample geometry only. It is not evidence to activate general n>16; domain breadth, current-artifact 100% coverage, qualifying human/current-head approval, code-current docs, prerequisite #492, immutable owner releases, and applicable release/buyer-path performance evidence remain required.

Scientific RED/RCA from #488 large-sample characterization:

At exact test head 1b50af75a4e2449922252f805552860fbb0494dc, the new non-singleton two-level contract intentionally evaluated the public validation_core::bias_standard_error fallback above the n=16 exact-proof ceiling. For n=17, m=5 zero residuals, 12 residuals equal to gap=2^52+1, the exact identity is SE(mean)^2 = gap^2 * m(n-m) / [n^2(n-1)]. Independent exact rational-square-root rounding gives binary64 0x42fd294a104aa492, while the current public fallback returned 0x42fd294a104aa490 on the hosted Rust 1.98.0 run. This is a two-ULP scientific discrepancy, not a flaky test or coverage artifact.

The RED run was Rust Foundation 34517036049, job 103004914630: fmt and Clippy were GREEN; nextest ran 1,704 tests and failed only this new characterization assertion, reporting decimal bits 4827059773688685712 (...a490) versus expected 4827059773688685714 (...a492). Coverage generation also failed downstream because the suite was RED; do not promote those partial coverage results.

Do not repair this by changing n=17 into another staircase admission or by weakening the exact target. #491 already rejects one-count widening. Commit b7902531511398a30f2650da92333e80d6811771 instead converts the test into an explicit characterization contract: prefix/suffix/rotation permutations and repeat determinism must all reproduce the current ...a490 fallback, while the known exact target ...a492 remains recorded as a distinct scientific target. This keeps CI honest while preserving the new discrepancy as a future systemic exact-proof acceptance case. Production admission remains n=3..=16; no estimator, coverage denominator, provider/model routing, or dependency changed.

The systemic next repair remains an evidence-bounded admission rule (or owner-correct exact two-level path) that can return the exact target without unbounded O(n²) resource growth and that satisfies the existing deterministic/refusal/permutation/resource/coverage/review gates before any n>16 activation.

#488 current-head repair in progress — exact 5e145c7597b98f85bdc10ef962a919a94a552b57

The new n=17, m=5, gap=2^52+1 public characterization produced a valid scientific RED on predecessor 1b50af75...: the established fallback returned 0x42fd294a104aa490, two ULP below the exact rational-square-root target 0x42fd294a104aa492. This is not being repaired with an n=17 staircase.

Causal source repair 591813e019b902390be1efba343960db2a2c75e0 changes exact_pair_distance_standard_error from a sample-count gate to arithmetic-proof admission: n>=3 first attempts the checked O(n) neutral-zero integer identity; only if that proof refuses may n<=16 use the existing O(n²) pairwise reference. For n>16, a linear-proof refusal delegates directly to the established fallback. Checked u128/Wide256 width, exponent alignment, reduced-denominator <=2^53 admission, the four-step exact midpoint correction bound, nonrepresentable-result refusal, and the n=2 direct identity remain unchanged. No quadratic scratch is enabled above 16.

Follow-up 5e145c75... promotes the three n=17 permutations from discrepancy characterization to exact target recovery while retaining the n=2,047 one-anchor bitwise/permutation/repeat fixture and the minimum-subnormal false-zero InvalidInput contract. The current Bias SE Exact-Proof Budget run 34519805352 and Documentation Quality 34519805244 are GREEN. Budget artifact 10169183010 (sha256:d6351df50e423959df786fe8e3dfaf9acca3c2dcd251e4424902eb79a43a57cf) records the same exact head and keeps the n=2,047 candidate/fallback isolated-process evidence. Rust Foundation 34519805174 is still current-head execution authority and has not yet completed, so no coverage or merge-readiness claim transfers from a predecessor.

This is a Draft proof-domain repair, not a protected-main activation claim. Before landing, require exact-head full tests, 100% owned-production authored line/branch coverage, current security/documentation gates, qualifying independent review, code-current #435 TRACEABILITY/gap authority, normal #492 prerequisite landing, and immutable contextual-orchestrator owner contracts. If current-head coverage exposes any new admission-branch miss, repair the reachable branch or tighten the implementation; do not suppress it.

RCA correction on the first 5e145c75... Rust Foundation attempt: this was not a regression in the exact linear route. Job 103014259773 failed the pre-existing 17-observation characterization because public output moved from stale fallback bits 0x41a0dd779ac38e98 to 0x41a0dd779ac38e99. Recomputing from that test's independent exact pair numerator 92,549,865,125,191,410,206 / 4,624 shows ...8e99 is the unique nearest binary64: after reduction to 46,274,932,562,595,705,103 / 2,312, the squared target lies strictly above the exact midpoint between ...8e98/...8e99 and strictly below the midpoint between ...8e99/...8e9a. The two midpoint comparisons fit in u128, so no rounded floating reference is needed.

Commit 6f0063d3f0ebba807bbde8763a5238cd0306702e repairs that stale characterization by encoding those two exact integer midpoint inequalities before accepting 0x41a0dd779ac38e99. It does not weaken an oracle to match production; it turns the existing exact pair-sum evidence into an independent rounding bracket. The predecessor coverage-generation failure is the same no-retry test failure propagating into llvm-cov, not infrastructure and not transferable to the new head. Fresh exact-head CI is required.

Current proof narrowing for #488@e07848a40229575d3f5926e7f40d8d3cfd143555 / bias_se.rs:307 (research trace only; not acceptance or a source-change authorization):

Rust 1.98.1 gives the three rounding premises needed for the seed analysis. The Rust Reference specifies integer→float casts as closest-value roundTiesToEven, and primitive floating addition/subtraction/multiplication/division as IEEE-754 roundTiesToEven; f64::sqrt is separately documented as the rounded infinite-precision IEEE-754 squareRoot result. Sources: https://doc.rust-lang.org/reference/expressions/operator-expr.html#numeric-cast and https://doc.rust-lang.org/std/primitive.f64.html#method.sqrt .

Let u=2^-53, q=numerator/denominator, and t=sqrt(q) before the exact power-of-two scale. Here 1 <= numerator <= u128::MAX and 1 <= denominator <= 2^53; the denominator cast is exact and all unscaled intermediates are finite normal binary64. Writing the numerator-cast, division and sqrt roundings as δ1,δ2,δ3, each with |δi|<=u, gives

seed/t = sqrt((1+δ1)(1+δ2)) * (1+δ3).

The extrema are bounded by (1-u)^2 <= seed/t <= (1+u)^2, hence the pre-restoration relative error is at most 2u+u^2. This is substantially stronger than an unspecified ‘few ULPs’ statement, but it is not yet the terminal proof: the missing lemma must convert that relative bound to a conservative count of adjacent positive binary64 values after exact power-of-two exponent translation, separately covering (a) ordinary normal binades including the power-of-two spacing discontinuity, (b) normal→subnormal restoration with the additional correctly-rounded scaling step, and (c) the max-finite/overflow threshold. In particular, returning the fourth moved candidate without the overflow case would be premature.

I have requested an exact-current CodeRabbit falsification review on #488 for those three boundary classes. Until that discrete adjacency/overflow lemma is closed, keep the fixed four-pass fail-closed exhaustion and keep line 307 as a real proof obligation. No unbounded loop, coverage exclusion, artificial private fixture, sample-budget expansion, or unverified candidate return is justified by this note.

Fresh target-architecture finding on current #488 exact head c1b31a745c233a44e5762a78a8eab44413be0065: the remaining bias.rs:148 true arm is not safe to delete as a locally redundant 64-bit guard yet.

The exact source checks denominator > usize::MAX as u128 after proving the rational numerator/denominator are exact integer roots. Elsewhere in the same exact source tree, topic_measurement::posterior_draw::plausible_values says a usize -> u64 panic is unreachable because of “supported targets and the bounded draw contract”, while a separate topic-measurement test explicitly has #[cfg(target_pointer_width = "64")] behavior. Fresh repository search did not locate a canonical architecture/TRD/ADR declaration that actually defines the supported CPU target/pointer-width set.

This turns the line-148 obligation into a cross-cutting contract gap, not just a coverage gap. Before removing the guard, TEPP should make the supported production target architecture explicit in the canonical architecture/TRD/ADR authority and bind it to CI/build/release evidence. If 32-bit is supported, exercise the relevant conversion/resource behavior on that target; if the product contract intentionally supports only 64-bit targets, prove that invariant through build/release admission and then reassess whether the guard is structurally unreachable. Do not infer a 64-bit-only policy from the present hosted runner or silently change portability semantics to make coverage green.

No numerical source mutation was made from this finding. The current 3-arm / 3-zero-line authority remains unchanged until a target contract plus exact-head evidence resolves this branch.

Current-head reachability review has now falsified the proposed universal interception explanation for the remaining bias.rs:68-69 arm.

CodeRabbit reviewed exact #488@c1b31a745c233a44e5762a78a8eab44413be0065 and constructed a valid source-domain 64-bit public input family: n = 2^54, q = f64::from_bits(1) = 2^-1074, M = f64::from_bits(0x0020_0000_0000_0000) = 2^-1021 = 2^53 q, truth = [0.0; n], with recovered containing one M and n-1 copies of q. The translation midpoint blocks the earlier exact-anchor admissions; the fallback helper then has scale M, normalized square sum 1, and computes normalized SE 2^-54, so restoration is exactly M * 2^-54 = 2^-1075 = q/2, which binary64 rounds ties-to-even to 0.0. The line-68 guard therefore fires and correctly returns InvalidInput rather than false zero.

This is a reachability proof, not a realistic materialized acceptance fixture: two length-2^54 f64 input slices are far beyond a practical test/runtime memory budget. Therefore:

do not delete the guard and do not call it unreachable;
do not allocate this witness in CI merely to make coverage green;
treat the current uncovered arm as a conflict between source-domain safety coverage and realistic resource-bounded testing that needs a causal design resolution, e.g. a production-reachable bounded representation/streaming contract or a scientifically justified explicit sample/resource admission boundary—not a private-only coverage fixture or arbitrary cutoff;
keep the current 4,451/4,454 branch and 41,991/41,994 line evidence authoritative until such a production design change is implemented and revalidated.

This finding also strengthens the separate supported-target contract gap just recorded here: the construction explicitly depends on a 64-bit usize domain, so target architecture and resource-admission semantics need to be made canonical before line 148 or line 68 can be resolved cleanly.

Exact-current narrowing for the remaining translated-dispersion obligation (#488@5d801fdb8245fb8b7a109f23553f882b1a277d75): for the represented normalized values actually passed to the two compensated sums, the exact mathematical dispersion cannot be zero.

Reason: canonical exact translation contributes an exact zero at its selected anchor. When max_magnitude != 0, exact_power_of_two_scale(max_magnitude) is the leading-binade power of two, so the maximum-magnitude translated value normalizes to a finite represented value with magnitude in [1, 2). Therefore the represented normalized vector contains both 0 and some x with |x| >= 1. For exact real arithmetic on those represented values,

n * Σ x_i² - (Σ x_i)² = Σ_{i<j} (x_i - x_j)² >= x² >= 1.

This does not prove the current floating implementation's dispersion_numerator positive. normalized_square_sum uses rounded binary64 products, first and second moments are compensated/rounded independently, sample_count * normalized_square_sum is rounded, and only the final subtraction is fused. The remaining question is now narrower: either (a) derive a complete forward-error bound showing those rounding stages cannot move an exact dispersion of at least 1 to <= 0 over the admitted 64-bit/materializable domain, or (b) produce a compact caller-valid counterexample. Until one of those is repository-owned and independently verified, retain the fail-closed guard and do not count the algebraic identity itself as coverage/acceptance.

Navigation Menu

Repository navigation

validation: replace bias-SE sample-count staircase with measured exact-proof budget #491

Problem

Current #488 authority

Resource admission is not metric cardinality

Exact-head evidence

Remaining obligations

#488 exact-head proof frontier update

16 remaining items

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

validation: replace bias-SE sample-count staircase with measured exact-proof budget #491

Description

Problem

Current #488 authority

Resource admission is not metric cardinality

Exact-head evidence

Remaining obligations

Activity

seonghobae commented on Sep 5, 2026

seonghobae commented on Sep 6, 2026

seonghobae commented on Sep 7, 2026

seonghobae commented on Sep 8, 2026

seonghobae commented on Sep 8, 2026

seonghobae commented on Sep 8, 2026

seonghobae commented on Sep 9, 2026

seonghobae commented on Sep 9, 2026

seonghobae commented on Sep 9, 2026

seonghobae commented on Sep 9, 2026

#488 exact-head proof frontier update

seonghobae commented on Sep 9, 2026

seonghobae commented on Sep 9, 2026

seonghobae commented on Sep 9, 2026

16 remaining items

seonghobae commented on Sep 10, 2026

seonghobae commented on Sep 10, 2026

seonghobae commented on Sep 10, 2026

seonghobae commented on Sep 10, 2026

seonghobae commented on Sep 10, 2026

seonghobae commented on Sep 10, 2026

seonghobae commented on Sep 10, 2026

seonghobae commented on Sep 10, 2026

seonghobae commented on Sep 10, 2026

seonghobae commented on Sep 10, 2026

seonghobae commented on Sep 10, 2026

seonghobae commented on Sep 10, 2026

seonghobae commented on Sep 11, 2026

seonghobae commented on Sep 11, 2026

seonghobae commented on Sep 11, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions