Raise matched P112 phase-event floors to 140 and 556 (no κ)

research/matched-phase-integrality/PROOF.md

@@ -0,0 +1,130 @@
+# One more event from Fourier integrality
+
+This proof and its finite corroboration were produced by Nick Petalas.
+
+## Claim and inherited contract
+
+Under Jose Manuel's [PR2070](https://github.com/CrocSwap/integer-mult-bounds/pull/2070)
+matched P112 endpoint and commuting-phase program contract, one bank requires
+at least **140** nontrivial single-array phase events. Four independent banks,
+even with shared role-linear processing and private workspace, require at least
+**556**. These are lower bounds, with no attaining constructions claimed.
+
+We use the mathematical conclusions in the pinned predecessor README,
+Sections 1 through 3, as premises. We do not audit them or replay its code.
+In particular, the new result is conditional on the same causal factorization,
+character-sector construction and matched-endpoint rank statements.
+
+The contract permits fixed constant complex linear processing of the role
+coordinates, including singular COPY/CLEAR, clean private scratch, finite
+restored dirty workspace, and uniform tensor Paulis. A paid event acts on
+one role by a commuting directional-phase product with a nonzero binary
+symmetric polar. It excludes nonlinear or data-dependent programs,
+noncommuting payload adapters, arbitrary payload-coordinate mixing, and
+new joint multirole child interfaces. All independent inputs and declared
+outputs are retained exactly as in PR2070.
+
+This theorem concerns one direct matched bank or four independent direct
+matched banks. It does not claim a stronger normalized bound for nonuniform
+coherent-cover programs, a new physical tariff, or a full supplier.
+
+## Cited rank and character premises
+
+Write G for the binary vector space of symmetric polars. Every character
+chi of G is simultaneously available in the predecessor's common
+Pauli-trivial sector at a sufficiently large tensor length. Each of k
+nontrivial events has a fixed nonzero polar p_j in G, and acts by
+(-1)^(chi(p_j)). Repetitions among the p_j are allowed.
+
+Let t(chi) count the active events, those with chi(p_j)=1. The predecessor's
+causal rank inequality is
+
+    rank Delta_chi >= d_image + d_row - 2k + t(chi).
+
+For b independent matched P112 banks its stated premises are
+
+    d_image = d_row = 112b,
+    rank Delta_chi <= 16b   for every chi.
+
+Consequently every character must satisfy
+
+    t(chi) <= 2k - 208b.                                      (1)
+
+Each p_j is nonzero, so averaging t over all characters gives k/2.
+Thus k >= ceil(416b/3), the predecessor's 139 and 555 bounds for b=1
+and b=4. No computation in this package re-establishes the quoted
+source dimensions, endpoint, or tensor-sector realization.
+
+## A finite-group rigidity lemma
+
+Let G be any finite binary vector space. Let p_1,...,p_k be a multiset
+of nonzero elements, with k positive and odd. If
+
+    t(chi) <= (k+1)/2   for every character chi,                 (2)
+
+then the multiset is exactly H minus {0}, each element occurring once,
+for a nonzero linear subspace H of G. In particular k+1 is a power of two.
+Conversely, every such multiset satisfies (2).
+
+Proof. Set f(0)=1, and set f(g) to the multiplicity of g for g nonzero.
+Its unnormalized real Fourier transform is
+
+    f_hat(chi) = 1 + sum_j (-1)^(chi(p_j))
+               = 1 + k - 2t(chi) >= 0.
+
+Fourier inversion at zero gives sum_chi f_hat(chi)=|G|. Therefore
+w_chi=f_hat(chi)/|G| is a probability distribution, and inversion gives
+
+    f(g) = sum_chi w_chi (-1)^(chi(g)).                         (3)
+
+Equation (3) implies |f(g)|<=1. The multiplicities are nonnegative
+integers, so f takes only values 0 and 1. Moreover, f(g)=1 exactly when
+every character with w_chi>0 vanishes on g. The set H on which f is 1
+is therefore the intersection of the kernels of those characters, a
+linear subspace. This proves both the support statement and the absence
+of repeated polars. Since sum_g f(g)=k+1, we get |H|=k+1.
+
+Conversely, if f is the indicator of H, summing a character over H gives
+|H| if the character vanishes on H, and zero otherwise. Hence f_hat>=0,
+which is (2). This completes the proof for every finite dimension.
+
+Equivalently, if positive odd k has k+1 not a power of two, some character
+activates at least (k+3)/2 events. This is an arithmetic obstruction;
+it does not depend on the ambient dimension or on a bound on repetitions.
+Finite-group Fourier inversion and positivity are classical ingredients.
+No global priority for the abstract lemma is claimed.
+
+## The new matched-endpoint bounds
+
+For b=1, the cited average bound already gives k>=139. If k=139,
+(1) requires t(chi)<=70 for every chi. This equals (k+1)/2, so the
+lemma would require 140 to be a power of two. It is not. Thus k>=140.
+
+For b=4, the cited average bound gives k>=555. If k=555, (1) requires
+t(chi)<=278 for every chi. Again this is (k+1)/2, but 556 is not a
+power of two. Thus k>=556.
+
+The argument applies separately at every sufficiently large tensor length
+in the cited character-sector construction, even if the program and its
+constant coefficients depend on that length. Its polar multiset at that
+length is still finite and subject to the same lemma.
+
+## Limits and relevance
+
+This strengthens the historical matched terminal obstruction by one event.
+PR2070 already excluded its stated comparison invoice; we do not recompute
+that invoice, claim a new exclusion of the selected PR6030 caller, or change
+kappa. The result explains one additional reason the averaged event-count
+boundary cannot be attained in this alphabet.
+
+A zero-polar event violates the lemma's premise. Uncharged adapters that
+move between character sectors violate the common-character premise.
+Different terminal endpoints need their own image, row and defect bounds.
+Event counts do not by themselves determine a native tariff or a complete
+signed target/paid moment. The five selected framework assumptions remain.
+Independent human and formal proof-kernel review are unclaimed.
+
+The verifier enumerates only its explicitly reported small multisets. Its
+finite checks corroborate the new Fourier argument and its implementation;
+they do not enumerate candidate 139-event or 555-event circuits, and they
+do not replace this all-dimension proof.

