From a7be2b132ff325cd08e15754d859eab1ae58b70c Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Sat, 24 Oct 2026 20:54:21 -0700 Subject: [PATCH 1/2] Prove six-call floor with arbitrary dirty auxiliary outputs --- research/bit-fivecall-dirty-block/PROOF.md | 169 ++++++++++++++ research/bit-fivecall-dirty-block/README.md | 75 +++++++ research/bit-fivecall-dirty-block/RESULT.json | 66 ++++++ .../bit-fivecall-dirty-block/SOURCES.json | 36 +++ research/bit-fivecall-dirty-block/TASK.json | 64 ++++++ research/bit-fivecall-dirty-block/VERIFY.json | 34 +++ research/bit-fivecall-dirty-block/verify.py | 211 ++++++++++++++++++ 7 files changed, 655 insertions(+) create mode 100644 research/bit-fivecall-dirty-block/PROOF.md create mode 100644 research/bit-fivecall-dirty-block/README.md create mode 100644 research/bit-fivecall-dirty-block/RESULT.json create mode 100644 research/bit-fivecall-dirty-block/SOURCES.json create mode 100644 research/bit-fivecall-dirty-block/TASK.json create mode 100644 research/bit-fivecall-dirty-block/VERIFY.json create mode 100644 research/bit-fivecall-dirty-block/verify.py diff --git a/research/bit-fivecall-dirty-block/PROOF.md b/research/bit-fivecall-dirty-block/PROOF.md new file mode 100644 index 0000000000..a8a6e36aff --- /dev/null +++ b/research/bit-fivecall-dirty-block/PROOF.md @@ -0,0 +1,169 @@ +# Six calls for three rank-two targets, with arbitrary diagonal dirty outputs + +## Statement and inherited facts + +In the formal abelian BIT model, let a paid factor be +`I+([A]-1)xy^t`, where `A` is a nonzero rational rank-one 2-by-2 matrix, +`x,y` are binary scalar vectors of any common finite length R, and `y^t x=1`. +Every input is arbitrary. Suppose the product is diagonal with monomial entries, +and its first three addresses C1,C2,C3 are invertible. The remaining diagonal +addresses are unrestricted: we do **not** assume restored auxiliary outputs. +Then there are at least six calls. Six coordinate calls attain this bound while +restoring every auxiliary input. + +We use two pinned predecessor statements, not a new independent proof of them: + +* The arbitrary-register low-span and one-relation bounds in + `bit-dirty-auxiliary-registers/README.md`, sections 2–3. +* The **three-scalar-register** six-call theorem for arbitrary invertible + 2-by-2 targets in `three-register-no-target-flag/README.md`, section 5. + Its proof uses sections 2–4, including the finite 28-projector classification. + +These imply that a counterexample of at most five calls has exactly five +nonzero calls and rational address span V of dimension three. Indeed the only +possible pair below six is (call count, span)=(5,3). The proof below excludes +that pair without bounding R or enumerating words. Scalar coefficients are +binary, but address linear algebra, rank and projective geometry are rational. + +## Projection and image lemma + +For any rational linear quotient pi of V, replace each address by pi(A). +The induced group-algebra homomorphism preserves the complete endpoint. +Zero projected calls disappear. The subgroup generated by the surviving +addresses is finitely generated torsion-free, so its binary group algebra +is a Laurent polynomial domain; use its fraction field F. + +For l surviving factors, product minus identity has image contained in +`span_F(x_1,...,x_l)`: expand the product, or use +`UV-I=(U-I)V+(V-I)`. Consequently its rank is at most l. If l active target +entries are nonzero projected addresses, their diagonal differences +`[pi(C)]-1` are nonzero. If these are all l first active coordinates, that +span of x vectors is exactly their coordinate space. There can be no other +nonzero projected diagonal endpoint. Since the x vectors are binary, equality +of their F-span to a binary coordinate space forces each x to belong to that +same coordinate space over F2. This conclusion does not discard dirty inputs. + +## The address conic, including its degenerate case + +Every three-dimensional V is the kernel of a nonzero linear form +`A -> trace(MA)` on M2(Q). Independent invertible left/right changes preserve +ranks and reduce M to either rank one or rank two. + +If M has rank one, choose coordinates with V given by A22=0. Write +`A=[[a,b],[c,0]]`. Rank-one calls satisfy bc=0, whereas every invertible target +has both b and c nonzero. Projecting separately to b and c and using the image +lemma requires at least three calls with b nonzero and at least three with c +nonzero. These call sets are disjoint, giving six. + +If M is invertible, choose coordinates with V the traceless matrices +`[[a,b],[c,-a]]`. Their determinant is `-a^2-bc`. Its projective zero locus is +a nonsingular conic over Q. Any projective line meets it in at most two distinct +points: substituting a parametrization of a line gives a quadratic; it cannot +vanish identically because this quadratic form has rank three and therefore +cannot have a linear factor (a product of two linear forms has rank at most two). +Thus any three distinct rank-one directions in V are independent. + +Let t be the number of distinct projective directions among the five calls. +The span condition gives 3<=t<=5. Every full-rank target is off the conic. +For a fixed such target C, pairs of the t conic points whose secant contains C +form a matching: two distinct secants sharing a conic endpoint intersect only +at that endpoint, which C cannot equal. This elementary incidence fact is the +only conic combinatorics used below. + +## Three directions + +The three directions are linearly independent. Project onto each coefficient +in this basis. The number of calls on a direction is at least the number of +active targets using it, by the image lemma. Each invertible target uses at +least two directions, since one rank-one direction cannot be invertible. +Summing requires at least six calls, contradicting five. + +## Four directions: the repeated direction cannot serve three targets + +Name the repeated direction p and the three singleton frames B1,B2,B3 on +directions q1,q2,q3. For each i, quotient V by span(p,qi). This kills the two +p calls and the qi call and leaves exactly two calls. If no active target +lay in that plane, all three target differences would be nonzero, violating +the image lemma. Hence each of the three planes contains an active target. +They intersect pairwise in p, a rank-one direction, so no invertible target +can belong to two of them. Relabel the active targets so Ci belongs to +span(p,qi), and to neither other such plane. + +Under quotient by span(p,qi), the surviving singleton images xj (j!=i) +lie in the coordinate plane of the other two active targets. Intersecting +the two such constraints on xj forces `xj=e_j`, including zero coordinates +on **every** auxiliary role. Each singleton scalar projector is therefore +`e_j y_j^t`; its covector is not assumed coordinate yet. + +Now quotient by Qp. Both repeated calls vanish. The remaining three singleton +factors each write a distinct active row, once. The endpoint is diagonal. +For the factor writing row j, no later factor changes that row. Just before +it, earlier factors have not changed row j. Hence its final row is +`e_j^t + ([Bj]-1)y_j^t P_before`. Off-diagonal vanishing in the Laurent domain +implies every off-diagonal component of `y_j^t P_before` is zero, because +Bj has nonzero quotient. Evaluate this last polynomial identity at augmentation: +`P_before(1)=I`, so yj has no off-diagonal component. Idempotence gives +`y_j^t e_j=1`; consequently this singleton projector is exactly Ejj. +This proves coordinate behavior on all R inputs, not just active ones. + +It also proves that, modulo Qp, the endpoint is exactly the diagonal product +of these singleton factors. Thus `Ci-Bi` belongs to Qp. It is nonzero, +since Ci is invertible whereas Bi is rank one. + +Return to the full group algebra and its fraction field. Move all three +invertible singleton diagonal factors to the left. The remaining two factors +are conjugates of the p-call factors by products of those diagonals. Each is +identity plus a matrix of rank one. Multiplication by the inverse singleton +product leaves a diagonal endpoint whose first three differences from identity +are `[Ci-Bi]-1`, all nonzero. Its rank difference is at least three. A product +of two rank-one updates has rank difference at most two. Contradiction. + +## Five directions: reduce to three scalar roles without assuming restoration + +All five directions are distinct. Call a pair bad if its secant contains at +least one of the three active targets. Each target accounts for a matching +with at most two edges, so there are at most six bad pairs among the ten. +For each good pair, quotient by its plane. Exactly its two calls disappear, +and none of the three active target addresses vanishes. The image lemma forces +the scalar image vectors of the other three calls into the active coordinate +space A=span(e1,e2,e3). + +At most one call index can fail to occur in such a surviving triple. Indeed +an uncovered index j means all six pairs on the other four indices are bad. +Two uncovered indices would require the union of two distinct K4 edge sets, +which has nine edges, exceeding six. Thus at least four scalar image vectors +lie in A. + +If all five lie in A, A is invariant under every factor. Their restrictions +are binary rank-one idempotents: the nonzero image vector x lies in A and is +fixed because y^t x=1. The restricted endpoint is precisely the three active +targets. The inherited three-register six-call theorem gives a contradiction. + +Otherwise let j be the sole factor whose image vector is outside A. Every +other factor preserves A and has an invertible restriction to A over F. In +the quotient of the output scalar space by A, the active-input block of the +whole product is + +`([Aj]-1) * (xj mod A) * (yj^t P_before|A)`. + +Later factors induce the identity on this quotient because their image vectors +lie in A. The diagonal endpoint has zero such block. The first two displayed +factors are nonzero, and `P_before|A` is invertible; therefore yj vanishes on A. +The exceptional factor acts identically on A. Restriction of the full word to +A now gives at most four rank-one calls for the same three invertible targets, +again forbidden by the inherited theorem. No condition on the auxiliary +endpoint addresses was used. + +## Consequence for the span-four handoff + +The pinned `bit-span4-auxiliary-structure/PROOF.md` reduces an eight-call, +span-four word for three invertible 3-by-3 targets, with arbitrary diagonal +dirty auxiliary outputs, to exactly three calls on a 1-by-1 address block +and five on a 2-by-2 block of span three. The theorem above excludes the latter. +Thus **every span-four word in that model needs at least nine calls**. +Together with the inherited low-span bound this closes all spans at most four. +Spans five and six, changed alphabets, clean/discarded inputs, nondiagonal +auxiliary endpoints and nonabelian address groups are not covered. + +The result is a written proof using named inherited lemmas and finite diagnostic +checks, not a proof-assistant theorem, a new native supplier or a new kappa. diff --git a/research/bit-fivecall-dirty-block/README.md b/research/bit-fivecall-dirty-block/README.md new file mode 100644 index 0000000000..06d98ab3d1 --- /dev/null +++ b/research/bit-fivecall-dirty-block/README.md @@ -0,0 +1,75 @@ +# Six calls for three rank-two targets with arbitrary dirty auxiliaries + +**Scoped written lower bound.** Three invertible rational 2-by-2 targets need +at least six rank-one calls in the formal abelian BIT register model, for any +finite number of dirty auxiliary registers with arbitrary diagonal monomial +outputs. Six coordinate calls attain the bound and restore all auxiliaries. +This closes the five-call/span-three block left open by +`bit-span4-auxiliary-structure`. Its reduction then gives **nine calls for every +span-four word with three invertible 3-by-3 targets**, with the same arbitrary +diagonal auxiliary-output contract. + +[PROOF.md](PROOF.md) is the argument. The new mechanism is a projective conic +split into three, four or five distinct rank-one directions. In the four-point +case, two-copy direction incidence forces three singleton scalar projectors to +be coordinate; the remaining two rank-one updates cannot supply a rank-three +endpoint difference. In the five-point case, the secant graph forces all but +at most one scalar image into the three active roles. The remaining factor +either restricts or acts identically there, enabling the inherited +three-register theorem. The reduction does not assume restored auxiliaries. + +The low-span/one-relation theorems and the three-register six-call theorem are +explicit inherited dependencies, not independently re-proved here. Their source +text is byte-pinned. This is not a formal-kernel proof, new supplier, physical +cost improvement, complete multiplication theorem or selected-frontier change. +The selected conditional value remains PR5413's 0.003027288235. + +## Verification + +Standard-library Python 3.12; each direct check is under a second locally: + +```sh +python3 -I -B research/bit-fivecall-dirty-block/verify.py +python3 -I -O -B research/bit-fivecall-dirty-block/verify.py +python3 -B scripts/research_package.py --package research/bit-fivecall-dirty-block +``` + +Expected: `PASS_FIVECALL_DIRTY_BLOCK`. The read-only replay authenticates source, +proof and checker bytes and compares [RESULT.json](RESULT.json). Explicit +`--write-result` regenerates the receipt. Two independently implemented exact +formal engines check the six-call arbitrary-input endpoint, all six deletions, +a changed address, and non-coordinate dirty cancellation. Exact rational conic +fixtures check all secant incidences; all 17,576 triples of five-vertex matchings +check the graph reduction. Singular-target and nine-bad-edge controls show why +its assumptions matter. The finite checks corroborate the written universal +argument; they are not a five-call word enumeration or a new proof of inherited +lemmas. No 120^5 search, historical supplier replay, Lean or Docker was run. + +## Sources, overlap and credit + +Scientific base `32890bc5de034ab8fc93ac88ead7279a6a416d04`, priority 7. +Canonical investigation: [Discussion5473](https://github.com/CrocSwap/integer-mult-bounds/discussions/5473). +The root checked 342 open PRs and 4,736 Discussion records before assignment; +local source checks include the span-four handoff, span-six flag/cyclic-line +successors, four-role pattern census and mixed-target compression. The latter +requires restored extras and is not used to justify this broader contract. +Arbitrary diffs and unpublished work are outside that overlap coverage. + +Credit unpaidmoon for the span-four equality reduction and explicit remaining +five-call question; waynenilsen for arbitrary-register low-span and one-relation +bounds; David Govea for arbitrary-target three-register six-call reduction; +Ali Romman PR468 for the original algebraic/flag/finite-classification methods, +with eumemic PR288 and huxint PR203 retained. The geometric incidence and +rank-update tools are classical. New proof and diagnostics by JoyboyBrian, +with substantial OpenAI Codex assistance. Apache-2.0. No independent human +review is claimed. + +## Open next questions + +Spans five and six for eight rank-one calls and three rank-three targets remain +outside this result. Start with a named unresolved relation class and its exact +endpoint/auxiliary contract; check later successor results first. The conic +proof does not automatically extend to a larger rank-one determinantal variety. +A positive candidate would still require native address realization, all scalar +role changes, owned/dirty restoration, hosting and a full recursive invoice. +[TASK.json](TASK.json) records the same scoped handoff and stop gate. diff --git a/research/bit-fivecall-dirty-block/RESULT.json b/research/bit-fivecall-dirty-block/RESULT.json new file mode 100644 index 0000000000..af6c76df47 --- /dev/null +++ b/research/bit-fivecall-dirty-block/RESULT.json @@ -0,0 +1,66 @@ +{ + "claim": "written proof; finite diagnostics are not exhaustive word search", + "conic": { + "conic_triples": 56, + "controls": [ + "singular target", + "degenerate conic" + ], + "five_point_target_cases": 6048, + "four_point_targets": [ + [ + 1, + -1, + -1 + ], + [ + 0, + -2, + 2 + ], + [ + -1, + -1, + -1 + ] + ] + }, + "formal": { + "active_idempotents_checked": 56, + "address_control": true, + "deletion_controls": 6, + "dirty_cancellation_control": true, + "six_call_targets": [ + [ + 1, + 0, + 0, + 1 + ], + [ + 1, + 1, + 0, + 1 + ], + [ + 0, + 1, + -1, + 0 + ] + ] + }, + "graph": { + "matchings": 26, + "nine_edge_control": true, + "triple_cases": 17576, + "zero_or_one_uncovered": [ + 17546, + 30 + ] + }, + "proof_sha256": "2f2da2b475e3b21effd27a2feae2933a687759d47da4fda0d27ed11f6c8eb21e", + "schema_version": 1, + "verifier_sha256": "b8e57a9151cbf2ffa33ff687e0d48e096c06e8e5096f2d229944a7e5cf59322c" +} diff --git a/research/bit-fivecall-dirty-block/SOURCES.json b/research/bit-fivecall-dirty-block/SOURCES.json new file mode 100644 index 0000000000..0c5e813e42 --- /dev/null +++ b/research/bit-fivecall-dirty-block/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/bit-dirty-auxiliary-registers/README.md", + "usage": "input", + "git_blob": "273bb963ee40869145cf8309db4f8dddebcfe43d", + "sha256": "da984fddaa09bfa7b1a3e11505e737283cee36e7972b2081f9de28ec420607cd" + }, + { + "path": "research/bit-span4-auxiliary-structure/PROOF.md", + "usage": "input", + "git_blob": "84833a7ef6711c2db9a7af8150e690fb03f9ac4c", + "sha256": "58f95c1fbe14cfec8b5d772fec7cc6a1ac6d603f3e1cec2d2ec6178b79444f7f" + }, + { + "path": "research/three-register-no-target-flag/README.md", + "usage": "input", + "git_blob": "290bfb79db5f4177b8b03bc2027c3848671fac9e", + "sha256": "95d4483da9b19df051c7d13fe290eefb82da019ab4be8e66ad9216199ddda4eb" + } + ] +} diff --git a/research/bit-fivecall-dirty-block/TASK.json b/research/bit-fivecall-dirty-block/TASK.json new file mode 100644 index 0000000000..e890286c6a --- /dev/null +++ b/research/bit-fivecall-dirty-block/TASK.json @@ -0,0 +1,64 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 7, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "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": "refined", + "actual_scope": "Exclude five rank-one 2x2 address calls of rational span three for three invertible targets with arbitrary finite dirty auxiliary roles and diagonal monomial outputs.", + "scope_change_reason": "Resolve the explicit span-four handoff through a conic incidence and scalar restriction proof, rather than a new word census.", + "bottleneck_link": "Closes the sole surviving 1+2 equality branch of the arbitrary-auxiliary span-four theorem; no kappa or physical supplier inference.", + "budget_minutes": 60, + "stop_rule": "20-minute structural gate passed; stop at the scoped proof, diagnostics and source-bound reproduction, without expanding to spans five or six.", + "outcome": "scoped-proof", + "evidence": "PROOF.md and RESULT.json", + "author": "JoyboyBrian", + "ai_assistance": "Substantial OpenAI Codex assistance; no independent human review claimed.", + "open_questions": [ + { + "question": "Can an eight-call span-five or span-six word realize three invertible rank-three targets in the dirty diagonal-output contract?", + "why_it_matters": "These are the remaining address-span branches after the span-four closure.", + "first_step": "Check current successor coverage, then select one unresolved relation class with exact scalar endpoint and native cost allowance.", + "blocked_by": "No universal rank-one variety analogue of the conic restriction and no favorable fully priced witness supplied here." + } + ] +} diff --git a/research/bit-fivecall-dirty-block/VERIFY.json b/research/bit-fivecall-dirty-block/VERIFY.json new file mode 100644 index 0000000000..532a0a0dee --- /dev/null +++ b/research/bit-fivecall-dirty-block/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit-dirty-auxiliary-registers/README.md", + "research/bit-span4-auxiliary-structure/PROOF.md", + "research/three-register-no-target-flag/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Conic incidence, all matching triples, two formal endpoint engines, deletion/dirty/singular-target controls and source/proof/receipt hashes" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Conic incidence, all matching triples, two formal endpoint engines, deletion/dirty/singular-target controls and source/proof/receipt hashes" + } + ] +} diff --git a/research/bit-fivecall-dirty-block/verify.py b/research/bit-fivecall-dirty-block/verify.py new file mode 100644 index 0000000000..a9a9924d42 --- /dev/null +++ b/research/bit-fivecall-dirty-block/verify.py @@ -0,0 +1,211 @@ +#!/usr/bin/env python3 +"""Exact diagnostics for the written conic proof; no word-search theorem claim. +JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0. +""" +from fractions import Fraction as Q +from itertools import combinations, product +from pathlib import Path +import hashlib +import json +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent + + +def need(value, message): + if not value: + raise ValueError(message) + + +def rank(rows): + a = [list(map(Q, row)) for row in rows] + k = 0 + for j in range(len(a[0]) if a else 0): + pivot = next((i for i in range(k, len(a)) if a[i][j]), None) + if pivot is None: + continue + a[k], a[pivot] = a[pivot], a[k] + c = a[k][j] + a[k] = [x / c for x in a[k]] + for i in range(len(a)): + if i != k: + c = a[i][j] + a[i] = [x - c*y for x, y in zip(a[i], a[k])] + k += 1 + return k + + +def det(a): + return a[0]*a[3] - a[1]*a[2] + + +def cross(a, b): + return (a[1]*b[2]-a[2]*b[1], a[2]*b[0]-a[0]*b[2], + a[0]*b[1]-a[1]*b[0]) + + +def dot(a, b): + return sum(x*y for x, y in zip(a, b)) + + +def frame(a): + return (a[0], a[1], a[2], -a[0]) + + +def matchings(n): + edges = tuple(combinations(range(n), 2)) + return [frozenset(s) for k in range(n//2+1) + for s in combinations(edges, k) + if len({v for e in s for v in e}) == 2*k] + + +def graph_check(): + edges = frozenset(combinations(range(5), 2)) + ms = matchings(5) + counts = [0, 0] + for triple in product(ms, repeat=3): + bad = frozenset.union(*triple) + need(len(bad) <= 6, 'three targets exceed six bad secants') + good = edges-bad + covered = set().union(*(set(range(5))-set(e) for e in good)) + uncovered = 5-len(covered) + need(uncovered <= 1, 'two scalar images can escape the active space') + counts[uncovered] += 1 + # Dropping the six-edge premise really permits two uncovered indices. + bad = frozenset(e for e in edges if 0 not in e or 1 not in e) + covered = set().union(*(set(range(5))-set(e) for e in edges-bad)) + need(5-len(covered) == 2 and len(bad) == 9, 'edge-budget control') + return {'matchings': len(ms), 'triple_cases': sum(counts), + 'zero_or_one_uncovered': counts, 'nine_edge_control': True} + + +def conic_check(): + points = [(t, 1, -t*t) for t in range(-3, 4)] + [(0, 0, 1)] + need(all(det(frame(p)) == 0 and any(p) for p in points), 'conic points') + triples = list(combinations(points, 3)) + need(all(rank(t) == 3 for t in triples), 'three points collinear') + targets = [t for t in product(range(-2, 3), repeat=3) if det(frame(t))] + checked = 0 + for subset in combinations(points, 5): + for target in targets: + bad = [e for e in combinations(range(5), 2) + if dot(cross(subset[e[0]], subset[e[1]]), target) == 0] + need(len({v for e in bad for v in e}) == 2*len(bad), 'secants not matching') + checked += 1 + p, *qs = [points[-1], points[2], points[3], points[4]] + four_targets = [] + for i in range(3): + others = [qs[j] for j in range(3) if j != i] + c = cross(cross(p, qs[i]), cross(*others)) + need(det(frame(c)) != 0, 'four-point diagonal intersection singular') + four_targets.append(c) + for j in range(3): + masks = [sum(1 << k for k in range(3) if k != i) for i in range(3) if i != j] + need(masks[0] & masks[1] == 1 << j, 'singleton image intersection') + # A singular target at a conic point violates the matching premise. + bad = [e for e in combinations(range(5), 2) + if dot(cross(points[e[0]], points[e[1]]), points[0]) == 0] + need(len(bad) == 4, 'singular-target control') + # In the degenerate plane A22=0 no rank-one frame has both b,c nonzero. + degenerate = [(a,b,c,0) for a,b,c in product(range(-3,4), repeat=3)] + need(all(not (a[1] and a[2]) for a in degenerate if det(a) == 0), 'degenerate partition') + return {'conic_triples':len(triples), 'five_point_target_cases':checked, + 'four_point_targets':four_targets, 'controls':['singular target', 'degenerate conic']} + + +def xor_term(row, key, value): + row[key] = row.get(key, 0) ^ value + if not row[key]: + del row[key] + + +def propagate(word, n): + zero = (0,0,0,0) + columns = [] + for source in range(n): + v = {zero:1 << source} + for addr, x, y in word: + delta = {} + for key, value in v.items(): + if (value & y).bit_count() % 2: + xor_term(delta, key, x) + xor_term(delta, tuple(a+b for a,b in zip(key,addr)), x) + for key, value in delta.items(): + xor_term(v, key, value) + columns.append(v) + return columns + + +def polynomial_matrix(word, n): + # Independent row-polynomial multiplication, not symbolic-vector propagation. + z = (0,0,0,0) + matrix = [[{z} if i == j else set() for j in range(n)] for i in range(n)] + for addr, x, y in word: + old = [[set(e) for e in row] for row in matrix] + for i in range(n): + if not (x >> i & 1): + continue + for j in range(n): + for k in range(n): + if y >> k & 1: + matrix[i][j] ^= old[k][j] + matrix[i][j] ^= {tuple(a+b for a,b in zip(key,addr)) for key in old[k][j]} + columns = [] + for j in range(n): + col = {} + for i in range(n): + for key in matrix[i][j]: + col[key] = col.get(key, 0) | (1 << i) + columns.append(col) + return columns + + +def formal_check(): + targets = [(1,0,0,1), (1,1,0,1), (0,1,-1,0)] + word = [] + for i, (a,b,c,d) in enumerate(targets): + word += [((a,0,c,0),1< Date: Sat, 24 Oct 2026 20:55:42 -0700 Subject: [PATCH 2/2] Check proof publication with independent Git-free corruption controls --- research/bit-fivecall-dirty-block/PROOF.md | 3 ++ research/bit-fivecall-dirty-block/README.md | 3 +- research/bit-fivecall-dirty-block/RESULT.json | 4 +- research/bit-fivecall-dirty-block/TASK.json | 2 +- research/bit-fivecall-dirty-block/VERIFY.json | 10 +++++ .../bit-fivecall-dirty-block/test_verify.py | 42 +++++++++++++++++++ research/bit-fivecall-dirty-block/verify.py | 2 +- 7 files changed, 61 insertions(+), 5 deletions(-) create mode 100644 research/bit-fivecall-dirty-block/test_verify.py diff --git a/research/bit-fivecall-dirty-block/PROOF.md b/research/bit-fivecall-dirty-block/PROOF.md index a8a6e36aff..dc10506db4 100644 --- a/research/bit-fivecall-dirty-block/PROOF.md +++ b/research/bit-fivecall-dirty-block/PROOF.md @@ -24,6 +24,9 @@ nonzero calls and rational address span V of dimension three. Indeed the only possible pair below six is (call count, span)=(5,3). The proof below excludes that pair without bounding R or enumerating words. Scalar coefficients are binary, but address linear algebra, rank and projective geometry are rational. +Chronological factors act on column vectors, so later factors multiply on the +left: P = P_after D_j P_before. Every endpoint address lies in V because a +nonzero endpoint monomial occurs among subset sums of the paid addresses. ## Projection and image lemma diff --git a/research/bit-fivecall-dirty-block/README.md b/research/bit-fivecall-dirty-block/README.md index 06d98ab3d1..c5d557d6b2 100644 --- a/research/bit-fivecall-dirty-block/README.md +++ b/research/bit-fivecall-dirty-block/README.md @@ -41,7 +41,8 @@ formal engines check the six-call arbitrary-input endpoint, all six deletions, a changed address, and non-coordinate dirty cancellation. Exact rational conic fixtures check all secant incidences; all 17,576 triples of five-vertex matchings check the graph reduction. Singular-target and nine-bad-edge controls show why -its assumptions matter. The finite checks corroborate the written universal +its assumptions matter. A separate behavioral test runs a closed Git-free copy +and rejects changed proof, source, receipt and checker bytes in both modes. The finite checks corroborate the written universal argument; they are not a five-call word enumeration or a new proof of inherited lemmas. No 120^5 search, historical supplier replay, Lean or Docker was run. diff --git a/research/bit-fivecall-dirty-block/RESULT.json b/research/bit-fivecall-dirty-block/RESULT.json index af6c76df47..7ecdbcccaf 100644 --- a/research/bit-fivecall-dirty-block/RESULT.json +++ b/research/bit-fivecall-dirty-block/RESULT.json @@ -60,7 +60,7 @@ 30 ] }, - "proof_sha256": "2f2da2b475e3b21effd27a2feae2933a687759d47da4fda0d27ed11f6c8eb21e", + "proof_sha256": "9bae10083e68fb1bccf38827741100e394a5e66b19f7020d6c90fad8887dc50c", "schema_version": 1, - "verifier_sha256": "b8e57a9151cbf2ffa33ff687e0d48e096c06e8e5096f2d229944a7e5cf59322c" + "verifier_sha256": "5d7bd7583a5984c997df4a88b46f2570b7a44e6c8e44b04fb68f152dcffd8e6e" } diff --git a/research/bit-fivecall-dirty-block/TASK.json b/research/bit-fivecall-dirty-block/TASK.json index e890286c6a..d65959f629 100644 --- a/research/bit-fivecall-dirty-block/TASK.json +++ b/research/bit-fivecall-dirty-block/TASK.json @@ -49,7 +49,7 @@ "bottleneck_link": "Closes the sole surviving 1+2 equality branch of the arbitrary-auxiliary span-four theorem; no kappa or physical supplier inference.", "budget_minutes": 60, "stop_rule": "20-minute structural gate passed; stop at the scoped proof, diagnostics and source-bound reproduction, without expanding to spans five or six.", - "outcome": "scoped-proof", + "outcome": "negative-result", "evidence": "PROOF.md and RESULT.json", "author": "JoyboyBrian", "ai_assistance": "Substantial OpenAI Codex assistance; no independent human review claimed.", diff --git a/research/bit-fivecall-dirty-block/VERIFY.json b/research/bit-fivecall-dirty-block/VERIFY.json index 532a0a0dee..c052ca9853 100644 --- a/research/bit-fivecall-dirty-block/VERIFY.json +++ b/research/bit-fivecall-dirty-block/VERIFY.json @@ -29,6 +29,16 @@ ], "timeout_seconds": 30, "checks": "Conic incidence, all matching triples, two formal endpoint engines, deletion/dirty/singular-target controls and source/proof/receipt hashes" + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 30, + "checks": "Git-free relocation and normal/optimized source, proof, receipt and code corruption rejection" } ] } diff --git a/research/bit-fivecall-dirty-block/test_verify.py b/research/bit-fivecall-dirty-block/test_verify.py new file mode 100644 index 0000000000..045648c60d --- /dev/null +++ b/research/bit-fivecall-dirty-block/test_verify.py @@ -0,0 +1,42 @@ +#!/usr/bin/env python3 +"""Behavioral publication controls in a closed, Git-free temporary tree.""" +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +with tempfile.TemporaryDirectory(prefix='fivecall-proof-controls-') as tmp: + root = Path(tmp) + package = root/'research'/HERE.name + shutil.copytree(HERE, package) + inputs = json.loads((HERE/'VERIFY.json').read_text())['inputs'] + for name in inputs: + target = root/name + target.parent.mkdir(parents=True,exist_ok=True) + shutil.copyfile(ROOT/name,target) + def run(optimized=False): + return subprocess.run([sys.executable,'-I',*(['-O'] if optimized else []),'-B',str(package/'verify.py')], + capture_output=True,text=True,timeout=10) + for optimized in (False,True): + result=run(optimized) + if result.returncode or 'PASS_FIVECALL_DIRTY_BLOCK' not in result.stdout: + raise RuntimeError(result.stdout+result.stderr) + for name in ['PROOF.md','RESULT.json','verify.py']: + target=package/name + old=target.read_bytes() + target.write_bytes(old+b'\n') + for optimized in (False,True): + if run(optimized).returncode == 0: + raise RuntimeError('accepted changed '+name) + target.write_bytes(old) + target=root/inputs[0] + target.write_bytes(target.read_bytes()+b'\n') + for optimized in (False,True): + result=run(optimized) + if result.returncode == 0 or 'source hash mismatch' not in result.stderr: + raise RuntimeError('source corruption did not fail closed') +print('PASS_FIVECALL_PUBLICATION_CONTROLS git_free normal_optimized four_corruptions') diff --git a/research/bit-fivecall-dirty-block/verify.py b/research/bit-fivecall-dirty-block/verify.py index a9a9924d42..dc1cd1d506 100644 --- a/research/bit-fivecall-dirty-block/verify.py +++ b/research/bit-fivecall-dirty-block/verify.py @@ -203,7 +203,7 @@ def main(): (HERE/'RESULT.json').write_text(json.dumps(result,indent=2,sort_keys=True)+'\n') else: need(not sys.argv[1:], 'unknown arguments') - need(json.loads((HERE/'RESULT.json').read_text()) == result, 'receipt differs') + need((HERE/'RESULT.json').read_text() == json.dumps(result,indent=2,sort_keys=True)+'\n', 'receipt differs') print('PASS_FIVECALL_DIRTY_BLOCK six_call_floor arbitrary_diagonal_auxiliary_outputs')