Prove the F′ certificate ceiling 360/17 on P120, down from 24 (no new κ)

research/e8-fprime-uniform-ceiling/README.md

@@ -0,0 +1,124 @@
+# The F′ certificate ceiling on P120 is 360/17
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+**Claim type: scoped proof with an exact finite certificate. No new κ,
+supplier or frontier change.**
+
+[PR #2962](https://github.com/CrocSwap/integer-mult-bounds/pull/2962)
+(DreamingOfClouds, `research/decoder-certificate-ceilings`, §2.1) proves that
+every linear rank-counting certificate in its larger family **F′** gives at most
+**24** on the E8 unit P120, and records as OPEN whether the sharper Theorem C
+value **360/17** also bounds F′. This package settles that item for P120:
+
+> Among all sets of `k` lines of E8, the least number of frames meeting the set
+> is **765** for `k = 8` and **701** for `k = 7`. Both are attained only by
+> pairwise-orthogonal sets. Hence the least feasible uniform weight is
+> `y = 8/765`, and the uniform F′ ceiling on P120 is
+> `2025 · 8/765 = 360/17`.
+
+With the predecessor's fake-decoder argument, every F′ certificate on P120
+gives at most 360/17 ≈ 21.18, not 24. F′ is therefore no stronger than F on
+P120 under this witness, and both stop far below the targeted floor 72.
+
+## Model (unchanged from PR #2962)
+
+`L` is the 120 root lines of E8. A frame is a maximal set of pairwise-orthogonal
+lines. There are 2025 frames, each of size 8. For a set `D` of lines, `meet(D)`
+is the number of frames meeting `D`. A uniform fake decoder puts weight `y` on
+every frame and costs `2025 y`. For F′ it is feasible when
+
+```text
+y · meet(D) >= min(|D|, 8)    for every set D of lines.
+```
+
+PR #2962 takes `y = 8/675` from a Bonferroni bound and gets the ceiling 24.
+Its script requires only `min(|D|-1, 8)` for non-orthogonal `D`. The result
+below is the same under both forms, because every binding set is a frame.
+
+## Proof
+
+Write `μ_k` for the least `meet(D)` over `k`-sets and `p(D)` for the number of
+non-orthogonal pairs in `D`.
+
+1. **Incidences.** Every line lies in 135 frames, every orthogonal pair in 15,
+   and no non-orthogonal pair in any frame (checked).
+2. **Bonferroni.** `meet(D) >= 135k - 15·(C(k,2) - p(D))`. For `k <= 6` this
+   gives `μ_k >= 135, 255, 360, 450, 525, 585`.
+3. **Pair caps.** A frame meets 765 frames and any 7 of its lines meet 701. By
+   step 2, an 8-set with `meet <= 765` has `p <= 7`. A 7-set with `meet <= 701`
+   has `p <= 4`.
+4. **Orthogonal cores.** By Caro–Wei, a graph on `k` vertices with `P` edges
+   has an independent set of size at least `k²/(k+2P)`. Apply it to the
+   non-orthogonality graph of `D`. Every candidate 8-set then contains an
+   orthogonal triple, and every candidate 7-set contains an orthogonal 4-set.
+5. **Symmetry.** The reflections in the 120 roots permute the lines and the
+   frames (checked), so they preserve `meet` and `p`. Under the group they
+   generate, orthogonal triples form one orbit and orthogonal 4-sets form two.
+6. **Search.** Every extension of each orbit representative within the pair cap
+   is enumerated exhaustively. The least meet is 765 for `k = 8` and 701 for
+   `k = 7`. Every minimiser has `p = 0`.
+7. **Ceiling.** `8/765` exceeds `k/μ_k` for every `k <= 7`, where the bound
+   uses step 2 for `k <= 6` and `7/701` for `k = 7`. For `|D| >= 9`, `meet(D) >= μ_8`. The least
+   feasible uniform weight is therefore `8/765`, and a frame makes it tight.
+   `2025 · 8/765 = 360/17`.
+
+**Positive control.** The same search on E7 (63 lines, 135 frames of size 7)
+reproduces the predecessor's MILP minima 55, 62 and 68 for `k = 5, 6, 7`. There
+the least meet 68 is below the frame value 71, attained by sets with six
+non-orthogonal pairs. So the search does find non-frame minimisers where they
+exist. It also shows that uniform weights cannot reach Theorem C's 945/71 on E7.
+That gap does not occur on P120.
+
+## Reproduce
+
+From the repository root, with the repository interpreter (CPython 3.12.15,
+standard library only):
+
+```sh
+python3.12 -W error -I -B research/e8-fprime-uniform-ceiling/verify.py
+python3.12 -W error -I -O -B research/e8-fprime-uniform-ceiling/verify.py
+python3.12 -B scripts/research_package.py --package research/e8-fprime-uniform-ceiling
+```
+
+Expected: `PASS_E8_FPRIME_UNIFORM_CEILING mu8 765 ceiling 360/17 no_new_kappa`.
+Each run takes about 35 seconds. `--emit` prints the recomputed
+[RESULT.json](RESULT.json). A normal run requires byte equality with it.
+The checks use `require()`, so they stay active under `-O`. A rejecting
+control confirms that weight `8/766` violates a frame's constraint.
+
+## Scope and limits
+
+- Uniform frame weights only. A non-uniform F′ certificate is bounded by this
+  witness. Whether 360/17 is the exact F′ optimum is not decided.
+- P120 only. P112, where the proven F′ ceiling is still 15968/667, is not
+  computed.
+- Theorem C, the F′ constraint form and the fake-decoder argument are cited
+  from PR #2962. They are not replayed here.
+- This is a statement about certificate families. It gives no decoder floor,
+  supplier, invoice or κ.
+
+## Open next questions
+
+1. **P112.** Does 15968/757 also bound F′ on P112? First step: the stabilizer
+   of the removed frame acts on the 112 lines. Use it with these pair caps and
+   orthogonal cores for `k = 7, 8`. Blocker: P112 is not line-transitive, its
+   1996 maximal orthogonal sets have mixed sizes, and no generators are
+   supplied here.
+2. **Non-uniform optimum.** Is 360/17 the exact F′ optimum on P120? First
+   step: an orbit-reduced linear program over W(E8) orbits of line sets, with
+   an exact dual.
+3. **E7 and E6.** On E7, uniform weights stop at 945/68 because a non-frame
+   7-set meets only 68 frames. Can non-uniform weights reach 945/71 there?
+
+## Credit
+
+DreamingOfClouds's PR #2962 supplies the certificate families F and F′,
+Theorem C, the fake-decoder argument, the F′ constraint, the Bonferroni
+ceiling 24 and the E7/E6 MILP values used as a control. The charging
+certificate shape is from #1977 and #798, as credited there. Those results are
+cited, not rechecked. The new contribution is the exact least meets for
+`k = 7, 8`, the orbit-reduced proof that frames minimise them, and the
+resulting 360/17 ceiling for F′ on P120. No predecessor credit line or frozen
+package is changed. Independent human and formal proof-kernel review are
+unclaimed.

research/e8-fprime-uniform-ceiling/RESULT.json

@@ -0,0 +1,70 @@
+{
+  "binding_size": 8,
+  "bonferroni_floor_k_le_6": {
+    "1": 135,
+    "2": 255,
+    "3": 360,
+    "4": 450,
+    "5": 525,
+    "6": 585
+  },
+  "e7_positive_control": {
+    "5": {
+      "frame_subset": 55,
+      "minimiser_nonorthogonal_pairs": [
+        0,
+        1,
+        2
+      ],
+      "minimum": 55
+    },
+    "6": {
+      "frame_subset": 63,
+      "minimiser_nonorthogonal_pairs": [
+        3,
+        4
+      ],
+      "minimum": 62
+    },
+    "7": {
+      "frame_subset": 71,
+      "minimiser_nonorthogonal_pairs": [
+        6
+      ],
+      "minimum": 68
+    }
+  },
+  "exact_minimum_meet": {
+    "7": {
+      "core_orbits": 2,
+      "k": 7,
+      "minimiser_nonorthogonal_pairs": [
+        0
+      ],
+      "minimum": 701,
+      "orthogonal_core": 4,
+      "pair_cap": 4,
+      "seed_frame_subset": 701
+    },
+    "8": {
+      "core_orbits": 1,
+      "k": 8,
+      "minimiser_nonorthogonal_pairs": [
+        0
+      ],
+      "minimum": 765,
+      "orthogonal_core": 3,
+      "pair_cap": 7,
+      "seed_frame_subset": 765
+    }
+  },
+  "maximal_orthogonal_sets": 2025,
+  "previous_proven_fprime_ceiling": "24",
+  "sets_through_line": 135,
+  "sets_through_nonorthogonal_pair": 0,
+  "sets_through_orthogonal_pair": 15,
+  "theorem_c_f_ceiling": "360/17",
+  "uniform_fprime_ceiling": "360/17",
+  "uniform_weight": "8/765",
+  "unit": "P120 (all 120 E8 root lines)"
+}

research/e8-fprime-uniform-ceiling/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/decoder-certificate-ceilings/README.md",
+      "usage": "provenance",
+      "git_blob": "bf5a8fd5d353c304aa42e3333a9799ba082122bb",
+      "sha256": "22c0f68e0b553ce70054ece41a13b18b6e3fb45d84165ec6f0bfe78e2f39cc75"
+    }
+  ]
+}

