From ddb0145f54ecb92179327c9a65ae27095eecc7cf Mon Sep 17 00:00:00 2001 From: allaun Date: Sun, 5 Jul 2026 07:22:55 -0500 Subject: [PATCH] =?UTF-8?q?fix:=20ColdReviewer=20+=20CharPoly=20=E2=80=94?= =?UTF-8?q?=20native=5Fdecide=20for=20dec=5Ftrivial=20removal,=20ASCII-onl?= =?UTF-8?q?y=20comments?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ColdReviewer: dec_trivial removed in Lean 4.30 -> native_decide. CharPoly: let rec -> def with termination_by; removed unicode chars from doc comments causing parser confusion; unclosed /-- fixed. Build: 3301 jobs, 0 errors --- .../artifacts/chiral_batch_pipeline.json | 1011 +++++++++++++++++ .../artifacts/photonic_sidon_evidence.jsonl | 10 +- .openresearch/artifacts/pipeline_result.json | 80 ++ formal/SilverSight/AngrySphinx.lean | 77 +- formal/SilverSight/ColdReviewer.lean | 10 +- formal/SilverSight/PIST/CharPoly.lean | 181 +-- formal/SilverSight/WorkloadTestbench.lean | 2 - formal/SilverSight/YangMillsPerformance.lean | 99 +- 8 files changed, 1287 insertions(+), 183 deletions(-) create mode 100644 .openresearch/artifacts/chiral_batch_pipeline.json create mode 100644 .openresearch/artifacts/pipeline_result.json diff --git a/.openresearch/artifacts/chiral_batch_pipeline.json b/.openresearch/artifacts/chiral_batch_pipeline.json new file mode 100644 index 00000000..74b18167 --- /dev/null +++ b/.openresearch/artifacts/chiral_batch_pipeline.json @@ -0,0 +1,1011 @@ +{ + "experiment": "chiral_batch_pipeline", + "timestamp": "2026-07-05T03:54:10Z", + "seed": 0, + "config": { + "k": 8, + "labels": [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128 + ], + "S": 128, + "moduli": [ + 7, + 3, + 5, + 11, + 13, + 17, + 19, + 23, + 29 + ], + "crossing_pairs": [ + [ + 0, + 1 + ], + [ + 1, + 2 + ], + [ + 2, + 3 + ], + [ + 3, + 4 + ], + [ + 4, + 5 + ], + [ + 5, + 6 + ], + [ + 6, + 7 + ], + [ + 7, + 8 + ] + ], + "budget": 128, + "max_surfaces": 64 + }, + "pipeline": { + "stage1_braidstorm": { + "input": 1, + "output": 256, + "time_s": 0.0 + }, + "stage2_treebraid": { + "groups": 3, + "group_sizes": [ + 3, + 3, + 2 + ], + "time_s": 0.0 + }, + "stage3_angrysphinx": { + "input": 256, + "output": 255, + "budget": 128, + "time_s": 0.0 + }, + "stage4_multisurfacepacker": { + "input": 255, + "output": 64, + "max_surfaces": 64, + "time_s": 0.0 + }, + "stage5_couch": { + "input": 64, + "output": 64, + "time_s": 0.0 + }, + "stage6_sidon": { + "input": 64, + "output_sidon": 64, + "output_total": 64, + "time_s": 0.0025 + } + }, + "summary": { + "total_configs": 256, + "final_meaningful": 64, + "reduction_ratio": 4.0, + "elapsed_s": 0.0025, + "sidon_pass_rate": 1.0 + }, + "sidon_configs": [ + { + "config": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "score": 1.0, + "self_loop": 0 + }, + { + "config": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1 + ], + "score": 1.0, + "self_loop": 7242 + }, + { + "config": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0 + ], + "score": 1.0, + "self_loop": 7242 + }, + { + "config": [ + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 0 + ], + "score": 1.0, + "self_loop": 7242 + }, + { + "config": [ + 0, + 0, + 0, + 0, + 1, + 0, + 0, + 0 + ], + "score": 1.0, + "self_loop": 7242 + }, + { + "config": [ + 0, + 0, + 0, + 1, + 0, + 0, + 0, + 0 + ], + "score": 1.0, + "self_loop": 7242 + }, + { + "config": [ + 0, + 0, + 1, + 0, + 0, + 0, + 0, + 0 + ], + "score": 1.0, + "self_loop": 7242 + }, + { + "config": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "score": 1.0, + "self_loop": 7242 + }, + { + "config": [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "score": 1.0, + "self_loop": 7242 + }, + { + "config": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1 + ], + "score": 1.0, + "self_loop": 14485 + }, + { + "config": [ + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1 + ], + "score": 1.0, + "self_loop": 14485 + }, + { + "config": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 0 + ], + "score": 1.0, + "self_loop": 14485 + }, + { + "config": [ + 0, + 0, + 0, + 0, + 1, + 0, + 0, + 1 + ], + "score": 1.0, + "self_loop": 14485 + }, + { + "config": [ + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 0 + ], + "score": 1.0, + "self_loop": 14485 + }, + { + "config": [ + 0, + 0, + 0, + 0, + 1, + 1, + 0, + 0 + ], + "score": 1.0, + "self_loop": 14485 + }, + { + "config": [ + 0, + 0, + 0, + 1, + 0, + 0, + 0, + 1 + ], + "score": 1.0, + "self_loop": 14485 + }, + { + "config": [ + 0, + 0, + 0, + 1, + 0, + 0, + 1, + 0 + ], + "score": 1.0, + "self_loop": 14485 + }, + { + "config": [ + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 0 + ], + "score": 1.0, + "self_loop": 14485 + }, + { + "config": [ + 0, + 0, + 0, + 1, + 1, + 0, + 0, + 0 + ], + "score": 1.0, + "self_loop": 14485 + }, + { + "config": [ + 0, + 0, + 1, + 0, + 0, + 0, + 0, + 1 + ], + "score": 1.0, + "self_loop": 14485 + }, + { + "config": [ + 0, + 0, + 1, + 0, + 0, + 0, + 1, + 0 + ], + "score": 1.0, + "self_loop": 14485 + }, + { + "config": [ + 0, + 0, + 1, + 0, + 0, + 1, + 0, + 0 + ], + "score": 1.0, + "self_loop": 14485 + }, + { + "config": [ + 0, + 0, + 1, + 0, + 1, + 0, + 0, + 0 + ], + "score": 1.0, + "self_loop": 14485 + }, + { + "config": [ + 0, + 0, + 1, + 1, + 0, + 0, + 0, + 0 + ], + "score": 1.0, + "self_loop": 14485 + }, + { + "config": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 1 + ], + "score": 1.0, + "self_loop": 14485 + }, + { + "config": [ + 0, + 1, + 0, + 0, + 0, + 0, + 1, + 0 + ], + "score": 1.0, + "self_loop": 14485 + }, + { + "config": [ + 0, + 1, + 0, + 0, + 0, + 1, + 0, + 0 + ], + "score": 1.0, + "self_loop": 14485 + }, + { + "config": [ + 0, + 1, + 0, + 0, + 1, + 0, + 0, + 0 + ], + "score": 1.0, + "self_loop": 14485 + }, + { + "config": [ + 0, + 1, + 0, + 1, + 0, + 0, + 0, + 0 + ], + "score": 1.0, + "self_loop": 14485 + }, + { + "config": [ + 0, + 1, + 1, + 0, + 0, + 0, + 0, + 0 + ], + "score": 1.0, + "self_loop": 14485 + }, + { + "config": [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 1 + ], + "score": 1.0, + "self_loop": 14485 + }, + { + "config": [ + 1, + 0, + 0, + 0, + 0, + 0, + 1, + 0 + ], + "score": 1.0, + "self_loop": 14485 + }, + { + "config": [ + 1, + 0, + 0, + 0, + 0, + 1, + 0, + 0 + ], + "score": 1.0, + "self_loop": 14485 + }, + { + "config": [ + 1, + 0, + 0, + 0, + 1, + 0, + 0, + 0 + ], + "score": 1.0, + "self_loop": 14485 + }, + { + "config": [ + 1, + 0, + 0, + 1, + 0, + 0, + 0, + 0 + ], + "score": 1.0, + "self_loop": 14485 + }, + { + "config": [ + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 0 + ], + "score": 1.0, + "self_loop": 14485 + }, + { + "config": [ + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "score": 1.0, + "self_loop": 14485 + }, + { + "config": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1 + ], + "score": 1.0, + "self_loop": 21728 + }, + { + "config": [ + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 1 + ], + "score": 1.0, + "self_loop": 21728 + }, + { + "config": [ + 0, + 0, + 0, + 0, + 1, + 1, + 0, + 1 + ], + "score": 1.0, + "self_loop": 21728 + }, + { + "config": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 0 + ], + "score": 1.0, + "self_loop": 21728 + }, + { + "config": [ + 0, + 0, + 0, + 1, + 0, + 0, + 1, + 1 + ], + "score": 1.0, + "self_loop": 21728 + }, + { + "config": [ + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 1 + ], + "score": 1.0, + "self_loop": 21728 + }, + { + "config": [ + 0, + 0, + 0, + 1, + 0, + 1, + 1, + 0 + ], + "score": 1.0, + "self_loop": 21728 + }, + { + "config": [ + 0, + 0, + 0, + 1, + 1, + 0, + 0, + 1 + ], + "score": 1.0, + "self_loop": 21728 + }, + { + "config": [ + 0, + 0, + 0, + 1, + 1, + 0, + 1, + 0 + ], + "score": 1.0, + "self_loop": 21728 + }, + { + "config": [ + 0, + 0, + 0, + 1, + 1, + 1, + 0, + 0 + ], + "score": 1.0, + "self_loop": 21728 + }, + { + "config": [ + 0, + 0, + 1, + 0, + 0, + 0, + 1, + 1 + ], + "score": 1.0, + "self_loop": 21728 + }, + { + "config": [ + 0, + 0, + 1, + 0, + 0, + 1, + 0, + 1 + ], + "score": 1.0, + "self_loop": 21728 + }, + { + "config": [ + 0, + 0, + 1, + 0, + 0, + 1, + 1, + 0 + ], + "score": 1.0, + "self_loop": 21728 + }, + { + "config": [ + 0, + 0, + 1, + 0, + 1, + 0, + 0, + 1 + ], + "score": 1.0, + "self_loop": 21728 + }, + { + "config": [ + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 0 + ], + "score": 1.0, + "self_loop": 21728 + }, + { + "config": [ + 0, + 0, + 1, + 0, + 1, + 1, + 0, + 0 + ], + "score": 1.0, + "self_loop": 21728 + }, + { + "config": [ + 0, + 0, + 1, + 1, + 0, + 0, + 0, + 1 + ], + "score": 1.0, + "self_loop": 21728 + }, + { + "config": [ + 0, + 0, + 1, + 1, + 0, + 0, + 1, + 0 + ], + "score": 1.0, + "self_loop": 21728 + }, + { + "config": [ + 0, + 0, + 1, + 1, + 0, + 1, + 0, + 0 + ], + "score": 1.0, + "self_loop": 21728 + }, + { + "config": [ + 0, + 0, + 1, + 1, + 1, + 0, + 0, + 0 + ], + "score": 1.0, + "self_loop": 21728 + }, + { + "config": [ + 0, + 1, + 0, + 0, + 0, + 0, + 1, + 1 + ], + "score": 1.0, + "self_loop": 21728 + }, + { + "config": [ + 0, + 1, + 0, + 0, + 0, + 1, + 0, + 1 + ], + "score": 1.0, + "self_loop": 21728 + }, + { + "config": [ + 0, + 1, + 0, + 0, + 0, + 1, + 1, + 0 + ], + "score": 1.0, + "self_loop": 21728 + }, + { + "config": [ + 0, + 1, + 0, + 0, + 1, + 0, + 0, + 1 + ], + "score": 1.0, + "self_loop": 21728 + }, + { + "config": [ + 0, + 1, + 0, + 0, + 1, + 0, + 1, + 0 + ], + "score": 1.0, + "self_loop": 21728 + }, + { + "config": [ + 0, + 1, + 0, + 0, + 1, + 1, + 0, + 0 + ], + "score": 1.0, + "self_loop": 21728 + }, + { + "config": [ + 0, + 1, + 0, + 1, + 0, + 0, + 0, + 1 + ], + "score": 1.0, + "self_loop": 21728 + } + ], + "sha256": "f07556b1b468aa228015bf3f61afa554318cb948dfd6afbf3ca025a473799868" +} \ No newline at end of file diff --git a/.openresearch/artifacts/photonic_sidon_evidence.jsonl b/.openresearch/artifacts/photonic_sidon_evidence.jsonl index 9d438ce5..e766b609 100644 --- a/.openresearch/artifacts/photonic_sidon_evidence.jsonl +++ b/.openresearch/artifacts/photonic_sidon_evidence.jsonl @@ -1,9 +1,9 @@ {"module": "T1_sidon_verify", "severity": "CRITICAL", "claim": "Exact IsSidon verification correctly identifies known Sidon/non-Sidon sets", "verdict": "PASS", "details": {"sidon_sets_tested": 4, "all_sidon": true, "non_sidon_sets_tested": 3, "all_non_sidon": true}} {"module": "T1_sidon_verify", "severity": "HIGH", "claim": "Brute-force h(N) matches known OEIS A003022 values for N \u2264 16", "verdict": "PASS", "details": {"checks": [{"N": 1, "expected_h": 1, "computed_h": 1, "match": true, "sample_set": [1]}, {"N": 2, "expected_h": 2, "computed_h": 2, "match": true, "sample_set": [1, 2]}, {"N": 3, "expected_h": 2, "computed_h": 2, "match": true, "sample_set": [1, 2]}, {"N": 4, "expected_h": 3, "computed_h": 3, "match": true, "sample_set": [1, 2, 4]}, {"N": 5, "expected_h": 3, "computed_h": 3, "match": true, "sample_set": [1, 2, 4]}, {"N": 6, "expected_h": 3, "computed_h": 3, "match": true, "sample_set": [1, 2, 4]}, {"N": 7, "expected_h": 4, "computed_h": 4, "match": true, "sample_set": [1, 2, 5, 7]}, {"N": 8, "expected_h": 4, "computed_h": 4, "match": true, "sample_set": [1, 2, 4, 8]}, {"N": 9, "expected_h": 4, "computed_h": 4, "match": true, "sample_set": [1, 2, 4, 8]}, {"N": 10, "expected_h": 4, "computed_h": 4, "match": true, "sample_set": [1, 2, 4, 8]}, {"N": 11, "expected_h": 4, "computed_h": 4, "match": true, "sample_set": [1, 2, 4, 8]}, {"N": 12, "expected_h": 5, "computed_h": 5, "match": true, "sample_set": [1, 2, 5, 10, 12]}, {"N": 13, "expected_h": 5, "computed_h": 5, "match": true, "sample_set": [1, 2, 4, 8, 13]}, {"N": 14, "expected_h": 5, "computed_h": 5, "match": true, "sample_set": [1, 2, 4, 8, 13]}, {"N": 15, "expected_h": 5, "computed_h": 5, "match": true, "sample_set": [1, 2, 4, 8, 13]}, {"N": 16, "expected_h": 5, "computed_h": 5, "match": true, "sample_set": [1, 2, 4, 8, 13]}]}} {"module": "T2_photonic", "severity": "HIGH", "claim": "Perceval circuit builds for Sidon set [1,2,5,7]", "verdict": "PASS", "details": {"labels": [1, 2, 5, 7], "n_modes": 6}} -{"module": "T2_photonic", "severity": "HIGH", "claim": "SLOS simulation produces output distribution for Sidon set", "verdict": "PASS", "details": {"omega_q16": 19791, "omega_float": 0.3019866943359375, "entropy": 1.789441, "hist_sample": {"0": 0.768, "1": 0.746, "2": 0.184, "3": 0.302}}} -{"module": "T3_omega", "severity": "CRITICAL", "claim": "Sidon sets have lower Omega than non-Sidon (3/4 pairs)", "verdict": "PASS", "details": {"test_pairs": 4, "sidon_lower_count": 3, "results": [{"sidon_set": [1, 2, 5, 7], "non_sidon_set": [1, 2, 3, 4], "omega_sidon": 20381, "omega_non": 23265, "omega_diff": 2884, "entropy_sidon": 1.8205, "entropy_non": 1.895, "collisions_sidon": 0, "collisions_non": 3, "sidon_lower_omega": true}, {"sidon_set": [1, 2, 5, 10], "non_sidon_set": [1, 2, 3, 5], "omega_sidon": 19005, "omega_non": 23658, "omega_diff": 4653, "entropy_sidon": 1.6978, "entropy_non": 1.8186, "collisions_sidon": 0, "collisions_non": 2, "sidon_lower_omega": true}, {"sidon_set": [1, 3, 6, 10], "non_sidon_set": [1, 3, 5, 7], "omega_sidon": 22282, "omega_non": 22151, "omega_diff": -131, "entropy_sidon": 1.7944, "entropy_non": 1.8207, "collisions_sidon": 0, "collisions_non": 3, "sidon_lower_omega": false}, {"sidon_set": [1, 2, 4, 8], "non_sidon_set": [1, 2, 3, 6], "omega_sidon": 21364, "omega_non": 24117, "omega_diff": 2753, "entropy_sidon": 1.7478, "entropy_non": 1.7755, "collisions_sidon": 0, "collisions_non": 1, "sidon_lower_omega": true}]}} -{"module": "T4_h_values", "severity": "HIGH", "claim": "Size-4 Sidon sets have lower avg Omega than non-Sidon (N=8)", "verdict": "PASS", "details": {"avg_omega_sidon": 0.335791, "avg_omega_non": 0.392959, "n_sidon": 10, "n_non": 60}} +{"module": "T2_photonic", "severity": "HIGH", "claim": "SLOS simulation produces output distribution for Sidon set", "verdict": "PASS", "details": {"omega_q16": 22413, "omega_float": 0.3419952392578125, "entropy": 1.803481, "hist_sample": {"0": 0.754, "1": 0.73, "2": 0.174, "3": 0.342}}} +{"module": "T3_omega", "severity": "CRITICAL", "claim": "Sidon sets have lower Omega than non-Sidon (4/4 pairs)", "verdict": "PASS", "details": {"test_pairs": 4, "sidon_lower_count": 4, "results": [{"sidon_set": [1, 2, 5, 7], "non_sidon_set": [1, 2, 3, 4], "omega_sidon": 20840, "omega_non": 27590, "omega_diff": 6750, "entropy_sidon": 1.8192, "entropy_non": 1.897, "collisions_sidon": 0, "collisions_non": 3, "sidon_lower_omega": true}, {"sidon_set": [1, 2, 5, 10], "non_sidon_set": [1, 2, 3, 5], "omega_sidon": 20119, "omega_non": 25755, "omega_diff": 5636, "entropy_sidon": 1.7052, "entropy_non": 1.8427, "collisions_sidon": 0, "collisions_non": 2, "sidon_lower_omega": true}, {"sidon_set": [1, 3, 6, 10], "non_sidon_set": [1, 3, 5, 7], "omega_sidon": 20905, "omega_non": 24510, "omega_diff": 3605, "entropy_sidon": 1.7788, "entropy_non": 1.8711, "collisions_sidon": 0, "collisions_non": 3, "sidon_lower_omega": true}, {"sidon_set": [1, 2, 4, 8], "non_sidon_set": [1, 2, 3, 6], "omega_sidon": 21823, "omega_non": 23986, "omega_diff": 2163, "entropy_sidon": 1.7302, "entropy_non": 1.7685, "collisions_sidon": 0, "collisions_non": 1, "sidon_lower_omega": true}]}} +{"module": "T4_h_values", "severity": "HIGH", "claim": "Size-4 Sidon sets have lower avg Omega than non-Sidon (N=8)", "verdict": "PASS", "details": {"avg_omega_sidon": 0.354593, "avg_omega_non": 0.391393, "n_sidon": 10, "n_non": 60}} {"module": "T4_h_values", "severity": "CRITICAL", "claim": "h(8) = 4 (no size-5 Sidon set exists in {1,...,8})", "verdict": "PASS", "details": {"n_size5_candidates": 56, "any_sidon_5": false}} {"module": "T5_tensor", "severity": "HIGH", "claim": "Tensor network entropy computation works for power-of-2 Sidon set", "verdict": "PASS", "details": {"result": {"entropy": 0.9145505754555368, "entropy_k2": 1.8635303956315334, "method": "tensor_k1_k2", "n_modes": 8}}} {"module": "T5_tensor", "severity": "HIGH", "claim": "Tensor entropy computation works; collision count is the ground truth", "verdict": "PASS", "details": {"sidon_k1_entropy": 1.0155, "non_sidon_k1_entropy": 1.4008, "sidon_k2_entropy": 2.1909, "non_sidon_k2_entropy": 2.8276, "sidon_collisions": 0, "non_sidon_collisions": 3, "explanation": "K=1 entropy is higher for non-Sidon because repeated sums diversify eigenvalues. The photonic Omega metric (T3/T4) is the correct proxy \u2014 it correctly distinguishes Sidon from non-Sidon. The tensor entropy alone is not sufficient; it must be combined with the collision count (exact integer verification)."}} @@ -11,8 +11,8 @@ {"module": "T7_counterexample", "severity": "CRITICAL", "claim": "{1,2,4,8,13} is Sidon (exact verification)", "verdict": "PASS", "details": {"set": [1, 2, 4, 8, 13], "is_sidon": true, "collisions": 0}} {"module": "T7_counterexample", "severity": "CRITICAL", "claim": "{1,2,4,8,13} is NOT a perfect difference set mod 21", "verdict": "PASS", "details": {"set": [1, 2, 4, 8, 13], "modulus": 21, "is_pds": false, "explanation": "This is the counterexample: Sidon but not extendable to PDS"}} {"module": "T7_counterexample", "severity": "CRITICAL", "claim": "No extension of {1,2,4,8,13} to a perfect difference set (conjecture disproven)", "verdict": "PASS", "details": {"checked_orders": [5, 6, 7], "extension_found": false, "explanation": "Confirms the 2025/2026 disproof: this Sidon set cannot be extended to any perfect difference set"}} -{"module": "T7_counterexample", "severity": "HIGH", "claim": "Photonic Omega for {1,2,4,8,13} is low (Sidon-like)", "verdict": "PASS", "details": {"omega_q16": 21954, "omega_float": 0.334991455078125, "entropy": 1.7783}} +{"module": "T7_counterexample", "severity": "HIGH", "claim": "Photonic Omega for {1,2,4,8,13} is low (Sidon-like)", "verdict": "PASS", "details": {"omega_q16": 22544, "omega_float": 0.343994140625, "entropy": 1.759}} {"module": "T8_density", "severity": "HIGH", "claim": "h(N) computed for N=1..24 (brute-force, exact)", "verdict": "PASS", "details": {"h_values": {"1": 1, "2": 2, "3": 2, "4": 3, "5": 3, "6": 3, "7": 4, "8": 4, "9": 4, "10": 4, "11": 4, "12": 5, "13": 5, "14": 5, "15": 5, "16": 5, "17": 5, "18": 6, "19": 6, "20": 6, "21": 6, "22": 6, "23": 6, "24": 6}, "ratios": [{"N": 1, "h(N)": 1, "sqrt(N)": 1.0, "ratio": 1.0, "best_set": [1]}, {"N": 2, "h(N)": 2, "sqrt(N)": 1.4142, "ratio": 1.4142, "best_set": [1, 2]}, {"N": 3, "h(N)": 2, "sqrt(N)": 1.7321, "ratio": 1.1547, "best_set": [1, 2]}, {"N": 4, "h(N)": 3, "sqrt(N)": 2.0, "ratio": 1.5, "best_set": [1, 2, 4]}, {"N": 5, "h(N)": 3, "sqrt(N)": 2.2361, "ratio": 1.3416, "best_set": [1, 2, 4]}, {"N": 6, "h(N)": 3, "sqrt(N)": 2.4495, "ratio": 1.2247, "best_set": [1, 2, 4]}, {"N": 7, "h(N)": 4, "sqrt(N)": 2.6458, "ratio": 1.5119, "best_set": [1, 2, 5, 7]}, {"N": 8, "h(N)": 4, "sqrt(N)": 2.8284, "ratio": 1.4142, "best_set": [1, 2, 4, 8]}, {"N": 9, "h(N)": 4, "sqrt(N)": 3.0, "ratio": 1.3333, "best_set": [1, 2, 4, 8]}, {"N": 10, "h(N)": 4, "sqrt(N)": 3.1623, "ratio": 1.2649, "best_set": [1, 2, 4, 8]}, {"N": 11, "h(N)": 4, "sqrt(N)": 3.3166, "ratio": 1.206, "best_set": [1, 2, 4, 8]}, {"N": 12, "h(N)": 5, "sqrt(N)": 3.4641, "ratio": 1.4434, "best_set": [1, 2, 5, 10, 12]}]}} {"module": "T8_density", "severity": "CRITICAL", "claim": "h(N) <= sqrt(N) + N^0.25 + 1 (Erd\u0151s-Tur\u00e1n upper bound) for N \u2264 24", "verdict": "PASS", "details": {"checked": "N=1..24", "holds": true}} -{"module": "T8_density", "severity": "HIGH", "claim": "Photonic Omega computed for best Sidon sets at N=8,16,24", "verdict": "PASS", "details": {"omega_data": [{"N": 8, "set": [1, 2, 4, 8], "h(N)": 4, "omega": 0.3239898681640625, "sqrt_N": 2.8284}, {"N": 16, "set": [1, 2, 4, 8, 13], "h(N)": 5, "omega": 0.339996337890625, "sqrt_N": 4.0}, {"N": 24, "set": [1, 2, 4, 8, 13, 21], "h(N)": 6, "omega": 0.365997314453125, "sqrt_N": 4.899}]}} +{"module": "T8_density", "severity": "HIGH", "claim": "Photonic Omega computed for best Sidon sets at N=8,16,24", "verdict": "PASS", "details": {"omega_data": [{"N": 8, "set": [1, 2, 4, 8], "h(N)": 4, "omega": 0.329986572265625, "sqrt_N": 2.8284}, {"N": 16, "set": [1, 2, 4, 8, 13], "h(N)": 5, "omega": 0.3639984130859375, "sqrt_N": 4.0}, {"N": 24, "set": [1, 2, 4, 8, 13, 21], "h(N)": 6, "omega": 0.3339996337890625, "sqrt_N": 4.899}]}} {"module": "T8_density", "severity": "HIGH", "claim": "Tensor network entropy for power-of-2 Sidon sets at N=32,64,128", "verdict": "PASS", "details": {"tensor_data": [{"N": 32, "set_size": 6, "set": [1, 2, 4, 8, 16, 32], "entropy": 0.9163, "entropy_k2": 1.9013, "sqrt_N": 5.6569}, {"N": 64, "set_size": 6, "set": [1, 2, 4, 8, 16, 32], "entropy": 0.9163, "entropy_k2": 1.9013, "sqrt_N": 8.0}, {"N": 128, "set_size": 6, "set": [1, 2, 4, 8, 16, 32], "entropy": 0.9163, "entropy_k2": 1.9013, "sqrt_N": 11.3137}], "explanation": "Entropy scales with set size, not N. Larger Sidon sets = more modes = higher entropy."}} diff --git a/.openresearch/artifacts/pipeline_result.json b/.openresearch/artifacts/pipeline_result.json new file mode 100644 index 00000000..329c2946 --- /dev/null +++ b/.openresearch/artifacts/pipeline_result.json @@ -0,0 +1,80 @@ +{ + "experiment": "pipeline_core", + "timestamp": "2026-07-05T03:54:18Z", + "stages": [ + "BraidStorm(k=8)", + "TreeBraid", + "AngrySphinx(budget=128)", + "MultisurfacePacker(max=64)", + "COUCH(threshold=49152)", + "QuaternionSidonFilter" + ], + "labels": [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128 + ], + "S": 128, + "moduli": [ + 7, + 3, + 5, + 11, + 13, + 17, + 19, + 23, + 29 + ], + "phases": [ + 0, + 45, + 90, + 135, + 180, + 225, + 270, + 315 + ], + "stage_timings": { + "BraidStorm(k=8)": { + "input": 1, + "output": 256, + "time_s": 0.0004 + }, + "TreeBraid": { + "input": 256, + "output": 256, + "time_s": 0.0 + }, + "AngrySphinx(budget=128)": { + "input": 256, + "output": 256, + "time_s": 0.0001 + }, + "MultisurfacePacker(max=64)": { + "input": 256, + "output": 64, + "time_s": 0.0 + }, + "COUCH(threshold=49152)": { + "input": 64, + "output": 64, + "time_s": 0.0 + }, + "QuaternionSidonFilter": { + "input": 64, + "output": 0, + "time_s": 0.0011 + } + }, + "total_output": 0, + "elapsed_s": 0.0016, + "final_configs": [], + "sha256": "f922489a57b79546e7bedfd8b77ac09e3ec01f4b3fd082f44e6c50b51a2a47fd" +} \ No newline at end of file diff --git a/formal/SilverSight/AngrySphinx.lean b/formal/SilverSight/AngrySphinx.lean index 34bcd396..e0bd6701 100644 --- a/formal/SilverSight/AngrySphinx.lean +++ b/formal/SilverSight/AngrySphinx.lean @@ -254,33 +254,70 @@ equation returns `none`. The infinity is converted to a closed system. theorem frustration_bounded (pressure : AttackPressure) : frustrationUnderPressure pressure = { value := Q16_16.one } ∨ frustrationUnderPressure pressure ≠ { value := Q16_16.one } := by - cases pressure with | mk j => - simp [frustrationUnderPressure] - split_ifs with h - · left; rfl - · right; intro heq; simpa [h] using heq + unfold frustrationUnderPressure + by_cases h : pressure.joules = 0 + · left; simp [h] + · right; intro h_eq + have : Q16_16.ofRatio 1 (pressure.joules + 1) = Q16_16.one := by + simpa [h] using h_eq + -- ofRatio 1 (j+1) with j ≠ 0 means 65536/(j+1) < 65536 = one.toInt + have h_gt1 : 1 < pressure.joules + 1 := by omega + have h_div : 65536 / (pressure.joules + 1) < 65536 := + Nat.div_lt_self (by omega) h_gt1 + have h_val_lt : (Q16_16.ofRatio 1 (pressure.joules + 1)).toInt < Q16_16.one.toInt := by + unfold Q16_16.ofRatio Q16_16.scale Q16_16.toInt + have h_ne_zero : pressure.joules + 1 ≠ 0 := by omega + simp [h_ne_zero] + have h_one_val : (↑Q16_16.one : ℤ) = 65536 := rfl + rw [h_one_val] + have h_nonneg : 0 ≤ (65536 : Int) / (↑(pressure.joules) + 1) := by positivity + have h_le_self : (65536 : Int) / (↑(pressure.joules) + 1) ≤ 65536 := by + apply Int.ediv_le_self; omega + have h_id : q16Clamp ((65536 : Int) / (↑(pressure.joules) + 1)) = (65536 : Int) / (↑(pressure.joules) + 1) := + q16Clamp_id_of_inRange _ (by + have : q16MinRaw = (-2147483648 : ℤ) := rfl + omega) + (by + have h_max : (65536 : ℕ) ≤ q16MaxRaw := by unfold q16MaxRaw; norm_num + omega) + rw [h_id] + have h_nat : (65536 : ℕ) / (pressure.joules + 1) < 65536 := + Nat.div_lt_self (by norm_num) h_gt1 + exact_mod_cast h_nat + have h_val_eq : (Q16_16.ofRatio 1 (pressure.joules + 1)).toInt = Q16_16.one.toInt := by + simpa using congrArg Q16_16.toInt this + exact h_val_lt.ne h_val_eq /-- For any pressure p ≥ 1, frustration F(p) < 1 (strictly decreasing). The defense is weakening but hasn't collapsed yet. -/ theorem frustration_decreases (p : Nat) (hp : p ≥ 1) : (frustrationUnderPressure { joules := p }).value < Q16_16.one := by unfold frustrationUnderPressure - split_ifs with h + by_cases h : p = 0 · omega - · -- F = Q16_16.ofRatio 1 (p+1) where p ≥ 1, so p+1 ≥ 2 - -- ofRatio 1 n = Q16_SCALE / n when n ≥ 1 - -- Q16_SCALE / (p+1) < Q16_SCALE when p+1 > 1 (i.e., p ≥ 1) - have h_denom_ne_zero : p + 1 ≠ 0 := by omega - have h_denom_pos : 0 < p + 1 := by omega - have h_div_nat : 65536 / (p + 1) < 65536 := - Nat.div_lt_self (by norm_num : 1 ≤ 65536) h_denom_pos - have h_div_int : (Int.ofNat (65536 / (p + 1))) < (65536 : ℤ) := by - exact_mod_cast h_div_nat - -- Unfold Q16_16 <, which is toInt a < toInt b - -- ofRatio 1 (p+1) when p+1 ≠ 0 = ofRawInt (Int.ofNat (65536 / (p+1))) - -- toInt extracts the value, giving Int.ofNat (65536 / (p+1)) - -- one = ⟨65536, ...⟩, toInt gives 65536 - simpa [Q16_16.ofRatio, Q16_16.one, Q16_16.toInt, h_denom_ne_zero, Q16_16.scale] using h_div_int + · have h_one_lt : 1 < p + 1 := by omega + have h_val_lt : (Q16_16.ofRatio 1 (p + 1)).toInt < (Q16_16.one).toInt := by + unfold Q16_16.ofRatio Q16_16.scale Q16_16.toInt + have h_ne_zero : p + 1 ≠ 0 := by omega + simp [h_ne_zero] + have h_one_val : (↑Q16_16.one : ℤ) = 65536 := rfl + rw [h_one_val] + have h_nonneg : 0 ≤ (65536 : Int) / (↑(p : ℤ) + 1) := by positivity + have h_le_self : (65536 : Int) / (↑(p : ℤ) + 1) ≤ 65536 := by + apply Int.ediv_le_self; omega + have h_id : q16Clamp ((65536 : Int) / (↑(p : ℤ) + 1)) = (65536 : Int) / (↑(p : ℤ) + 1) := + q16Clamp_id_of_inRange _ (by + have : q16MinRaw = (-2147483648 : ℤ) := rfl + omega) + (by + have h_max : (65536 : ℕ) ≤ q16MaxRaw := by unfold q16MaxRaw; norm_num + omega) + rw [h_id] + have h_nat : (65536 : ℕ) / (p + 1) < 65536 := + Nat.div_lt_self (by norm_num) h_one_lt + exact_mod_cast h_nat + simp [h] + simpa using h_val_lt /-! §7 Evaluation Witnesses -/ diff --git a/formal/SilverSight/ColdReviewer.lean b/formal/SilverSight/ColdReviewer.lean index 392b4903..0e72fdd7 100644 --- a/formal/SilverSight/ColdReviewer.lean +++ b/formal/SilverSight/ColdReviewer.lean @@ -4,8 +4,10 @@ import CoreFormalism.FixedPoint import SilverSight.AdjugateMatrix +import Mathlib.Tactic set_option linter.dupNamespace false +set_option maxRecDepth 200000 namespace SilverSight.ColdReviewer @@ -44,7 +46,8 @@ def psiInversion (M adjM : Matrix8) (detM : Q16_16) : Q16_16 := maxAbsEntry residual theorem psiInversion_identity : psiInversion identity8 identity8 one = zero := by - dec_trivial + -- `dec_trivial` removed in Lean 4.30; concrete 8×8 Q16_16 computation + native_decide -- ═══════════════════════════════════════════════════════════════════════════ -- §2 Ψ_gap @@ -89,7 +92,7 @@ def psiSidon (s : Array Nat) : Nat := if isSidonSet8 s then 0 else 1 theorem psiSidon_canonical : psiSidon ((#[0,1,3,7,12,20,30,44] : Array Nat)) = 0 := by - dec_trivial + native_decide -- ═══════════════════════════════════════════════════════════════════════════ -- §4 Unified Cold Reviewer Operator @@ -110,6 +113,7 @@ theorem canonical_scores_zero (h_gap : sigma.toInt ≥ (threshold_1_7).toInt) : have h_gap' : psiSpectral sigma = zero := psiSpectral_above sigma h_gap have h_sidon : psiSidon ((#[0,1,3,7,12,20,30,44] : Array Nat)) = 0 := psiSidon_canonical simp [h_inv, h_gap', h_sidon, mul_zero, one_mul] - dec_trivial + -- remaining: zero.add (zero.add (ofInt 0)) = zero + native_decide end SilverSight.ColdReviewer diff --git a/formal/SilverSight/PIST/CharPoly.lean b/formal/SilverSight/PIST/CharPoly.lean index c6134974..7acf58b6 100644 --- a/formal/SilverSight/PIST/CharPoly.lean +++ b/formal/SilverSight/PIST/CharPoly.lean @@ -2,10 +2,10 @@ Copyright (c) 2026 SilverSight Contributors. All rights reserved. Released under Apache 2.0 license. -Exact characteristic polynomial computation for n×n integer matrices. -Uses the Faddeev–LeVerrier algorithm: all integer arithmetic, no floats. +Exact characteristic polynomial computation for nxn integer matrices. +Uses the Faddeev-LeVerrier algorithm: all integer arithmetic, no floats. -The characteristic polynomial p(λ) = det(λI - A) has integer coefficients +The characteristic polynomial p(lambda) = det(lambdaI - A) has integer coefficients when A has integer entries. This module computes them exactly. Key advantage over powerIteration: provably correct for all matrices, @@ -22,147 +22,87 @@ open SilverSight.FixedPoint open SilverSight.FixedPoint.Q16_16 open SilverSight.PIST.MatrixN --- ── Matrix trace ────────────────────────────────────────────────────────── +-- -- Matrix trace ---------------------------------------------------------- -/-- Trace of an n×n integer matrix: sum of diagonal entries. -/ +/-- Trace of an nxn integer matrix: sum of diagonal entries. -/ def matrixTrace (n : Nat) (mat : Array (Array Int)) : Int := (List.range n).foldl (fun acc i => acc + getEntry mat i i) 0 --- ── Matrix multiplication (integer) ─────────────────────────────────────── +-- -- Matrix multiplication (integer) --------------------------------------- -/-- Multiply two n×n integer matrices. All entries are exact integers. -/ +/-- Multiply two nxn integer matrices. All entries are exact integers. -/ def matMulInt (n : Nat) (a b : Array (Array Int)) : Array (Array Int) := Array.ofFn (n := n) fun i => Array.ofFn (n := n) fun j => (List.range n).foldl (fun acc k => acc + getEntry a i.val k * getEntry b k j.val) 0 --- ── Matrix power (integer) ──────────────────────────────────────────────── +-- -- Matrix power (integer) ------------------------------------------------ /-- Compute A^k for integer matrix A via repeated squaring. Returns (A^1, A^2, ..., A^k) as a list for trace extraction. -/ +def matPowersLoop (n : Nat) (mat : Array (Array Int)) (current : Array (Array Int)) + (remaining : Nat) (acc : List (Array (Array Int))) : List (Array (Array Int)) := + match remaining with + | 0 => acc.reverse + | Nat.succ r => + let next := matMulInt n current mat + matPowersLoop n mat next r (current :: acc) + def matPowers (n : Nat) (mat : Array (Array Int)) (k : Nat) : List (Array (Array Int)) := - let rec loop (current : Array (Array Int)) (remaining : Nat) (acc : List (Array (Array Int))) : List (Array (Array Int)) := - match remaining with - | 0 => acc.reverse - | Nat.succ r => - let next := matMulInt n current mat - loop next r (current :: acc) if k = 0 then [] - else loop mat (k - 1) [mat] + else matPowersLoop n mat mat (k - 1) [mat] --- ── Faddeev–LeVerrier algorithm ─────────────────────────────────────────── +-- -- Faddeev-LeVerrier algorithm ----------------------------------------- +-- See comment block below for the math derivation. -/-- Newton identity coefficients for the characteristic polynomial. - - The Faddeev–LeVerrier recurrence: - c₀ = 1 - cₖ = -(1/k) * (tr(A^k) + Σᵢ₌₁ᵏ⁻¹ cₖ₋ᵢ * tr(A^i)) - - Since we work in integers, we compute: - k! * cₖ = -(k-1)! * tr(A^k) - Σᵢ₌₁ᵏ⁻¹ (k-1)!/(i-1)! * cₖ₋ᵢ * tr(A^i) / ... - - Actually, the simplest integer approach: compute the Faddeev sequence - Bₖ = A·Bₖ₋₁ + cₖ₋₁·A (with B₀ = I, c₀ = -tr(A)) - and cₖ = -tr(Bₖ)/k - - For integer matrices, Bₖ has integer entries but cₖ may be rational. - To avoid fractions, we scale: let D = lcm(1,2,...,n) and work in D·ℤ. - - For n=8: D = lcm(1,2,3,4,5,6,7,8) = 840. - - Alternative simpler approach: directly compute det(λI - A) via - cofactor expansion or Bareiss algorithm. For n=8 this is feasible. - - We use the direct trace-based formula: - p(λ) = λⁿ - σ₁λⁿ⁻¹ + σ₂λⁿ⁻₂ - ... + (-1)ⁿσₙ - - where σₖ = (1/k)(pₖ - σ₁pₖ₋₁ + σ₂pₖ₋₂ - ... + (-1)ᵏ⁻¹σₖ₋₁p₁) - and pₖ = tr(Aᵏ) - - Working in scaled integers: let Sₖ = k!·σₖ. Then: - Sₖ = k!·σₖ = (k-1)!·pₖ - Σᵢ₌₁ᵏ⁻¹ (k-1)!·σₖ₋ᵢ·pᵢ·(-1)ⁱ⁻¹ - - Wait, this still has division. Let me use the simplest correct approach. - - DIRECT COMPUTATION via the formula: - c₀ = 1 - cₖ = -(1/k) * Σᵢ₌₀ᵏ⁻¹ cᵢ * tr(Aᵏ⁻ⁱ) - - Scale by k! to get integers: - Cₖ = k!·cₖ - C₀ = 1 - Cₖ = -(k-1)! * Σᵢ₌₀ᵏ⁻¹ Cᵢ/k! * tr(Aᵏ⁻ⁱ) ... still messy. - - CLEANEST APPROACH: Use the fact that for integer matrices, the - characteristic polynomial has integer coefficients. Compute them - via the recursive formula with exact rational arithmetic. - - Since Lean has Rat, we can use that. But for the integer-only - doctrine, we use the scaled version. - - Actually, the simplest approach for n=8: compute the 8 traces - p₁,...,p₈, then apply Newton's identities with integer division - at each step. The division is exact (always produces integer). --/ section FaddeevLeVerrier - -/-- Compute traces of A¹, A², ..., Aᵏ. -/ +/-- Compute traces of A1, A2, ..., Ak. -/ def matrixTraces (n : Nat) (mat : Array (Array Int)) (k : Nat) : Array Int := let powers := matPowers n mat k Array.ofFn (fun (i : Fin k) => matrixTrace n (powers.getD i.val mat)) -/-- Newton identity: compute σₖ from traces p₁,...,pₖ. +-- Newton identity: compute sigma_k from traces p_1,...,p_k. +-- The division by k is exact for integer matrices. - σ₀ = 1 - σₖ = (1/k) * (pₖ - Σᵢ₌₁ᵏ⁻¹ σᵢ · pₖ₋ᵢ · (-1)ⁱ⁻¹) ... no, the sign is: - σₖ = (1/k) * (pₖ·(-1)⁰ + σ₁·pₖ₋₁·(-1)¹ + ... + σₖ₋₁·p₁·(-1)ᵏ⁻¹) +-- Algorithm details: Newton identities for characteristic polynomial. +-- Standard recurrence: c_1 = -p_1, c_k = -(1/k) * sum_{i=1..k} c_{k-i} * p_i. - Wait, the standard Newton identities for characteristic polynomial - p(λ) = λⁿ + c₁λⁿ⁻¹ + ... + cₙ are: - - c₁ = -p₁ - c₂ = -(p₂ + c₁·p₁)/2 - c₃ = -(p₃ + c₁·p₂ + c₂·p₁)/3 - ... - cₖ = -(1/k) * Σᵢ₌₁ᵏ cₖ₋ᵢ · pᵢ (with c₀ = 1) - - Equivalently: k·cₖ = -Σᵢ₌₁ᵏ cₖ₋ᵢ · pᵢ - - The division by k is always exact for integer matrices. --/ +-- Algorithm details: Newton identities for characteristic polynomial. +-- Standard recurrence: c_1 = -p_1, c_k = -(1/k) * sum_{i=1..k} c_{k-i} * p_i. +-- The division by k is exact for integer matrices. /-- Characteristic polynomial coefficients via Newton identities. - Returns [c₁, c₂, ..., cₙ] where p(λ) = λⁿ + c₁λⁿ⁻¹ + ... + cₙ. + Returns [c_1, c_2, ..., c_n] where p(lambda) = lambda^n + c_1 lambda^{n-1} + ... + c_n. All coefficients are exact integers. -/ +def charPolyLoop (n : Nat) (traces : Array Int) (k : Nat) (cs : Array Int) : Array Int := + if k > n then cs + else + let p_k := traces.getD (k - 1) 0 + let sum := (List.range k).foldl (fun acc i => + let idx := i + let c_prev := if k - 1 - idx = 0 then 1 else cs.getD (k - 2 - idx) 0 + let p_i := traces.getD idx 0 + acc + c_prev * p_i) 0 + let c_k := -sum / (k : Int) + charPolyLoop n traces (k + 1) (cs.push c_k) +termination_by n.succ - k + def charPolyCoeffs (n : Nat) (mat : Array (Array Int)) : Array Int := if n = 0 then #[] else let traces := matrixTraces n mat n - -- Newton identity recurrence: k·cₖ = -Σᵢ₌₁ᵏ cₖ₋ᵢ · pᵢ - let rec loop (k : Nat) (cs : Array Int) : Array Int := - if k > n then cs - else - let p_k := traces.getD (k - 1) 0 -- p_k = tr(A^k), 1-indexed - -- Sum: Σᵢ₌₁ᵏ cₖ₋ᵢ · pᵢ where c₀ = 1 - let sum := (List.range k).foldl (fun acc i => - let idx := i -- 0-indexed, so i corresponds to i+1 in the formula - let c_prev := if k - 1 - idx = 0 then 1 else cs.getD (k - 2 - idx) 0 - let p_i := traces.getD idx 0 - acc + c_prev * p_i) 0 - let c_k := -sum / (k : Int) - loop (k + 1) (cs.push c_k) - loop 1 #[] + -- Newton identity recurrence: k*ck = -Sumi?1k ck?i * pi + charPolyLoop n traces 1 #[] -end FaddeevLeVerrier --- ── Spectral radius from characteristic polynomial ──────────────────────── +-- -- Spectral radius from characteristic polynomial ------------------------ /-- Newton's method to find the largest real root of a polynomial. - Given coefficients [c₁, ..., cₙ] for p(λ) = λⁿ + c₁λⁿ⁻¹ + ... + cₙ, + Given coefficients [c1, ..., cn] for p(lambda) = lambdan + c1lambdan?1 + ... + cn, finds the root with largest absolute value. Uses Q16_16 arithmetic with a fixed number of iterations. - Starting guess: max(|cᵢ|)^(1/i) heuristic. + Starting guess: max(|ci|)^(1/i) heuristic. -/ def newtonLargestRoot (coeffs : Array Int) (maxIter : Nat := 50) : Q16_16 := if coeffs.size = 0 then zero @@ -170,14 +110,14 @@ def newtonLargestRoot (coeffs : Array Int) (maxIter : Nat := 50) : Q16_16 := let n := coeffs.size -- Evaluate polynomial and its derivative at x (Q16_16) let evalPoly (x : Q16_16) : Q16_16 := - -- Horner's method: p(x) = (...((x + c₁)x + c₂)x + ... + cₙ) + -- Horner's method: p(x) = (...((x + c1)x + c2)x + ... + cn) let result := (List.range n).foldl (fun acc i => let c := coeffs.getD i 0 add (mul acc x) (ofRawInt c)) x result let evalDeriv (x : Q16_16) : Q16_16 := - -- p'(x) = n·xⁿ⁻¹ + (n-1)·c₁·xⁿ⁻² + ... + cₙ₋₁ - let result := (List.range (n - 1)).foldl (fun acc i := + -- p'(x) = n*xn?1 + (n-1)*c1*xn?2 + ... + cn?1 + let result := (List.range (n - 1)).foldl (fun acc i => let c := coeffs.getD i 0 let coeff := ofRawInt ((n - i : Int) * c) add (mul acc x) coeff) (ofRawInt (n : Int)) @@ -214,12 +154,12 @@ def spectralRadiusFromCharPoly (coeffs : Array Int) : Q16_16 := else let root := newtonLargestRoot coeffs -- Return absolute value (spectral radius is non-negative) - if root.toInt ≥ 0 then root else ofRawInt (-root.toInt) + if root.toInt >= 0 then root else ofRawInt (-root.toInt) --- ── Cayley-Hamilton theorem (statement) ─────────────────────────────────── +-- -- Cayley-Hamilton theorem (statement) ----------------------------------- /-- The Cayley-Hamilton theorem: every matrix satisfies its own - characteristic polynomial. For A with charpoly p(λ), p(A) = 0. + characteristic polynomial. For A with charpoly p(lambda), p(A) = 0. This is stated as a Prop for future proof. The computational content is in charPolyCoeffs and the matrix evaluation. @@ -230,9 +170,9 @@ theorem cayley_hamilton_statement (n : Nat) (mat : Array (Array Int)) : -- matrix polynomial evaluation which is TODO. True := trivial --- ── Integration: exact spectral profile ─────────────────────────────────── +-- -- Integration: exact spectral profile ----------------------------------- -/-- Exact spectral radius of an n×n integer matrix. +/-- Exact spectral radius of an nxn integer matrix. Uses characteristic polynomial instead of power iteration. Provably correct for all matrices. -/ def exactSpectralRadius (n : Nat) (mat : Array (Array Int)) : Q16_16 := @@ -241,14 +181,13 @@ def exactSpectralRadius (n : Nat) (mat : Array (Array Int)) : Q16_16 := let coeffs := charPolyCoeffs n mat spectralRadiusFromCharPoly coeffs -/-- Test: characteristic polynomial of identity matrix is (λ-1)^8. - Coefficients: c₁=-8, c₂=28, c₃=-56, c₄=70, c₅=-56, c₆=28, c₇=-8, c₈=1. -/ -#eval charPolyCoeffs 2 #[#[1, 0], #[0, 1]] -- expect: [-2, 1] (λ² - 2λ + 1) +-- Test: characteristic polynomial of identity matrix is (lambda-1)^8. +#eval charPolyCoeffs 2 #[#[1, 0], #[0, 1]] -/-- Test: trace of 2×2 identity is 2. -/ -#eval matrixTrace 2 #[#[1, 0], #[0, 1]] -- expect: 2 +-- Test: trace of 2x2 identity is 2. +#eval matrixTrace 2 #[#[1, 0], #[0, 1]] -/-- Test: exact spectral radius of 2×2 identity is 1.0 (65536 in Q16_16). -/ -#eval (exactSpectralRadius 2 #[#[1, 0], #[0, 1]]).toInt -- expect: 65536 +-- Test: exact spectral radius of 2x2 identity is 1.0 (65536 in Q16_16). +#eval (exactSpectralRadius 2 #[#[1, 0], #[0, 1]]).toInt end SilverSight.PIST.CharPoly diff --git a/formal/SilverSight/WorkloadTestbench.lean b/formal/SilverSight/WorkloadTestbench.lean index 52115f3e..470e8c45 100644 --- a/formal/SilverSight/WorkloadTestbench.lean +++ b/formal/SilverSight/WorkloadTestbench.lean @@ -120,7 +120,6 @@ theorem random_highest_self_loop : workloadSelfLoop .random ≥ workloadSelfLoop .stream ∧ workloadSelfLoop .random ≥ workloadSelfLoop .strided := by simp [workloadSelfLoop, workloadToOp, HCMR.selfLoopProb] - omega /-- Stream workloads have the highest throughput. -/ theorem stream_highest_throughput (baseRate : ℕ) : @@ -150,6 +149,5 @@ theorem random_causes_reset : CacheSieve.sieveTransition .unstable 10 (workloadSelfLoop .random) = (.reset, .demote) := by simp [workloadSelfLoop, workloadToOp, HCMR.selfLoopProb, CacheSieve.sieveTransition, CacheSieve.ContentionThreshold] - omega end SilverSight.WorkloadTestbench diff --git a/formal/SilverSight/YangMillsPerformance.lean b/formal/SilverSight/YangMillsPerformance.lean index cf6ea38e..57c6437f 100644 --- a/formal/SilverSight/YangMillsPerformance.lean +++ b/formal/SilverSight/YangMillsPerformance.lean @@ -85,7 +85,6 @@ def fullStackThroughput (baseRate : ℕ) : ℕ := /-- Layer multiplier is non-negative (overhead ≤ 1). -/ theorem multiplier_nonneg (layer : PerfLayer) : layerMultiplier layer ≥ 0 := by simp [layerMultiplier, overheadFactor] - omega /-- Cache layer has the highest overhead (most contention). -/ theorem cache_highest_overhead : @@ -94,7 +93,6 @@ theorem cache_highest_overhead : overheadFactor .cache ≥ overheadFactor .compression ∧ overheadFactor .cache ≥ overheadFactor .network := by simp [overheadFactor] - omega /-- Network layer has the second-highest overhead. -/ theorem network_second_highest : @@ -102,51 +100,88 @@ theorem network_second_highest : overheadFactor .network > overheadFactor .sync ∧ overheadFactor .network > overheadFactor .memory := by simp [overheadFactor] - omega + +/-- Key step: multiplying by a layer multiplier and dividing by 65536 + never increases the accumulator (since `layerMultiplier ≤ 65536`). -/ +private lemma mul_div_le_self (acc : ℕ) (layer : PerfLayer) : + acc * layerMultiplier layer / 65536 ≤ acc := by + have hle : layerMultiplier layer ≤ 65536 := by + simp [layerMultiplier, overheadFactor] + have hpos : (0 : ℕ) < 65536 := by norm_num + -- acc * lm / 65536 ≤ acc * 65536 / 65536 (monotonic div) = acc (cancel after comm) + have h_step : acc * layerMultiplier layer / 65536 ≤ acc * 65536 / 65536 := + Nat.div_le_div_right (Nat.mul_le_mul_left acc hle) + have h_cancel : acc * 65536 / 65536 = acc := by + rw [Nat.mul_comm]; exact Nat.mul_div_cancel_left acc hpos + rw [h_cancel] at h_step + exact h_step + +/-- Composed throughput never exceeds the starting accumulator: + each layer can only reduce throughput (since `layerMultiplier ≤ 65536`). -/ +private lemma composed_decreasing (acc : ℕ) (layers : List PerfLayer) : + composedThroughput acc layers ≤ acc := by + induction layers generalizing acc with + | nil => simp [composedThroughput] + | cons head tail ih => + simp only [composedThroughput, List.foldl_cons] + refine Nat.le_trans (ih _) ?_ + exact mul_div_le_self _ head /-- Composed throughput is monotonically decreasing with more layers. -/ theorem more_layers_less_throughput (baseRate : ℕ) (layers : List PerfLayer) (hbase : baseRate > 0) (layer : PerfLayer) : composedThroughput baseRate (layers ++ [layer]) ≤ composedThroughput baseRate layers := by - induction layers with + -- Prove by induction on layers, generalizing the accumulator. + -- `clear hbase` first so it isn't generalized into the IH (the IH would + -- then require a positivity proof for the new accumulator, which may be 0). + clear hbase + induction layers generalizing baseRate with | nil => - simp [composedThroughput] - -- baseRate * (1 - overhead) ≤ baseRate when overhead ≥ 0 - have h : layerMultiplier layer ≤ 65536 := by omega - nlinarith - | cons head tail IH => - simp [composedThroughput] - have : (baseRate * layerMultiplier head / 65536) * layerMultiplier layer / 65536 ≤ - baseRate * layerMultiplier head / 65536 := by - have h : layerMultiplier layer ≤ 65536 := by omega - nlinarith - omega + simp only [composedThroughput, List.nil_append, List.foldl_cons, List.foldl_nil] + exact mul_div_le_self baseRate layer + | cons head tail ih => + simp only [composedThroughput, List.cons_append, List.foldl_cons] + exact ih (baseRate * layerMultiplier head / 65536) /-- HCMR connection: cache layer overhead = SUBLEQ self-loop probability. -/ theorem cache_overhead_equals_subleq : overheadFactor .cache = HCMR.selfLoopProb .subleqWord := rfl -/-- Full stack throughput is strictly less than base rate (overhead exists). -/ +/-- Full stack throughput is strictly less than base rate (overhead exists). + + The cache layer alone (overhead 53908/65536 ≈ 0.823) reduces throughput + to `baseRate * 11628 / 65536 < baseRate` for any `baseRate > 0`. + The remaining 4 layers can only decrease throughput further. -/ theorem full_stack_throughput_lt_base (baseRate : ℕ) (hbase : baseRate > 0) : fullStackThroughput baseRate < baseRate := by - simp [fullStackThroughput, composedThroughput, fullStack] - -- Each layer reduces throughput; with 5 layers of overhead, total < base - have h : layerMultiplier .cache < 65536 := by - simp [layerMultiplier, overheadFactor]; omega - -- After first layer: baseRate * (65536 - 53908) / 65536 < baseRate - nlinarith + -- Step 1: the first layer (cache) strictly decreases throughput. + have h_first : baseRate * layerMultiplier .cache / 65536 < baseRate := by + have hlm : layerMultiplier .cache = 11628 := by + unfold layerMultiplier overheadFactor; norm_num + rw [hlm] + have hpos : (0 : ℕ) < 65536 := by norm_num + rw [Nat.div_lt_iff_lt_mul hpos] + omega + -- Step 2: the remaining layers can only decrease throughput further. + have h_rest : fullStackThroughput baseRate ≤ baseRate * layerMultiplier .cache / 65536 := by + simp only [fullStackThroughput, composedThroughput, fullStack, List.foldl_cons, List.foldl_nil] + exact composed_decreasing _ [.memory, .sync, .compression, .network] + -- Combined: fullStackThroughput ≤ first_layer < baseRate. + omega -/-- Conservation law connection: compression overhead is bounded below. +/- Conservation law connection: compression overhead is bounded below. - The compression layer's overhead ≥ K(data) / data_size. - This is the conservation law from weird_machine_conservation_law.md. -/ -theorem compression_overhead_bounded (kData : ℕ) (dataSize : ℕ) - (h : dataSize > 0) : - overheadFactor .compression ≥ kData * 65536 / dataSize := by - -- This is a placeholder — the actual bound depends on the data - -- The conservation law states: program + residual ≥ K(data) - -- The compression overhead = residual / data_size ≥ K(data) / data_size - sorry + CONJECTURE (not proven): the compression layer's overhead ≥ K(data) / data_size. + This requires the conservation law from weird_machine_conservation_law.md: + program + residual ≥ K(data), so compression overhead = residual / data_size + ≥ K(data) / data_size. The bound depends on the Kolmogorov complexity K(data), + which is uncomputable in general — see PIST/ManifoldShortcut.lean's + `conservation_law` axiom for the formal statement. + + Not stated as a theorem here because `overheadFactor .compression` is a fixed + constant (32768) while K(data) is unbounded — the inequality only holds under + the conservation-law hypothesis, not universally. -/ +-- theorem compression_overhead_bounded : omitted pending conservation law formalization end SilverSight.YangMillsPerformance