Prove the E8 d=0 kernel floor and scoped rigid C1 bounds

research/e8-d0-root-swaps/SOURCES.json

@@ -0,0 +1,178 @@
+{
+  "schema_version": 1,
+  "base_commit": "997e6a9ca7b4f95d50e366f61412fd640d72a88a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"
+    },
+    {
+      "path": "research/root-unit-decoder-lemmas/README.md",
+      "usage": "provenance",
+      "pin": "head:08e134b4a0c7f04869dae703f2a2e688e53c44f0:research/root-unit-decoder-lemmas/README.md",
+      "git_blob": "de305484c78226a3f8da5f3277ced78974116fbb",
+      "sha256": "e3c856bc361a57cc2424c829001dba94e8f3a1bc8f6616f9c2f740e9665506a9",
+      "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/1590",
+      "contributor": "DreamingOfClouds",
+      "role": "Two-factor fitting lemma A; finite-order field extension is proved here."
+    },
+    {
+      "path": "research/one-sided-decoders-all-m/README.md",
+      "usage": "provenance",
+      "pin": "head:4c32ac3b88d63ad06d2b30e526aa07a12929db36:research/one-sided-decoders-all-m/README.md",
+      "git_blob": "614ff7397c3510ca740b09bf8846034fef16fa13",
+      "sha256": "7c22a8d73d8e2cf1ec9ce259035fe97be7261b0f71d5555ee50fc4b821872bf8",
+      "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/2816",
+      "contributor": "DreamingOfClouds",
+      "role": "One-sided lift model, greedy peeling and classical parabolic intersection argument C3."
+    },
+    {
+      "path": "research/one-sided-decoders-all-m/data/data.json",
+      "usage": "provenance",
+      "pin": "head:4c32ac3b88d63ad06d2b30e526aa07a12929db36:research/one-sided-decoders-all-m/data/data.json",
+      "git_blob": "2b799f9238d11018edb2aa6ac542024dfabcb1b3",
+      "sha256": "8e4b2a306dfe3499b9d2104753a4cb203e14fbfa94fda03f6a415da956ba642b",
+      "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/2816",
+      "contributor": "DreamingOfClouds",
+      "role": "Literal frame/root chart; provenance only, no imported executable."
+    },
+    {
+      "path": "research/one-sided-excess-three/README.md",
+      "usage": "provenance",
+      "pin": "head:18f7d4da808edb82d32e2081f869b8c993eca891:research/one-sided-excess-three/README.md",
+      "git_blob": "b8d8f987ca2235f6a8bc491441c689192f8a38ec",
+      "sha256": "3d53f0d808523baf07e1fefae5b15a2633d7662f864edbfea165f4b099316475",
+      "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/2862",
+      "contributor": "DreamingOfClouds",
+      "role": "Restricted carrier predecessor through kappa<=3; comparison boundary."
+    },
+    {
+      "path": "research/one-sided-padding-audit/PROOF.md",
+      "usage": "provenance",
+      "pin": "head:41826461eaceb25b77c026148b50b884e3c9780e:research/one-sided-padding-audit/PROOF.md",
+      "git_blob": "986e4b9464a5c2d0ec3455c45cd8e5551c5db43d",
+      "sha256": "5b8ef47091aaf09610b66194d834afa6724f0b8cadcf582a25705bc6933c35b7",
+      "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/3095",
+      "contributor": "CubeJerry",
+      "role": "Exact full/P112 support chart and field/normalization boundary; no certificates imported."
+    },
+    {
+      "path": "formal/lean/lean-toolchain",
+      "usage": "provenance",
+      "git_blob": "980709bbbae28702ec58c368b84fdf6638093c63",
+      "sha256": "d24fed434d3b13adfaab57724a0a7f270ea8bf1c818b5ae5cf25cbce24dd685c",
+      "role": "Pinned optional Lean verification environment; not a Python replay dependency."
+    },
+    {
+      "path": "formal/lean/lakefile.toml",
+      "usage": "provenance",
+      "git_blob": "b6abf04c93acf5ec745aa06aa1b503575b454186",
+      "sha256": "e5b1a6ff207cdd5e64b04ebfd944274d0ccde896f415bb578deb6090b4175ed5",
+      "role": "Pinned optional Lean verification environment; not a Python replay dependency."
+    },
+    {
+      "path": "formal/lean/lake-manifest.json",
+      "usage": "provenance",
+      "git_blob": "36433bd6697cc16c39ff03acf97431386cb0f2c2",
+      "sha256": "702bd5bcfbf4a4739bea2e1cba72b471e8f0680520c67547f5daf3d0f26b6ddf",
+      "role": "Pinned optional Lean verification environment; not a Python replay dependency."
+    }
+  ],
+  "source_binding": {
+    "model": "D8 plus half-integral E8, squared root norm 2; the full 120-root-line set and literal PR2816 ordered frame.",
+    "reuse": "All roots, labels, parabolics and normal profiles are regenerated; no predecessor census, PASS receipt or numerical linear-algebra result is a live input.",
+    "classical_facts": "Even unimodular E8 lattice of minimum norm 2; Weyl chamber/parabolic classification as stated and credited in PR2816 C3.",
+    "chart_check": "Exact rational comparison: all 120 E8 lines, all 112 nonframe lines and all 8 ordered frame representatives match the pinned PR2816 chart."
+  },
+  "related_work": [
+    {
+      "path": "research/one-sided-residue-closures/README.md",
+      "git_blob": "f59ffdc7189d4107483064d7644254efec45c67c",
+      "sha256": "a72e954568dcd4c95e486c478f7db97187385c0eb618dcfbc252ebb8c06326ed",
+      "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/2985",
+      "contributor": "DreamingOfClouds",
+      "role": "Full-E8 residue and geometric-cap context; no ledger kills imported.",
+      "head": "b07b0e3226bcbe32a90c1b43ab225c339086f7b5",
+      "status": "Documentary citation only; unmerged head, not an imported theorem or executable input. Hash checked locally; generic replay does not fetch or validate this external head."
+    },
+    {
+      "path": "research/one-sided-residue-closures/checks/gtab.py",
+      "git_blob": "104a4a872617615178112a5ebebdd8842e096701",
+      "sha256": "12e15b34873cd8ab8ef9ab6c7183711ade2e7fd3d0f2b10d7db8892d6db00393",
+      "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/2985",
+      "contributor": "DreamingOfClouds",
+      "role": "Confirms that the predecessor cap domain is full E8; no code copied or executed.",
+      "head": "b07b0e3226bcbe32a90c1b43ab225c339086f7b5",
+      "status": "Documentary citation only; unmerged head, not an imported theorem or executable input. Hash checked locally; generic replay does not fetch or validate this external head."
+    },
+    {
+      "path": "research/one-sided-padding-lemma/README.md",
+      "git_blob": "9fca2bc3897ab41120bcebf21aa5b963a55768ac",
+      "sha256": "b056475ca54f685a26ff1de6ad2986fd31c4d448e02bac428afd85b9cd2443d1",
+      "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/3074",
+      "contributor": "DreamingOfClouds",
+      "role": "Exact open d=0 nonzero-kernel obligation and downstream padding boundary.",
+      "head": "3cc41f260c31052c933d0e75ea02f2b7677e780c",
+      "status": "Documentary citation only; unmerged head, not an imported theorem or executable input. Hash checked locally; generic replay does not fetch or validate this external head."
+    },
+    {
+      "path": "research/p112-reduction-to-conjectures/CONJECTURES.md",
+      "git_blob": "4d41043842b30f4f741caf198f72d2920b70d382",
+      "sha256": "998a97f29bffbf4d2cfa8a0f36f4ce1e2759d992b1158b794cce58cabd796791",
+      "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/3154",
+      "contributor": "DreamingOfClouds",
+      "role": "Fresh C7 statement and separation from C1-C6; other closure claims are unimported and unaudited.",
+      "head": "708f0ad8928c383de8294aea3c126e9461d2066d",
+      "status": "Documentary citation only; unmerged head, not an imported theorem or executable input. Hash checked locally; generic replay does not fetch or validate this external head."
+    },
+    {
+      "path": "research/p112-reduction-to-conjectures/checks/L120D0/NOTES.md",
+      "git_blob": "5cb8ec47c8e86407cb012dd09d4e45c4f8b944b6",
+      "sha256": "fbd8caf1e697f2bd14f69f4a05b18be8c0113ffa97d8ac31a0d7c6bc23bcab20",
+      "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/3154",
+      "contributor": "DreamingOfClouds",
+      "role": "C7 exact inherited model and nonzero-kernel case in Section 4; alternative-frame lead not used.",
+      "head": "708f0ad8928c383de8294aea3c126e9461d2066d",
+      "status": "Documentary citation only; unmerged head, not an imported theorem or executable input. Hash checked locally; generic replay does not fetch or validate this external head."
+    },
+    {
+      "path": "research/p112-reduction-to-conjectures/checks/CONJG2/NOTES.md",
+      "git_blob": "6de90e8f0f0d80cad1c1228d8cd3f19d8f1569be",
+      "sha256": "0e2a78bd38f68fcfbf922c6eb6485b7f114c856a0db416d8f6823c5ebdc67740",
+      "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/3154",
+      "contributor": "DreamingOfClouds",
+      "head": "708f0ad8928c383de8294aea3c126e9461d2066d",
+      "role": "Conditional C1 premises: d=0 rigid basis shape, N8 and weight-eight high directions; source of the Section 2(ii) obligation resolved at kappa<=7.",
+      "status": "Documentary citation only; unmerged head. Its model premises are assumed explicitly in EXTENSION.md; the broader reduction is not imported or independently validated."
+    },
+    {
+      "path": "research/p112-reduction-to-conjectures/checks/CONJ-G/NOTES.md",
+      "git_blob": "fe45a56747f1bf91805e79283abe5c4279d9acae",
+      "sha256": "8609121fe3d6c0fbab5c2fbdfbd87fffb20a91452f1d3bcc3d0697a9b3dfabf8",
+      "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/3154",
+      "contributor": "DreamingOfClouds",
+      "head": "708f0ad8928c383de8294aea3c126e9461d2066d",
+      "role": "Conditional C1 premises: corrected-row duality, corrected ledger, pivot rebate and F1 support identities.",
+      "status": "Documentary citation only; unmerged head. Its model premises are assumed explicitly in EXTENSION.md; the broader reduction is not imported or independently validated."
+    },
+    {
+      "path": "research/p112-reduction-to-conjectures/checks/CONJ-G/f1.py",
+      "git_blob": "d4b294328062390b4fe3224040c57226746c8fc4",
+      "sha256": "4c995d4a58809f0c297c44809ec488b99e2bb11bb5a64c1818adcc2f58bde0e5",
+      "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/3154",
+      "contributor": "DreamingOfClouds",
+      "head": "708f0ad8928c383de8294aea3c126e9461d2066d",
+      "role": "Documentary definition of O_v from the complement and cardinality assertions at lines 2 and 10-12; no executable imported.",
+      "status": "Documentary citation only; unmerged head, checked locally. The local replay constructs O_v afresh and does not execute this source checker or its imports."
+    }
+  ],
+  "provenance_boundary": "The registered validator authenticates files against reachable Git objects. related_work records exact documentary citations outside the base ancestry; these rows are not replay dependencies or a claim of CI source validation."
+}