Joint frame compiler: conditional κ = 4.669442391e-5

Makefile

@@ -295,3 +295,9 @@ formal-historical-verify:
 formal-gaussian-verify:
 	$(MAKE) -C research/gaussian-parity-synthesis verify
 	python3 scripts/check_lean_axioms.py --project research/gaussian-parity-synthesis --audit research/gaussian-parity-synthesis/AuditAll.lean
+
+.PHONY: skip-frame-verify
+skip-frame-verify:
+	python3 scripts/experiments/verify_skip_frame.py
+
+verify-community: skip-frame-verify

NOTICE

@@ -203,3 +203,16 @@ Ryan S / princezuda contributes historical Lean certificate arithmetic, algebrai
 frame/movement/guard lemmas and independent paired-circuit checks (#26). Original
 source notices and historical snapshots are preserved. Neither formal package
 claims a full formal proof of the multiplication algorithm or a new kappa.
+
+Joint frame compilation of skip-prefix strips
+
+The local compiler and exact finite witnesses were prepared by eumemic with
+substantial OpenAI Codex assistance. Avi Eisenberg / ikeboy with Anthropic
+Claude assistance supplied the unmodified PR #53 skip-prefix producer.
+The pinned PR #48 pipeline is Chafik Boukhalfa's contribution, incorporating
+Rohan Arun, RaD / hipotures, icekylinx, Dominik Scholz, James Chang,
+Zhihao Chen, Aurel Prosz / Paureel, Swapnil Jain, eumemic, Douglas Colkitt,
+OpenAI, David Harvey, Joris van der Hoeven and the earlier contributors
+credited in the retained sources. See references/frame-compiler/pr48/NOTICE
+and references/frame-compiler/pr53/NOTICE for their original attribution.
+No authorship or review by those predecessors is claimed for this compiler.

certificates/skip-frame-compiler.json

@@ -0,0 +1,223 @@
+{
+  "axes": {
+    "23": {
+      "compiled": {
+        "all_physical_frame_inclusions": true,
+        "baseline_pr48_roles": 36432,
+        "baseline_pr53_roles": 32946,
+        "complete_dirty_basis_both_orientations": true,
+        "dirty_basis_vectors": 34958,
+        "elementary_xors": 111687,
+        "h": 23,
+        "histogram": {
+          "0": 224441,
+          "1": 41963,
+          "10": 3066,
+          "11": 199,
+          "12": 2842,
+          "13": 182,
+          "14": 3698,
+          "15": 693,
+          "16": 2028,
+          "17": 464,
+          "18": 8238,
+          "19": 4308,
+          "2": 37406,
+          "21": 28,
+          "22": 23,
+          "3": 6490,
+          "4": 17479,
+          "5": 8001,
+          "6": 4554,
+          "7": 1783,
+          "8": 3533,
+          "9": 643
+        },
+        "mode": {
+          "matching": true,
+          "reclaim": true
+        },
+        "rank_mass": 723074,
+        "roles": 31416,
+        "scalar": {
+          "additions": 40329,
+          "all_additions_disjoint": true,
+          "all_partial_outputs_exact": true,
+          "circuit_sha256": "0e309c2023b2832f82badf010649417acfa0cf423b3137c25babf0d7746eb32c",
+          "every_node_has_common_point": true,
+          "h": 23,
+          "inputs": 1771,
+          "merged_additions": 5379,
+          "partial_outputs": 5336,
+          "roles": 45665
+        },
+        "source_pr53_head": "3ffd4021995c959ac02d12920e0279ae97dd03c7",
+        "stats": {
+          "augmentations": 165,
+          "clearing_xors": 3184,
+          "matched": 12029,
+          "multi_node_regions": 4324,
+          "reclaimed": 1530,
+          "regions": 36626
+        },
+        "word_path": "/private/tmp/frame-pr53-compiler/word23.json.gz",
+        "word_sha256": "15c6ed702033d3bc55c17bee42bbaf7ed45245c3cf1ea14e9eedd225f8af9823"
+      },
+      "gzip_sha256": "15c6ed702033d3bc55c17bee42bbaf7ed45245c3cf1ea14e9eedd225f8af9823",
+      "replay": {
+        "elementary_xors": 111687,
+        "full_basis_vectors": 34958,
+        "h": 23,
+        "histogram": {
+          "0": 119612,
+          "1": 41963,
+          "10": 3066,
+          "11": 199,
+          "12": 2842,
+          "13": 182,
+          "14": 3698,
+          "15": 693,
+          "16": 2028,
+          "17": 464,
+          "18": 8238,
+          "19": 4308,
+          "2": 37406,
+          "21": 28,
+          "22": 23,
+          "3": 6490,
+          "4": 17479,
+          "5": 8001,
+          "6": 4554,
+          "7": 1783,
+          "8": 3533,
+          "9": 643
+        },
+        "output_roles": 5336,
+        "rank_mass": 723074,
+        "roles": 31416,
+        "status": "independent serialized word, exact frames, full input and dirty basis both orientations PASS",
+        "word_length": 471542
+      },
+      "word_sha256": "1e1160caecbdfbb75961bf7a88a53189217840262c6bb724248c38f2b8f4c61a"
+    },
+    "25": {
+      "compiled": {
+        "all_physical_frame_inclusions": true,
+        "baseline_pr48_roles": 48329,
+        "baseline_pr53_roles": 43409,
+        "complete_dirty_basis_both_orientations": true,
+        "dirty_basis_vectors": 45864,
+        "elementary_xors": 148996,
+        "h": 25,
+        "histogram": {
+          "0": 298212,
+          "1": 54790,
+          "10": 3160,
+          "11": 356,
+          "12": 3951,
+          "13": 336,
+          "14": 2971,
+          "15": 155,
+          "16": 4523,
+          "17": 1151,
+          "18": 2722,
+          "19": 267,
+          "2": 49085,
+          "20": 10833,
+          "21": 5514,
+          "23": 36,
+          "24": 25,
+          "3": 8302,
+          "4": 24492,
+          "5": 10155,
+          "6": 4451,
+          "7": 2776,
+          "8": 5261,
+          "9": 696
+        },
+        "mode": {
+          "matching": true,
+          "reclaim": true
+        },
+        "rank_mass": 1032200,
+        "roles": 41264,
+        "scalar": {
+          "additions": 53475,
+          "all_additions_disjoint": true,
+          "all_partial_outputs_exact": true,
+          "circuit_sha256": "52eca99391ab5b7cf85ee80e20846570cfc7b8812e2949990f4f081d6c67bfd4",
+          "every_node_has_common_point": true,
+          "h": 25,
+          "inputs": 2300,
+          "merged_additions": 7008,
+          "partial_outputs": 6925,
+          "roles": 60400
+        },
+        "source_pr53_head": "3ffd4021995c959ac02d12920e0279ae97dd03c7",
+        "stats": {
+          "augmentations": 231,
+          "clearing_xors": 5425,
+          "matched": 16341,
+          "multi_node_regions": 5875,
+          "reclaimed": 2145,
+          "regions": 48675
+        },
+        "word_path": "/private/tmp/frame-pr53-compiler/word25.json.gz",
+        "word_sha256": "cd60a7721d09dd76ed4abd5d003f28f72fb27c2b055f73fc02bc3f6d2e51705c"
+      },
+      "gzip_sha256": "cd60a7721d09dd76ed4abd5d003f28f72fb27c2b055f73fc02bc3f6d2e51705c",
+      "replay": {
+        "elementary_xors": 148996,
+        "full_basis_vectors": 45864,
+        "h": 25,
+        "histogram": {
+          "0": 159398,
+          "1": 54790,
+          "10": 3160,
+          "11": 356,
+          "12": 3951,
+          "13": 336,
+          "14": 2971,
+          "15": 155,
+          "16": 4523,
+          "17": 1151,
+          "18": 2722,
+          "19": 267,
+          "2": 49085,
+          "20": 10833,
+          "21": 5514,
+          "23": 36,
+          "24": 25,
+          "3": 8302,
+          "4": 24492,
+          "5": 10155,
+          "6": 4451,
+          "7": 2776,
+          "8": 5261,
+          "9": 696
+        },
+        "output_roles": 6925,
+        "rank_mass": 1032200,
+        "roles": 41264,
+        "status": "independent serialized word, exact frames, full input and dirty basis both orientations PASS",
+        "word_length": 628184
+      },
+      "word_sha256": "206f27211025bea997f8c546b0e1dd40675e0d8d77febf65040554ac1b1ba900"
+    }
+  },
+  "source": {
+    "attribution": "Avi Eisenberg / ikeboy with Anthropic Claude assistance: skip-prefix layout; inherited authors retained in NOTICE and source headers. Local joint frame synthesis uses OpenAI Codex assistance.",
+    "files": {
+      "LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4",
+      "NOTICE": "40a3066696e0de23e46b565460d19e85b435990ba837da5c1ca925335f4ba829",
+      "research/skip-strips/skip_graph.py": "03ee019cdaf73391455aaf4f5dcb4873f4fdcb278179b296c02ea39eafd047e4"
+    },
+    "head": "3ffd4021995c959ac02d12920e0279ae97dd03c7",
+    "repository": "ikeboy/integer-mult-bounds",
+    "scope": "Unmodified skip-prefix graph and attribution; shared circuit code and analytic/data interfaces are the byte-identical pinned PR48 sources in ../pr48.",
+    "shared_dependency_manifest": "../pr48/SOURCE.json",
+    "shared_dependency_manifest_sha256": "6ccc673f88d3650d75ed600b082fe2fc2866dd88a172d182a38c1d0cd27d24b3",
+    "source_pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/53"
+  },
+  "status": "Exact finite scalar/frame word; full recursive profiles and assembly separate"
+}