Constrain fifteen-owner equality graphs (no new κ)

research/centre-fifteen-owner-equality/PROOF.md

@@ -0,0 +1,128 @@
+# The fifteen-owner equality case
+
+## Statement
+
+Let G=(B,D,E) be a finite nonempty simple bipartite graph. Assume minimum
+degree at least three, no four-cycles, |B|=15, and the following bounds on
+the number c6(d) of unoriented simple six-cycles through each d in D:
+
+    c6(d) <= 1                    when deg(d)=3;
+    c6(d) <= floor(deg(d)^2/4)    when deg(d)>=4.
+
+Then both parts have fifteen vertices and every vertex has degree three.
+The six-cycles are vertex disjoint. Write t for their number. Either t=0,
+or 2<=t<=5. In particular, an equality graph cannot have exactly one
+six-cycle.
+
+There is also an explicit necessary matrix identity. Let C be its 15 by 15
+zero-one incidence matrix, with rows indexed by B. Let J be the all-ones
+matrix. There are partial permutation matrices P and Q with exactly the
+same 3t active rows and 3t active columns such that
+
+    C C^T C = 4 C + J + P - Q.                         (1)
+
+P matches each vertex of B on a six-cycle to the opposite vertex of D on
+that cycle. Q matches it to a vertex on a different six-cycle. Every active
+row and column of either matrix contains exactly one 1. Furthermore
+
+    (P-Q) C^T = C (P-Q)^T.                            (2)
+
+These are integer identities. No coefficient-field reduction is used.
+When t=0, (1) reduces to C C^T C = 4 C + J.
+
+## 1. The new equality reduction
+
+We use Sagar Thakrar's local path-counting inequality from PR3291,
+PROOF.md section 2, as a cited lemma:
+
+    |B| >= 5 deg(d) - c6(d).                          (3)
+
+Its hypotheses are precisely minimum degree three and absence of four-cycles.
+We do not re-audit the route extraction or the predecessor's floor proof.
+For 4<=k<=15, the lower bound 5k-floor(k^2/4) takes the values
+
+    16,19,21,23,24,25,25,25,24,23,21,19.
+
+Every value exceeds 15. A simple graph with fifteen vertices in B has
+no D degree greater than fifteen, so all vertices of D have degree three.
+
+If b in B had degree at least four, root at an adjacent d. Its three B
+neighbors have at least 3+2+2=7 other D neighbors. They are distinct because
+there are no four-cycles. Each has two further B neighbors. There are at
+least fourteen incidences to level three. Collapsing them to distinct B
+vertices can save at most c6(d)<=1 vertices, by the collision count used in
+(3). These vertices are outside the three first-level vertices. This would
+require |B|>=3+14-1=16. Thus every B vertex also has degree three. Counting
+edges gives 3|D|=3|B|, hence |D|=15.
+
+This extends the predecessor's fourteen-owner contradiction to a structural
+statement at its sharp equality size. It does not improve the bound fifteen.
+
+## 2. Six-cycles are disjoint
+
+Two distinct six-cycles cannot share a D vertex, by its cap. If they shared
+a B vertex, each would use two of its three edges. They would therefore
+share an edge and its D endpoint, also impossible. Thus all six-cycles are
+vertex disjoint. The same cap of one now holds at B vertices. Each cycle
+uses three vertices of each part, so t<=5.
+
+## 3. The signed defect
+
+For b in B and d in D, (C C^T C)_(b,d) counts length-three walks from b to d.
+If they are adjacent, exactly five such walks exist: three backtrack at b
+and three backtrack at d, with the single-edge backtrack counted twice.
+A further walk would form a four-cycle. Thus the entry is five.
+
+If b and d are not adjacent, all these walks are simple paths. Let p_b(d)
+be their number. Two different paths between these endpoints have disjoint
+interiors: sharing either interior vertex would create a four-cycle. Hence
+
+    c6(b) = sum_(d not adjacent to b) binom(p_b(d),2).  (4)
+
+Each six-cycle through b has a unique opposite endpoint d, which proves
+both directions of this counting identity.
+
+There are twelve length-three paths from b to nonneighbors: choose one of
+three first edges, one of two second edges, and one of two third edges.
+No such path can return to a neighbor, since there are no four-cycles.
+There are also exactly twelve nonneighbors in D.
+
+If c6(b)=0, (4) forces all twelve path counts to be one. If c6(b)=1, it
+forces exactly one count to be two, exactly one to be zero, and the other
+ten to be one. The doubled endpoint is the opposite vertex on b's unique
+six-cycle. The zero endpoint is unique.
+
+Apply the same argument after interchanging B and D. It shows that a
+column of the defect matrix
+
+    E = C C^T C - 4C - J
+
+is zero off the six-cycles; on a six-cycle it has one +1 and one -1.
+The row statement is identical. Thus the positive entries form P, the
+negative entries form -Q, and their active row and column sets are exactly
+the vertices on the six-cycles. This proves (1) and the asserted partial
+permutation structure.
+
+For an active b, its own six-cycle contains three D vertices. Two are
+adjacent to b, while the third has two length-three paths from b. None is
+the zero-path endpoint. The Q endpoint therefore lies on another cycle.
+If there were exactly one six-cycle, there would be no such endpoint.
+This excludes t=1.
+
+Finally, E C^T = (C C^T)^2 - 4 C C^T - 3J is symmetric, since every row
+of C has sum three. Transposing gives (2).
+
+## 4. What this does and does not settle
+
+The six-cycle-free duad/perfect-matching graph in PR3291 attains the
+hypotheses, so the equality class is nonempty. Its established floor and
+classical geometry retain their credit. We do not claim uniqueness of that
+graph, nor exclude equality graphs with two through five six-cycles.
+
+For a future route-labelled fifteen-owner search, every candidate can now
+be restricted to a cubic fifteen-by-fifteen incidence with the signed defect
+above. If it has a six-cycle, it must have at least two disjoint ones, and
+the negative defect matches between different cycles. Actual route labels,
+scalar coefficient equations and physical realization are additional
+obligations. The present theorem supplies no common-kernel vector, cheaper
+repair, paid profile, supplier admission or new kappa.

