Prove the sharp 240-return minimum in the frozen p2 oracle model

research/p2-exact-oracle-repair/PROOF.md

@@ -0,0 +1,141 @@
+# Exactly 240 returns in the frozen p2 oracle model
+
+The minimum is 240 new returns, for every width f >= 72, in the enlarged
+linear-oracle model of PR5587. Keep its 39 observed bank fields, original paid
+input expressions, capacities, ordinary algebra and target credit fixed.
+New returns may be arbitrary linear fields and may use earlier new returns.
+This is a scoped negative result. It does not construct 240 native calls.
+It does not change complete kappa or the selected result.
+
+## Credited premises
+
+Use the source proof at commit 49811a9a37cc1b71bcbe851dd20da3cbf479ff35:
+[PR #5587](https://github.com/CrocSwap/integer-mult-bounds/pull/5587),
+[proof](https://github.com/aliromman/integer-mult-bounds/blob/49811a9a37cc1b71bcbe851dd20da3cbf479ff35/research/p2-full-history-deficit/PROOF.md).
+At f >= 72 the ordinary algebra A is the twisted group algebra of the full
+projective monomial Clifford group H on 17 axes. Write h = |H|.
+The pointwise faithfulness premise is credited to
+[PR #5526](https://github.com/CrocSwap/integer-mult-bounds/pull/5526).
+Sections 4 and 5 of the source proof give these two results:
+
+* The required target module has deficit at least 224h + r, where r is the
+  complex rank of right multiplication by L = I - C3 C1 on A^112.
+* A linear oracle can supply the targets with 240 returns. The construction
+  uses 224 negative targets and 16 factored repair rows.
+
+Each new same-capacity return adds at most h dimensions, including with
+feedback. We retain these source results as premises. The new proof bounds
+r/h strongly enough to close the integer gap from 225 through 240.
+
+## 1. Two rank-eight defects
+
+Let C be the pinned scalar matrix F^T. The checker verifies C^2 = I and
+tr(C) = 96. Thus P = (I-C)/2 has rank eight. Write P = UV with U of size
+112 by 8 and V of size 8 by 112. Set D_s = diag(K_s), where the K_s are the
+pinned signed monomial normalizers in the two fresh blocks. Then
+
+    P_s = D_s^-1 P D_s = U_s V_s,
+    L = 2P1 + 2P3 - 4P3 P1
+      = [U1 U3] [[2I, 0], [-4 V3 U1, 2I]] [V1; V3].
+
+Use the regular representation of A. Its group basis is orthonormal and its
+signed monomials are unitary, for every phase cocycle. Left and right regular
+matrix ranks agree: the conjugate-linear map x -> x* converts right
+multiplication to left multiplication by the adjoint, which has the same rank.
+The middle block above is invertible. Let delta_c be the dimension of the
+intersection of the two column spaces and delta_r the corresponding row-space
+intersection. The rank inequality for a product gives
+
+    r >= 16h - delta_c - delta_r.                      (1)
+
+## 2. One projector bounds both intersections
+
+The scalar orthogonal projector R onto im(P) has rank eight, is real symmetric,
+and has every diagonal entry equal to d = 1/14. The checker derives R from
+eight independent columns with an exact Gram inverse. It verifies all entries
+of R^2 = R, RP = P and the constant diagonal using integers after scaling by 28.
+
+Let W have entry -1/11 at the eight positions where C_ii = 12 and entry 1
+elsewhere. The checker verifies R W P^T = W P^T. Both spaces have rank eight,
+so W im(P^T) = im(P). Since W is invertible and commutes with both D_s,
+it maps both row spaces to the corresponding column spaces. In particular,
+delta_r = delta_c. Division by 11 is only an invertible change of metric in
+a rank proof. It is not a proposed ordinary operation or an unpaid map.
+
+The two orthogonal projectors onto the column spaces are
+R_s = D_s^-1 R D_s. For two orthogonal projections E,F, their common space has
+eigenvalue one in EFE; the other eigenvalues are nonnegative. Therefore
+
+    delta_c/h <= Tr((R1 R3)^2)/h.                     (2)
+
+Here Tr is the ordinary trace on the 112h-dimensional regular space.
+
+## 3. Exact second moment
+
+Set J_i = K_(1,i) K_(3,i)^-1. The checker proves that all 112*111 ordered
+products J_i J_j^-1 with i != j have different binary linear parts. None has
+the identity linear part. The 112 diagonal products are exactly identity,
+including phase. Thus these are 12433 distinct classes in H. This test uses
+all 17 axes. A separate chronological action checks each signed product on
+all 17 basis addresses. The phase functions are linear, so these basis tests
+check the full signed maps.
+
+In a twisted regular group algebra, the normalized trace of a nonidentity
+group element is zero. Expand the trace in (2) and group ordered pairs by
+J_i J_j^-1. Every off-diagonal class has one pair. The identity class has the
+112 diagonal pairs. The coefficient in each surviving term is positive phase
+one: a group word is followed by its exact inverse. Thus
+
+    tau = Tr((R1 R3)^2)/h
+        = d^2 sum_(i,k) R_ik^2 + d^2 sum_(i != j) R_ij^2
+        = 2*8*d^2 - 112*d^4
+        = 27/343.                                    (3)
+
+The verifier also sums the grouped expression directly, without this reduction:
+for each pair class, sum R_ij R_kl R_ik R_jl over its pairs (i,j),(k,l).
+The first moment is 4/7; it would not close the integer gap. The second moment
+does so. No computation of an irreducible decomposition or exact r is needed.
+
+## 4. Integer optimum
+
+Equations (1)--(3) give
+
+    r/h >= 16 - 54/343 = 5434/343,
+    q >= (224h+r)/h >= 82266/343 > 239.
+
+The number q of returns is an integer, so q >= 240. The credited 240-return
+construction attains this bound in the same enlarged oracle model. This proves
+the exact minimum. The full right-multiplication rank may still exceed this
+lower bound; its exact value cannot improve the minimum return count.
+
+## Verification and limits
+
+The registered normal and optimized Python checks use exact arithmetic only.
+They verify the source hashes, involution, full projector identities, balanced
+row spaces, all ordered signed products, and both forms of the second moment.
+Four controls reject repeated normalizers, a wrong scalar diagonal, a singular
+normalizer and a false 239-return capacity. The committed receipt is compared
+with a fresh result. The package uses the standard library.
+
+We did not replay all 39 source observations, the full Clifford faithfulness
+proof, a native compiler, a physical caller, the selected cold replay, or the
+complete kappa calculation. Those source statements remain credited premises.
+The earlier 225-return tariff obstruction already excludes this frozen caller;
+this proof settles its exact oracle repair optimum. A productive next caller
+must change a frozen input, observation, ordinary alphabet, capacity or target.
+
+## Attribution
+
+Dugongue supplies [PR #4948](https://github.com/CrocSwap/integer-mult-bounds/pull/4948)
+and its native source. Chris R / Clear1nsight supplies
+[PR #4978](https://github.com/CrocSwap/integer-mult-bounds/pull/4978), the D-left
+audit and the fixed-alphabet and owned-reset clarifications. Ali Romman supplies
+the consumed PR5587 deficit and oracle construction, PR5526 faithfulness and
+[PR #5449](https://github.com/CrocSwap/integer-mult-bounds/pull/5449) history model.
+josecarlosgonzalezroque-design supplies the
+[PR #5570](https://github.com/CrocSwap/integer-mult-bounds/pull/5570) bridge audit.
+Retain Cao Yifan, Cinna Davis, DLamdata, zxv and their native, controller,
+Clifford and interval lineage, as recorded in the source proof.
+Projection moments and the product rank inequality are classical. The balanced
+projector, exact pair-class certificate and sharp 240-return conclusion here
+are by Ali Romman with substantial OpenAI Codex assistance. Apache-2.0.

research/p2-exact-oracle-repair/README.md

@@ -0,0 +1,29 @@
+# Exact p2 oracle repair minimum
+
+The frozen p2 model of PR5587 needs exactly **240 new returns** at every width
+f >= 72. Its previous bounds were 225 and 240. The new second-moment certificate
+closes the integer gap. This is an arbitrary-linear-oracle optimum, with fixed
+original inputs, history, capacities, ordinary algebra and targets.
+Complete kappa is unchanged. No native 240-call supplier is supplied.
+
+Read [PROOF.md](PROOF.md), [RESULT.json](RESULT.json) and [SOURCES.json](SOURCES.json).
+
+```sh
+python3 -B scripts/research_package.py --package research/p2-exact-oracle-repair
+```
+
+Use Python 3.12 and the standard library. Expected markers:
+`PASS_P2_EXACT_ORACLE_REPAIR_240` and `PASS_REGISTERED_RESEARCH_PACKAGE`.
+Normal and optimized checks use exact integer and rational arithmetic.
+
+The source deficit, the source 240-return construction and the pointwise
+Clifford theorem are credited premises, not independently replayed here.
+The proof identifies the checked identities and the remaining caller obligations.
+Ali Romman with substantial OpenAI Codex assistance. Apache-2.0.
+
+## Open next questions
+
+Can a changed original paid input evade the fixed-history deficit with a
+complete profitable bill? Specify that input, then rebuild the full history
+module and invoice. More exact rank computation in this frozen model cannot
+lower its now sharp return count.

research/p2-exact-oracle-repair/RESULT.json

@@ -0,0 +1,26 @@
+{
+  "status": "PASS_P2_EXACT_ORACLE_REPAIR_240",
+  "source_rank": 8,
+  "selected": [
+    0,
+    7,
+    20,
+    23,
+    86,
+    93,
+    108,
+    111
+  ],
+  "projector_scale": 28,
+  "projector_sha256": "8f6f9d2fa8a5f8ca241bc7d7225c1a753c401433ab2b5a9a95e997fb96f72553",
+  "distinct_linear_products": 12433,
+  "pair_partition_sha256": "f95bd17aa3984a785643058a891ae9a606d3ca5902b2022f4eb2bf8ca91ff6f7",
+  "signed_basis_actions": 213248,
+  "second_moment": "27/343",
+  "rank_lower_over_h": "5434/343",
+  "target_deficit_lower_over_h": "82266/343",
+  "exact_oracle_returns": 240,
+  "minimum_width": 72,
+  "rejected_controls": 4,
+  "kappa_change": null
+}

research/p2-exact-oracle-repair/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "6cf7a683f447b9f1e2333791907fd92be5009a63",
+  "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/p2-full-history-deficit/PROOF.md",
+      "usage": "input",
+      "git_blob": "19d144ec498b3661100ecadbc07b4b3304a08085",
+      "sha256": "d47c683d680996715a741268f03b8a3e5aea5ec9cd071116fc469b90809f58b3"
+    },
+    {
+      "path": "research/p2-full-history-deficit/inputs/INVOLUTIVE-WORD.json.gz",
+      "usage": "input",
+      "git_blob": "eac634fb1d09428aa6715a47d652ae701dd0efc5",
+      "sha256": "ff2999f022e93e05a250160808aa3c32a08041039d7edfb01068c0308f50c138"
+    },
+    {
+      "path": "research/p2-full-history-deficit/inputs/NORMALIZERS.json",
+      "usage": "input",
+      "git_blob": "bca92c222c395d3d75c047fbb678f3cd0947c60f",
+      "sha256": "ae8aad06aa5d1811d725895b3ab5a4f4daa9dcdd88294aa0d5f723e78bb1e0da"
+    }
+  ]
+}

research/p2-exact-oracle-repair/TASK.json

@@ -0,0 +1,100 @@
+{
+  "schema_version": 1,
+  "task_id": "independent-moment",
+  "priority_revision": 7,
+  "base_commit": "6cf7a683f447b9f1e2333791907fd92be5009a63",
+  "original_card": {
+    "id": "independent-moment",
+    "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/staged544-mixed-fourth-entry/README.md",
+      "research/staged-fourth-mixture-ceiling/README.md",
+      "research/r437-two-window-carrier/README.md"
+    ],
+    "methods": [
+      "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.",
+      "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls."
+    ],
+    "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.",
+    "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.",
+    "allowed_variations": [
+      "Reconstruct either a source ledger or a numeric enclosure with a different method."
+    ],
+    "scope_change_triggers": [
+      "Importing the primary function and calling its output independent verification.",
+      "Calling an aggregate histogram or source archive an independently accepted physical supplier."
+    ],
+    "overlap_terms": [
+      "independent moment",
+      "rank histogram",
+      "exact enclosure",
+      "2979",
+      "rank7 joint endframes",
+      "paired extraction",
+      "joint lowering",
+      "4088",
+      "4091",
+      "4067",
+      "staged544-mixed-fourth-entry",
+      "staged-fourth-mixture-ceiling",
+      "r437-two-window-carrier"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.",
+        "evidence": "research/staged544-mixed-fourth-entry/README.md",
+        "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.",
+        "status": "author-checked",
+        "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.",
+        "evidence": "research/staged-fourth-mixture-ceiling/README.md",
+        "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.",
+        "status": "author-checked",
+        "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.",
+        "evidence": "research/r437-two-window-carrier/README.md",
+        "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.",
+        "status": "author-checked",
+        "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Close the exact 225 to 240 return gap for the frozen p2 full-history oracle model with a new source-bound projection moment.",
+  "scope_change_reason": "The released PR5587 handoff asks for the module rank needed to close this gap. A second moment proves the sharp integer optimum without the full rank.",
+  "bottleneck_link": "Prove that no same-contract repair can improve on 240 returns; redirect caller work to a changed paid input or observation.",
+  "budget_minutes": 120,
+  "stop_rule": "Stop when the lower integer bound meets the existing 240-return construction.",
+  "outcome": "completed",
+  "evidence": "PROOF.md; RESULT.json; verify.py",
+  "author": "Ali Romman with substantial OpenAI Codex assistance",
+  "ai_assistance": "Substantial OpenAI Codex assistance with proof, exact computation, code, verification and text.",
+  "open_questions": [
+    {
+      "question": "Can a changed original paid input evade the fixed-history deficit with a complete profitable bill?",
+      "why_it_matters": "The frozen oracle model has no return-count slack.",
+      "first_step": "Specify a literal changed input and rebuild the complete history module and invoice.",
+      "blocked_by": "A changed physical caller is outside this package."
+    }
+  ]
+}

research/p2-exact-oracle-repair/VERIFY.json

@@ -0,0 +1,32 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/p2-full-history-deficit/PROOF.md",
+    "research/p2-full-history-deficit/inputs/INVOLUTIVE-WORD.json.gz",
+    "research/p2-full-history-deficit/inputs/NORMALIZERS.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Source pins, involution, exact balanced projector, every signed product, second moment, sharp integer count and four rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "The same scientific checks with assertions disabled."
+    }
+  ]
+}