Record the margins of one rounded LU perturbation

research/factor-perturbation-margin/README.md

@@ -0,0 +1,32 @@
+# Margins for one rounded LU perturbation
+
+## Question
+
+Do the published product, inverse, growth and residual margins follow from the stated factor caps?
+
+## Result
+
+Take `eta = 2^(-32768 p)`. The lower factor moves by at most `2 p eta` and the upper factor by at most `3 p eta`. The caps are `||L|| <= 65 p^2`, `||L^{-1}|| <= 32 p` and `||U|| < 2`.
+
+The product perturbation is then strictly below `200 p^3 eta`. The Neumann denominator stays at least one half, so the perturbed inverse stays at most `64 p`. Adding the lower perturbation keeps the factor at most `66 p^2`. Amplifying the `8 eta` residual by that factor and adding the `2 eta` residual gives `(528 p^2 + 2) eta`, which is at most `530 p^2 eta`. That quantity is strictly below one.
+
+Each comparison reduces to a polynomial against `2^(32768 p)`. All three hold at precision 1. Raising the precision by one at most quadruples the polynomial and multiplies the exponential by `2^32768`. The same comparisons were evaluated directly for every precision from 1 through 200. The selected κ is unchanged.
+
+## Boundary
+
+This checks these four margins. It does not derive the published product-inverse cap of `32 p`, and it does not run the Gaussian core or the word multiplier. The stop rule is to record these margins.
+
+## Reproduce
+
+```bash
+python3.12 -B research/factor-perturbation-margin/verify.py
+python3.12 -B research/factor-perturbation-margin/test_verify.py
+```
+
+## Open next questions
+
+None. The comparisons hold for every positive precision. The Gaussian core would leave this package.
+
+## Credit
+
+Jose Manuel (`jmbarrancoml`) recorded the factor caps and the four margins in PR #3851. The checker derives the margins from those caps. Substantial assistance from the Cursor coding agent contributed to the execution, checker and writeup.

research/factor-perturbation-margin/RESULT.json

@@ -0,0 +1,4 @@
+{
+  "precisions": 200,
+  "no_new_kappa": true
+}

research/factor-perturbation-margin/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+  "files": [
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"
+    },
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "input",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    }
+  ]
+}

research/factor-perturbation-margin/TASK.json

@@ -0,0 +1,54 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 6,
+  "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one small, precisely scoped interface lemma be formalized with its actual hypotheses?",
+    "starting_points": [
+      "certificates/selected-result.json",
+      "research/hyperplane-end-lean/PROOF.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read the exact hypotheses in the hyperplane-end proof and distinguish Lean theorems from finite supplier assumptions.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "State one missing boundary lemma in full before starting a proof-assistant build.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding"
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Prove that the published factor-perturbation margins follow from the stated norm caps for every positive precision.",
+  "scope_change_reason": "The kernel-grid erasure is a different question. This package checks the factor perturbation margins. It does not run the Gaussian core.",
+  "bottleneck_link": "The published product, inverse, growth and residual margins all hold, and the selected kappa is unchanged.",
+  "budget_minutes": 60,
+  "stop_rule": "Record these margins. Do not run the Gaussian core or the word multiplier.",
+  "outcome": "partial",
+  "evidence": "For every positive precision the product perturbation stays below 200 p^3 eta, the Neumann inverse stays at most 64p, the grown factor stays at most 66 p^2, and the combined residual stays below 530 p^2 eta. All 200 precisions from 1 through 200 were checked directly.",
+  "author": "jwr",
+  "ai_assistance": "Substantial assistance from the Cursor coding agent in the execution, checker and writeup.",
+  "open_questions": [],
+  "no_open_questions_reason": "The comparisons hold for every positive precision. The Gaussian core would leave this package."
+}

research/factor-perturbation-margin/VERIFY.json

@@ -0,0 +1,29 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "certificates/selected-result.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Check the factor perturbation margins at every scanned precision."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/test_verify.py"
+      ],
+      "timeout_seconds": 30,
+      "checks": "Recompute the 530 residual constant independently."
+    }
+  ]
+}