research/centre-fifteen-owner-equality/README.md

@@ -0,0 +1,110 @@
+# Cubic structure and a signed defect at fifteen owners
+
+**Scoped written proof with finite exact corroboration. No new kappa.**
+Every graph attaining Sagar Thakrar's PR3291 fifteen-owner abstract floor is
+cubic on fifteen vertices per side. Its six-cycles are vertex disjoint, and
+it cannot have exactly one six-cycle. This contribution is produced by
+Nick Petalas.
+
+The new structural identity, over the integers, is
+
+    C C^T C = 4C + J + P - Q,
+    (P-Q) C^T = C (P-Q)^T.
+
+C is the incidence matrix. P and Q are partial permutation matrices on the
+vertices lying on six-cycles. P matches opposite vertices on each cycle;
+Q matches vertices on different cycles. If there are t six-cycles, their
+active sets have size 3t. Thus t is either zero or one of 2,3,4,5.
+[PROOF.md](PROOF.md) gives the universal argument and exact hypotheses.
+
+This is a new restriction on the equality search left by PR3291 and
+Matarener's PR3656. Their floor, geometry, source extraction and coset
+certificate are cited without replay or audit. We do not classify every
+equality graph or prove that the six-cycle-free example is unique.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/centre-fifteen-owner-equality/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/centre-fifteen-owner-equality/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/centre-fifteen-owner-equality
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/centre-fifteen-owner-equality --check-source-history
+```
+
+Substitute an installed CPython 3.12 path elsewhere. The direct verifier is
+read-only and prints a generated receipt bound to every package file by
+SHA256, followed by `PASS_CENTRE_FIFTEEN_OWNER_EQUALITY`.
+
+The bounded corroboration visits all 531,441 local path profiles in
+{0,1,2}^12, including the 133 profiles admitted by the path-sum/cycle cap;
+checks the twelve possible noncubic root degrees; and checks the integer
+defect on the duad/perfect-matching graph. All 720 eligible two-edge switches
+of that graph are tested. Exactly 360 are four-cycle-free and all 360 fail
+the six-cycle cap. Independent intersection and literal-walk cycle counters
+agree on their complete cycle sets. This is a bounded control family, not
+an enumeration of all fifteen-owner graphs or evidence that the remaining
+cycle counts are impossible. No nonzero-defect equality graph is supplied;
+nonzero local profiles are checked independently of graph realization.
+
+Controls reject malformed equality boundaries and local path profiles, and
+a cubic C4-free fifteen-by-fifteen cyclic graph specifically at the six-cycle
+capacity gate. Literal matrix multiplication supplies a separate path-count
+check. Normal and optimized commands retain every check.
+
+## Connection and limits
+
+The original `centre-path-sharing` card is changed to a structural side
+question in the retained one-to-one block-repair model. The theorem assumes
+the abstract minimum-degree, C4-free and cycle-cap conditions. It does not
+recompute the routes or prove those conditions for another supplier.
+
+For a route-labelled equality search, the cubic restriction removes larger
+degrees, and the P/Q identity supplies necessary equations before checking
+route labels and scalar coefficients. These obligations remain open. No
+physical acquisition, dirty restoration, frame conversion, hosting, precision,
+stock, recursive invoice, all-size compiler, admitted supplier or complete
+multiplication theorem is supplied. The selected frontier remains unchanged.
+Independent human and formal proof-kernel review are unclaimed. No selected
+cold replay, Lean or Docker run is part of this result.
+
+The historical card control fails with `KeyError: 'complex_profile'` against
+the selected schema. The current `research_selected_baseline.py` binding
+control passes. These are orientation observations, not scientific premises.
+
+The checker has no recursion, subprocesses, network or write paths. Graphs
+are bounded to 32 vertices per side; actual cycle checks use cubic graphs
+with fifteen vertices per side. Walks have exactly five expansion rounds.
+The largest local profile domain is 3^12, processed one tuple at a time.
+Functions stay below sixty physical lines. Python allocates managed objects;
+fixed allocation is not claimed. These fixed domains and the registered
+120-second command bounds are the compensating limits. Raw-pointer and
+preprocessor rules have no direct Python counterpart. Warning-strict normal
+and optimized execution and AST inspection provide diagnostics; no project
+static type checker is configured for this isolated standard-library file.
+
+## Open next questions
+
+1. Can an equality graph have two through five six-cycles? Use the cubic
+   fifteen-by-fifteen boundary and signed partial permutations first. This
+   would decide whether a route search may restrict to girth eight. No such
+   exclusion or witness is supplied here.
+2. Can a graph satisfying this stronger boundary carry the actual routes
+   and scalar coefficient equations? Begin with one equality incidence and
+   retain every route relation. The route-labelled CSP and a favorable full
+   physical budget remain blockers to a supplier construction.
+
+The structured questions are also in [TASK.json](TASK.json).
+
+## Credit
+
+Sagar Thakrar #3291 supplies the local path-counting inequality and sharp
+fifteen-owner theorem. Matarener #3656 supplies the coset construction and
+minimum-support question. Retain dcharb78 #3147, Ross Richardson #3071,
+Gonzalo Mier #3097, Sudarsh Chaturvedi #3168, Aaron Wang/navinor, ywz65 and
+the selected source lineage for the block-repair model and route conditions.
+The duad/perfect-matching geometry and ordinary graph path counting are
+classical; no literature-priority claim is made for them. Only the equality
+reduction, signed defect and its consequences are new in this package.
+Predecessor files and notices remain unchanged. Apache-2.0.

research/centre-fifteen-owner-equality/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/centre-block-moore-bound/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "57e4adae5ab6247d7f82fefc2d91abccdb4bd39a",
+      "sha256": "4ff55b8d7c32f4ad2e32e267fd3e3340003b580dfa709577016eb605f157e137"
+    },
+    {
+      "path": "research/centre-block-moore-bound/README.md",
+      "usage": "provenance",
+      "git_blob": "82b2b72beaa1878dd933cf95a47ade8b2a0af643",
+      "sha256": "bbdf8be190f21ddffacc7babd79b1111e7948e4dfc37d7496bc199dd63d4d03c"
+    },
+    {
+      "path": "research/centre-block-coset-kernel/README.md",
+      "usage": "provenance",
+      "git_blob": "f27dc04894b04dfbe60152adb77ac69b5b5f0628",
+      "sha256": "c7594aa840999aa366d834500f0b13cd870c215b321eacdfb0da43bc35d7eef6"
+    }
+  ]
+}

research/centre-fifteen-owner-equality/TASK.json

@@ -0,0 +1,77 @@
+{
+  "schema_version": 1,
+  "task_id": "centre-path-sharing",
+  "priority_revision": 7,
+  "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13",
+  "original_card": {
+    "id": "centre-path-sharing",
+    "question": "Can the 64-per-call centre path (eight rank-8 COPY/ERASE totals through the private temporary) be shared across calls or shrunk?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/complex-local-word-ceiling/README.md",
+      "research/split-centres-global/proofs/PR386-BIT-GEOMETRY.txt",
+      "certificates/selected-result.json"
+    ],
+    "methods": [
+      "Derive a fully charged favorable relaxation for sharing one centre path across k calls, including restoration, hosting and precision.",
+      "Prove a lower bound on copied information per call for the selected decoder contract."
+    ],
+    "acceptance_gate": "Show the changed centre charge and copy profile per call with every added restoration or hosting cost charged, and its ceiling via ceiling.ceiling(centre=...). 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",
+        "research/complex-local-word-ceiling/verify.py"
+      ],
+      "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING",
+      "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.",
+      "scope": "Positive control and planning budget only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Write the per-call centre charge and copy children for sharing across k = 2 calls, charge the sharing overhead, and screen it; stop this route if even the ideal sharing gains under 10%. Ideal budgets: free 2.80x, shared by two 1.90x (levers.py).",
+    "bottleneck_link": "The centre path consumes 64 of about 99.6 unpaid coordinates per call, i.e. about 64% of the raw deficit.",
+    "allowed_variations": [
+      "One sharing pattern across a fixed number of calls.",
+      "One reduced copied-total contract for the existing decoder.",
+      "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope."
+    ],
+    "scope_change_triggers": [
+      "Removing copies without a replacement contract for the decoder's copied totals.",
+      "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts."
+    ],
+    "overlap_terms": [
+      "centre path",
+      "copied totals",
+      "private temporary",
+      "shared centre",
+      "batching"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Cubic structure and signed partial-permutation defect of the abstract fifteen-owner equality case; exact exclusion of one six-cycle.",
+  "scope_change_reason": "A structural side question before the route-labelled equality search, rather than a new centre supplier or a replay of predecessor claims.",
+  "bottleneck_link": "The necessary equality structure restricts candidates for the smallest common-kernel support before expensive route and coefficient searches; no physical cost improvement is claimed.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first proved equality restriction; leave the remaining six-cycle counts and physical route realization open.",
+  "outcome": "completed",
+  "evidence": "PROOF.md; generated read-only verifier receipt; 531441 local profiles, 720 edge switches, independent cycle sets and literal integer products.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can an equality graph have two through five six-cycles?",
+      "why_it_matters": "Decides whether girth eight is a valid restriction on the equality search.",
+      "first_step": "Apply the cubic boundary, signed partial permutations and defect symmetry before graph construction.",
+      "blocked_by": "No complete equality classification or nonzero-defect graph is supplied."
+    },
+    {
+      "question": "Can an equality graph carry the actual route labels and scalar coefficient equations?",
+      "why_it_matters": "Determines whether the abstract equality size is attainable in the retained observation model.",
+      "first_step": "Bind one equality incidence to the literal routes and all scalar equations.",
+      "blocked_by": "Route-labelled CSP and full physical budget remain open."
+    }
+  ],
+  "environment": {
+    "python": "3.12.15",
+    "platform": "macOS-27.0.1-arm64-arm-64bit"
+  }
+}

research/centre-fifteen-owner-equality/VERIFY.json

@@ -0,0 +1,32 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact local path profiles, integer defect, independent cycle sets and boundary controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "The same complete corroboration with optimization enabled."
+    }
+  ]
+}