Prove sharp P104 common-metric defect constant 37 (no κ)

research/p104-metric-energy/PROOF.md

@@ -0,0 +1,148 @@
+# Sharp common-metric orthogonality energy on P104
+
+This scoped proof was produced by Nick Petalas. Apache-2.0.
+
+## Statement and normalization
+
+Let R be the 120 E8 root lines represented by unit vectors in R^8. Choose
+one sign on each line. The quantities below are independent of these signs.
+Let F and G be any two disjoint orthonormal frames contained in R, each with
+eight lines, and put P = R \ (F union G). Thus P has 104 lines.
+
+For a real symmetric 8 by 8 matrix A, write
+
+    A0 = A - tr(A) I/8,
+    E_P(A) = sum_{unordered {u,v} subset P, u perpendicular v} (u^T A v)^2,
+    D_F(A0) = sum_{u in F} (u^T A0 u)^2,
+    X_FG(A0) = sum_{u in F, v in G, u perpendicular v} (u^T A0 v)^2.
+
+All norms below are Frobenius norms. The new quantitative identity is
+
+    E_P(A) = 37 ||A0||^2 + (17/2) [D_F(A0) + D_G(A0)] + X_FG(A0).    (1)
+
+Consequently E_P(A) >= 37 ||A0||^2 for every such P. The constant 37 is
+sharp uniformly over this family. Section 4 gives an equality example and an
+invertible rational common deformation attaining it arbitrarily near identity.
+
+The claim is a scoped proof using exact finite E8 premises, with a finite
+equality certificate. It is not a statement about independent motions of the
+120 lines, arbitrary masked fitting matrices, or a complete supplier.
+
+## 1. Exact finite E8 premises
+
+The verifier constructs one integer vector r per line. Its squared norm is 8.
+There are 56 vectors 2(e_i +/- e_j), i < j, with the first nonzero coordinate
+positive, and 64 vectors (1,s_1,...,s_7), with s_i in {1,-1} and an even
+number of minus signs. Set u=r/sqrt(8).
+
+Two finite identities are checked directly, without a predecessor executable:
+
+    sum_{v in R, v perpendicular u} v v^T = 9(I-u u^T)              (2)
+    E_R(A) = 54 [||A||^2 - tr(A)^2/8] = 54 ||A0||^2.              (3)
+
+For (2), every one of the 120 stars has 63 lines. In integer coordinates the
+checked identity is sum s s^T = 72 I - 9 r r^T, with all 64 entries checked
+for every r. This proves (2) exactly.
+
+For (3), use the 36 independent entries a of symmetric A, with eight diagonal
+entries followed by the 28 upper off-diagonal entries. For an orthogonal pair
+r,s, the coefficient vector c satisfies c.a = r^T A s. The verifier sums
+H = sum c c^T over all 3,780 unordered orthogonal pairs. It checks all 1,296
+entries of
+
+    H = 3456 W - 432 t t^T,
+    W = diag(1 repeated 8 times, 2 repeated 28 times),
+    t = (1 repeated 8 times, 0 repeated 28 times).
+
+Since a^T W a = ||A||^2 and t.a = tr(A), division by 64 gives (3).
+This coefficient identity proves (3) for all real symmetric A, not only
+sampled matrices. No floating eigenvalue computation is a premise.
+
+## 2. Removing one frame
+
+Let L_F(A) be the energy of all orthogonal pairs of R having at least one
+endpoint in F. Summing (2) over u in F gives
+
+    sum_{u in F} sum_{v perpendicular u} (u^T A v)^2
+        = 9 [||A||^2 - sum_{u in F}(u^T A u)^2].
+
+Pairs internal to F occur twice in this sum and once in L_F. Because F is
+an orthonormal basis and A is symmetric, their energy is
+
+    sum_{unordered u,v in F} (u^T A v)^2
+        = (1/2) [||A||^2 - sum_{u in F}(u^T A u)^2].
+
+Therefore, for every frame F in R,
+
+    L_F(A) = (17/2) [||A||^2 - sum_{u in F}(u^T A u)^2].           (4)
+
+This argument quantifies over arbitrary frames. It does not infer a universal
+frame statement from the two frames used for the equality example.
+
+## 3. Removing two frames and the deformation consequence
+
+Disjointness gives the exact inclusion-exclusion identity
+
+    E_P(A) = E_R(A) - L_F(A) - L_G(A) + X_FG(A).
+
+All energies on orthogonal pairs are unchanged by adding a scalar matrix.
+Apply (3) and (4) to A0. Since 54 - 2(17/2) = 37, this is (1).
+Every residual term is a square, so the lower bound follows. Equality holds
+exactly when the two frame diagonals and every cross-frame orthogonal defect
+of A0 vanish.
+
+For any common real linear map T, put M=T^T T. The deformed inner product
+between originally orthogonal unit roots is (Tu)^T(Tv)=u^T M v. Thus
+
+    ||M - tr(M) I/8|| <= sqrt(E_P(M)/37).                          (5)
+
+In particular an invertible common T preserving every such zero has
+T^T T=cI with c>0. Exact qualitative rigidity has prior literature in this
+repository; the contribution here is the sharp quantitative identity (1)
+and its equality certificate. Equation (5) uses absolute inner products
+before any separate normalization of the deformed lines. It does not price
+metric changes, physical native maps or recursive work.
+
+## 4. Sharpness and rational common deformations
+
+In integer coordinates take F to be
+
+    2(e_0+e_1), 2(e_0-e_1), ..., 2(e_6+e_7), 2(e_6-e_7),
+
+and G to be the eight Sylvester rows
+
+    g_i[j] = (-1)^{popcount(i AND j)},  0 <= i,j < 8.
+
+Normalize all these vectors by sqrt(8). They are disjoint E8 frames. Let A
+have the following nonzero entries, together with their symmetric partners:
+
+    A[0,7]=-1, A[1,6]=-1, A[2,5]=1, A[3,4]=1.
+
+Then tr(A)=0, A^2=I and ||A||^2=8. Direct integer evaluation checks both
+zero frame diagonals and every required cross-frame zero. In this example
+P has 2,860 unordered orthogonal pairs and there are 32 orthogonal F-G pairs.
+Their literal energy sum is E_P(A)=296=37*8. The pair counts refer to this
+explicit example; they are not asserted for every pair of deleted frames.
+
+For any nonzero rational s with |s|<1, T_s=I+sA is invertible and
+
+    T_s^T T_s = (1+s^2)I+2sA.
+
+Its trace-free part is 2sA. By homogeneity it attains equality in (5), and
+T_s tends to I as s tends to zero. Hence the constant cannot increase even
+when restricted to positive definite common metrics from rational invertible
+maps arbitrarily near the identity.
+
+## Evidence boundary
+
+The standard-library verifier checks the full E8 coefficient identity and
+all stars, the two explicit frame deletions, all coefficients of (1) for
+the example, and the literal equality sum. The written removal argument
+supplies the quantifiers over every pair of disjoint frames and every real
+symmetric matrix. Seven controls discriminate omitted data, changed constants,
+invalid frame boundaries and a changed witness. Source hashes in its printed
+receipt bind the exact proof, implementation and metadata bytes.
+
+No human or proof-kernel review is claimed. The selected result, all five
+framework assumptions, native/dirty restoration, compiler, precision/tape,
+complete invoice and multiplication theorem are unchanged.

