diff --git a/research/bit-two-use-lattice-descent/README.md b/research/bit-two-use-lattice-descent/README.md new file mode 100644 index 0000000000..0b29fc26fe --- /dev/null +++ b/research/bit-two-use-lattice-descent/README.md @@ -0,0 +1,257 @@ +# Two-use lattice descent excludes one eight-call bit candidate + +**Scoped negative result; No new κ.** The profile +`(A,B,P,Q,R,S) = (1,3,0,1,1,2)`, with `R=2A` and `S=P/2`, cannot realize +the four-target endpoint below, for **any finite number of restored dirty +registers**, any ordering, and any free address-independent binary mixing. +This resolves the specific example in open question 2 of +[JosieElliston's pending PR6111](https://github.com/CrocSwap/integer-mult-bounds/pull/6111), +at head `961b749fa40a1117d0746064528d2dfa290c57e0`. + +The candidate passes determinant, bounded subset-support, and every first-order +character-rank inequality on its actual address lattice. The new step is to +contract its two half-frame calls, then use a character on the smaller lattice. +No scalar-word search is needed. The all-width conclusion rests on the written +proof; the executable supplies exact, finite regression evidence. + +## Model and source boundary + +Use the rational address matrices + +\[ +A=\begin{pmatrix}1&0\\0&0\end{pmatrix},\quad +B=\begin{pmatrix}0&0\\0&1\end{pmatrix},\quad +P=\tfrac12\begin{pmatrix}1&1\\1&1\end{pmatrix},\quad +Q=\tfrac12\begin{pmatrix}1&-1\\-1&1\end{pmatrix}. +\] + +Thus `A+B=P+Q=I`, and set `R=2A`, `S=P/2`. Each allowed label is positive +rank one. The group algebra is `F2[Λ]`, where +`Λ=ZA+ZB+ZS` is a free abelian rank-three lattice. Rational frame entries +are not reduced modulo two. Write `[F][G]=[F+G]`. On `w>=4` registers a +paid call is + +\[ +E_F(N)=I+([F]-1)N,\qquad N\in M_w(\mathbb F_2),\quad N^2=N,\quad +\operatorname{rank}N=1. +\] + +The target is the complete matrix + +\[ +T_w=\operatorname{diag}([A+P],[A+Q],[B+P],[B+Q],1,\ldots,1). +\] + +Every register starts arbitrary; all extra registers must be restored. Free +maps are matrices in `GL_w(F2)`, independent of the address. Equality means +equality of every formal coefficient, not equality at a finite address size. + +The model and endpoint are inherited from Cinna Davis's PR2085/2112 through +[Nick Petalas's PR2910 note](../bit-fifth-frame-determinant-obstruction/README.md). +**Its fifth frame is different:** we use that note for the four old labels, +endpoint and operation model, not its five-frame exclusion theorem. PR6111 +supplies the concrete question; neither its seven-call theorem nor pending +PR6089's classification is assumed. No predecessor executable is imported. + +## Two-use descent lemma + +Let `H` be an index-two subgroup of an abelian address lattice `Λ`. Call an +exponent *even* if it lies in `H`, and *odd* otherwise. Suppose a word has an +even endpoint, exactly two paid calls with odd labels `s,t`, and all other +paid labels in `H`. Free binary mixing may occur anywhere. Then its two odd +calls can be replaced by one call with label `s+t` without changing the +endpoint, register count, or intervening even calls and free maps. + +The replacement is a legal paid call in a proposed alphabet only if `s+t` +is admitted there. A zero sum gives the identity. The lemma is an algebraic +reduction, not a claim that arbitrary summed frames have a native tariff. + +**Proof.** Write the two odd calls and everything between them as + +\[ +U=E_s(N_1)\,M\,E_t(N_2),\qquad M\in M_w(\mathbb F_2[H]). +\] + +The outer factors and their inverses are even: `E_h(N)^{-1}=E_{-h}(N)` +for `h in H`, and free binary maps are constant. Removing those factors +therefore shows that `U` is even. These inverses are used in the proof only; +no inverse calls are inserted in the replacement word. + +Put `C=I-N1` and `D=I-N2`. Idempotence gives `CN1=N1C=DN2=N2D=0`. +Since monomials commute with matrices, the block expansion is + +\[ +U=CMD+[t]CMN_2+[s]N_1MD+[s+t]N_1MN_2. +\] + +The middle two terms are the odd part. Multiplying their zero sum on the +left by `C` and on the right by `N2` isolates `[t]CMN2`; multiplying on the +left by `N1` and on the right by `D` isolates `[s]N1MD`. Monomials are +units, so `CMN2=N1MD=0`. It follows that + +\[ +M=CMD+N_1MN_2,\qquad N_1M=MN_2, +\] + +and hence + +\[ +U=CMD+[s+t]N_1MN_2=M E_{s+t}(N_2). +\] + +This leaves `M` unchanged and uses the same rank-one projector `N2` in the +new call. It applies to every finite width. The projectors need not be equal +when `M` contains free mixing. If all free maps have first been normalized +away, augmentation `M -> I` implies `N1=N2`. No such normalization is needed +for the contraction itself. ∎ + +## Exclusion of the candidate + +Here `H=ZA+ZB+ZP` is the index-two subgroup of `Λ=ZA+ZB+ZS`. Every old +label, `R=2A`, and every target exponent lies in `H`; only `S` lies outside. +There are exactly two `S` calls. The lemma replaces them by one `P` call, +giving the seven-call profile + +\[ +(A,B,P,Q,R)=(1,3,1,1,1). +\] + +For completeness, the character-rank obstruction is as follows. An additive +`χ:H -> F2` induces `[F] -> 1+χ(F)ε` in `F2[ε]/(ε²)`. Free binary maps +can be moved to the right by conjugating the paid projectors. Conjugation +preserves rank and idempotence. Augmentation of the target is `I`, so the +final free map is `I`. Comparing first-order coefficients now gives + +\[ +\sum_{i:\chi(F_i)=1}N_i +=\operatorname{diag}(\chi(A+P),\chi(A+Q),\chi(B+P),\chi(B+Q),0,\ldots,0). +\] + +Choose `χ(A)=χ(B)=0`, `χ(P)=1`. This is a character on the free basis of +`H`, and `Q=A+B-P` gives `χ(Q)=1`, while `χ(R)=χ(2A)=0`. Only the one +`P` and one `Q` calls contribute. The left side has rank at most two and +the right side has rank four. Contradiction. ∎ + +This character does **not** extend to `Λ`: there `P=2S` forces `χ(P)=0`. +That is why contracting before applying the character adds information. + +## What the original checks miss + +The candidate's determinant sum is +`A+3B+Q+2A+2S=4I`, the target determinant exponent. Literal enumeration of +all 256 subsets of its eight labelled occurrences finds target support +multiplicities `1,1,3,3`. In basis `(A,B,S)`, the eight characters give: + +| character | detected calls | target rank | +|---|---:|---:| +| 000 | 0 | 0 | +| 001 | 2 | 0 | +| 010 | 4 | 2 | +| 011 | 6 | 2 | +| 100 | 2 | 2 | +| 101 | 4 | 2 | +| 110 | 4 | 4 | +| 111 | 6 | 4 | + +All satisfy the necessary inequality. These checks are not sufficient for +realizability; this example is a concrete counterexample to treating them +as sufficient. It is not a counterexample to PR6111, which explicitly left +realizability open. + +Even the full first-order matrix equations are jointly consistent. At width +four, assign `A,R,S,S` to coordinate projector `E00`, the three `B` calls +to `E11,E22,E33`, and `Q` to `E33`. This one assignment satisfies all eight +character equations. Its exact product is not the target; both polynomial +engines check that distinction. Thus the contraction uses information beyond +simply solving the initial first-order equations together. + +## Reproduce and evidence + +From repository root, with Python 3.12 and the standard library: + +```sh +python3 -I -B research/bit-two-use-lattice-descent/verify.py +``` + +Expected: `PASS_BIT_TWO_USE_LATTICE_DESCENT ... descent_rank=2<4`. +The verifier recomputes and compares every field of [RESULT.json](RESULT.json). +It never rewrites the receipt. Normal and optimized modes have explicit +checks rather than Python assertions. Replay takes a few seconds. + +- Exact rational matrices and integer lattice coordinates independently check + the determinant and target support; all eight raw characters and the joint + first-order projector witness are checked. +- Every ordered triple of rank-one binary projectors at widths two and three + is tested in `E_S(N1) E_(2S)(K) E_S(N2)`: 216 and 21,952 cases. Exactly + 12 and 196 have even endpoints; each contracts as claimed. A separate + entry-wise polynomial-set engine checks all 216 width-two products. +- The block expansion and contraction are checked on 9,120 matrix-unit cases: + every projector pair at widths two and three, and equal-projector pairs at + width four. The labels `-3S,5S` test unequal odd labels and negative exponents. +- Both coefficientwise engines check the direct eight-call construction and + a nine-call subdivision with separated `S` calls, at widths 4, 5 and 7, + directly and with explicit free mixing. All 12 endpoints pass; extra dirty + registers are restored. The nine-call profile differs from the excluded one. +- Controls detect a noncommuting middle, unequal normalized projectors, a + single odd call, a non-idempotent, all nine single-call deletions, both + `S->P` corruptions, and source-byte mutation. Positive controls include + inverse-pair cancellation and a free middle map intertwining unequal + projectors. CLI tests reject altered receipts and pins in normal and + optimized mode and accept an isolated source export with an empty `PATH`. + +The finite domains are exhaustive only as stated above. They are regression +checks for the displayed algebra, not a formal proof of its arbitrary-width +statement. Both implementations were prepared in this contribution; no +independent human review or proof-kernel verification is claimed. + +Base: `721c03822c421b7f7fcbb2598993b947c4d88419`. +[SOURCES.json](SOURCES.json) pins the canonical model note, task catalogue and +selected record. The live model note has Git blob +`608a24af8bc3d27ee1554c94872601bb3a409f67` and SHA256 +`fa3f0f951146caa5b1eb7b7417175eb7a380cae8674e4a470407517dac40f227`. +The pending PR6111 README is context only, pinned at the head above and blob +`98eb6718d0ae424c129cf08b186fd2a5593ca783`; it is not needed to run or prove +this result. No external download or predecessor code is needed for replay. + +## Scope and cost gate + +This is a changed-scope side result under `bit-new-register-model`; [TASK.json](TASK.json) +records the OS draw 19, diversification seed, three candidates, local claim, +overlap limitations and refresh decisions. PR1974's three-register rational +`3x3` theorem and PR2027's two-register nonabelian `GL3(F2)` census do not +cover this four-target rational `2x2` endpoint at arbitrary restored width. + +The optimistic bill is already eight paid calls with all scalar mixing free, +equal to the direct endpoint cost. The proposed profile cannot realize even +that relaxed bill. No native address implementation, source-access schedule, +storage saving, recursive profile or physical caller is constructed, and no +conversion from formal calls to native cost is asserted. The selected +conditional result remains `781451/250000000`; its five inherited framework +assumptions are unchanged. No supplier or selected-certificate cold replay +is claimed or needed for this isolated algebraic result. `upstream/` is untouched. + +## Open next questions + +1. Which other eight-call survivors in PR6111 admit an index-two quotient + with exactly two odd occurrences? This could prune its open list without + searching scalar words. First extract each exact candidate lattice and + character, contract only when the summed label is priced, and rerun + support/rank conditions. This package does not classify those survivors. +2. What can replace two-use descent when four calls occupy the odd coset? + The two cross blocks no longer isolate in the same way. A first step is + a small exact four-odd-factor example with an even endpoint, including + realizable subdivision controls. There is no claimed four-use reduction + or justification for a larger search here. + +## Credit + +Prepared for **@CubeJerry** with substantial **OpenAI Codex** assistance; +new proof application, code and prose are Apache-2.0. The classical idempotent +block decomposition and dual-number rank method are not claimed as new. +Credit JosieElliston/Claude for PR6111's concrete unresolved candidate; +JoyboyBrian (PR6104) for the two-frame question; apoursh (PR6089) for the +one-frame work and subdivision motivation; Nick Petalas (PR2910) for the +determinant model note; Cinna Davis (PR2085/2112) for the endpoint and model; +Philippe Van Velzen for the earlier eight-call floor; and their retained BIT +lineage. The contribution resolves one pending example rather than repeating +their lower bounds or claiming a literature-priority result. diff --git a/research/bit-two-use-lattice-descent/RESULT.json b/research/bit-two-use-lattice-descent/RESULT.json new file mode 100644 index 0000000000..6abfe2d50f --- /dev/null +++ b/research/bit-two-use-lattice-descent/RESULT.json @@ -0,0 +1,182 @@ +{ + "schema": "bit-two-use-lattice-descent/1", + "source_sha256": "fa3f0f951146caa5b1eb7b7417175eb7a380cae8674e4a470407517dac40f227", + "candidate": { + "profile": { + "A": 1, + "B": 3, + "P": 0, + "Q": 1, + "R": 1, + "S": 2 + }, + "lattice_basis": [ + "A", + "B", + "S=P/2" + ], + "literal_subset_count": 256, + "target_support_multiplicities": [ + 1, + 1, + 3, + 3 + ], + "joint_first_order_witness_label_role": [ + [ + "A", + 0 + ], + [ + "B", + 1 + ], + [ + "B", + 2 + ], + [ + "B", + 3 + ], + [ + "Q", + 3 + ], + [ + "R", + 0 + ], + [ + "S", + 0 + ], + [ + "S", + 0 + ] + ], + "raw_characters": [ + { + "chi": [ + 0, + 0, + 0 + ], + "calls": 0, + "target_rank": 0 + }, + { + "chi": [ + 0, + 0, + 1 + ], + "calls": 2, + "target_rank": 0 + }, + { + "chi": [ + 0, + 1, + 0 + ], + "calls": 4, + "target_rank": 2 + }, + { + "chi": [ + 0, + 1, + 1 + ], + "calls": 6, + "target_rank": 2 + }, + { + "chi": [ + 1, + 0, + 0 + ], + "calls": 2, + "target_rank": 2 + }, + { + "chi": [ + 1, + 0, + 1 + ], + "calls": 4, + "target_rank": 2 + }, + { + "chi": [ + 1, + 1, + 0 + ], + "calls": 4, + "target_rank": 4 + }, + { + "chi": [ + 1, + 1, + 1 + ], + "calls": 6, + "target_rank": 4 + } + ], + "contracted_profile": { + "A": 1, + "B": 3, + "P": 1, + "Q": 1, + "R": 1, + "S": 0 + }, + "contracted_detected_calls": 2, + "contracted_target_rank": 4 + }, + "descent_regressions": { + "complete_three_factor_censuses": [ + { + "width": 2, + "projectors": 6, + "triples": 216, + "even_endpoints": 12 + }, + { + "width": 3, + "projectors": 28, + "triples": 21952, + "even_endpoints": 196 + } + ], + "matrix_unit_block_cases": 9120, + "independent_entry_engine_triples": 216 + }, + "controls": { + "positive_endpoints_two_engines": 12, + "widths": [ + 4, + 5, + 7 + ], + "single_call_deletions_rejected": 9, + "half_frame_replacements_rejected": 2, + "other_controls": [ + "noncommuting middle", + "single odd call", + "unequal projectors", + "inverse-pair identity", + "non-idempotent", + "free-middle intertwiner", + "source mutation" + ] + }, + "scope": "Finite exact regression evidence for README's all-finite-width proof; no new kappa." +} diff --git a/research/bit-two-use-lattice-descent/SOURCES.json b/research/bit-two-use-lattice-descent/SOURCES.json new file mode 100644 index 0000000000..71e4b3eede --- /dev/null +++ b/research/bit-two-use-lattice-descent/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/bit-fifth-frame-determinant-obstruction/README.md", + "usage": "input", + "git_blob": "608a24af8bc3d27ee1554c94872601bb3a409f67", + "sha256": "fa3f0f951146caa5b1eb7b7417175eb7a380cae8674e4a470407517dac40f227" + } + ] +} diff --git a/research/bit-two-use-lattice-descent/TASK.json b/research/bit-two-use-lattice-descent/TASK.json new file mode 100644 index 0000000000..b27871636b --- /dev/null +++ b/research/bit-two-use-lattice-descent/TASK.json @@ -0,0 +1,164 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. 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": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Resolve the eight-call profile (A,B,P,Q,R,S)=(1,3,0,1,1,2), R=2A and S=P/2, in PR6111 open question 2, for any finite restored dirty width.", + "scope_change_reason": "Scoped formal-model side result: replace the generic larger/nonabelian construction task with a two-use index-two lattice descent for one concrete rational-frame candidate. No native implementation or supplier admission is claimed.", + "bottleneck_link": "A necessary-condition survivor can misdirect bit-primitive construction. Prove or falsify its realizability before attempting physical integration. Eight calls already match the direct endpoint cost, so even favorable pricing gives no new kappa.", + "budget_minutes": 120, + "stop_rule": "One candidate, no scalar-word search or frame grid. Stop discovery by 2026-10-28T15:45:34Z; reserve at least 30 minutes for verification/publication. If the descent argument fails, retain only concrete verified evidence; no unpriced supplier claim.", + "outcome": "negative-result", + "evidence": "README proves index-two two-use descent for any finite width, then excludes the exact PR6111 example by rank 2<4. RESULT.json records exact finite corroboration and controls, not a machine-checked universal theorem.", + "author": "@CubeJerry, with OpenAI Codex assistance", + "ai_assistance": "Prepared for @CubeJerry with substantial OpenAI Codex assistance; no independent human or proof-assistant review.", + "open_questions": [ + { + "question": "Which other PR6111 eight-call survivors admit a two-use index-two quotient?", + "why_it_matters": "Prune the open list before scalar-word construction.", + "first_step": "Compute each exact lattice and character, contract only with an admitted sum label, then recheck support and rank.", + "blocked_by": "Other survivors have not been analyzed in this package." + }, + { + "question": "What obstruction survives with four odd-coset calls?", + "why_it_matters": "Two-use block isolation does not extend automatically.", + "first_step": "Check a small exact four-odd-factor word with even endpoint and subdivision positive controls.", + "blocked_by": "No four-use reduction or native cost benefit has been established." + } + ], + "selection": { + "track_draw": 19, + "track": "Bit supplier", + "os_random_seed": 6854149918199383969, + "picker_nonce": "00000000000000005f1ed509278c07a1", + "candidate_index_mod_3": 1, + "candidates": [ + "Later joint-dead G20 capture: deferred because PR6117 already closes all first-read subsets and a new physical restoration bill is unresolved.", + "Two-use descent for the explicit PR6111 eight-call half-frame candidate: selected.", + "R437 pooled request/precision integration: deferred; reverse coefficient already established by PR4147." + ] + }, + "claim": { + "status": "DONE / author-checked scoped negative result", + "created_utc": "2026-10-28T14:32:35.887846+00:00", + "expires_utc": "2026-10-28T16:15:34Z", + "coordination": "No pinned sprint issue found. GitHub connector has no Discussion-write capability; locally recorded under the user fallback. Visible #1163/#1166/#1167 pages checked; no complete discussion-pagination claim.", + "method": "Normalize free binary scalar maps; descend across parity kernel when exactly two calls lie outside it; test the contracted word with an old-lattice first-order character.", + "expected_deliverable": "Self-contained proof or counterexample, exact stdlib checker with positive and negative controls, frozen context, one reproducible package.", + "updated_utc": "2026-10-28T14:54:28.722668+00:00", + "result": "The exact eight-call profile is impossible at every finite restored dirty width. Two-use descent exposes a rank-two versus rank-four contradiction. No new kappa.", + "artifact": "https://github.com/CubeJerry/integer-mult-bounds/tree/research/seed19-bit-two-use-descent-20261028-5f1ed509/research/bit-two-use-lattice-descent" + }, + "predecessors": [ + { + "pr": 6111, + "head": "961b749fa40a1117d0746064528d2dfa290c57e0", + "path": "research/bit-two-positive-frames-seven-call/README.md", + "role": "Question and candidate only; no predecessor executable or lower-bound theorem is used.", + "git_blob": "98eb6718d0ae424c129cf08b186fd2a5593ca783" + }, + { + "pr": 2910, + "role": "Canonical pinned model and determinant method." + }, + { + "pr": 6089, + "role": "Half-frame subdivision motivation and character method; its classification is not assumed." + }, + { + "pr": 1974, + "role": "Three-register M3 rational-frame census: different address dimension, endpoint and role restriction." + }, + { + "pr": 2027, + "role": "Two-register nonabelian GL3 coordinate-CNOT tariff: different alphabet and endpoint." + } + ], + "overlap": { + "checked_utc": "2026-10-28T14:32:35.887864+00:00", + "canonical_main": "721c03822c421b7f7fcbb2598993b947c4d88419", + "priority_revision": 8, + "selected_record_sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa", + "live_open_pr_snapshot_through": 6143, + "related": [ + 6111, + 6089, + 6079, + 6032, + 2910, + 2085, + 2112, + 1974, + 2027, + 800, + 6113, + 6116, + 6117 + ], + "local_overlap": "find_overlap --offline: 8348/8348 HEAD README/TASK records; no remote helper cache. Live plugin PR inspection and visible discussion pages supplement it. No exhaustive novelty claim.", + "decision": "Continue the explicitly open PR6111 profile. PR800 is a fixed Clifford-word obstruction, not this abelian dyadic alphabet; G20 and complex-word work is outside scope.", + "completion_refresh": { + "utc": "2026-10-28T14:51:40Z", + "canonical_main": "721c03822c421b7f7fcbb2598993b947c4d88419", + "priority_revision": 8, + "guidance_selected_and_catalogue": "All bytes unchanged against the base; continue with frozen inputs.", + "live_open_prs": "100 most recently updated, through PR6143; PR6111 head unchanged. Not a complete open-queue or discussion-pagination census.", + "nearby_comparison": "PR6114/6120 use even-part rank for rational p16 shears; PR6130 removes low-use dyadic source gauges. They do not establish this idempotent half-frame contraction or decide this BIT profile. No dependency on those results.", + "decision": "Complete and publish the single claimed formal-model result; no scope expansion or new research round." + } + }, + "verification": { + "environment": "CPython 3.12.14, Linux; standard library only", + "registered_command": "python3 -B scripts/research_package.py --package research/bit-two-use-lattice-descent", + "observed_result": "PASS_REGISTERED_RESEARCH_PACKAGE; normal and optimized exact checks; 7 CLI methods each in both modes (14 child checks).", + "coverage": "22168 normalized projector triples, 9120 matrix-unit block cases, all eight character equations jointly satisfiable, 12 positive endpoints at widths 4/5/7 in two engines, explicit algebraic and CLI failure controls.", + "not_claimed": [ + "proof-assistant verification", + "independent human acceptance", + "native conversion or supplier admission", + "selected supplier cold replay", + "hosted CI result" + ] + } +} diff --git a/research/bit-two-use-lattice-descent/VERIFY.json b/research/bit-two-use-lattice-descent/VERIFY.json new file mode 100644 index 0000000000..dd45a2ac7d --- /dev/null +++ b/research/bit-two-use-lattice-descent/VERIFY.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit-fifth-frame-determinant-obstruction/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact candidate filters, two-use block identities, full stated finite censuses, two polynomial engines, dirty-register positive constructions and failure controls; compare RESULT.json." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "The identical exact replay with Python assertions disabled." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-W", + "error", + "{package}/test_replay.py" + ], + "timeout_seconds": 120, + "checks": "Seven CLI test methods, each in normal and optimized mode: isolated empty-PATH source export and source, repinning, manifest, rank, profile and Boolean/integer receipt rejection." + } + ] +} diff --git a/research/bit-two-use-lattice-descent/test_replay.py b/research/bit-two-use-lattice-descent/test_replay.py new file mode 100644 index 0000000000..4413f9e48b --- /dev/null +++ b/research/bit-two-use-lattice-descent/test_replay.py @@ -0,0 +1,97 @@ +#!/usr/bin/env python3 +"""CLI failure controls in isolated source trees, normal and optimized Python. + +Prepared for @CubeJerry with OpenAI Codex assistance. Apache-2.0. +""" +from hashlib import sha256, sha1 +import json +import os +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parent.parent +SOURCE = "research/bit-fifth-frame-determinant-obstruction/README.md" + + +class ReplayControls(unittest.TestCase): + def run_case(self, mutate=None, expected_error=None): + for optimized in (False, True): + with self.subTest(optimized=optimized), tempfile.TemporaryDirectory(prefix="bit-descent-") as tmp: + root = Path(tmp) + package = root / "research" / PACKAGE.name + package.mkdir(parents=True) + for name in ("verify.py", "SOURCES.json", "RESULT.json"): + shutil.copyfile(PACKAGE / name, package / name) + source = root / SOURCE + source.parent.mkdir(parents=True) + shutil.copyfile(ROOT / SOURCE, source) + if mutate: + mutate(package, source) + before = {str(p.relative_to(root)): p.read_bytes() for p in root.rglob("*") if p.is_file()} + argv = [sys.executable, "-I", "-B", "-W", "error"] + if optimized: + argv.append("-O") + argv.append(str(package / "verify.py")) + env = dict(os.environ, PATH="", PYTHONDONTWRITEBYTECODE="1") + result = subprocess.run(argv, cwd=root, env=env, text=True, capture_output=True, timeout=60) + after = {str(p.relative_to(root)): p.read_bytes() for p in root.rglob("*") if p.is_file()} + self.assertEqual(before, after, "verification changed the exported inputs") + if expected_error is None: + self.assertEqual(result.returncode, 0, result.stderr) + self.assertIn("PASS_BIT_TWO_USE_LATTICE_DESCENT", result.stdout) + else: + self.assertNotEqual(result.returncode, 0) + self.assertIn(expected_error, result.stderr) + self.assertNotIn("PASS_BIT_TWO_USE_LATTICE_DESCENT", result.stdout) + + def test_clean_source_export(self): + self.run_case() + + def test_corrupted_source(self): + self.run_case(lambda p, s: s.write_bytes(s.read_bytes() + b"\n"), "source SHA256 mismatch") + + def test_repinned_corrupted_source(self): + def mutate(package, source): + raw = source.read_bytes() + b" altered" + source.write_bytes(raw) + path = package / "SOURCES.json" + data = json.loads(path.read_text()) + row = next(row for row in data["files"] if row["path"] == SOURCE) + row["sha256"] = sha256(raw).hexdigest() + row["git_blob"] = sha1(b"blob " + str(len(raw)).encode() + b"\0" + raw).hexdigest() + path.write_text(json.dumps(data)) + self.run_case(mutate, "source SHA256 mismatch") + + def test_manifest_pin_only(self): + def mutate(package, source): + path = package / "SOURCES.json" + data = json.loads(path.read_text()) + next(row for row in data["files"] if row["path"] == SOURCE)["git_blob"] = "0" * 40 + path.write_text(json.dumps(data)) + self.run_case(mutate, "source manifest binding mismatch") + + def test_wrong_rank_receipt(self): + self.receipt_mutation(lambda d: d["candidate"].update(contracted_target_rank=2)) + + def test_wrong_profile_receipt(self): + self.receipt_mutation(lambda d: d["candidate"]["profile"].update(S=1)) + + def test_boolean_integer_receipt(self): + self.receipt_mutation(lambda d: d["candidate"]["raw_characters"][0].update(calls=False)) + + def receipt_mutation(self, change): + def mutate(package, source): + path = package / "RESULT.json" + data = json.loads(path.read_text()) + change(data) + path.write_text(json.dumps(data)) + self.run_case(mutate, "RESULT.json differs from recomputed evidence") + + +if __name__ == "__main__": + unittest.main(verbosity=2) diff --git a/research/bit-two-use-lattice-descent/verify.py b/research/bit-two-use-lattice-descent/verify.py new file mode 100644 index 0000000000..ff8dbf673c --- /dev/null +++ b/research/bit-two-use-lattice-descent/verify.py @@ -0,0 +1,368 @@ +#!/usr/bin/env python3 +"""Exact regression evidence for the written two-use descent proof. + +Prepared for @CubeJerry with OpenAI Codex assistance. Apache-2.0. +No predecessor executable, finite-address quotient, or third-party dependency. +""" +from fractions import Fraction as F +from functools import lru_cache +from hashlib import sha256, sha1 +from itertools import product +import json +from pathlib import Path +import sys + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parent.parent +SOURCE = "research/bit-fifth-frame-determinant-obstruction/README.md" +SOURCE_SHA256 = "fa3f0f951146caa5b1eb7b7417175eb7a380cae8674e4a470407517dac40f227" +SOURCE_BLOB = "608a24af8bc3d27ee1554c94872601bb3a409f67" +ZERO = (0, 0, 0) +LABELS = {"A": (1, 0, 0), "B": (0, 1, 0), "P": (0, 0, 2), + "Q": (1, 1, -2), "R": (2, 0, 0), "S": (0, 0, 1)} +PROFILE = {"A": 1, "B": 3, "P": 0, "Q": 1, "R": 1, "S": 2} +TARGETS = [(1, 0, 2), (2, 1, -2), (0, 1, 2), (1, 2, -2)] + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def add(a, b): + return tuple(x + y for x, y in zip(a, b)) + + +def unit(w): + return sum(1 << (i * w + i) for i in range(w)) + + +@lru_cache(maxsize=65536) +def mul_bits(a, b, w): + """Row-packed binary multiplication, used only by the coefficient engine.""" + out = 0 + mask = (1 << w) - 1 + for i in range(w): + row = (a >> (i * w)) & mask + value = 0 + while row: + bit = row & -row + value ^= (b >> ((bit.bit_length() - 1) * w)) & mask + row ^= bit + out |= value << (i * w) + return out + + +def projectors(w): + return [sum(((v if (u >> i) & 1 else 0) << (i * w)) for i in range(w)) + for u in range(1, 1 << w) for v in range(1, 1 << w) + if (u & v).bit_count() % 2] + + +def plus(*matrices): + out = {} + for matrix in matrices: + for exponent, coefficient in matrix.items(): + out[exponent] = out.get(exponent, 0) ^ coefficient + return {e: c for e, c in out.items() if c} + + +def times(a, b, w): + out = {} + for e, c in a.items(): + for f, d in b.items(): + g = add(e, f) + out[g] = out.get(g, 0) ^ mul_bits(c, d, w) + return {e: c for e, c in out.items() if c} + + +def call(e, n, w): + return plus({ZERO: unit(w) ^ n}, {e: n}) + + +def word(factors, w): + out = {ZERO: unit(w)} + for factor in factors: + out = times(out, factor, w) + return out + + +def endpoint(w): + out = {} + for i in range(w): + e = TARGETS[i] if i < 4 else ZERO + out[e] = out.get(e, 0) ^ (1 << (i * w + i)) + return out + + +def entry_engine(factors, w): + """Independent entry-wise sets of monomials; no packed multiplication.""" + state = [[{ZERO} if i == j else set() for j in range(w)] for i in range(w)] + for factor in factors: + right = [[{e for e, c in factor.items() if (c >> (i * w + j)) & 1} + for j in range(w)] for i in range(w)] + nxt = [[set() for _ in range(w)] for _ in range(w)] + for i in range(w): + for j in range(w): + for k in range(w): + for a in state[i][k]: + for b in right[k][j]: + term = (a[0] + b[0], a[1] + b[1], a[2] + b[2]) + if term in nxt[i][j]: + nxt[i][j].remove(term) + else: + nxt[i][j].add(term) + state = nxt + return {e: sum((1 << (i * w + j)) for i in range(w) for j in range(w) + if e in state[i][j]) + for row in state for entry in row for e in entry} + + +def odd_part(matrix): + return {e: c for e, c in matrix.items() if e[2] % 2} + + +def authenticate_bytes(data): + require(sha256(data).hexdigest() == SOURCE_SHA256, "source SHA256 mismatch") + header = b"blob " + str(len(data)).encode() + b"\0" + require(sha1(header + data).hexdigest() == SOURCE_BLOB, "source Git blob mismatch") + + +def check_source(): + authenticate_bytes((ROOT / SOURCE).read_bytes()) + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + rows = [row for row in manifest["files"] if row["path"] == SOURCE] + require(len(rows) == 1 and rows[0]["usage"] == "input" + and rows[0]["sha256"] == SOURCE_SHA256 and rows[0]["git_blob"] == SOURCE_BLOB, + "source manifest binding mismatch") + + +def rejection(action, message): + try: + action() + except ValueError: + return + raise ValueError("negative control was accepted: " + message) + + +def frame(e): + # Independent rational-matrix realization in the basis A, B, S=P/2. + a, b, s = e + return (F(a) + F(s, 4), F(s, 4), F(s, 4), F(b) + F(s, 4)) + + +def sum_frames(frames): + frames = list(frames) + return tuple(sum(row[i] for row in frames) for i in range(4)) + + +def rank(rows): + basis = {} + for row in rows: + while row: + pivot = row.bit_length() - 1 + if pivot in basis: + row ^= basis[pivot] + else: + basis[pivot] = row + break + return len(basis) + + +def candidate_checks(): + for e in LABELS.values(): + a, b, c, d = frame(e) + require(a * d == b * c and a + d > 0 and a >= 0 and d >= 0, + "paid frame is not positive rank one") + labels = [LABELS[name] for name, count in PROFILE.items() for _ in range(count)] + require(len(labels) == 8, "wrong candidate length") + require(sum_frames(map(frame, labels)) == sum_frames(map(frame, TARGETS)) + == (F(4), F(0), F(0), F(4)), "determinant sum mismatch") + require(tuple(sum(e[j] for e in labels) for j in range(3)) + == tuple(sum(t[j] for t in TARGETS) for j in range(3)) == (4, 4, 0), + "integer-lattice determinant sum mismatch") + # Compare literal 2^8 rational-matrix subset expansion with bounded lattice counts. + literal = [] + for mask in range(1 << len(labels)): + literal.append(sum_frames([frame(e) for i, e in enumerate(labels) if (mask >> i) & 1])) + support_counts = [literal.count(frame(t)) for t in TARGETS] + require(all(support_counts), "candidate does not pass the support condition") + lattice_sums = set() + for counts in product(*(range(n + 1) for n in PROFILE.values())): + lattice_sums.add(tuple(sum(c * LABELS[name][j] for name, c in zip(PROFILE, counts)) + for j in range(3))) + require(all(t in lattice_sums for t in TARGETS), "lattice support disagrees") + characters = [] + for chi in product(range(2), repeat=3): + value = lambda e: sum(x * y for x, y in zip(chi, e)) % 2 + paid = sum(map(value, labels)) + target = sum(map(value, TARGETS)) + require(paid >= target, "raw lattice character already excludes candidate") + characters.append({"chi": list(chi), "calls": paid, "target_rank": target}) + # A single projector assignment satisfies ALL raw first-order matrix + # equations jointly, not just their separate rank inequalities. + linear_witness = [("A", 0), ("B", 1), ("B", 2), ("B", 3), + ("Q", 3), ("R", 0), ("S", 0), ("S", 0)] + for chi in product(range(2), repeat=3): + derivative = 0 + for name, role in linear_witness: + if sum(x * y for x, y in zip(chi, LABELS[name])) % 2: + derivative ^= 1 << (role * 4 + role) + target = sum((sum(x * y for x, y in zip(chi, e)) % 2) << (i * 4 + i) + for i, e in enumerate(TARGETS)) + require(derivative == target, "joint first-order witness failed") + linear_factors = [call(LABELS[name], 1 << (role * 4 + role), 4) + for name, role in linear_witness] + require(word(linear_factors, 4) == entry_engine(linear_factors, 4) != endpoint(4), + "first-order witness must not be an exact construction") + # Descent removes the two S factors and adds one P. H uses A,B,P as its basis. + contracted = dict(PROFILE, P=1, S=0) + contracted_labels = [LABELS[name] for name, count in contracted.items() for _ in range(count)] + require(all(e[2] % 2 == 0 for e in contracted_labels + TARGETS), "descent not in H") + detected = sum((e[2] // 2) % 2 for e in contracted_labels) + target_derivative = [((t[2] // 2) % 2) << i for i, t in enumerate(TARGETS)] + require(detected == 2 and rank(target_derivative) == 4, "descent rank gap lost") + require(all(e[2] % 2 == 0 for name, e in LABELS.items() if name != "S") + and all(t[2] % 2 == 0 for t in TARGETS), "index-two premise fails") + return {"profile": PROFILE, "lattice_basis": ["A", "B", "S=P/2"], + "literal_subset_count": len(literal), "target_support_multiplicities": support_counts, + "joint_first_order_witness_label_role": linear_witness, + "raw_characters": characters, "contracted_profile": contracted, + "contracted_detected_calls": detected, "contracted_target_rank": 4} + + +def descent_regressions(): + census = [] + for w in (2, 3): + ps = projectors(w) + require(len(set(ps)) == ((1 << w) - 1) * (1 << (w - 1)), "projector count") + for n in ps: + require(mul_bits(n, n, w) == n, "projector not idempotent") + even_endpoints = checked = 0 + for first, middle, last in product(ps, repeat=3): + factors = [call((0, 0, 1), first, w), call((0, 0, 2), middle, w), + call((0, 0, 1), last, w)] + result = word(factors, w) + if w == 2: + require(result == entry_engine(factors, w), "independent engine mismatch") + expected = first == last and mul_bits(first, middle, w) == mul_bits(middle, first, w) + require((not odd_part(result)) == expected, "two-use criterion mismatch") + if expected: + fused = word([factors[1], call((0, 0, 2), first, w)], w) + require(result == fused, "contraction changed endpoint") + even_endpoints += 1 + checked += 1 + census.append({"width": w, "projectors": len(ps), "triples": checked, + "even_endpoints": even_endpoints}) + # Arbitrary middle matrix: test the stronger P M = M Q intertwiner lemma. + # These finite matrix-unit regressions are not a proof for arbitrary width. + block_cases = 0 + for w in (2, 3, 4): + ps = projectors(w) + pairs = product(ps, repeat=2) if w < 4 else ((n, n) for n in ps) + for p, q in pairs: + c, d = unit(w) ^ p, unit(w) ^ q + for ij in range(w * w): + m = 1 << ij + middle = {(0, 0, 2): m} + actual = word([call((0, 0, -3), p, w), middle, + call((0, 0, 5), q, w)], w) + cmq = mul_bits(mul_bits(c, m, w), q, w) + pmd = mul_bits(mul_bits(p, m, w), d, w) + expanded = plus({(0, 0, 2): mul_bits(mul_bits(c, m, w), d, w)}, + {(0, 0, 7): cmq}, {(0, 0, -1): pmd}, + {(0, 0, 4): mul_bits(mul_bits(p, m, w), q, w)}) + require(actual == expanded, "Peirce block expansion mismatch") + require((not odd_part(actual)) == (cmq == 0 and pmd == 0), + "cross blocks failed to isolate") + if not odd_part(actual): + require(mul_bits(p, m, w) == mul_bits(m, q, w), "intertwiner failed") + require(actual == word([middle, call((0, 0, 2), q, w)], w), + "general contraction failed") + block_cases += 1 + return {"complete_three_factor_censuses": census, "matrix_unit_block_cases": block_cases, + "independent_entry_engine_triples": 216} + + +def construction_controls(): + direct = [("A", 0), ("P", 0), ("A", 1), ("Q", 1), + ("B", 2), ("P", 2), ("B", 3), ("Q", 3)] + divided = [("A", 0), ("S", 0), ("B", 2), ("S", 0), ("A", 1), + ("Q", 1), ("P", 2), ("B", 3), ("Q", 3)] + positives = 0 + for w in (4, 5, 7): + for pattern in (direct, divided): + factors = [call(LABELS[label], 1 << (role * w + role), w) for label, role in pattern] + expected = endpoint(w) + require(word(factors, w) == expected == entry_engine(factors, w), "positive endpoint") + positives += 1 + # At w>4, the temporary scalar mixing uses dirty role w-1. + mixed = [] + for label, role in pattern: + other = w - 1 if w > 4 else (role + 1) % w + g = unit(w) ^ (1 << (other * w + role)) + n = mul_bits(mul_bits(g, 1 << (role * w + role), w), g, w) + mixed.extend([{ZERO: g}, call(LABELS[label], n, w), {ZERO: g}]) + require(word(mixed, w) == expected == entry_engine(mixed, w), "free-mixing endpoint") + positives += 1 + w = 2 + n, k = 1, 3 + bad = [call((0, 0, 1), n, w), call((0, 0, 2), k, w), call((0, 0, 1), n, w)] + require(bool(odd_part(word(bad, w))), "noncommuting middle escaped detection") + require(word(bad, w) != word([bad[1], call((0, 0, 2), n, w)], w), "bad contraction accepted") + require(bool(odd_part(word([bad[0]], w))), "single odd call escaped detection") + unequal = [call((0, 0, 1), 1, w), call((0, 0, 1), 8, w)] + require(bool(odd_part(word(unequal, w))), "unequal projectors escaped detection") + require(word([call((0, 0, -1), n, w), call((0, 0, 1), n, w)], w) + == {ZERO: unit(w)}, "inverse pair failed") + nonprojector = 2 + require(word([call((0, 0, 1), nonprojector, w)] * 2, w) + != call((0, 0, 2), nonprojector, w), "idempotence negative control") + # Equal projectors are required only after normalization: a free middle + # map can intertwine different projectors while preserving contraction. + g = unit(w) ^ 4 + p = mul_bits(mul_bits(g, n, w), g, w) + require(p != n, "free-middle fixture is trivial") + free_middle = [call((0, 0, 1), p, w), {ZERO: g}, call((0, 0, 1), n, w)] + require(not odd_part(word(free_middle, w)), "free-middle parity") + require(word(free_middle, w) == word([{ZERO: g}, call((0, 0, 2), n, w)], w) + == entry_engine(free_middle, w), "free-middle contraction") + w = 5 + factors = [call(LABELS[label], 1 << (role * w + role), w) for label, role in divided] + for i in range(len(factors)): + require(word(factors[:i] + factors[i+1:], w) != endpoint(w), "deleted call accepted") + for i, (label, role) in enumerate(divided): + if label == "S": + altered = factors[:] + altered[i] = call(LABELS["P"], 1 << (role * w + role), w) + require(word(altered, w) != endpoint(w), "half-frame mutation accepted") + rejection(lambda: authenticate_bytes((ROOT / SOURCE).read_bytes() + b"\n"), "source mutation") + return {"positive_endpoints_two_engines": positives, "widths": [4, 5, 7], + "single_call_deletions_rejected": 9, "half_frame_replacements_rejected": 2, + "other_controls": ["noncommuting middle", "single odd call", "unequal projectors", + "inverse-pair identity", "non-idempotent", "free-middle intertwiner", + "source mutation"]} + + +def compute(): + check_source() + return {"schema": "bit-two-use-lattice-descent/1", "source_sha256": SOURCE_SHA256, + "candidate": candidate_checks(), "descent_regressions": descent_regressions(), + "controls": construction_controls(), + "scope": "Finite exact regression evidence for README's all-finite-width proof; no new kappa."} + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":"), allow_nan=False) + + +def main(): + require(len(sys.argv) == 1, "no arguments accepted; verification never regenerates evidence") + actual = compute() + expected = json.loads((PACKAGE / "RESULT.json").read_text()) + require(canonical(actual) == canonical(expected), "RESULT.json differs from recomputed evidence") + print("PASS_BIT_TWO_USE_LATTICE_DESCENT profile=1,3,0,1,1,2 raw_characters=8 descent_rank=2<4") + + +if __name__ == "__main__": + main()