diff --git a/research/bit-single-scaled-frame-floor/README.md b/research/bit-single-scaled-frame-floor/README.md new file mode 100644 index 0000000000..826e8e4e7a --- /dev/null +++ b/research/bit-single-scaled-frame-floor/README.md @@ -0,0 +1,257 @@ +# One arbitrary scaled rank-one frame still needs eight calls + +**Scoped proof.** For the four-target endpoint of PR2085, adding any one +symmetric rational rank-one address matrix does not reduce the minimum below +**eight paid calls**. This includes arbitrary signed rational scaling and any +finite number of additional dirty roles, provided those roles are exactly +restored. Free mixing is address-independent and binary. This settles the +one-added-frame part of PR6032's scaled-frame question; two added frames remain +outside the theorem. + +The proof combines the determinant method already used in PR2910 with +exponent support and first-order rank constraints. The new part is the +all-scalings reduction: every hypothetical word of at most seven calls reduces +to four doubled-axis count profiles, and each has rank capacity two where the +target needs four. There is no native supplier, paid-profile improvement, or +new multiplication bound here. The selected result is unchanged. + +## Exact model and theorem + +Write rational symmetric 2-by-2 matrices as addresses, with + +``` +A = [[1,0],[0,0]] B = [[0,0],[0,1]] +P = (1/2)[[1,1],[1,1]] Q = (1/2)[[1,-1],[-1,1]]. +``` + +Thus `Q=A+B-P`; each old address has trace one. Fix one nonzero symmetric +rational rank-one matrix `R`. Equivalently, `R=c vv^T` for nonzero rational +`c` and rational vector `v`; neither sign nor normalization is restricted. +Let `Lambda` be the additive subgroup of `Sym_2(Q)` generated by these five +addresses. In the commutative group algebra `F_2[Lambda]`, `[F][G]=[F+G]` and +`[0]=1`; distinct addresses remain distinct formal monomials. + +For any finite `w>=4`, a paid call is + +``` +D_N(F) = I_w + ([F]-1)N, +F in {A,B,P,Q,R}, N in M_w(F_2), rank N=1, N^2=N. +``` + +Arbitrary interspersed matrices in `GL_w(F_2)` are free. They cannot depend on +addresses. Every role starts arbitrary (no clean auxiliary assumption). The +required endpoint on all roles is + +``` +T_w = diag([A+P], [A+Q], [B+P], [B+Q], 1, ..., 1). +``` + +**Theorem.** Every exact finite word for `T_w` uses at least eight paid calls, +and eight suffice, for every such `R` and `w`. Allowing `R=0` as a redundant +identity call also leaves the minimum eight. Inverse old addresses are not +extra free or paid labels; a negative `R` is permitted only as that one label. +The theorem does not assert that every exact word has length eight. + +## Proof + +### 1. Normalize mixing and take the determinant + +Each paid factor augments to `I_w` under `[F] -> 1`. The target does too, so the +product of all free binary matrices is `I_w`. Move the free matrices to one end +by conjugating paid projectors. Conjugation preserves rank, idempotence and +address labels; the residual free product is identity. It is therefore enough +to study a product of the specified paid factors. + +A rank-one idempotent is conjugate over `F_2` to `diag(1,0,...,0)`, so +`det D_N(F)=[F]`. Binary invertible matrices have determinant one. If the +multiplicities are `(a,b,p,q,r)`, an exact word consequently satisfies + +``` +a A + b B + p P + q Q + r R = 4 I_2. (1) +``` + +This is equality of rational matrices, since the formal monomials are +independent. If `r=0`, taking traces gives exactly eight calls. Zero-address +calls can simply be deleted, giving the same lower bound when `R=0`. + +Suppose for contradiction that `k=a+b+p+q+r<=7` and `r>=1`. Put +`n=a+b+p+q`, `d=a-b`, `e=p-q`. Equation (1) gives + +``` +2 r R = [[8-n-d, -e], [-e, 8-n+d]], +d^2 + e^2 = (8-n)^2. (2) +``` + +Nonnegative counts give `|d|+|e|<=n`. Hence `8-n<=n`, so `4<=n<=6`. +For radii `8-n=4,3,2`, the integer circle in (2) has only axial points. +Substitution back into (2) gives + +``` +r R = (8-n) F, F in {A,B,P,Q}, 1<=r<=7-n. +``` + +In particular every candidate is `R=sF` with `s>1`. The possible scales are +`4,3,2,3/2,4/3`. This conclusion was derived without assuming that `R` is +positive or aligned. It eliminates every negative or off-axis `R` from a +word of at most seven calls. The exact finite enumeration finds 40 count +profiles, with 20 distinct matrices `R`. + +### 2. Exponent support leaves four profiles + +Expanding the normalized word, every monomial exponent is a subset sum of +its paid addresses; cancellations may remove exponents but cannot create a +new one. Thus each of the four required diagonal exponents must have a +nonnegative integral representation using the available label counts. + +Every target exponent has trace two and rank two. No such representation +can contain `R=sF` with `s>1`: if an old label is also used, the trace exceeds +two; if only copies of `R` are used, the sum has rank at most one. Without +`R`, trace two forces exactly two old labels. Comparing the ten unordered +old pairs shows that each target has its unique named pair. Consequently +`a,b,p,q>=1`. + +It follows that `|d|+|e|<=n-4`. Combined with (2), this gives `8-n<=n-4`, +so `n=6`. Now `r=1`, and the only remaining profiles are + +| R | a | b | p | q | r | +|---|---:|---:|---:|---:|---:| +| 2A | 1 | 3 | 1 | 1 | 1 | +| 2B | 3 | 1 | 1 | 1 | 1 | +| 2P | 1 | 1 | 1 | 3 | 1 | +| 2Q | 1 | 1 | 3 | 1 | 1 | + +### 3. First-order rank excludes those profiles at every width + +For these four cases `R=2F`, the address lattice is exactly +`Lambda_0=ZA+ZB+ZP`, a free rank-three group, and `R` is zero modulo +`2 Lambda_0`. Map its group algebra to the square-zero algebra with variables +`x_A,x_B,x_P`, where all products of variables vanish, by sending a monomial +with coordinates `(u,v,z)` to `1+(u mod2)x_A+(v mod2)x_B+(z mod2)x_P`. +This is a ring homomorphism. In particular `Q` contributes to all three +variables, while `R` contributes zero. + +Let `S_F` be the sum over `F`-labelled call projectors. The first-order +coefficient equations of the exact word are + +``` +S_A + S_Q = diag(1,0,0,1,0,...,0), +S_B + S_Q = diag(0,1,1,0,0,...,0), +S_P + S_Q = D, D=diag(1,1,1,1,0,...,0). +``` + +Adding the first two also gives `S_A+S_B=D`. If `R=2A` or `2B`, the counts +of `P` and `Q` are one each, so `rank(S_P+S_Q)<=2`. If `R=2P` or `2Q`, the +counts of `A` and `B` are one each, so `rank(S_A+S_B)<=2`. Both contradict +`rank D=4`. This argument holds for every finite `w`; it does not enumerate +projectors or assume that auxiliary roles are untouched between calls. + +### 4. Attainment + +On active role 1 use `A,P`; on role 2 use `A,Q`; on role 3 use `B,P`; on +role 4 use `B,Q`. Use its coordinate projector for each call. The two calls +on a role multiply to the monomial at the sum of their addresses; all other +roles are unchanged. This is an eight-call identity for every `w` and every +choice of `R`, because it does not use the added label. + +Signed scales do permit longer words: after this construction, an `A` call +and an `R=-A` call on the same projector multiply to identity. Thus a +10-call exact word may use the extra frame. The minimum, rather than +prohibition of all extra-frame uses, is what was proved. + +## Reproduction and evidence + +Python 3.12, standard library only. The registered runner validates source +and task metadata and executes both ordinary and optimized modes: + +```sh +python3.12 -B scripts/research_package.py --package research/bit-single-scaled-frame-floor +python3.12 -I -W error -B research/bit-single-scaled-frame-floor/verify.py +python3.12 -I -O -W error -B research/bit-single-scaled-frame-floor/verify.py +``` + +`verify.py` authenticates the three live predecessor READMEs, verifies the +integer-circle reduction and unique old-pair supports, and loads the literal +bytes of `independent.py` without a bytecode-cache import. The independent +checker derives `R` from all 462 nonnegative multiplicity profiles with +`r>=1` and total count at most seven. It obtains 40 determinant candidates, +20 frames, 160 target-support checks, four survivors, and four rank-two +versus rank-four certificates. It does not assume axis alignment in advance. + +Literal group-algebra multiplication verifies six direct/free-conjugated +attaining words at widths 4, 5 and 7, including non-coordinate projectors and transient writes to dirty roles; +49 dropped-factor, doubled-address and non-idempotent mutations are rejected. +Additional controls check longer words for `R=-A` and `R=A/2`, a broken +negative loop, a failure to restore an extra dirty role, and two hand-computed products of +noncommuting projectors that distinguish reversed multiplication. These finite +fixtures test the code and hypotheses. The universal result is the proof +above, not an exhaustive search over rational frames or role widths. + +Local evidence: CPython 3.12.14, macOS arm64; normal and optimized replay. +No native conversion, addition invoice, all-size multiplication theorem, +formal-kernel proof, or new selected-frontier cold replay is supplied. + +## Task, overlap and source context + +Base `721c03822c421b7f7fcbb2598993b947c4d88419`, priority revision 8. +Task `bit-new-register-model`, scope key `7084092dd726e7ba1f2f`; the full +original catalogue card is retained in [TASK.json](TASK.json). +**Scope changed:** the user selected PR6032's one-scaled-frame handoff, +so this is a formal alphabet barrier for its four-target endpoint, rather +than a native larger/nonabelian supplier construction. It identifies a +specific extension that cannot save a call; no κ implication is asserted. +The selected-record binding orientation passed at this same base; that is +not a scientific replay of the selected construction. + +Canonical claim/status: +[handoff reply](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19233747). +Live all-state PR searches on 2026-10-28 for `6032`, `scaled frame eight` +and `rank-one 2910` found the predecessors below and no general one-scaled-frame +successor. The offline overlap helper searched only 18 local note records +out of 8,348 at HEAD, with no usable cached remote snapshot. These searches +are not a novelty certificate; sparse files and unpublished work remain +coverage gaps. The inspected handoff and nearest merged results determine +this bounded scope. + +| Predecessor | Inspected head | Role here | +|---|---|---| +| [PR2085](https://github.com/CrocSwap/integer-mult-bounds/pull/2085) | `5302b9bad6345413a0cabb0afd926d84e44c12e3` | Four-target model and augmentation method | +| [PR2910](https://github.com/CrocSwap/integer-mult-bounds/pull/2910) | `26ce4ed46112438b237fab54e6da1953c1d16174` | Earlier determinant obstruction for the fixed t=1/2 frame, including dirty workspace | +| [PR6032](https://github.com/CrocSwap/integer-mult-bounds/pull/6032) | `3b098803eb854afbd5d63ad3bf4d75cdb1e515d5` | Every normalized rational-slope frame, support method, and scaled-frame next question | + +[SOURCES.json](SOURCES.json) pins their canonical README bytes at the base. +No predecessor executable is imported, and no finite predecessor census is +needed for the zero-extra-call case: determinant trace already gives eight. +PR2910 had settled the fixed `t=1/2` case before PR6032; it is not a new +conclusion of this package. + +## Open next questions + +Structured relevance, first steps and blockers are in [TASK.json](TASK.json). + +1. **Can two added rational rank-one frames beat eight for this endpoint?** + Start with the joint determinant equation and simultaneous exponent-support + constraints for at most seven calls, then test surviving first-order + equations. This is the remaining alphabet extension explicitly suggested + in PR6032. A candidate still needs an exact word and a fully charged native + implementation before it can contribute to the multiplication bound. +2. **Which positive rank-one frames can occur in any exact word, at any + length?** The present proof excludes savings, not all uses. Start from + equation (1) and the support/rank constraints without the seven-call cap; + distinguish reciprocal old-frame subdivisions (which have explicit longer + words) from off-axis frames. An all-length classification is not proved + or certified here. + +## Credit and license + +Prepared by **apoursh**, with substantial OpenAI Codex assistance in proof, +implementation and separate adversarial proof/code audits. These are agent +audits, not independent human or formal-kernel acceptance. Apache-2.0. + +Cinna Davis's PR2085/2112 supplies the endpoint, four-register/fifth-frame +investigations and augmentation lineage. Nick Petalas's PR2910 supplies the +earlier determinant obstruction; PR6032 supplies the all-rational normalized +family and scaled-frame handoff. Credit also Philippe Van Velzen's earlier +fixed-frame argument, as retained in PR2910 and +[Discussion2091](https://github.com/CrocSwap/integer-mult-bounds/discussions/2091#discussioncomment-18935374), +and the retained BIT precursor lineage. The determinant lemma, subset-support +necessity and first-order technique are inherited methods, not new claims. diff --git a/research/bit-single-scaled-frame-floor/SOURCES.json b/research/bit-single-scaled-frame-floor/SOURCES.json new file mode 100644 index 0000000000..784c2b1ace --- /dev/null +++ b/research/bit-single-scaled-frame-floor/SOURCES.json @@ -0,0 +1,36 @@ +{ + "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" + }, + { + "path": "research/bit-fifth-rational-frame-every-rational-t/README.md", + "usage": "input", + "git_blob": "a7c6b3a06b8f215b983536934bb37cd6a0324945", + "sha256": "90ba9a56a928c4dc44fa771413e0356ea2ab05979b5cd91f14aa5ed2eeaafe3e" + }, + { + "path": "research/bit-four-register-rational-frame-floor-seed3573e12e/README.md", + "usage": "input", + "git_blob": "32f600d6cb56c94f931a4dc98fb97573ecc134f7", + "sha256": "40cbc4ec8e5c49930d7cb8ecf9e462a08266fe604ea426aa5c7b0d5e547fdffd" + } + ] +} diff --git a/research/bit-single-scaled-frame-floor/TASK.json b/research/bit-single-scaled-frame-floor/TASK.json new file mode 100644 index 0000000000..121c332625 --- /dev/null +++ b/research/bit-single-scaled-frame-floor/TASK.json @@ -0,0 +1,72 @@ +{ + "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": "Prove the exact eight-call minimum for the PR2085 four-target endpoint after adding one arbitrary symmetric rational rank-one address, including signed scaling and any finite number of restored dirty roles with free address-independent binary mixing.", + "scope_change_reason": "Explicit user-selected follow-up to PR6032 Open next questions. This is a scoped formal alphabet barrier, not the original card's larger/nonabelian native supplier construction. It removes one proposed escape without claiming a paid supplier or kappa gain.", + "bottleneck_link": "Side result: one scaled rank-one extension cannot improve the eight-call formal primitive. Two-frame alphabets or changed endpoints remain possible; native implementation and complete paid invoices are separate obligations.", + "budget_minutes": 60, + "stop_rule": "Stop after a self-contained proof, independent exact count/support/rank verification, meaningful controls and one focused package; stop earlier if a gap invalidates the theorem. Do not launch broader word searches.", + "outcome": "completed", + "evidence": "README.md gives the arbitrary-R/all-finite-width proof. verify.py and independent.py check 462 count profiles, 40 determinant candidates/20 frames, 160 support conditions, four survivors/four rank obstructions, six exact words at widths 4/5/7, 49 rejected mutations, two longer-word witnesses and three additional failure controls and two hand-computed noncommuting products. Source hashes and normal/optimized registered replay are checked. Universal claims rest on the proof, not finite fixtures.", + "author": "apoursh", + "ai_assistance": "Substantial OpenAI Codex assistance in proof, code, source review and separate agent proof/code audits; no independent human or formal-kernel acceptance claimed.", + "open_questions": [ + { + "question": "Can two added rational rank-one frames beat eight calls for the same endpoint?", + "why_it_matters": "This is the next alphabet extension suggested by PR6032 and is not excluded by the one-frame theorem.", + "first_step": "Use the joint determinant equation and target-support constraints for at most seven calls; test the first-order equations only for surviving multiplicities.", + "blocked_by": "No joint universal classification or exact saving word is supplied. Native implementation and a full paid invoice are required before any multiplication-bound use." + }, + { + "question": "Which positive rank-one frames can occur in exact words of arbitrary length?", + "why_it_matters": "The minimum-eight theorem does not classify all possible extra-frame use; reciprocal old-frame subdivisions have explicit longer words.", + "first_step": "Remove the seven-call cap from the determinant/support/rank argument and classify positive frames, beginning with reciprocal old-frame subdivisions.", + "blocked_by": "An all-length classification and its certificate are not provided in this package." + } + ], + "coordination_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19233747", + "scope_key": "7084092dd726e7ba1f2f" +} diff --git a/research/bit-single-scaled-frame-floor/VERIFY.json b/research/bit-single-scaled-frame-floor/VERIFY.json new file mode 100644 index 0000000000..af6f961ba8 --- /dev/null +++ b/research/bit-single-scaled-frame-floor/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit-fifth-frame-determinant-obstruction/README.md", + "research/bit-fifth-rational-frame-every-rational-t/README.md", + "research/bit-four-register-rational-frame-floor-seed3573e12e/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Source hashes; integer-circle and pair-support reductions; independent exact multiplicity/support/rank certificate; full group-algebra words and semantic failure controls. No assertions or predecessor executable imports." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Source hashes; integer-circle and pair-support reductions; independent exact multiplicity/support/rank certificate; full group-algebra words and semantic failure controls. No assertions or predecessor executable imports." + } + ] +} diff --git a/research/bit-single-scaled-frame-floor/independent.py b/research/bit-single-scaled-frame-floor/independent.py new file mode 100644 index 0000000000..9907b37f64 --- /dev/null +++ b/research/bit-single-scaled-frame-floor/independent.py @@ -0,0 +1,268 @@ +"""Independent exact certificate for one extra symmetric rank-one address. + +No predecessor executable is imported. Rational matrix entries determine the +finite determinant candidates before any alignment assumption. Group-algebra +coefficients are binary matrices; literal paid-factor multiplication checks the +attaining word at selected dirty-role widths and with free basis changes. +Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0. +""" +from fractions import Fraction as Q +from itertools import product + +A = (Q(1), Q(0), Q(0)) +B = (Q(0), Q(1), Q(0)) +P = (Q(1, 2), Q(1, 2), Q(1, 2)) +QFRAME = (Q(1, 2), Q(1, 2), Q(-1, 2)) +OLD = (A, B, P, QFRAME) +ZERO = (Q(0),) * 3 +TOTAL = (Q(4), Q(4), Q(0)) + + +def need(value, message): + if not value: + raise ValueError(message) + + +def add(*frames): + return tuple(sum(frame[j] for frame in frames) for j in range(3)) + + +def scale(c, frame): + return tuple(c * x for x in frame) + + +TARGETS = (add(A, P), add(A, QFRAME), add(B, P), add(B, QFRAME)) + + +def det(frame): + x, y, z = frame + return x * y - z * z + + +def enumerate_candidates(): + """All nonnegative five-label counts <=7 with the new label used. + + Derive the putative new address directly from the determinant identity. + Symmetric 2x2 rank-one is exactly nonzero matrix and determinant zero; + signs, slopes and scaling are not restricted in this candidate filter. + """ + candidates, visited = [], 0 + for old_counts in product(range(8), repeat=4): + for r in range(1, 8 - sum(old_counts)): + visited += 1 + remaining = add(TOTAL, *(scale(-n, frame) for n, frame in zip(old_counts, OLD))) + frame = scale(Q(1, r), remaining) + if frame != ZERO and det(frame) == 0: + candidates.append((old_counts + (r,), frame)) + need(visited == 462, 'count-domain coverage') + need(len(candidates) == 40, 'forty determinant-compatible count profiles') + need(len({frame for _, frame in candidates}) == 20, 'twenty derived frames') + expected_frames = {scale(c, f) for f in OLD for c in (Q(4), Q(3), Q(2), Q(3, 2), Q(4, 3))} + need({frame for _, frame in candidates} == expected_frames, 'derived frame set') + for counts, frame in candidates: + need(add(*(scale(n, f) for n, f in zip(counts, OLD + (frame,)))) == TOTAL, + 'literal determinant equation') + return candidates, visited + + +def representations(target, frames, bounds): + return [powers for powers in product(*(range(n + 1) for n in bounds)) + if add(*(scale(n, f) for n, f in zip(powers, frames))) == target] + + +def old_coordinates(frame): + x, y, z = frame + return x - z, y - z, 2 * z + + +def parity(value): + need(value.denominator == 1, 'integral old-lattice coordinate required') + return int(value) % 2 + + +def support_and_rank(candidates): + survivors, decisions = [], 0 + representations_with_extra = 0 + for counts, frame in candidates: + supports = [representations(t, OLD + (frame,), counts) for t in TARGETS] + decisions += len(supports) + representations_with_extra += sum(n[-1] > 0 for rows in supports for n in rows) + if all(supports): + survivors.append((counts, frame)) + need(representations_with_extra == 0, 'no target representation may use extra frame') + need(len(survivors) == 4, 'four support-compatible profiles') + expected = {((1, 3, 1, 1, 1), scale(2, A)), + ((3, 1, 1, 1, 1), scale(2, B)), + ((1, 1, 1, 3, 1), scale(2, P)), + ((1, 1, 3, 1, 1), scale(2, QFRAME))} + need(set(survivors) == expected, 'residual count identities') + witnesses = [] + for counts, frame in survivors: + label_parities = [tuple(map(parity, old_coordinates(f))) for f in OLD + (frame,)] + target_parities = [tuple(map(parity, old_coordinates(t))) for t in TARGETS] + need(label_parities[-1] == (0, 0, 0), 'doubled frame vanishes to first order') + found = [] + for functional in product(range(2), repeat=3): + label_bits = [sum(a*b for a,b in zip(functional, f)) % 2 for f in label_parities] + target_bits = [sum(a*b for a,b in zip(functional, t)) % 2 for t in target_parities] + available_rank = sum(n*b for n,b in zip(counts, label_bits)) + needed_rank = sum(target_bits) + if needed_rank > available_rank: + found.append((functional, available_rank, needed_rank)) + need(any(cap == 2 and rank == 4 for _, cap, rank in found), 'rank-two versus rank-four certificate') + witnesses.append((counts, found)) + return survivors, decisions, witnesses + + +# Binary matrices are tuples of row bit masks, with bit j indicating column j. +def eye(n): + return tuple(1 << j for j in range(n)) + + +def bxor(a, b): + return tuple(x ^ y for x, y in zip(a, b)) + + +def bmul(a, b): + out = [] + for row in a: + result = 0 + for j in range(len(b)): + if row >> j & 1: + result ^= b[j] + out.append(result) + return tuple(out) + + +def brank(matrix): + pivots = {} + for original in matrix: + row = original + while row: + j = row.bit_length() - 1 + if j in pivots: + row ^= pivots[j] + else: + pivots[j] = row + break + return len(pivots) + + +def clean(poly): + return {f: matrix for f, matrix in poly.items() if any(matrix)} + + +def algebra_product(left, right): + """Full coefficientwise matrix product in F2[Sym_2(Q)].""" + out = {} + for f, a in left.items(): + for g, b in right.items(): + address = add(f, g) + value = bmul(a, b) + out[address] = bxor(out.get(address, (0,) * len(a)), value) + return clean(out) + + +def paid(frame, projector): + n = len(projector) + need(frame != ZERO, 'nonzero paid address') + need(brank(projector) == 1, 'paid projector rank one') + need(bmul(projector, projector) == projector, 'paid projector idempotent') + return clean({ZERO: bxor(eye(n), projector), frame: projector}) + + +def coordinate(n, j): + return tuple((1 << j) if i == j else 0 for i in range(n)) + + +def endpoint(n): + out = {} + for j in range(n): + address = TARGETS[j] if j < 4 else ZERO + out[address] = bxor(out.get(address, (0,) * n), coordinate(n, j)) + return clean(out) + + +def scalar(matrix): + return {ZERO: matrix} + + +def shear(n, dst, src): + need(dst != src, 'distinct shear indices') + matrix = list(eye(n)); matrix[dst] ^= 1 << src + return tuple(matrix) + + +def replay(word, n): + result = scalar(eye(n)) + for frame, projector in word: + result = algebra_product(result, paid(frame, projector)) + return result + + +def formal_controls(): + constructions = mutations = noncoordinate = 0 + pairs = ((A, P), (A, QFRAME), (B, P), (B, QFRAME)) + for n in (4, 5, 7): + word = [(frame, coordinate(n, j)) for j, pair in enumerate(pairs) for frame in pair] + need(replay(word, n) == endpoint(n), 'direct eight-call endpoint') + constructions += 1 + # Each transvection is its own inverse. Conjugate all projectors by H, + # then undo that free role basis at the two ends of the word. + mixers = [shear(n, 0, 1), shear(n, 2, n-1)] + if n > 4: + mixers.append(shear(n, n-1, 1)) + H, Hinv = eye(n), eye(n) + for M in mixers: + H = bmul(M, H) + Hinv = bmul(Hinv, M) + need(bmul(H, Hinv) == eye(n) == bmul(Hinv, H), 'binary free-mixing inverse') + transformed = [(f, bmul(H, bmul(N, Hinv))) for f,N in word] + noncoordinate += sum(brank(N) == 1 and N not in [coordinate(n,j) for j in range(n)] + for _,N in transformed) + prod = replay(transformed, n) + if n > 4: + need(any(matrix[-1] != ((1 << (n-1)) if address == ZERO else 0) + for address, matrix in prod.items()), + 'paid segment must transiently modify a dirty role') + restored = algebra_product(scalar(Hinv), algebra_product(prod, scalar(H))) + need(restored == endpoint(n), 'free-conjugated word restores every dirty role') + constructions += 1 + for index in range(8): + need(replay(word[:index] + word[index+1:], n) != endpoint(n), 'dropped-call mutant survived') + mutations += 1 + for index in range(8): + changed = list(word) + changed[index] = (scale(2, changed[index][0]), changed[index][1]) + need(replay(changed, n) != endpoint(n), 'scaled-label mutant survived') + mutations += 1 + need(noncoordinate > 0, 'noncoordinate projectors exercised') + # A rank-one nilpotent is not a paid idempotent. + nilpotent = (2, 0, 0, 0) + need(brank(nilpotent) == 1 and bmul(nilpotent,nilpotent) != nilpotent, 'nilpotent fixture') + try: + paid(A, nilpotent) + except ValueError: + mutations += 1 + else: + raise ValueError('non-idempotent call accepted') + return constructions, mutations, noncoordinate + + +def run(): + candidates, profiles = enumerate_candidates() + survivors, support_checks, ranks = support_and_rank(candidates) + constructions, mutations, noncoordinate = formal_controls() + print('PASS_SCALED_FRAME_INDEPENDENT ' + f'count_profiles={profiles} determinant_candidates={len(candidates)} distinct_frames=20 ' + f'target_support_checks={support_checks} survivors={len(survivors)} ' + f'rank_obstructions={len(ranks)} formal_words={constructions} ' + f'noncoordinate_paid_factors={noncoordinate} mutations_rejected={mutations}') + return {'count_profiles': profiles, 'candidates': len(candidates), 'frames': 20, + 'target_support_checks': support_checks, 'survivors': len(survivors), + 'rank_obstructions': len(ranks), 'formal_words': constructions, + 'noncoordinate_paid_factors': noncoordinate, 'mutations_rejected': mutations} + + +if __name__ == '__main__': + run() diff --git a/research/bit-single-scaled-frame-floor/verify.py b/research/bit-single-scaled-frame-floor/verify.py new file mode 100644 index 0000000000..efbdcb7905 --- /dev/null +++ b/research/bit-single-scaled-frame-floor/verify.py @@ -0,0 +1,88 @@ +"""Source-bound exact checks for the scoped proof in README.md. + +Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0. +""" +from fractions import Fraction +import hashlib +import json +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] + + +def need(value, message): + if not value: + raise ValueError(message) + + +def source_checks(): + sources = json.loads((PACKAGE / 'SOURCES.json').read_text()) + manifest = json.loads((PACKAGE / 'VERIFY.json').read_text()) + count = 0 + for row in sources['files']: + if row['usage'] == 'input': + need(row['path'] in manifest['inputs'], 'undeclared live source') + data = (ROOT / row['path']).read_bytes() + need(hashlib.sha256(data).hexdigest() == row['sha256'], + 'predecessor source changed: ' + row['path']) + count += 1 + need(count == 3, 'three predecessor inputs') + return count + + +def main(): + sources = source_checks() + # Compile the package-local source bytes rather than trusting cached pyc. + namespace = {'__name__': 'independent_certificate'} + path = PACKAGE / 'independent.py' + exec(compile(path.read_bytes(), str(path), 'exec'), namespace) + independent = namespace['run']() + # Independently check the integer-circle step in the written proof. + circles = {} + for n in range(7): + radius = 8 - n + points = {(d, e) for d in range(-n, n + 1) for e in range(-n, n + 1) + if abs(d) + abs(e) <= n and d*d + e*e == radius*radius} + expected = set() if n < 4 else {(radius,0),(-radius,0),(0,radius),(0,-radius)} + need(points == expected, 'integer-circle reduction') + circles[n] = points + old, targets = namespace['OLD'], namespace['TARGETS'] + add, scale = namespace['add'], namespace['scale'] + expected_pairs = ((0,2),(0,3),(1,2),(1,3)) + for target, expected in zip(targets, expected_pairs): + pairs = {(i,j) for i in range(4) for j in range(i,4) if add(old[i],old[j]) == target} + need(pairs == {expected}, 'unique old-pair support') + replay, coordinate = namespace['replay'], namespace['coordinate'] + endpoint, A = namespace['endpoint'], old[0] + word = [(old[i],coordinate(5,j)) for j,pair in enumerate(expected_pairs) for i in pair] + # A negative frame may occur in longer words; do not certify a false ban. + loop = [(A,coordinate(5,0)), (scale(-1,A),coordinate(5,0))] + need(replay(word + loop,5) == endpoint(5), 'negative-frame identity padding') + broken = word + [loop[0], (scale(-2,A),coordinate(5,0))] + need(replay(broken,5) != endpoint(5), 'broken negative loop accepted') + # Replacing one A call by two A/2 calls gives a legal nine-call word. + half = (scale(Fraction(1,2), A),coordinate(5,0)) + need(replay([half,half] + word[1:],5) == endpoint(5), 'subdivided frame witness') + leaked = word + [(A,coordinate(5,4))] + need(replay(leaked,5) != endpoint(5), 'dirty auxiliary not restored') + # A hand-computed noncommuting pair detects a reversed product engine. + N, M = (1,0,0,0), (3,0,0,0) + paid, multiply = namespace['paid'], namespace['algebra_product'] + zero, B = namespace['ZERO'], old[1] + forward = multiply(paid(A,N), paid(B,M)) + backward = multiply(paid(B,M), paid(A,N)) + need(forward == {zero:(0,2,4,8), A:(2,0,0,0), add(A,B):(3,0,0,0)}, + 'literal ordered noncommuting coefficients') + need(backward == {zero:(2,2,4,8), B:(2,0,0,0), add(A,B):(1,0,0,0)}, + 'literal reversed noncommuting coefficients') + need(forward != backward, 'reversed product mutation accepted') + need(independent['survivors'] == 4 and independent['mutations_rejected'] == 49, + 'independent certificate totals') + print('PASS_SINGLE_SCALED_FRAME_MINIMUM_8 ' + f'live_sources={sources} circle_domains={len(circles)} unique_target_pairs=4 ' + 'longer_words=2 extra_failure_controls=3 noncommuting_products=2 finite_widths=4,5,7') + + +if __name__ == '__main__': + main()