research/p104-metric-energy/README.md

@@ -0,0 +1,99 @@
+# Sharp common-metric orthogonality energy on P104
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+A common ambient deformation of a two-frame-punctured E8 configuration obeys
+an exact sum-of-squares constraint. For any real symmetric metric A, let
+A0=A-tr(A)I/8 and sum the squared values u^T A v over unordered orthogonal
+unit-root pairs remaining after two disjoint frames are removed. Then
+
+    E_P(A) = 37 ||A0||_F^2
+             + (17/2) sum_{u in the two frames}(u^T A0 u)^2
+             + sum_{orthogonal u,v in different deleted frames}(u^T A0 v)^2.
+
+Thus E_P(A) >= 37 ||A0||_F^2. An explicit rational symmetric involution has
+norm squared 8 and energy 296, proving the uniform constant sharp. Rational
+invertible common maps I+sA attain equality arbitrarily near identity.
+For M=T^T T, the defect energy bounds distance from a conformal metric by
+||M-tr(M)I/8||_F <= sqrt(E_P(M)/37).
+
+Claim type: scoped proof with exact finite premises and an equality
+certificate. [PROOF.md](PROOF.md) gives the quantified argument. [verify.py](verify.py)
+uses integer arithmetic and the standard library. This is a quantitative
+obstruction to changing the common ambient metric while keeping the E8
+orthogonality constraints approximately exact. It supplies no new kappa.
+
+## Evidence and reproduction
+
+From the repository root:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/p104-metric-energy/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/p104-metric-energy/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-metric-energy
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p104-metric-energy --check-source-history
+```
+
+Any CPython 3.12 interpreter can replace the local absolute path. Expected
+status: `PASS_P104_METRIC_ENERGY`. The checker enumerates 120 root lines,
+3,780 full orthogonal pairs and all 120 stars, checks 1,296 coefficients per
+quadratic identity, and evaluates all 2,860 orthogonal pairs of the explicit
+sharp example. Seven controls reject changed premises or stronger constants.
+The printed receipt is generated from current file hashes and computed values.
+No generated files or logs are written into the checkout.
+
+Local normal and optimized direct checks and both registered commands passed
+on CPython 3.12.15, macOS 27.0.1 arm64. Each direct command took 0.13 seconds
+in the initial timed run. Hosted CI is recorded separately in the PR body.
+
+The checker has fixed dimension eight, 36 symmetric coordinates and at most
+7,140 candidate root pairs. Every loop ranges over one of these fixed finite
+collections. Managed Python allocation is bounded by those inventories; no
+fixed-allocation claim is made. Six fixed callbacks are used only for rejecting
+controls. Functions have at most 26 physical lines. Warning-strict normal and
+optimized execution supply the local Python diagnostics; no external static
+analyzer was available. These are implementation limits, not extra premises
+of the mathematical theorem.
+
+## Scope, predecessors and novelty
+
+The exact E8 masked-realization questions and qualitative rigidity precede
+this result. Credit Brett Halligan / [PR1212](https://github.com/CrocSwap/integer-mult-bounds/pull/1212),
+Aaron Wang / PR1292, Josie Elliston / PR1389 and PR1399, and their retained
+E8 decoder lineage. Their broader decoder theorems are context, not premises
+replayed here. The root coordinates and elementary frame identities are
+standard. No predecessor implementation is imported or copied. The new step
+is the explicit quantitative energy identity, constant 37 and sharpness family.
+
+This changes the `complex-rank-shape-decoder` card to a geometry boundary
+question. It quantifies the absolute orthogonality defect forced by a common
+ambient deformation. It does not bound independent port motions,
+general fitting matrices, normalized correlation errors, helper topology or
+productive credits. The sharp example is not identified with the selected
+frame-pair orbit. The lower bound itself holds for every disjoint frame pair.
+No selected supplier replay, physical implementation, full signed invoice,
+formal proof-kernel check or complete multiplication theorem is supplied.
+Independent human and formal proof-kernel review are unclaimed.
+
+The selected-binding orientation command passed at base
+`2485805a6d47f36ea83ddde6327d453ac82d44dc`, priority revision 8. The selected
+conditional kappa remains 781451/250000000. Its five framework assumptions
+remain. Live open PRs, active Discussions, account history, claims, main
+READMEs and merged formula/object searches were checked before claiming;
+these bounded and sparse searches do not establish literature priority.
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19294832)
+records the original question.
+
+## Open next questions
+
+- Is 37 also the sharp constant for each individual disjoint-frame orbit,
+  including the selected P104 orbit? First fix that orbit and evaluate the
+  residual squares on trace-free symmetric matrices. This could strengthen
+  a source-specific obstruction. The present uniform theorem does not identify
+  the selected orbit's equality space.
+- Can a useful decoder change escape common-metric rigidity through independent
+  port motions while retaining legal labels and a favorable complete bill?
+  First exhibit one arbitrary-input local identity with its restored outputs
+  and actual consumer. Native realization and the complete invoice remain open.
+
+See [TASK.json](TASK.json) for the structured questions and scope declaration.

research/p104-metric-energy/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc",
+  "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"
+    }
+  ]
+}

research/p104-metric-energy/TASK.json

@@ -0,0 +1,81 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 8,
+  "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc",
+  "original_card": {
+    "id": "complex-rank-shape-decoder",
+    "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?",
+    "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",
+      "docs/research/recursive-invoice-preflight.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": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.",
+    "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": [
+      "coframe",
+      "signed moment",
+      "5693",
+      "5698"
+    ],
+    "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": "Sharp common-metric orthogonality energy on every two-disjoint-frame puncture of E8, with a rational equality family.",
+  "scope_change_reason": "Replace a complete coframe itinerary search with an originally posed quantitative geometry obstruction for one common ambient deformation. No complete signed invoice is claimed.",
+  "bottleneck_link": "The complex supplier binds. A common ambient metric deformation is a possible changed-geometry route; the sum-of-squares identity constrains its absolute orthogonality defects, without excluding independent line motions or new helper topologies.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first verified quantitative identity and sharp equality example; leave orbit-specific constants and different deformation models as open questions.",
+  "outcome": "completed",
+  "evidence": "PROOF.md and verify.py: exact E8 energy coefficients, 120 tight stars, frame deletion identities, sharp energy 296 and seven controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Is 37 sharp for every individual disjoint-frame orbit, including the selected P104 orbit?",
+      "why_it_matters": "An orbit-specific constant could strengthen the quantitative obstruction.",
+      "first_step": "Fix the selected frame-pair orbit and compute the kernel of the residual squares in equation (1).",
+      "blocked_by": "The present sharp example is not identified with the selected frame-pair orbit."
+    },
+    {
+      "question": "Can independently moved ports yield a legal improved decoder outside the common-metric class?",
+      "why_it_matters": "The common-metric obstruction does not cover this possible escape.",
+      "first_step": "Give one arbitrary-input local identity, restored boundary and physical consumer, then price its complete signed invoice.",
+      "blocked_by": "No native realization, complete caller or favorable complete bill is supplied here."
+    }
+  ]
+}

research/p104-metric-energy/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": 60,
+      "checks": "Exact all-E8 quadratic identity, all tight stars, frame removal, sum of squares, sharp equality and seven controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Same complete certificate and controls with Python assertions disabled."
+    }
+  ]
+}