research/e8-fprime-uniform-ceiling/TASK.json

@@ -0,0 +1,97 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 8,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "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": "Settle the OPEN item of PR2962 (research/decoder-certificate-ceilings, section 2.1) for the unit P120: compute the exact least number of maximal orthogonal sets meeting any k lines of E8 for k = 7, 8 and decide whether the uniform-weight fake decoder certifies the Theorem C value 360/17 for the larger family F'.",
+  "scope_change_reason": "This is an open question posed by the predecessor package about ceilings for linear rank-counting certificates of the E8 decoder cost. It sharpens a proven certificate ceiling (24 to 360/17) rather than constructing or pricing a changed decoder.",
+  "bottleneck_link": "Side result. It shows that the larger certificate family F' is no stronger than F on P120 under uniform weights, so linear rank-counting certificates of this shape still stop at 360/17, far below the targeted floor 72. No supplier, invoice or kappa is affected.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the exact P120 uniform ceiling and an E7 positive control. Do not extend to P112, non-uniform weights or the true decoder floor.",
+  "outcome": "completed",
+  "evidence": "Standard-library verifier: E8 lines and 2025 frames, incidence counts 135/15/0, reflection automorphisms, Bonferroni pair caps, Caro-Wei orthogonal cores, orbit representatives and exhaustive extension search for k = 7, 8; exact Fraction ceiling; E7 control reproduces the predecessor MILP minima 55, 62, 68; RESULT.json byte equality.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Does 15968/757 also bound F' on P112?",
+      "why_it_matters": "It would settle the same OPEN item for the second unit, where the proven F' ceiling is still 15968/667.",
+      "first_step": "Compute exact least meets for k = 7, 8 over the 112 lines with automorphisms of P112 (the stabilizer of the removed frame), then reuse this pair-cap and orthogonal-core search.",
+      "blocked_by": "P112 is not line-transitive and its 1996 maximal orthogonal sets have mixed sizes; generators of the frame stabilizer are not supplied here."
+    },
+    {
+      "question": "Is 360/17 the exact optimum of F' on P120 over non-uniform weights?",
+      "why_it_matters": "The uniform witness gives an upper ceiling; a dual certificate would show no F' certificate exceeds a smaller value.",
+      "first_step": "Write the F' ceiling as an orbit-reduced linear program over W(E8) orbits of line sets and solve it exactly.",
+      "blocked_by": "The F' constraint family ranges over all line sets; an exact orbit LP is not built here."
+    },
+    {
+      "question": "Does the uniform F' ceiling on E6 or E7 improve beyond the predecessor's MILP-computed values with non-uniform weights?",
+      "why_it_matters": "On E7 the least meet 68 lies below the frame value 71, so uniform weights there cannot reach the Theorem C value 945/71.",
+      "first_step": "Use the same orbit LP on W(E7).",
+      "blocked_by": "No non-uniform witness or dual is computed."
+    }
+  ],
+  "claim_type": "scoped proof with an exact finite certificate",
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19220126",
+  "unrun_obligations": [
+    "No replay of PR2962's Theorem C witness, Bonferroni or MILP checks; Theorem C and the F' constraint form are cited premises.",
+    "No P112 computation, non-uniform F' optimum, true decoder floor, supplier, Lean, Docker or complete multiplication theorem."
+  ],
+  "environment": {
+    "python": "Python 3.12.15",
+    "platform": "Darwin arm64"
+  }
+}

research/e8-fprime-uniform-ceiling/VERIFY.json

@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "E8 frames and incidence counts, reflection automorphisms, exact least meets for k = 7, 8 by pair caps, Caro-Wei cores and orbit search, exact 360/17 ceiling, rejecting weight control, E7 positive control and RESULT.json equality."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-I",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "The same exact checks under python -O; contracts use explicit require() and stay active."
+    }
+  ]
+}