diff --git a/research/compact-switch-sharp-density/PROOF.md b/research/compact-switch-sharp-density/PROOF.md new file mode 100644 index 0000000000..f7132bb89b --- /dev/null +++ b/research/compact-switch-sharp-density/PROOF.md @@ -0,0 +1,143 @@ +# Sharp-window density against the printed CRT repair room + +Scoped proof. No new κ. The selected conditional exponent is unchanged. +This does not accept PR #4100, and it does not extend the simultaneous +carry argument from the published `2B` margin to the sharp window. + +## Parameters + +CRT.md §3, for integers `ell ≥ 1` and `p ≥ 2`, sets + +```text +G = 64 (ell + ceil(log2(p+2))), B = 2^G, K = 64 G. +``` + +A batch has `r` targets with `r ≤ floor(L / (100 G))`. The absorption +hypothesis used below is the same one as PR #4328: `L ≤ p`. It is not +proved here that every address layout satisfies `L ≤ p`. On this domain +`G ≥ 192`. + +## Two window predicates + +A `K`-bit guard stores the target in its least bit and the window `W` in +the other `m = K − 1` bits, so `W` is an integer in `0, …, 2^m − 1`. +This is the layout in `check_batched_crt.py`: the published predicate is + +```text +2B ≤ W < 2^m − 2B. +``` + +Whenever `4B ≤ 2^m`, exactly `4B` windows fail, and the fraction is + +```text +4B / 2^m = 8B / 2^K. +``` + +That is the window summand in CRT.md §4. + +The isolated post-increment step, with digit `τ ≤ B − 2`, is the map + +```text +y1 = y + 2 z τ, τ' = τ + (y1 mod 2), y2 = y1 + z (1 − 2 τ'). +``` + +For `z = 1`, `τ = B − 2` and a zero target bit, direct expansion shows +that `y1` first leaves the `m`-bit window at + +```text +W = 2^m − (B − 2) = 2^m − B + 2. +``` + +Every smaller window, `0 ≤ W ≤ 2^m − B + 1`, returns `y2 = y + z(1−2b)` +with the window restored and with no bit at position `m+1` or above. +Thus the sharp bad set has size exactly `B − 2` (and size `0` when +`B = 2`). Its fraction is + +```text +β = (B − 2) / 2^m = 2(B − 2) / 2^K. +``` + +For `B > 2` and `4B ≤ 2^m`, + +```text +β = ((B − 2) / (4B)) · (8B / 2^K) < (1/4) · (8B / 2^K). +``` + +Every published-good window is sharp-good: `2B ≤ W ≤ 2^m − 2B − 1` +implies `W ≤ 2^m − B + 1` because `B ≥ 2`. The inclusion is proper +whenever a window below `2B` exists. + +## What the substitution does not prove + +CRT.md uses the `2B` margin to keep simultaneous carries inside disjoint +guards. The count above is for one isolated target. Replacing `8B/2^K` +by `β` in the density line is valid for that isolated predicate. It does +not by itself certify the simultaneous macro on the extra windows +`W < 2B` or `2^m − 2B ≤ W ≤ 2^m − B + 1`. + +## Union bound + +Charge a target as bad when either control digit equals `B − 1` or its +window is sharp-bad. The two digit failures contribute `2/B = 2^{1−G}`. +For `r` targets, + +```text +δ ≤ r (2/B + β) = r (2^{1−G} + 2(2^G − 2) 2^{−64G}). +``` + +Factor `2^{−G}`: + +```text +2/B + β = 2^{−G} (2 + 2(1 − 2^{1−G}) 2^{−62G}) + < 2^{−G} (2 + 2^{1−62G}). +``` + +The published window summand `8B/2^K` produces the same identity with +`2^{1−62G}` replaced by `2^{3−62G}`. Either window term is smaller than +`2^{−60}` times the digit term `2/B` once `G ≥ 1`. + +## The printed room does not contain the window term + +CRT.md §2 allows `E(p, ell) ≤ C_E 2^{4 ell} (p+2)^{16}`. With the §3 +formula for `G`, + +```text +2^{−G} 2^{4 ell} (p+2)^{16} + = 2^{−60 ell} (p+2)^{16} / 2^{64 ceil(log2(p+2))} + ≤ 2^{−60 ell} (p+2)^{−48}, +``` + +because `2^{ceil(log2(p+2))} ≥ p+2`. The factor `8B/2^K` does not occur. +Substituting `β` leaves this line unchanged, including the constant +`C_E` in front of `E`. + +## Absorption + +Assume `L ≤ p` and `r ≤ floor(L/(100G))`. Then `r ≤ p/(100G) ≤ p/19200`, +and + +```text +r (2/B + β) < r (2 + 2^{1−62G}) 2^{−G} ≤ p 2^{−G} / 6400. +``` + +The same bound holds with `8B/2^K` in place of `β`, because that only +increases the tiny summand from `2^{1−62G}` to `2^{3−62G}`, and +`2 + 2^{3−62G} < 3` still gives a factor below `1/6400`. Therefore both + +```text +r (2/B + β) ≤ C p 2^{−G}, r (2/B + 8B/2^K) ≤ C p 2^{−G} +``` + +hold for every `C ≥ 1/6400`, and in particular for every `C ≥ 1`. +Multiplying by the room line, + +```text +r (2/B + β) E ≤ (C_E p / 6400) 2^{−60 ell} (p+2)^{−48}. +``` + +The scalar prefactor that CRT.md compares with `2^{−G}` gets smaller +when `8B/2^K` is replaced by `β`, and the displayed `2^{−G} E` factor +is unchanged. The `O(V)` comparison does not lose room. + +This is a comparison of those two displayed scalars. It is not a +fixed-tape replay of bad-key evaluation, sorting, or reinsertion. diff --git a/research/compact-switch-sharp-density/README.md b/research/compact-switch-sharp-density/README.md new file mode 100644 index 0000000000..22bc6c1b75 --- /dev/null +++ b/research/compact-switch-sharp-density/README.md @@ -0,0 +1,94 @@ +# Sharp-window bad density for the compact switch + +**Scoped comparison. No new κ.** The selected conditional exponent is +unchanged. This does not accept PR #4100. + +## Result + +CRT.md §4 bounds the bad density of one batch by + +```text +r [2/B + 8B/2^K] ≤ C p 2^{-G} +``` + +and then uses the separate room + +```text +2^{-G} E(p, ell) ≤ C 2^{-60 ell} (p+2)^{-48}. +``` + +The window summand `8B/2^K` is the fraction of `K−1`-bit windows outside +the published margin `2B ≤ W < 2^m − 2B`. The isolated post-increment +step admits the larger range `0 ≤ W ≤ 2^m − B + 1`. On that predicate the +bad-window count is exactly `B − 2`, so the summand is + +```text +β = 2(B − 2) / 2^K = ((B − 2) / (4B)) · (8B / 2^K). +``` + +For every `B > 2` this is strictly less than one quarter of the published +window term. It is zero when `B = 2`. + +Under CRT.md's parameters `G = 64(ell + ceil(log2(p+2)))`, `B = 2^G`, +`K = 64G`, with `ell ≥ 1`, `p ≥ 2`, `L ≤ p` and `r ≤ floor(L/(100G))`, + +```text +r (2/B + β) < p 2^{-G} / 6400. +``` + +The same ceiling holds for the published window term. The displayed +`2^{-G} E` line does not contain `8B/2^K`, so it is unchanged. Replacing +the window term therefore does not shrink the scalar room CRT.md uses to +put bad-key work in `O(V)`. + +The argument is in [PROOF.md](PROOF.md). The executable checks the window +count by running the isolated step, the integer form of the ratio, the +room identity, and the `C = 1/6400` comparison on a finite parameter grid. + +## Scope + +Card `formal-interface-lemma`, scope **refined**. The catalogue's first +experiment for #4100 is to audit the compact-switch contract before a +formalization campaign. That audit is PR #4321. Its open question 2 asks +whether the section-4 density still fits `O(V)` if the window hypothesis +is the sharp range. This package answers that question. + +The simultaneous carry argument in CRT.md still assumes the stricter `2B` +margin. This count does not extend that argument to the extra windows. +No tape repair, Lean proof, or multiplication theorem is claimed. + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -B research/compact-switch-sharp-density/verify.py +python3.12 -B scripts/research_package.py --package research/compact-switch-sharp-density +``` + +The direct command prints `PASS_COMPACT_SWITCH_SHARP_DENSITY`. + +## Open next questions + +1. Does one two-target macro with disjoint guards still restore both + controls on a window that is sharp-good but outside the published `2B` + margin? The density line can use `β` for the isolated predicate only. + First step: run the live two-target macro at `W = 0` and at + `W = 2^m − B + 1` with `K`-separated positions. Blocker: the twelve + paid `H`-bit exchanges are not replayed here. +2. Is `L ≤ p` true for a real #4174 placement, or only a sufficient + hypothesis inherited from #4328? The constant `1/6400` uses that + hypothesis. First step: read one production plan's address length + against its `p`. Blocker: reservoir placement is not an input here. + +## Credit + +Cinna Davis, PR #4100, for CRT.md and `check_batched_crt.py`. The +live-digit lemma and the sharp window are the compact-switch contract +audit, PR #4321. The published density identity and the `L ≤ p` +absorption hypothesis are PR #4328. The uniform evaluator constant is +PR #4377 and is not reused. The guard-coloring decision is PR #4329. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. +Apache-2.0. No independent human review and no formal-kernel acceptance +are claimed. diff --git a/research/compact-switch-sharp-density/SOURCES.json b/research/compact-switch-sharp-density/SOURCES.json new file mode 100644 index 0000000000..ad3c35c60f --- /dev/null +++ b/research/compact-switch-sharp-density/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "fbc9ea0249746acca4f504d4fda2b84e0e36cf0d", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/unconditional-batched-crt/CRT.md", + "usage": "input", + "git_blob": "d98dd8e368431cac33d5fc1c8c336696663641d6", + "sha256": "02c3a1e38cbee25aefe2640cc72676da62ba10eb7519fbcb9adb9d48b74eff2b" + }, + { + "path": "research/unconditional-batched-crt/check_batched_crt.py", + "usage": "input", + "git_blob": "1cf78abccd5e06beecc3ed21ba55f7c03b65fdbc", + "sha256": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e" + } + ] +} diff --git a/research/compact-switch-sharp-density/TASK.json b/research/compact-switch-sharp-density/TASK.json new file mode 100644 index 0000000000..d8e4a7ac70 --- /dev/null +++ b/research/compact-switch-sharp-density/TASK.json @@ -0,0 +1,101 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "fbc9ea0249746acca4f504d4fda2b84e0e36cf0d", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Replace CRT.md section 4's window term 8B/2^K by the sharp-window fraction 2(B-2)/2^K and compare the union bound with the printed 2^{-G} E room.", + "scope_change_reason": "The card asks for one uncovered interface statement after the compact-switch contract is reviewed. PR #4321 is that review and leaves the section-4 density recomputation open. This package answers that question. It does not formalize the live-digit lemma in a proof assistant and does not repeat the gate-operand or certified-endpoint arithmetic.", + "bottleneck_link": "PR #4100's repair amortization charges bad records at the section-4 density. The sharp window shrinks that window term and leaves the printed 2^{-G} E line unchanged, so the scalar room does not shrink. This does not change kappa.", + "budget_minutes": 60, + "stop_rule": "Stop after the isolated window count, the ratio, and the scalar comparison under L <= p. Do not replay simultaneous carries, the tape repair, or Lean.", + "outcome": "completed", + "evidence": "PROOF.md. Verifier PASS_COMPACT_SWITCH_SHARP_DENSITY: sharp bad count B-2 on seven (B, m) pairs, room identity on seven (ell, p) pairs, C=1/6400 absorption on 15 parameter rows including 6 with r > 0, and two failure controls.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance.", + "open_questions": [ + { + "question": "Does one two-target macro with disjoint guards restore both controls on a window that is sharp-good but outside the published 2B margin?", + "why_it_matters": "The density substitution uses the isolated predicate. CRT.md's simultaneous carry argument still assumes the stricter margin.", + "first_step": "Run the live two-target macro at W=0 and at W=2^m-B+1 with K-separated positions.", + "blocked_by": "The twelve paid H-bit exchanges are not replayed here." + }, + { + "question": "Is L <= p true for a real #4174 placement, or only a sufficient hypothesis inherited from #4328?", + "why_it_matters": "The constant 1/6400 uses L <= p. A larger address length needs its own constant.", + "first_step": "Read one production plan's address length against its p.", + "blocked_by": "Reservoir placement is not an input to this package." + } + ] +} diff --git a/research/compact-switch-sharp-density/VERIFY.json b/research/compact-switch-sharp-density/VERIFY.json new file mode 100644 index 0000000000..7594a39719 --- /dev/null +++ b/research/compact-switch-sharp-density/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/unconditional-batched-crt/CRT.md", + "research/unconditional-batched-crt/check_batched_crt.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Sharp bad-window count equals B-2 by executing the isolated step; published count is 4B and strictly larger; ratio (B-2)/(4B); 2^{-G} E room identity; C=1/6400 absorption for L<=p on a parameter grid; failure controls reject a forged 4B count and a room line that drops E." + } + ] +} diff --git a/research/compact-switch-sharp-density/verify.py b/research/compact-switch-sharp-density/verify.py new file mode 100644 index 0000000000..952984aa1a --- /dev/null +++ b/research/compact-switch-sharp-density/verify.py @@ -0,0 +1,213 @@ +#!/usr/bin/env python3 +"""Sharp-window bad density against CRT.md's printed repair room. + +The published section-4 window term is 8B/2^K. The isolated compact-switch +step admits every window 0 <= W <= 2^m - B + 1. This verifier checks that +the resulting bad-window count is B-2, that this fraction is strictly below +the published term, and that the printed 2^{-G} E comparison does not use +the window term and still dominates the sharp union bound. + +No new kappa and no simultaneous multi-target carry theorem are claimed. +""" + +import importlib.util +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +CRT = ROOT / "research/unconditional-batched-crt/CRT.md" +CHECKER = ROOT / "research/unconditional-batched-crt/check_batched_crt.py" + +PUBLISHED_DENSITY = "r [2/B + 8B/2^K] <= C p 2^-G." +PUBLISHED_ROOM = "2^-G E(p,ell) <= C 2^(-60 ell) (p+2)^(-48)," +PARAMETER_LINE = "G=64(ell+ceil(log2(p+2))), B=2^G, K=64G," + + +def need(condition, message): + if not condition: + raise SystemExit("FAIL: " + message) + + +def load_checker(): + spec = importlib.util.spec_from_file_location("batched_crt_predecessor", CHECKER) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def post_step(y, z, tau): + """One target at bit 0. Second coefficient is the post-increment digit.""" + y1 = y + 2 * z * tau + bit = y1 & 1 + tau_post = tau + bit + y2 = y1 + z * (1 - 2 * tau_post) + return y1, y2, tau_post, bit + + +def ceil_log2(n): + need(n >= 1, "log of a positive integer") + return n.bit_length() - 1 if n.bit_count() == 1 else n.bit_length() + + +def parameters(ell, p): + need(ell >= 1 and p >= 2, "CRT size domain") + g_value = 64 * (ell + ceil_log2(p + 2)) + return g_value, 1 << g_value, 64 * g_value + + +def sharp_bad_count(base, width): + """Bad windows for the isolated step, by executing the step.""" + limit = 1 << width + safe_last = limit - (base - 2) - 1 + bad = 0 + tau = base - 2 + for window in range(limit): + y = window << 1 + y1, y2, _, bit = post_step(y, 1, tau) + overflows = (y1 >> 1) >= limit or (y2 >> 1) >= limit or y2 < 0 + if window <= safe_last: + need(bit == 0, "zero target is read as zero") + need(not overflows, "sharp window must not overflow") + need(y2 == y + 1, "z=1 flips a zero target by +1") + else: + need(overflows, "window past the sharp bound must overflow") + bad += 1 + return bad + + +def published_bad_count(base, width): + limit = 1 << width + bad = 0 + for window in range(limit): + if not (2 * base <= window < limit - 2 * base): + bad += 1 + return bad + + +def bind_sources(checker): + text = CRT.read_text(encoding="utf-8") + need(PUBLISHED_DENSITY in text, "CRT.md density line moved") + need(PUBLISHED_ROOM in text, "CRT.md room line moved") + need(PARAMETER_LINE in text, "CRT.md parameter line moved") + need(checker.good(1, 0, 17, bits=2, positions=(0,), guard=6), + "published good predicate rejects the known interior window") + need(not checker.good(1, 0, 1, bits=2, positions=(0,), guard=6), + "published good predicate accepts a low window") + + +def count_identity(): + """B-2 bad windows, and the published count 4B when the margin fits.""" + cases = 0 + for bits, width in ((1, 4), (1, 6), (2, 6), (2, 8), (3, 8), (4, 8), (3, 10)): + base = 1 << bits + limit = 1 << width + sharp = sharp_bad_count(base, width) + need(sharp == base - 2, "sharp bad count is B-2") + published = published_bad_count(base, width) + if 4 * base <= limit: + need(published == 4 * base, "published bad count is 4B") + need(sharp < published, "sharp bad set is a proper subset") + need(sharp * 4 * base == (base - 2) * published or 4 * base > limit, + "fraction identity on the fitting domain") + # (B-2)/(4B) * 8B = 2(B-2), so the sharp numerator is that factor + # times the published numerator. Both sides are integers. + need((base - 2) * 8 * base == 2 * (base - 2) * 4 * base, + "window-term ratio (B-2)/(4B)") + need(sharp << 1 == 2 * (base - 2), "sharp numerator is 2(B-2)") + cases += 1 + return cases + + +def room_identity(): + """2^{-G} 2^{4 ell} (p+2)^16 <= 2^{-60 ell} (p+2)^{-48}.""" + cases = 0 + for ell, p in ((1, 2), (1, 14), (2, 2), (2, 6), (3, 30), (5, 2**16), (8, 10**6)): + g_value, _, _ = parameters(ell, p) + c_log = ceil_log2(p + 2) + # Cross-multiply: 2^{4 ell} (p+2)^64 <= 2^{G - 60 ell} = 2^{4 ell + 64 c_log}. + need((p + 2) ** 64 <= 1 << (64 * c_log), "power-of-two ceiling") + need(g_value - 60 * ell == 4 * ell + 64 * c_log, "exponent split") + need(g_value >= 192, "minimum G on ell>=1, p>=2") + cases += 1 + return cases + + +def absorption(): + """r * sharp union bound < p 2^{-G} / 6400 when L <= p.""" + rows = 0 + positive_r = 0 + samples = [] + for ell in (1, 2, 4): + for p in (2, 100, 20_000, 2**20, 10**7): + g_value, _, _ = parameters(ell, p) + length = p + rank = length // (100 * g_value) + # p * 2^{62 G} >= r * (2 * 2^{62 G} + 2) proves + # p >= r (2 + 2^{1-62 G}) > r (2 + 2(1-2^{1-G}) 2^{-62 G}). + shift = 62 * g_value + sharp_left = rank * ((2 << shift) + 2) + published_left = rank * ((2 << shift) + 8) + right = p << shift + # r (2 + 2^{1-62G}) <= p, hence r * alpha < p 2^{-G}. + need(sharp_left <= right, "sharp union bound fits C = 1") + # The same comparison with the published window numerator 8. + need(published_left <= right, "published union bound fits C = 1") + # r <= p/(100G) and G >= 192 give the sharper factor 1/6400. + need(6400 * sharp_left <= right, "sharp union bound fits C = 1/6400") + if rank > 0: + positive_r += 1 + samples.append((ell, p, g_value, rank)) + rows += 1 + need(positive_r >= 1, "grid includes a positive batch size") + return rows, positive_r, samples + + +def ratio_and_dominance(): + """Window term is < 1/4 of the published term and << 2/B.""" + for g_value in (1, 2, 192, 256): + base = 1 << g_value + # (B-2)/(4B) < 1/4. + need(4 * (base - 2) < 4 * base, "strict window shrinkage") + need((base - 2) * 4 < base * 4 or base > 2, "ratio below one") + # 2(B-2)/2^K divided by 2/B is 2(B-2) B / 2^K = (B-2) 2^{1-63 G}. + # For G >= 1 this is < 2^{-60}. + if g_value >= 1: + need(1 + g_value < 63 * g_value - 60, "window/digit exponent gap") + return 4 + + +def failure_controls(): + """A count that restores 4B, or a room line that drops the E factor, fails.""" + base, width = 4, 8 + sharp = sharp_bad_count(base, width) + forged = 4 * base + need(forged != sharp, "forged published count is not the sharp count") + need(not (forged == base - 2), "control rejects the old numerator") + # Dropping E from the room would claim 2^{-G} <= 2^{-60 ell} (p+2)^{-48}, + # which is false once the 2^{4 ell} (p+2)^16 factor is required. + ell, p = 1, 2 + g_value, _, _ = parameters(ell, p) + bare = 1 << g_value + room = (1 << (60 * ell)) * (p + 2) ** 48 + need(bare > room, "2^{-G} alone is not the printed room") + return 2 + + +def main(): + checker = load_checker() + bind_sources(checker) + counts = count_identity() + rooms = room_identity() + rows, positive_r, samples = absorption() + gaps = ratio_and_dominance() + controls = failure_controls() + ell, p, g_value, rank = samples[0] + print( + "PASS_COMPACT_SWITCH_SHARP_DENSITY" + f" counts={counts} rooms={rooms} rows={rows}" + f" positive_r={positive_r} gaps={gaps} controls={controls}" + f" sample_ell={ell} sample_p={p} sample_G={g_value} sample_r={rank}" + ) + + +if __name__ == "__main__": + main()