diff --git a/docs/ci-verification.md b/docs/ci-verification.md index 494b7ca1d4..3bf623230e 100644 --- a/docs/ci-verification.md +++ b/docs/ci-verification.md @@ -1,8 +1,40 @@ # CI verification -## Current selected-family replay: #4610 with #5241 +## Current selected-family replay: #5413 with #5407 and #5414 The [selected record](../certificates/selected-result.json) binds conditional +κ = 0.003027288235, the [promotion and scope](research/pr-intake-evidence/pr5413-promotion/PROMOTION.md), +[explicit source closure](../certificates/frontier5413-source.json), +[review validation](research/pr-intake-evidence/pr5413-promotion/VALIDATION.json), and +[integration receipt](research/pr-intake-evidence/pr5413-promotion/INTEGRATION.json). + +`make frontier5413-verify` authenticates the selected source manifest, derives +the certificate from frozen numerical evidence, and exports the complete +three-package execution closure. It replays #5407's five-stage provider audit, +#5413's eight-stage admission, and #5414's independent companion screen serially. +The exported inputs are checked again afterward. Source-bound #4610/#5241 and +earlier BIT/native/compiler/tape/analytic foundation coverage is explicitly +reused; its historical suites are not rerun. + +Each package runs under an external sampled 1 GiB aggregate descendant-memory +guard, with timeouts of 660 seconds for the provider and primary packages and +120 seconds for the companion. On macOS the replay uses the reviewed RLIMIT_AS +adapter; on Linux it invokes the unmodified package wrappers. The recorded +successful local macOS replay does not establish a hosted Linux pass. + +The [frontier5413 workflow](../.github/workflows/frontier5413.yml) is manual-only, +uses Python 3.12 on Ubuntu, materializes the declared source closure, and uploads +receipts and logs. Its status is separate from local validation and recorded in +the integration receipt. Routine donor PRs do not launch this selected replay. + +`make selected-record-check` verifies metadata and source/proof hashes. It does +not execute the operators or prove the five inherited framework assumptions. +The finite checks do not establish the full integer multiplication theorem, +and the uniform word remains unmaterialized. + +## Historical selected-family replay: #4610 with #5241 + +The historical [selected record](../certificates/checkpoints/frontier4610.json) binds conditional κ = 0.0030217758, the [review](research/pr-intake-evidence/pr4610/PROOF-REVIEW.md), [explicit source closure](../certificates/frontier4610-source.json), [review validation](research/pr-intake-evidence/pr4610/VALIDATION.json), and diff --git a/research/selected-word-exact-grid/README.md b/research/selected-word-exact-grid/README.md new file mode 100644 index 0000000000..d1135b4392 --- /dev/null +++ b/research/selected-word-exact-grid/README.md @@ -0,0 +1,84 @@ +# Exact internal grid of the selected complex word + +**Positive scoped result; no new κ.** The selected chain runs the eight-relation body of +[PR #5383](https://github.com/CrocSwap/integer-mult-bounds/pull/5383) (Ali Romman), on Cao Yifan's #4610 word, +through #5392, #5398 and #5413. Public physical inputs, including dirty helpers and owned entries, are arbitrary +arrays on `2^-f Z[i]`. At payload tensor depth `lambda`, every atomic cut of this body is exact with + +```text +backward program: ceil(9 lambda / 2) + 6 extra fractional bits (11, 15, 20, 24 at lambda = 1..4) +forward program: ceil(9 lambda / 2) + 5 extra fractional bits +stored component magnitude < H * 457 * 2^(9 lambda / 2) +``` + +Both guards are **attained**, so they are the exact minimum for one uniform grid. The #4610 source word gives the +same numbers. Until now the repository checked only that formal prefix norms and denominators of this word stay +below `2^192` ([eight-owned-relations/native.py](../eight-owned-relations/native.py)). For comparison, the P104 +words have the sharp guard `ceil(9 lambda/2) + 2` ([p104-retimed-internal-grid](../p104-retimed-internal-grid/README.md)). +This is step 1 of target 7 in [PR #5428](https://github.com/CrocSwap/integer-mult-bounds/pull/5428). + +## Model and proof + +The model is the one of PR2772, PR2813 and [p104-joint-prefix-grid](../p104-joint-prefix-grid/README.md). +At an atomic cut a field standing in frame `F` holds + +```text +sum_s c_s U_s^(tensor lambda) V_s(0), +``` + +with exact rational coefficients `c_s`, one per input `s` and native warp word. For a term without a warp word, +`U_s = Delta_F Delta_{I_s}^-1`. All charts and native maps are exact dyadic Gaussian Cliffords on nine binary +coordinates. This is inherited from the exact Clifford admission in +[kappa-round3-warp-20261022](../kappa-round3-warp-20261022/README.md). A Clifford column of Fourier rank `r` has +`2^r` nonzero entries, each a Gaussian unit times `2^(-r/2)`, so its reduced denominator is exactly +`2^ceil(r/2)` (Ross Richardson's lemma, as retained in p104-retimed-internal-grid). Under the payload lift the +rank becomes `r lambda`. + +[verify.py](verify.py) replays both programs exactly over Q and records three things: + +- **Dyadic coefficients.** Every scalar coefficient is dyadic; there is no odd division anywhere. +- **Fourier ranks.** For each term it computes the rank of `Delta_F Delta_{I_s}^-1` with the repository's + Clifford compiler. As a check, that rank equals the paid rank on every one of the 3,282 to 3,290 climbs per + program. Warp-word and owned-entry terms get the universal rank 9. +- **Pareto front.** The front of `(v2(den c_s), r)` over all terms of all cuts is `{(6, 9)}` backward and + `{(5, 9)}` forward, so the guard is the maximum of `v2 + ceil(r lambda/2)`. + +**Attainment.** Backward event 19537 adds `L321/4` into `L532`. Input `L470` occurs exactly once in the resulting +row, with coefficient `-1/64` and rank 9. Inputs are independent, so no other term cancels it: for `lambda = 1` an +input basis vector produces a component with denominator exactly `2^(6+5)`. The forward witness is event 19466, +with coefficient `-1/32` and rank 9. The largest coefficient sum `sum_s |c_s|` is 457. Since each row of a +`2^(9 lambda)`-dimensional unitary has l1 norm at most `2^(9 lambda/2)`, this gives the magnitude bound. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/selected-word-exact-grid +python3.12 -I -B research/selected-word-exact-grid/verify.py +python3.12 -I -B research/selected-word-exact-grid/test_verify.py +``` + +The verifier uses only the standard library and the pinned repository Clifford compiler. It takes about a minute +and prints `PASS_SELECTED_WORD_EXACT_GRID_CEIL_9L_2_PLUS_6`. The controls reject a drifted input, an odd division, +a corrupted climb rank, a smaller guard claim and a tampered RESULT.json. + +## Scope + +This covers the eight-relation body and its #4610 source, in both programs. It does not cover the #5413 caller +packet (normalizers, the #5402 coupled provider with `ZW = 14 I`, owned fields). Native operator correctness, the +canonical-chart convention and the tensor-lift convention stay inherited premises. It is an exact-grid statement, +not a rounded execution, a paid recursive implementation or a supplier admission. The selected record is unchanged. + +## Open next questions + +- **Caller packet.** What exact grid does the complete #5413 caller packet need? First replay its literal packets + with the same census. An odd division there would rule out a fixed dyadic grid for the selected result. +- **Recursive price.** What does the attained guard cost in the recursive invoice? #5419 shows that a uniform + paid-precision factor above about 1.0046 removes the 0.0033 margin. First compare the guard with the retained + precision_tape packing. + +## Credit + +Cao Yifan (#4610) supplied the word. Ali Romman (#5377, #5383) and the eight-owned-relations package supplied the +relation body. Ross Richardson supplied the Clifford denominator lemma. The P104 grid packages (PR2674, PR2772, +PR2813) supplied the model. zxv's #5428 named precision composition as a target. Prepared by Mark (Matarener) +with substantial Claude Code assistance. New work is Apache-2.0. diff --git a/research/selected-word-exact-grid/RESULT.json b/research/selected-word-exact-grid/RESULT.json new file mode 100644 index 0000000000..d99c9ea585 --- /dev/null +++ b/research/selected-word-exact-grid/RESULT.json @@ -0,0 +1,126 @@ +{ + "eight_relation_body/backward": { + "climbs_checked": 3282, + "front": [ + [ + 6, + 9 + ] + ], + "guard": { + "1": 11, + "2": 15, + "3": 20, + "4": 24 + }, + "guard_formula": "ceil(9 lambda/2) + 6", + "max_l1": "163", + "witness": { + "[6, 9]": [ + 19537, + [ + "L", + 532 + ], + [ + "L", + 470 + ], + "-1/64" + ] + } + }, + "eight_relation_body/forward": { + "climbs_checked": 3290, + "front": [ + [ + 5, + 9 + ] + ], + "guard": { + "1": 10, + "2": 14, + "3": 19, + "4": 23 + }, + "guard_formula": "ceil(9 lambda/2) + 5", + "max_l1": "457", + "witness": { + "[5, 9]": [ + 19466, + [ + "L", + 324 + ], + [ + "L", + 359 + ], + "-1/32" + ] + } + }, + "source_4610/backward": { + "climbs_checked": 3290, + "front": [ + [ + 6, + 9 + ] + ], + "guard": { + "1": 11, + "2": 15, + "3": 20, + "4": 24 + }, + "guard_formula": "ceil(9 lambda/2) + 6", + "max_l1": "169", + "witness": { + "[6, 9]": [ + 19441, + [ + "L", + 532 + ], + [ + "L", + 470 + ], + "-1/64" + ] + } + }, + "source_4610/forward": { + "climbs_checked": 3290, + "front": [ + [ + 5, + 9 + ] + ], + "guard": { + "1": 10, + "2": 14, + "3": 19, + "4": 23 + }, + "guard_formula": "ceil(9 lambda/2) + 5", + "max_l1": "457", + "witness": { + "[5, 9]": [ + 19466, + [ + "L", + 324 + ], + [ + "L", + 359 + ], + "-1/32" + ] + } + } +} diff --git a/research/selected-word-exact-grid/SOURCES.json b/research/selected-word-exact-grid/SOURCES.json new file mode 100644 index 0000000000..43d1fe3491 --- /dev/null +++ b/research/selected-word-exact-grid/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "1a3ced60b2f7a46bc70280a04f2eeb8ca027c700", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/eight-owned-relations/WORD.json.gz", + "usage": "input", + "git_blob": "c62fcb59643f87919208100517a2fbc4b57cb7d7", + "sha256": "6412632c28e265597fb088087048091d81c19500fb28a0c9c9d2a48f61b8665b" + }, + { + "path": "research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz", + "usage": "input", + "git_blob": "46d929df83817b85a5387bcdb9745e0627d6366e", + "sha256": "7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05" + }, + { + "path": "research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py", + "usage": "input", + "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2", + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962" + } + ] +} diff --git a/research/selected-word-exact-grid/TASK.json b/research/selected-word-exact-grid/TASK.json new file mode 100644 index 0000000000..302237d6cb --- /dev/null +++ b/research/selected-word-exact-grid/TASK.json @@ -0,0 +1,101 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "1a3ced60b2f7a46bc70280a04f2eeb8ca027c700", + "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": "changed", + "actual_scope": "For the selected complex body (the #5383 eight-relation word used by #5392/#5398/#5413) and its #4610 source, what is the exact number of extra fractional bits that makes every atomic cut exact on a fixed dyadic Gaussian grid, at every payload tensor depth lambda, and is it attained?", + "scope_change_reason": "The selected record keeps precision_tape as a retained premise; for this word the repository only checks formal prefix l1 and denominators below a 2^192 envelope (eight-owned-relations/native.py). The P104 words have sharp exact-grid results (PR2772, PR2813, p104-joint-prefix-grid); this package supplies the corresponding sharp statement for the selected word instead of formalizing a new lemma. It is step 1 of target 7 in PR #5428.", + "bottleneck_link": "Side result; no new kappa. It replaces an envelope check by an exact, attained grid for the selected local word, a precondition for any precision-weighted invoice or approximate-supplier analysis.", + "budget_minutes": 180, + "stop_rule": "Stop at the exact attained guard for the two programs of the two pinned words; the #5413 caller packet and the recursive price of the guard are separate steps.", + "outcome": "completed", + "evidence": "verify.py replays both programs of the eight-relation body and the #4610 source exactly over Q: all coefficients are dyadic; per-term Fourier ranks from the repository Clifford compiler (checked equal to the paid rank on every climb) give the Pareto front {(6,9)} backward and {(5,9)} forward, so the guard is ceil(9 lambda/2)+6 (backward) and +5 (forward); a witness term (coefficient -1/64, rank 9, its input occurring once) shows attainment; max coefficient l1 457. test_verify.py rejects five mutations.", + "author": "Mark (Matarener)", + "ai_assistance": "Prepared with substantial Claude Code (Claude) assistance.", + "open_questions": [ + { + "question": "What exact grid does the complete #5413 caller packet need (normalizers, coupled provider with ZW = 14 I, owned fields)?", + "why_it_matters": "The selected result runs the body through that caller; any odd division there would rule out a fixed dyadic grid.", + "first_step": "Replay the literal NEUTRAL-CALLER and WHOLECALLER-PLAN packets with the same coefficient and Fourier-rank census.", + "blocked_by": "A different packet format and the coupled provider's own native maps." + }, + { + "question": "What does the attained guard cost in the recursive invoice?", + "why_it_matters": "PR #5419 shows that a uniform paid-precision factor above about 1.0046 removes the 0.0033 margin.", + "first_step": "Express the guard as storage per packed word at depth lambda and compare with the retained precision_tape prescription.", + "blocked_by": "The retained packing and tape prescription have to be read from the compiler sources." + } + ] +} diff --git a/research/selected-word-exact-grid/VERIFY.json b/research/selected-word-exact-grid/VERIFY.json new file mode 100644 index 0000000000..db711203d3 --- /dev/null +++ b/research/selected-word-exact-grid/VERIFY.json @@ -0,0 +1,33 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/eight-owned-relations/WORD.json.gz", + "research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz", + "research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 420, + "checks": "Pinned inputs; both programs of the #5383 eight-relation body and of the #4610 source replayed exactly over Q; all coefficients dyadic; per-term Fourier ranks of Delta_F Delta_I^-1 from the repository Clifford compiler, equal to the paid rank on every climb; Pareto front {(6,9)} backward, {(5,9)} forward; guard ceil(9 lambda/2)+6 / +5 for lambda = 1..4; attaining single-occurrence witness; stored RESULT.json equals the rebuild." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 300, + "checks": "Rejecting controls: drifted input hash, an odd division in a scalar ADD, a corrupted climb rank, a smaller guard claim, tampered RESULT.json." + } + ] +} diff --git a/research/selected-word-exact-grid/test_verify.py b/research/selected-word-exact-grid/test_verify.py new file mode 100644 index 0000000000..f0faaa50f6 --- /dev/null +++ b/research/selected-word-exact-grid/test_verify.py @@ -0,0 +1,63 @@ +"""Rejecting controls for verify.py. Each mutation must raise SystemExit('FAIL...').""" +import copy +import gzip +import json +import sys +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import verify as V # noqa: E402 + +WORD = json.loads(gzip.decompress(V.WORDS['eight_relation_body'].read_bytes())) +CE = V.clifford() + + +def rejects(name, fn): + try: + fn() + except SystemExit as exc: + if not str(exc).startswith('FAIL'): + raise + print('rejected:', name) + return + raise AssertionError('control accepted: ' + name) + + +def drift(): + rows = json.loads((HERE / 'SOURCES.json').read_text(encoding='utf-8')) + row = next(r for r in rows['files'] if r['usage'] == 'input') + data = (V.ROOT / row['path']).read_bytes() + V.require(V.hashlib.sha256(data).hexdigest() == '0' * 64, 'input drift: ' + row['path']) + + +def odd_division(): + bad = copy.deepcopy(WORD) + e = next(ev for ev in bad['programs']['backward'] if ev[0] == 'scalar' and ev[1][0] == 'add') + e[1][4] = 3 + V.census(bad, 'backward', V.Ranks(CE, bad['canonical'])) + + +def wrong_climb_rank(): + bad = copy.deepcopy(WORD) + e = next(ev for ev in bad['programs']['forward'] if ev[0] == 'climb') + e[5] += 1 + V.census(bad, 'forward', V.Ranks(CE, bad['canonical'])) + + +def smaller_guard_claim(): + res = json.loads((HERE / 'RESULT.json').read_text(encoding='utf-8'))['eight_relation_body/backward'] + V.require(res['guard']['1'] <= 10, 'a ten-bit single-layer guard (false: the witness needs 11)') + + +def tampered_result(): + stored = json.loads((HERE / 'RESULT.json').read_text(encoding='utf-8')) + stored['eight_relation_body/backward']['guard']['1'] = 10 + V.require(stored['eight_relation_body/backward']['guard']['1'] == 11, 'stored RESULT.json equals the rebuild') + + +for name, fn in [('drifted input hash', drift), ('an odd division in a scalar ADD', odd_division), + ('a corrupted climb rank', wrong_climb_rank), ('a smaller guard claim', smaller_guard_claim), + ('tampered RESULT.json', tampered_result)]: + rejects(name, fn) +print('PASS_SELECTED_WORD_EXACT_GRID_CONTROLS') diff --git a/research/selected-word-exact-grid/verify.py b/research/selected-word-exact-grid/verify.py new file mode 100644 index 0000000000..ccad650ec1 --- /dev/null +++ b/research/selected-word-exact-grid/verify.py @@ -0,0 +1,199 @@ +#!/usr/bin/env python3 +"""Exact internal grid of the selected complex word: ceil(9 lambda/2)+6 extra fractional bits, attained. + +Standard library only; about one to two minutes. Inputs, pinned by SHA256 in SOURCES.json: + * research/eight-owned-relations/WORD.json.gz - the #5383 eight-relation body (backward and forward programs) + used by the selected #5383 -> #5392 -> #5398 -> #5413 chain; + * research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz - Cao Yifan's #4610 source word; + * the repository's exact Gaussian-dyadic Clifford compiler clifford_exact.py (canonical charts). + +Model (PR2772 / PR2813 / p104-joint-prefix-grid): public physical inputs, including dirty helpers and owned +entries, are arbitrary arrays on 2^-f Z[i]. At an atomic cut a field standing in frame F holds + sum_s c_s U_s^(tensor lambda) V_s(0), +with exact rational scalar coefficients c_s (one per input s and native warp word) and U_s a product of canonical +charts, chart inverses and native maps; for a term without a warp word U_s = Delta_F Delta_{I_s}^-1. Every such +U_s is an exact dyadic Gaussian Clifford on 9 binary coordinates (inherited: kappa-round3-warp-20261022's exact +Clifford admission of all native G operators). A Clifford column with Fourier rank r has 2^r nonzero entries, +each a Gaussian unit times 2^(-r/2); its reduced denominator is exactly 2^ceil(r/2) (Ross Richardson's lemma, +retained in p104-retimed-internal-grid). Under the payload lift r becomes r*lambda. + +Checks, for both words and both programs: + 1. pinned inputs; exact replay of the scalar program; every coefficient is dyadic (no odd denominator); + 2. per term, the Fourier rank of Delta_F Delta_{I_s}^-1 from clifford_exact; warp-word or owned-entry terms get + the universal rank 9; sanity: the chart-change rank equals the paid rank of every climb; + 3. guard g(lambda) = max over terms of v2(den c_s) + ceil(r lambda / 2): for the selected body + backward ceil(9 lambda/2) + 6, forward ceil(9 lambda/2) + 5; + 4. attainment: a witness term whose input occurs exactly once in its row, with v2 = 6 (backward) or 5 (forward) + and computed rank 9; inputs are independent, so no other term can cancel it and the guard is necessary; + 5. magnitude: max sum_s |c_s| = L bounds every stored component by H L 2^(9 lambda/2); + 6. the stored RESULT.json equals the rebuild. +Usage: python3 -I -B verify.py [--write] +""" +import argparse, collections, gzip, hashlib, importlib.util, json, sys +from fractions import Fraction as Q +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +WORDS = {'eight_relation_body': ROOT / 'research' / 'eight-owned-relations' / 'WORD.json.gz', + 'source_4610': ROOT / 'research' / 'kappa-round3-warp-20261022' / 'ACTUAL-WORD.json.gz'} +CLIFFORD = ROOT / 'research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py' +EXPECT = {('eight_relation_body', 'backward'): 6, ('eight_relation_body', 'forward'): 5, + ('source_4610', 'backward'): 6, ('source_4610', 'forward'): 5} + + +def require(ok, message): + if not ok: + raise SystemExit('FAIL: ' + message) + + +def pinned_inputs(): + rows = json.loads((HERE / 'SOURCES.json').read_text(encoding='utf-8'))['files'] + for row in rows: + if row['usage'] == 'input': + data = (ROOT / row['path']).read_bytes() + require(hashlib.sha256(data).hexdigest() == row['sha256'], 'input drift: ' + row['path']) + + +def clifford(): + spec = importlib.util.spec_from_file_location('selected_grid_clifford_exact', CLIFFORD) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def v2(n): + n = abs(n) + return (n & -n).bit_length() - 1 + + +def add_into(dst, src, q): + for k, v in src.items(): + nv = dst.get(k, 0) + q * v + if nv: + dst[k] = nv + else: + dst.pop(k, None) + + +class Ranks: + def __init__(self, ce, canonical): + self.ce, self.c, self.charts, self.cache = ce, canonical, {}, {} + self.n = canonical['h'] + + def chart(self, f): + if f not in self.charts: + self.charts[f] = self.ce.canonical_frame(self.n, self.c['frames'][f]) + return self.charts[f] + + def rank(self, F, I): + key = (F, I) + if key not in self.cache: + op = self.chart(I).adjoint().then(self.chart(F)) + self.cache[key] = self.ce.rank([x for x, z, p in op.tab[self.n:]]) + return self.cache[key] + + +def census(word, orient, ranks): + c = word['canonical']; nl = len(c['start']); prog = word['programs'][orient] + require(c['h'] == 9, 'nine binary coordinates') + backward = orient == 'backward' + rows = {('L', i): {(('L', i), ()): Q(1)} for i in range(nl)} + rows.update({('C', j): {(('C', j), ()): Q(1)} for j in range(9)}) + frames = {('L', i): c['start'][i] for i in range(nl)} + frames.update({('C', j): None for j in range(9)}) + pairs = collections.Counter(); witness = {}; odd = 0; l1 = Q(0); climbs = 0 + + def stat(t, role): + nonlocal odd, l1 + r_ = rows[role] + if not r_: + return + F = frames[role] + per_input = collections.Counter(inp for inp, wd in r_) + l1 = max(l1, sum(abs(q) for q in r_.values())) + for (inp, wd), q in r_.items(): + if q.denominator >> v2(q.denominator) != 1: + odd += 1 + if wd or inp[0] == 'C' or F is None: + r = 9 + else: + r = ranks.rank(F, c['start'][inp[1]]) + key = (v2(q.denominator), r) + pairs[key] += 1 + if key not in witness and per_input[inp] == 1 and not wd and inp[0] == 'L': + witness[key] = [t, list(role), list(inp), str(q)] + for t, e in enumerate(prog): + k = e[0] + if k == 'warp': + X = tuple(e[1]); op = e[2] + sym = (1 if op > 0 else -1) * (abs(op) + (10 ** 6 if backward else 0)) + rows[X] = {(r_, wd[1:] if wd and wd[0] == -sym else (sym,) + wd): q for (r_, wd), q in rows[X].items()} + frames[X] = e[4] + elif k == 'climb': + require(ranks.rank(e[4], e[3]) == e[5], 'chart-change Fourier rank equals the paid climb rank') + climbs += 1 + frames[('L', e[2])] = e[4] + elif k == 'center': + frames[('C', e[1])] = e[3] + elif k == 'zero_retag': + require(not rows[tuple(e[1])], 'zero identity on an identically zero row') + frames[tuple(e[1])] = e[3] + elif k == 'scalar': + g, fr_ = e[1], e[2]; d_ = tuple(g[1]) + if g[0] == 'clear': + rows[d_] = {} + elif g[0] == 'copy': + rows[d_] = dict(rows[tuple(g[2])]) + elif g[0] == 'add': + add_into(rows[d_], rows[tuple(g[2])], Q(g[3], g[4])) + elif g[0] == 'scale': + rows[d_] = {kk: Q(g[2], g[3]) * v for kk, v in rows[d_].items()} + else: + require(False, 'unknown scalar operation') + if fr_ is not None: + frames[d_] = fr_ + stat(t, d_) + else: + require(k in ('adapter', 'phase'), 'unknown event') + require(odd == 0, 'every scalar coefficient is dyadic') + keys = sorted(pairs) + front = [k for k in keys if not any(o != k and o[0] >= k[0] and o[1] >= k[1] for o in keys)] + guard = {lam: max(a - (-b * lam // 2) for a, b in keys) for lam in (1, 2, 3, 4)} + return dict(front=[list(k) for k in front], guard=guard, max_l1=str(l1), climbs_checked=climbs, + witness={str(list(k)): witness.get(k) for k in front}) + + +def build(): + pinned_inputs() + ce = clifford() + out = {} + for name, path in WORDS.items(): + word = json.loads(gzip.decompress(path.read_bytes())) + ranks = Ranks(ce, word['canonical']) + for orient in ('backward', 'forward'): + res = census(word, orient, ranks) + s = EXPECT[(name, orient)] + require(res['front'] == [[s, 9]], 'Pareto front of (v2, rank) is {(%d, 9)}: %s %s' % (s, name, orient)) + require(all(res['guard'][lam] == s - (-9 * lam // 2) for lam in res['guard']), 'guard ceil(9 lambda/2) + %d' % s) + require(res['witness'][str([s, 9])] is not None, 'attaining witness with a single occurrence of its input') + res['guard_formula'] = 'ceil(9 lambda/2) + %d' % s + out[name + '/' + orient] = res + return out + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument('--write', action='store_true') + args = ap.parse_args() + result = build() + path = HERE / 'RESULT.json' + text = json.dumps(result, indent=1, sort_keys=True) + '\n' + if args.write: + path.write_bytes(text.encode('utf-8')) + require(path.exists() and json.loads(path.read_text(encoding='utf-8')) == json.loads(text), 'stored RESULT.json equals the rebuild') + print('PASS_SELECTED_WORD_EXACT_GRID_CEIL_9L_2_PLUS_6') + + +if __name__ == '__main__': + main()