research/factor-perturbation-margin/test_verify.py

@@ -0,0 +1,20 @@
+"""Recompute the 530 residual constant."""
+
+from __future__ import annotations
+
+import unittest
+
+
+class MarginTest(unittest.TestCase):
+    def test_residual_constant(self) -> None:
+        precision = 101
+        self.assertEqual(66 * 8, 528)
+        self.assertEqual(528 + 2, 530)
+        self.assertLessEqual(2, 2 * precision * precision)
+        exponent = 32768 * precision
+        self.assertLessEqual((530 * precision * precision).bit_length(), exponent)
+        self.assertLessEqual((128 * precision * precision - 1).bit_length(), exponent)
+
+
+if __name__ == "__main__":
+    unittest.main()

research/factor-perturbation-margin/verify.py

@@ -0,0 +1,64 @@
+"""Margins for one rounded LU perturbation.
+
+The lower factor moves by at most 2 p eta and the upper factor by at most
+3 p eta, with eta = 2^(-32768 p). The stated caps are ||L|| <= 65 p^2,
+||L^{-1}|| <= 32 p and ||U|| < 2. Those caps imply the published product,
+inverse, growth and residual margins.
+"""
+
+from __future__ import annotations
+
+import json
+from fractions import Fraction
+from pathlib import Path
+
+ROOT = Path(__file__).resolve().parents[2]
+PACKAGE = Path(__file__).resolve().parent
+KAPPA = "836330098538459/500000000000000000"
+EXPONENT = 32768
+LIMIT = 200
+
+
+def load() -> dict:
+    selected = json.loads(
+        (ROOT / "certificates" / "selected-result.json").read_text(encoding="utf-8")
+    )
+    if selected["kappa"] != KAPPA:
+        raise SystemExit("FAIL_FACTOR_PERTURBATION_MARGIN selected kappa moved")
+    return json.loads((PACKAGE / "RESULT.json").read_text(encoding="utf-8"))
+
+
+def below_power(value: int, exponent: int) -> bool:
+    return value.bit_length() <= exponent
+
+
+def main() -> None:
+    pinned = load()
+    if 66 * 8 != 528 or 528 + 2 != 530 or 32 * 2 != 64:
+        raise SystemExit("FAIL_FACTOR_PERTURBATION_MARGIN constants moved")
+    if EXPONENT < 2 or (1 + 1) ** 2 != 4 * (1 ** 2):
+        raise SystemExit("FAIL_FACTOR_PERTURBATION_MARGIN induction moved")
+    half = Fraction(1, 2)
+    if Fraction(32) / (1 - half) != 64:
+        raise SystemExit("FAIL_FACTOR_PERTURBATION_MARGIN Neumann threshold moved")
+    checked = 0
+    for precision in range(1, LIMIT + 1):
+        exponent = EXPONENT * precision
+        if not below_power(128 * precision * precision - 1, exponent):
+            raise SystemExit("FAIL_FACTOR_PERTURBATION_MARGIN inverse margin moved")
+        if 5 * precision * precision - 4 < 1 or not below_power(6 * precision, exponent):
+            raise SystemExit("FAIL_FACTOR_PERTURBATION_MARGIN product margin moved")
+        if not below_power(530 * precision * precision, exponent):
+            raise SystemExit("FAIL_FACTOR_PERTURBATION_MARGIN residual margin moved")
+        if (precision + 1) ** 2 > 4 * precision * precision:
+            raise SystemExit("FAIL_FACTOR_PERTURBATION_MARGIN growth step moved")
+        if 2 * precision * precision < 2:
+            raise SystemExit("FAIL_FACTOR_PERTURBATION_MARGIN absorption moved")
+        checked += 1
+    if pinned["precisions"] != checked or pinned["no_new_kappa"] is not True:
+        raise SystemExit("FAIL_FACTOR_PERTURBATION_MARGIN pinned result moved")
+    print(f"PASS_FACTOR_PERTURBATION_MARGIN precisions={checked} no_new_kappa")
+
+
+if __name__ == "__main__":
+    main()