research/matched-phase-integrality/README.md

@@ -0,0 +1,107 @@
+# Matched phase-query floors of 140 and 556
+
+This contribution was produced by Nick Petalas.
+
+A Fourier integrality argument raises Jose Manuel's
+[PR2070](https://github.com/CrocSwap/integer-mult-bounds/pull/2070)
+commuting-phase lower bound from 139 to **140** single-array phase events
+for one matched P112 bank, and from 555 to **556** for four independent
+banks. Shared role-linear processing, COPY/CLEAR and private workspace
+remain permitted under the predecessor's contract.
+
+Claim type: scoped mathematical proof with exact finite corroboration.
+The bounds are not claimed optimal. There is no new kappa, physical supplier
+or selected-frontier change. This is a terminal-interface side result on
+the centre-path-sharing card, rather than a completed current-caller change.
+
+The new lemma says that an odd multiset of k nonzero binary polars with
+at most (k+1)/2 active events in every character must consist of all nonzero
+elements of a subspace, each once. Thus k+1 must be a power of two.
+PR2070's cited rank inequality forces exactly this threshold at k=139 and
+k=555; neither 140 nor 556 is a power of two. Read [PROOF.md](PROOF.md).
+
+The predecessor's causal inequality, common Pauli-trivial character sector,
+P112 span dimensions and defect-rank bound are mathematical premises.
+They are not new results here, and no predecessor scientific executable
+is imported, audited or replayed. [SOURCES.json](SOURCES.json) pins its
+README as historical provenance at canonical main
+`7c49fe32c55de02c2c873655c804b16e4c3fef0a`.
+
+## Reproduce
+
+From the repository root, use CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/matched-phase-integrality/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/matched-phase-integrality/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/matched-phase-integrality
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/matched-phase-integrality --check-source-history
+```
+
+Elsewhere substitute a local CPython 3.12 path. The direct marker is
+`PASS_MATCHED_PHASE_INTEGRALITY`. Direct runs generate a deterministic
+receipt on stdout, bound to the SHA256 of all six package files. They write
+no files. No hand-written receipt is committed.
+
+The checker exhausts every odd-size nonzero-polar multiset of sizes 1 through
+9 in dimensions 1 through 3, and sizes 1 through 5 in dimension 4. It checks
+19,727 multisets, including repetitions. Exactly 70 satisfy the character
+threshold; each is a subspace with zero omitted. Direct character evaluation
+and a separate butterfly transform agree. Fourier inversion, exact multiset
+counts and Gaussian-binomial subspace counts also agree. Thirteen invalid
+domains are rejected. Five semantic control groups cover two simplex sizes,
+repeated polars, the essential zero-polar exclusion and the exact threshold.
+Normal and optimized modes keep all checks active.
+
+These finite cases support the new lemma. They do not enumerate circuits
+with 139 or 555 events, prove the predecessor premises, or replace the
+all-dimension written argument.
+
+## Limits
+
+The proof requires fixed role-linear programs, nonzero commuting phase
+polars and the complete common-character family. Noncommuting payload
+adapters, nonlinear or data-dependent programs, changed endpoints and
+new multirole child interfaces require other arguments. This package does
+not strengthen the normalized nonuniform coherent-cover bound.
+
+The selected record at the pinned base is PR6030, conditional
+kappa 0.003125804. Its five framework assumptions remain. Native realization,
+physical tariffs, routing, ownership/erasure, restoration implementation,
+precision/tape, stock, compiler closure and complete supplier/outer bills
+are unprovided. The selected scientific cold replay, Lean and Docker are
+unrun. Independent human and formal proof-kernel review are unclaimed.
+
+The checker has no recursion or subprocesses. Every enumerated domain has
+an explicit bound. New functions are below 60 physical lines. Managed Python
+allocation is a Power-of-Ten rule-3 deviation; live mathematical arrays have
+at most 16 entries and each multiset has at most 9 entries. The 18 summary
+rows and fixed package-file hashes are bounded. It does not claim a fixed
+allocation runtime. Warnings are errors in both registered commands.
+
+## Open next questions
+
+- Can the 140-event or 556-event floor be attained in the exact matched
+  alphabet? An explicit polar multiset satisfying the necessary per-character
+  inequalities is a first step. It still needs a causal role-linear
+  realization and complete endpoint proof. No such construction is supplied.
+- Can one priced noncommuting payload adapter change the matched endpoint's
+  complete cost? Start with its explicit tensor-valid action between two
+  phase events. This is the predecessor's retained opening; the common
+  character decomposition and a physical price are the blockers.
+
+[TASK.json](TASK.json) records these questions, the scope change, live overlap
+coverage and the advance claim.
+
+## Credit
+
+Jose Manuel / jmbarrancoml supplies PR2070's causal, character and P112
+endpoint results. Credit eumemic / PR288 and Ali Romman / PR468 for the
+compact-WY, image/row-span and character lineage; Ali Romman / PR1862/1969
+for the source codes and phase conventions; Rohan Arun / PR1931 for source
+continuation; and Douglas Colkitt for the predecessor's arithmetic lineage.
+Their complete notices remain in the unmodified source package. Classical
+finite-group Fourier inversion and positivity retain their credit; no
+global priority for the abstract rigidity lemma is claimed. The new step
+is its integrality application to this matched endpoint. New work is
+Apache-2.0.

research/matched-phase-integrality/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "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/paired-log-phase-query-bound/README.md",
+      "usage": "provenance",
+      "git_blob": "0c7957111a8fc894cc01f017d221bf0f9c4673a6",
+      "sha256": "271300f434301af469026f0945d01ebf9108c50ccb7e1158170574b07f9455a4"
+    }
+  ]
+}

research/matched-phase-integrality/TASK.json

@@ -0,0 +1,95 @@
+{
+  "schema_version": 1,
+  "task_id": "centre-path-sharing",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "original_card": {
+    "id": "centre-path-sharing",
+    "question": "Can a specified persistent boundary eliminate a repeated centre operation in the current caller?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Write a two-call input/output contract on the current source word, including arbitrary centre baselines and every later read. Price producer, retention, native alignment and restoration jointly. Historical 64-per-call and 1.90x figures are not current budgets. Stop if a missing consumer or restored-input obligation consumes the saving; reopen only with a changed legal boundary.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "centre path",
+      "persistent boundary",
+      "dirty recoding"
+    ],
+    "existing_checks": [
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Fourier integrality raises the cited matched P112 commuting-phase event floors from 139 to 140 and 555 to 556, for one and four independent direct banks.",
+  "scope_change_reason": "The current-caller centre-sharing assignment is narrowed to an original historical terminal-interface obstruction. This does not meet the constructive supplier acceptance gate.",
+  "bottleneck_link": "A stronger necessary event count rules out attainment of the averaged terminal-query boundary within the cited alphabet. It supplies no new current-supplier invoice or kappa.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first proved integrality improvement; package it without searching for a larger bound.",
+  "outcome": "completed",
+  "evidence": "Written all-dimension Fourier proof; exact exhaustive small-multiset corroboration and domain/scope controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can the 140-event or 556-event floor be attained in the exact matched alphabet?",
+      "why_it_matters": "The new result is a necessary lower bound, with no matching construction.",
+      "first_step": "Find an explicit polar multiset satisfying all necessary per-character inequalities, then attempt causal realization.",
+      "blocked_by": "No causal role-linear endpoint construction or complete physical bill is supplied."
+    },
+    {
+      "question": "Can one priced noncommuting payload adapter change the complete matched-endpoint cost?",
+      "why_it_matters": "Such an adapter can escape the common-character premise.",
+      "first_step": "Specify its exact tensor-valid action between two phase events and its physical price.",
+      "blocked_by": "A realizable adapter and complete cost are missing; this is the predecessor opening, not new work here."
+    }
+  ],
+  "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19372194",
+  "predecessor": {
+    "pr": 2070,
+    "author": "jmbarrancoml",
+    "premises": "Causal rank inequality, common real-character sector, P112 spans and defect rank are cited without replay."
+  },
+  "overlap": {
+    "checked_at_utc": "2026-11-03T11:05:19Z",
+    "canonical_main": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+    "priority_revision": 8,
+    "selected_pr": 6030,
+    "source": "PR #2070",
+    "source_author": "jmbarrancoml",
+    "coverage": "Live recent handoffs and active Discussions; open/account PRs; source PR body; main README and merged general-form/object/formula searches; cached card overlap; local reservations.",
+    "limits": "Sparse local notes, arbitrary historical diffs and unpublished work are not covered."
+  }
+}

research/matched-phase-integrality/VERIFY.json

@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact new Fourier rigidity census, independent character evaluation, inversion, combinatorial counts and rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Same complete finite corroboration and controls with optimized assertions disabled."
+    }
+  ]
+}