From 4950117fd6d6f973d494e5e900b16809386b0644 Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Tue, 27 Oct 2026 23:15:39 -0700 Subject: [PATCH] Type the selected ordinary backend for conditional finite reseeding --- .../README.md | 157 ++++++++++++++++++ .../SOURCES.json | 94 +++++++++++ .../TASK.json | 77 +++++++++ .../VERIFY.json | 42 +++++ .../verify.py | 71 ++++++++ 5 files changed, 441 insertions(+) create mode 100644 research/selected-ordinary-reseed-contract/README.md create mode 100644 research/selected-ordinary-reseed-contract/SOURCES.json create mode 100644 research/selected-ordinary-reseed-contract/TASK.json create mode 100644 research/selected-ordinary-reseed-contract/VERIFY.json create mode 100644 research/selected-ordinary-reseed-contract/verify.py diff --git a/research/selected-ordinary-reseed-contract/README.md b/research/selected-ordinary-reseed-contract/README.md new file mode 100644 index 0000000000..ccc43e1543 --- /dev/null +++ b/research/selected-ordinary-reseed-contract/README.md @@ -0,0 +1,157 @@ +# Typing the selected ordinary BIT backend for finite reseeding + +**Conditional interface lemma, not a supplier admission or a new bound.** +The selected ordinary backend can replace the predecessor-valued A0 in the +PR4814 finite-level construction under the retained completed-endpoint, +ROW/spectator, native, compiler and fixed-tape assumptions. The replacement +uses the actual completed backend, not just its exponent. Six fixed levels +then reach PR5708's stated ordinary component; no G20 predecessor exponent +is needed as the starting backend. The G20 raw/native construction and its +other admission obligations remain separate. + +This answers the framework-reading question left in Matarener's +[PR5955](https://github.com/CrocSwap/integer-mult-bounds/pull/5955), at +`52115896549090117a3f3101b17106cad4466408`. It is a source-based mathematical +reading under existing premises, not maintainer approval. The source review +and substitution proof are below; [verify.py](verify.py) only checks the +selected-source bindings, adapter arithmetic and six strict separators. +It does not machine-prove the interface assertions. + +## Which source versions and which backend + +At base `721c03822c421b7f7fcbb2598993b947c4d88419`, +`certificates/selected-result.json` selects PR6030. Its CLAIM retains ordinary +BIT saving `8590884599/2500000000000 = .0034363538396`, separately from +conservatively admitted BIT `17/5000 = .0034`, uniform BIT before cover +`.003459`, and the complex/outer multiplication saving. This substitution +uses the ordinary value and its completed interface. + +PR4814's final merged head is `f56ae4533a7d97d782a2c596a33fe844cd051747`. +Its `research/bit-finite-ordinary-bootstrap/PROOF.md` is byte-identical to the +older `709fcb31cc66bd8ce2165d60f495259502325536` snapshot: +SHA256 `5cabee7e5264ab0d674d5d591b4a3880ad460a546bcf5d53067eeeb9aff68df2`. +Thus its sections 2 and 4 have no consumer-contract drift. That text names +PR4760 as A0; the substitution argument below establishes why that name is +not an essential mathematical restriction when another completed backend +has the same interface. + +The exact PR5708 head is `829d01fc031f7323ffcfa423fdfd1f24dcbe3190`. +Its original five levels use PR5679's stronger predecessor value. Its +`ORDINARY-RESULT.json` supplies the outer C1 and strict grid, not the seed +for this replacement. PR5955 separately checked wider tail guards down to +the selected seed; those numerical guards are not the missing endpoint type. + +## Clause-to-source map + +The selected source manifest `certificates/frontier6030-source.json` pins +both cited notes and the PR4359/PR4470 reviews below. The selected CLAIM +pins the numerical value. Their conclusions retain the five selected +framework assumptions; the table does not independently discharge them. + +| PR4814 consumer clause | Selected source evidence and its implication | +| --- | --- | +| Completed ordinary interchange on arbitrary widths and complete chunks | `notes/batched-bit-rows.tex`, “Bit interchange with a remainder” and “Supplying the bit rows from existing digits”, handle every integer width and the finite small-width range. PR4359 review section 3 explicitly identifies the two-call ordinary wrapper, its three paid additions and restored rows. The seed is this completed wrapper, not a raw reverse word or only the before-cover supplier. | +| Preserve preceding/intervening complete spectators | `notes/three-stage-cover-bit.tex`, “Atom contract and common endpoint”, requires every complete spectator and the row coordinate to be preserved. `notes/batched-bit-rows.tex` retains intervening G, unused main digits and remainders. The entire outer ROW is a complete ancestor/spectator coordinate of an inner call. | +| Internally borrow and return row stock | “Supplying the bit rows from existing digits” borrows high digits from the two argument chunks, pads complete rows, invokes the recursion, removes zero padded rows and undoes gathering. Every completed invocation preserves its row index. PR4359 review section 3 charges the logarithmic reserve and completed ordinary wrapper. No external empty stock or restoration by a raw reversed body is substituted. | +| Weighted leaves reduce to ordinary calls | `notes/three-stage-cover-bit.tex`, “Weighted leaves and a genuine local-ring fallback”, writes J_a using four ordinary atom interchanges, three prefix-controlled shifts and a sign. Generated weights depend only on ancestors; no stronger weighted primitive is demanded from A0. The old numerical leaf exponent in that note is replaceable only together with this completed call interface. | +| Fixed-radix outer chunks adapt to binary with volume below four | Proven directly below for two complete equal-range chunks. The selected backend's separate binary-to-internal-q conversion has a fixed factor below q^2 in `notes/batched-bit-rows.tex`; it is already part of that backend's constant and is not claimed to be below four. | +| Fresh finite constants and thresholds, frozen before varying e | PR4814 sections 2–4 freeze each A_(j−1), use it for atom/routing/high-part calls, and choose a new threshold at each fixed level. The selected backend already has fixed finite constants under its assumptions. PR5708's `fee_bounds.eventual_threshold` expressly depends on the completed backend constant and threshold; these must be regenerated for the replacement. | +| Correct saving with enough adapter/stock gap | Selected CLAIM and PR4470 review section 3 identify `.0034363538396`; PR4470 records the essential atom power `.004` rather than the obsolete `.003`. The six new exact separators below use this completed ordinary seed. | + +## Conditional substitution lemma + +Let B0 be the selected completed ordinary procedure just identified, with +cost `O(V e^(1-b0))`, fixed constants, arbitrary complete chunk widths, +complete spectators fixed at return, and internally borrowed stock returned. +Retain the PR4814/PR5708 uniform supplier and all its native, ownership, +compiler, cover, precision and tape premises. If the strict inequalities + + b_(j−1) < b_j < a_j = (1−rho) C1 + rho b_(j−1) + < C1 < rho < 1−a_j + +hold for a fixed finite list j=1,...,L, then that construction produces a +sequence of distinct completed procedures B1,...,BL with savings b_j. +Replacing the seed changes finite constants and thresholds; it does not +require admitting the exponent of an intervening G20 construction. + +**Proof.** At level j choose the already frozen completed B_(j−1). A weighted +leaf, routing call or high-part exchange uses the ordinary-call interface +in the table. Its outer row and all other complete fields are spectators, +so the inner procedure restores its own borrow before the outer program +resumes. The base procedure's correctness on arbitrary simultaneous data +and its complete endpoint allow composition; no intermediate state is +asserted to preserve the outer row or to commute with the outer program. + +For an outer q-ary chunk of width w put R=q^w and M=2^ceil(log2 R). +Pad both complete chunks to M, run the binary ordinary interchange, and +unpad. Since R <= M < 2R, the volume multiplier is `(M/R)^2 < 4`. +Swapping the two equal-range coordinates preserves the original square +`[0,R)^2` and its complement, so padded zeros return to the padded region. +Each spectator slice is complete and preserved. The binary width is +`ceil(w log2 q)=Theta_q(w)` for fixed q. The inner backend may choose its +own fixed radix and constants; its internal conversion is absorbed in +its already-established cost. Padding does not execute an unpriced +address-dependent map. + +The inherited root costs are + + O(V [ e^(1−rho) + + e^((1−rho)(1−C1)+rho(1−b_(j−1))) + + e^rho log e ]). + +The middle exponent is `1−a_j`; `rho−a_j>0` and `1−rho−a_j>0` pay the other +two terms, and `a_j−b_j>0` pays the final strict relaxation. All positive +primitive constants, inherited reserve bounds, radix factors and frozen +backend thresholds are finite. Choose a fresh threshold for B_j that +absorbs them and pays the positive gaps. Below that fixed threshold use +individual-digit interchange (or the completed slower backend with a +larger finite constant). A bounded width set cannot obstruct the stated +asymptotic saving, uniformly in the complete spectator volume V. + +Freeze this procedure and its constants before going to j+1. Coarse +recursion decreases atom count, while backend recursion decreases j. +There is no self-reference, no depth increasing with input size, and no +requirement that the fixed internal primes agree. Induction gives the +claimed completed interface at every one of the fixed L levels. This +establishes substitutability under the stated premises, not those premises +or the admission of the outer G20 supplier. ∎ + +## Six-level arithmetic and verification boundary + +For PR5708, `C1=14030876239/4000000000000`, `rho=1/100` and strict grid +`10^-15`, use `b_j=(ceil(10^15 a_j)-1)/10^15`. The registered verifier reads +b0 from the selected CLAIM, checks every strict inequality, and verifies +that level five is below and level six equals `.003507719059749`. +This corroborates PR5955's arithmetic only after the interface mapping. + +Run, using standard-library Python 3.12: + +```sh +python3.12 -B scripts/research_package.py --package research/selected-ordinary-reseed-contract +``` + +Expected marker: `PASS_SELECTED_ORDINARY_RESEED_CONTRACT_BINDINGS`. The +normal/optimized checks also test the strict-grid equality boundary and +integer radix padding controls. No G20 global/native replay is run; no +stale numerical threshold is claimed valid for the reseeded program. + +## Open next questions + +**Source-bound reseeded admission.** To use this in an admission, construct a +new PR5708 admission receipt naming this B0 and six levels, regenerate all +backend-dependent fee/stock/threshold constants, and bind applicable raw, +native and analytic evidence. This matters because the old receipt names a +different seed and five levels. First change those specific inputs in an +isolated admission package; the remaining blocker is the full inherited +supplier and framework obligations, not the scalar recurrence or seed type. + +## Credit + +Prepared by JoyboyBrian with substantial OpenAI Codex assistance, Apache-2.0. +Matarener (#5955, substantial Claude assistance) identified the direct-reseed +question and checked its arithmetic. Ali Romman supplied PR4814 and the G20 +composition sources; finite acyclic bootstrapping and nested restoration +are prior work of rohanarun (#185/#199/#204). Nicknames and contributors of +the selected native/compiler, BIT and outer framework retain their source +attribution, including zxv, Cinna Davis and Jacob Alan Sussman. No precursor +construction, selected record or frozen source is changed here. diff --git a/research/selected-ordinary-reseed-contract/SOURCES.json b/research/selected-ordinary-reseed-contract/SOURCES.json new file mode 100644 index 0000000000..ae20ac626e --- /dev/null +++ b/research/selected-ordinary-reseed-contract/SOURCES.json @@ -0,0 +1,94 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "files": [ + { + "path": "certificates/frontier6030-source.json", + "usage": "input", + "git_blob": "e58847094e2f631665030bb6f045f8bebe638c6c", + "sha256": "95ddc380f6b05499fccd8820ab7f84fb6d287b4e66a721ed41ca9d293c4eaa3e" + }, + { + "path": "certificates/frontier6030/CLAIM.json", + "usage": "input", + "git_blob": "f32ff3779274a349dc8af2e84a4c6234c6d62406", + "sha256": "9cee8a1304fa893be3d3b641eda42fdd9b2fd6a5ac2124fb891de7a1a5e8d92e" + }, + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "docs/research/pr-intake-evidence/pr4359/PROOF-REVIEW.md", + "usage": "input", + "git_blob": "cb95b6547c8dad5a90a29f6e1981e8bbaa86d4a9", + "sha256": "7d67bb814285f7634029fbd378c6457156545f0b38858cc1c6ec34b68cd9d162" + }, + { + "path": "docs/research/pr-intake-evidence/pr4470/PROOF-REVIEW.md", + "usage": "input", + "git_blob": "f4dc043b6d35cae2811c9bcc064e04877f9e0549", + "sha256": "5c111dd56beb53dc44ab727d96e1af03aaf50f3023d4342e2b0a89ede6cf585b" + }, + { + "path": "notes/batched-bit-rows.tex", + "usage": "input", + "git_blob": "cbaa8cb42cad1e714a1d24b16ab160ae6eaf60c9", + "sha256": "ef72c0ead19373cbc19c8a3aacb44dd0f75353ee5f4d055f775a986a4878022c" + }, + { + "path": "notes/three-stage-cover-bit.tex", + "usage": "input", + "git_blob": "f05225d21f92cf8cef21b6e12601d5b4d61991f0", + "sha256": "47123a756f823c83a0d48cca2bf5add6472cd88410b13aed345e70c8834fb511" + }, + { + "path": "research/bit-finite-ordinary-bootstrap/PROOF.md", + "usage": "input", + "git_blob": "7db6805f8a9ae77b28c5772ee6de3e47777912b1", + "sha256": "5cabee7e5264ab0d674d5d591b4a3880ad460a546bcf5d53067eeeb9aff68df2" + }, + { + "path": "research/g20-conjugation-admission/ORDINARY-RESULT.json", + "usage": "input", + "git_blob": "46308272ac871d5876406dbb59eb21f4035c3503", + "sha256": "3a379d5ba1e005ce57610d9a5954cce62f24939b7246bb785e76ff70f74c93fa" + }, + { + "path": "research/bit-finite-ordinary-bootstrap/PROOF.md", + "usage": "provenance", + "pin": "head:f56ae4533a7d97d782a2c596a33fe844cd051747:research/bit-finite-ordinary-bootstrap/PROOF.md", + "git_blob": "7db6805f8a9ae77b28c5772ee6de3e47777912b1", + "sha256": "5cabee7e5264ab0d674d5d591b4a3880ad460a546bcf5d53067eeeb9aff68df2" + }, + { + "path": "research/bit-finite-ordinary-bootstrap/PROOF.md", + "usage": "provenance", + "pin": "head:709fcb31cc66bd8ce2165d60f495259502325536:research/bit-finite-ordinary-bootstrap/PROOF.md", + "git_blob": "7db6805f8a9ae77b28c5772ee6de3e47777912b1", + "sha256": "5cabee7e5264ab0d674d5d591b4a3880ad460a546bcf5d53067eeeb9aff68df2" + }, + { + "path": "research/g20-independent-review/README.md", + "usage": "provenance", + "pin": "head:52115896549090117a3f3101b17106cad4466408:research/g20-independent-review/README.md", + "git_blob": "92deccb3ac4712b2047922fa9c426e046ebc7119", + "sha256": "d0a007f675f433372679f71686283a2b0150e9200cfe86a0d9b92d945489d41e" + }, + { + "path": "research/g20-conjugation-admission/ORDINARY-RESULT.json", + "usage": "provenance", + "pin": "head:829d01fc031f7323ffcfa423fdfd1f24dcbe3190:research/g20-conjugation-admission/ORDINARY-RESULT.json", + "git_blob": "46308272ac871d5876406dbb59eb21f4035c3503", + "sha256": "3a379d5ba1e005ce57610d9a5954cce62f24939b7246bb785e76ff70f74c93fa" + } + ] +} diff --git a/research/selected-ordinary-reseed-contract/TASK.json b/research/selected-ordinary-reseed-contract/TASK.json new file mode 100644 index 0000000000..b13c63459e --- /dev/null +++ b/research/selected-ordinary-reseed-contract/TASK.json @@ -0,0 +1,77 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "original_card": { + "id": "bit-helper-contract", + "question": "Can a changed G20 helper path or independent-target split improve the complete BIT moment without losing its physical endpoint?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "research/g20-helper-split/README.md", + "research/g20-conjugation-admission/README.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "First read #5679/#5708 and their audits as pending component proposals. Choose one uncovered helper group/cut on an exact word; compare arbitrary-input native action, targets, owned storage, both orientations and full signed bill. Stop if the gain is only a scalar count or repaid by lost targets. Do not rerun the frozen #5609 common-frame domain without changing its hypothesis.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "G20", + "helper split", + "5679", + "5708", + "independent target" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Type selected ordinary BIT backend as the finite PR4814 seed; conditional interface lemma and source table.", + "scope_change_reason": "Explicit preclaimed PR5955 handoff takes priority over the generic helper task.", + "bottleneck_link": "Removes the need for predecessor-valued G20 seeds while preserving completed ROW/spectator and framework obligations; no supplier admission.", + "budget_minutes": 25, + "stop_rule": "One source-bound conditional substitution lemma; no native replay or new bound.", + "outcome": "completed", + "evidence": "README.md clause table and substitution lemma; verify.py selected-source bindings, strict six-level separators and negative gap control.", + "author": "JoyboyBrian", + "ai_assistance": "Substantial OpenAI Codex assistance.", + "open_questions": [ + { + "question": "Construct a source-bound reseeded admission receipt.", + "why_it_matters": "The old PR5708 receipt names a different backend and five levels.", + "first_step": "Regenerate backend-dependent fee, stock and threshold constants for selected B0 and six levels.", + "blocked_by": "Remaining raw/native/compiler/ROW/precision/tape obligations and admission review." + } + ] +} diff --git a/research/selected-ordinary-reseed-contract/VERIFY.json b/research/selected-ordinary-reseed-contract/VERIFY.json new file mode 100644 index 0000000000..6999da1536 --- /dev/null +++ b/research/selected-ordinary-reseed-contract/VERIFY.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/frontier6030-source.json", + "certificates/frontier6030/CLAIM.json", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr4359/PROOF-REVIEW.md", + "docs/research/pr-intake-evidence/pr4470/PROOF-REVIEW.md", + "notes/batched-bit-rows.tex", + "notes/three-stage-cover-bit.tex", + "research/bit-finite-ordinary-bootstrap/PROOF.md", + "research/g20-conjugation-admission/ORDINARY-RESULT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Selected-source bindings, exact strict separators, equality-boundary negative control, finite padding controls; not semantic proof of the interface." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Selected-source bindings, exact strict separators, equality-boundary negative control, finite padding controls; not semantic proof of the interface." + } + ] +} diff --git a/research/selected-ordinary-reseed-contract/verify.py b/research/selected-ordinary-reseed-contract/verify.py new file mode 100644 index 0000000000..23a0513d7e --- /dev/null +++ b/research/selected-ordinary-reseed-contract/verify.py @@ -0,0 +1,71 @@ +#!/usr/bin/env python3 +"""Source bindings and exact separators only; does not prove interface semantics.""" +from fractions import Fraction as F +from pathlib import Path +import hashlib +import json + +ROOT = Path(__file__).resolve().parents[2] + + +def require(value, message): + if not value: + raise SystemExit('FAIL ' + message) + + +def read(path): + return json.loads((ROOT / path).read_text()) + + +def strict_below(value, denominator): + return F((value.numerator * denominator - 1) // value.denominator, denominator) + + +def step(backend, covered, rho, grid): + exact = (1-rho)*covered + rho*backend + admitted = strict_below(exact, grid) + if not backend < admitted < exact < covered < rho < 1-exact: + raise ValueError('completed seed or separator gap invalid') + return admitted + + +def main(): + selected = read('certificates/selected-result.json') + require(selected['source_manifest'] == 'certificates/frontier6030-source.json', 'selected source changed') + manifest = read(selected['source_manifest'])['files'] + for path in ('certificates/frontier6030/CLAIM.json', 'notes/three-stage-cover-bit.tex', + 'notes/batched-bit-rows.tex', 'docs/research/pr-intake-evidence/pr4359/PROOF-REVIEW.md', + 'docs/research/pr-intake-evidence/pr4470/PROOF-REVIEW.md'): + require(manifest.get(path) == hashlib.sha256((ROOT/path).read_bytes()).hexdigest(), + 'selected-source binding ' + path) + consumer = (ROOT/'research/bit-finite-ordinary-bootstrap/PROOF.md').read_bytes() + require(hashlib.sha256(consumer).hexdigest() == '5cabee7e5264ab0d674d5d591b4a3880ad460a546bcf5d53067eeeb9aff68df2', + 'PR4814 consumer clause version') + b = F(read('certificates/frontier6030/CLAIM.json')['ordinary_BIT_saving']) + require(b == F('0.0034363538396'), 'wrong ordinary seed') + outer = read('research/g20-conjugation-admission/ORDINARY-RESULT.json') + covered, rho, grid = F(outer['C1']), F(outer['params']['rho']), outer['params']['grid_denominator'] + levels = [] + for _ in range(6): + b = step(b, covered, rho, grid) + levels.append(str(b)) + require(F(levels[4]) < F(outer['admitted']) == F(levels[5]), 'six-level endpoint') + require(strict_below(F(3,10),10) == F(2,10), 'strict-grid equality control') + try: + step(covered, covered, rho, grid) + except ValueError: + pass + else: + raise SystemExit('FAIL equal seed/covered exponent must reject') + # Exact finite controls for the separate two-chunk padding lemma. + for radix in (3,5,17): + for width in (1,2,7): + size = radix**width + binary = 1 << (size-1).bit_length() + require(size <= binary < 2*size and F(binary**2,size**2) < 4, 'radix adapter control') + print('PASS_SELECTED_ORDINARY_RESEED_CONTRACT_BINDINGS ' + json.dumps({'levels':levels, + 'scope':'source bindings and arithmetic; conditional interface proof is README.md'})) + + +if __name__ == '__main__': + main()