Prove six-call floor with arbitrary dirty auxiliary outputs

research/bit-fivecall-dirty-block/PROOF.md

@@ -0,0 +1,172 @@
+# 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.
+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
+
+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.

research/bit-fivecall-dirty-block/README.md

@@ -0,0 +1,76 @@
+# 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. 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.
+
+## 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.

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": "9bae10083e68fb1bccf38827741100e394a5e66b19f7020d6c90fad8887dc50c",
+  "schema_version": 1,
+  "verifier_sha256": "5d7bd7583a5984c997df4a88b46f2570b7a44e6c8e44b04fb68f152dcffd8e6e"
+}

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"
+    }
+  ]
+}