From 08465c27282638153778825abfd82c43f86ff26c Mon Sep 17 00:00:00 2001 From: Hanhong Zhao Date: Tue, 13 Oct 2026 19:22:03 +0000 Subject: [PATCH] research: realize sharp T29 profile with exact capacity inventories --- research/t29-capacity-audit/ACCEPTANCE.json | 33 + research/t29-capacity-audit/CLAIM.json | 33 + research/t29-capacity-audit/EXPECTED.json | 632 ++++++++++++++++++ research/t29-capacity-audit/FINAL-REVIEW.json | 331 +++++++++ research/t29-capacity-audit/OVERLAP.json | 46 ++ .../t29-capacity-audit/POSTFIX-REVIEW.json | 241 +++++++ research/t29-capacity-audit/PROOF.md | 133 ++++ research/t29-capacity-audit/README.md | 114 ++++ research/t29-capacity-audit/REVIEW.md | 327 +++++++++ research/t29-capacity-audit/SOURCES.json | 18 + research/t29-capacity-audit/WITNESS.json | 18 + research/t29-capacity-audit/review.py | 227 +++++++ research/t29-capacity-audit/verify.py | 524 +++++++++++++++ 13 files changed, 2677 insertions(+) create mode 100644 research/t29-capacity-audit/ACCEPTANCE.json create mode 100644 research/t29-capacity-audit/CLAIM.json create mode 100644 research/t29-capacity-audit/EXPECTED.json create mode 100644 research/t29-capacity-audit/FINAL-REVIEW.json create mode 100644 research/t29-capacity-audit/OVERLAP.json create mode 100644 research/t29-capacity-audit/POSTFIX-REVIEW.json create mode 100644 research/t29-capacity-audit/PROOF.md create mode 100644 research/t29-capacity-audit/README.md create mode 100644 research/t29-capacity-audit/REVIEW.md create mode 100644 research/t29-capacity-audit/SOURCES.json create mode 100644 research/t29-capacity-audit/WITNESS.json create mode 100644 research/t29-capacity-audit/review.py create mode 100644 research/t29-capacity-audit/verify.py diff --git a/research/t29-capacity-audit/ACCEPTANCE.json b/research/t29-capacity-audit/ACCEPTANCE.json new file mode 100644 index 0000000000..ff8abc2baa --- /dev/null +++ b/research/t29-capacity-audit/ACCEPTANCE.json @@ -0,0 +1,33 @@ +{ + "accepted_at": "2026-10-13T19:18:51.199838+00:00", + "status": "ACCEPTED_FOR_PUBLICATION", + "review_receipt": "POSTFIX-REVIEW.json", + "review_receipt_sha256": "0dd6de88afd4a4644cbddf929fc4ae5e42f34d7bb6c8ff2efb5a5b65e77402b4", + "resolved_findings": { + "R1": "resolved: two explicit checked realizations, no claim all necessary-range values feasible", + "R2": "resolved: all seven aggregate and inventory deltas independently agree", + "R3": "resolved: semantic profile check before default and write; eight relocated malformed-profile CLI failures create no output", + "R4": "resolved: one Cartesian enumeration plus independent maximum-price DP" + }, + "scientific_scope": "historical fixed-U8 PR992 T29 integer packing; no chronology/geometry/physical owner/new kappa/PR1042 claim", + "reviewed_implementation_unchanged": true, + "leader_post_review_edits": { + "CLAIM.json": "Added supported result and scope; original prospective claim retained.", + "README.md": "Corrected file ownership and linked accepted post-fix review; mathematical content and reproduction unchanged." + }, + "package_sha256": { + "CLAIM.json": "56d1593d52cee036f22971c9acc28d84f8d9fc30f78dfea3fba9f7e905976f16", + "EXPECTED.json": "2d6301982d58e9176b3d1fd2353803ef1e183d8f22bf3ee2c9d26af4ed069384", + "FINAL-REVIEW.json": "73c73cc89f822d90f30ff1cc88e1dcc8f21a405a9d0d380a0409640705c25027", + "OVERLAP.json": "56dc7882e699c89533526e9914ea221ba141a353ab29fc4eda8c3431a7bc5a13", + "POSTFIX-REVIEW.json": "0dd6de88afd4a4644cbddf929fc4ae5e42f34d7bb6c8ff2efb5a5b65e77402b4", + "PROOF.md": "9fc548c21d2d7ee8b23dcb67d9001b8bc604f1e2a7bea32f3303b12e5053a02e", + "README.md": "a5fc57725fe397d57d35d860dbef42efe8051388b73b5d09f2f6ff7ca2fb8b47", + "REVIEW.md": "fc922062470afcc0b6c03a7a5de8b66ba64b5777fc9eeb5ecdc140662e227d53", + "SOURCES.json": "412117fd06d9f7b6f45ee394c5ad03f66ba20737a47ebb658f08719b37799695", + "WITNESS.json": "07f269952622b3cb562dd3988f1e5e55b491dc1fcc0c46f848208641b10aadbd", + "review.py": "344678eac3a3ddeef8ab91502ce33b375accfa4521c53107bbc40517f9a6f6df", + "verify.py": "6c58b45b5633c7f619d03cca0337d213c87d1192041b4eb3e5ea1c11605b7430" + }, + "review_type": "Separate AI agent review; not independent human peer review." +} diff --git a/research/t29-capacity-audit/CLAIM.json b/research/t29-capacity-audit/CLAIM.json new file mode 100644 index 0000000000..acf87c49e8 --- /dev/null +++ b/research/t29-capacity-audit/CLAIM.json @@ -0,0 +1,33 @@ +{ + "track": "adversarial mathematical audit", + "assignment_seed": 69, + "base_commit": "ba82555c64e1879e4b7decce28186f208fcb8262", + "claim_at": "2026-10-13T18:44:13.315534+00:00", + "object": "T29 sharp aggregate profile from t37-integrality-audit (PR992): capacity-tagged whole-helper integer bin-pattern realization", + "method": "Enumerate legal patterns; exact checked integer witness or exact obstruction certificate with independent implementation and meaningful inventory-preserving controls.", + "expected_deliverable": "One source-pinned scoped audit package with reproducible exact checker, evidence and limitations; at most one focused PR.", + "expected_finish": "Initial implementation and independent review within approximately60minutes; evidence-driven estimate, not a user hard budget.", + "scope_excluded": [ + "chronology", + "geometry", + "physical owner schedule", + "new kappa", + "current1042 changed supplier" + ], + "coordination": "No open coordination issue surfaced in Astra read-only check. Local claim, ongoing overlap refresh before submission.", + "hypothesis": "q_b6cf2a2ce15a43ed:e10", + "predecessors": [ + "PR942 fixed-U8 all-T bound", + "PR992 integrality sharpness witness" + ], + "assistance": "Fable5.1 max implementation; Astra mathematical review; Antigravity Gemini3.8Flash High brainstorming/controls; Codex leader.", + "result": { + "status": "supported", + "statement": "Two distinct exact integer realizations satisfy the fixed-U8 T29 capacity quotas, helper inventories and remainder profile.", + "bins": 58464, + "helpers": 131544, + "negative_controls": 31, + "independent_review": "POSTFIX-REVIEW.json", + "limits": "Abstract capacity-tagged packing only; no chronology, geometry, physical owner schedule, new kappa or changed PR1042 supplier claim." + } +} diff --git a/research/t29-capacity-audit/EXPECTED.json b/research/t29-capacity-audit/EXPECTED.json new file mode 100644 index 0000000000..f8805a08a7 --- /dev/null +++ b/research/t29-capacity-audit/EXPECTED.json @@ -0,0 +1,632 @@ +{ + "base_commit": "ba82555c64e1879e4b7decce28186f208fcb8262", + "bins": 58464, + "calls_per_replica": 9, + "capacities": { + "16": { + "bins_per_replica": 448, + "bonus": 4 + }, + "32": { + "bins_per_replica": 448, + "bonus": 8 + }, + "48": { + "bins_per_replica": 448, + "bonus": -13 + }, + "8": { + "bins_per_replica": 672, + "bonus": 2 + } + }, + "credit_slack": 0, + "declared_profile_checked_against_census": true, + "demands": { + "4": 20880, + "5": 8352, + "7": 14094, + "8": 31842, + "9": 56376 + }, + "enumeration": "one Cartesian product enumeration of all legal count vectors; u(r) recomputed independently by a maximum-price dynamic program over exact fills", + "helpers_per_call": { + "4": 80, + "5": 32, + "7": 54, + "8": 122, + "9": 216 + }, + "hypothesis": "q_b6cf2a2ce15a43ed:e10", + "legal_patterns": 1163, + "legal_patterns_by_capacity": { + "16": 27, + "32": 215, + "48": 915, + "8": 6 + }, + "negative_controls": [ + { + "invariants": { + "changed": [], + "delta": { + "bins": 0, + "dual_credit": 0, + "mass": 0, + "signed_price": 0 + }, + "preserved": [ + "bins", + "mass", + "dual_credit", + "signed_price" + ], + "violated_inventory": { + "demands": { + "7": -1, + "8": 2, + "9": -1 + } + } + }, + "name": "width_swap_16_9_7_to_16_8_8", + "reason": "width demand mismatch: width 7 used 14093 times, demand 14094" + }, + { + "invariants": { + "changed": [], + "delta": { + "bins": 0, + "dual_credit": 0, + "mass": 0, + "signed_price": 0 + }, + "preserved": [ + "bins", + "mass", + "dual_credit", + "signed_price" + ], + "violated_inventory": { + "demands": { + "5": -1, + "7": 2, + "9": -1 + } + } + }, + "name": "width_swap_32_9995_to_32_9977", + "reason": "width demand mismatch: width 5 used 8351 times, demand 8352" + }, + { + "invariants": { + "changed": [], + "delta": { + "bins": 0, + "dual_credit": 0, + "mass": 0, + "signed_price": 0 + }, + "preserved": [ + "bins", + "mass", + "dual_credit", + "signed_price" + ], + "violated_inventory": { + "demands": { + "4": 2, + "8": -1 + } + } + }, + "name": "rank2_alternative_32_9984_to_32_99444", + "reason": "width demand mismatch: width 4 used 20882 times, demand 20880" + }, + { + "invariants": { + "changed": [], + "delta": { + "bins": 0, + "dual_credit": 0, + "mass": 0, + "signed_price": 0 + }, + "preserved": [ + "bins", + "mass", + "dual_credit", + "signed_price" + ], + "violated_inventory": { + "demands": { + "8": 1 + }, + "quotas": { + "16": 1, + "8": -1 + } + } + }, + "name": "retag_8_8_to_16_88", + "reason": "capacity quota mismatch: capacity 8 has 19487 bins, quota 19488" + }, + { + "invariants": { + "changed": [ + "mass", + "signed_price" + ], + "delta": { + "bins": 0, + "dual_credit": 0, + "mass": -48, + "signed_price": 13 + }, + "preserved": [ + "bins", + "dual_credit" + ], + "violated_inventory": { + "demands": { + "4": 1, + "8": 1, + "9": 4 + }, + "profile": { + "0": 1, + "48": -1 + } + } + }, + "name": "retag_empty_48_to_full_48_999984", + "reason": "remainder profile mismatch: {0: 49771, 1: 4, 2: 1, 48: 8688}" + }, + { + "invariants": { + "changed": [ + "signed_price" + ], + "delta": { + "bins": 0, + "dual_credit": 0, + "mass": 0, + "signed_price": -25 + }, + "preserved": [ + "bins", + "mass", + "dual_credit" + ], + "violated_inventory": { + "demands": { + "4": -1, + "7": 1, + "8": 3, + "9": -3 + } + } + }, + "name": "rank1_untight_32_9994_to_32_8887", + "reason": "width demand mismatch: width 4 used 20879 times, demand 20880" + }, + { + "invariants": { + "changed": [ + "bins" + ], + "delta": { + "bins": -1, + "dual_credit": 0, + "mass": 0, + "signed_price": 0 + }, + "preserved": [ + "mass", + "dual_credit", + "signed_price" + ], + "violated_inventory": { + "demands": { + "8": -1 + }, + "profile": { + "0": -1 + }, + "quotas": { + "8": -1 + } + } + }, + "name": "one_bin_short_8_8", + "reason": "capacity quota mismatch: capacity 8 has 19487 bins, quota 19488" + }, + { + "name": "overfull_pattern_48_999994", + "reason": "illegal pattern: width 49 exceeds capacity 48" + }, + { + "name": "negative_count", + "reason": "count must be a nonnegative integer: -1" + }, + { + "name": "fractional_count", + "reason": "count must be a nonnegative integer: 0.5" + }, + { + "name": "boolean_count", + "reason": "count must be a nonnegative integer: True" + }, + { + "name": "unknown_width_6", + "reason": "unknown helper width in [6, 6]" + }, + { + "name": "unknown_capacity_24", + "reason": "unknown capacity: 24" + }, + { + "name": "duplicate_pattern_entry", + "reason": "duplicate pattern entry: 8:{8}" + }, + { + "name": "false_declared_remainder", + "reason": "declared remainder disagrees with capacity minus width" + }, + { + "name": "header_replicas_float", + "reason": "witness header replicas must be the integer 29" + }, + { + "name": "header_replicas_boolean", + "reason": "witness header replicas must be the integer 29" + }, + { + "name": "header_wrong_hypothesis", + "reason": "witness header hypothesis must be q_b6cf2a2ce15a43ed:e10" + }, + { + "name": "declared_profile_missing", + "reason": "witness must declare remainder_profile" + }, + { + "name": "declared_profile_false_rank0_count", + "reason": "declared remainder_profile disagrees with the recomputed census: declared {\"0\": 1, \"1\": 4, \"2\": 1, \"48\": 8689}, census {\"0\": 49770, \"1\": 4, \"2\": 1, \"48\": 8689}" + }, + { + "name": "declared_profile_missing_class_2", + "reason": "declared remainder_profile disagrees with the recomputed census: declared {\"0\": 49770, \"1\": 4, \"48\": 8689}, census {\"0\": 49770, \"1\": 4, \"2\": 1, \"48\": 8689}" + }, + { + "name": "declared_profile_extra_zero_class_3", + "reason": "declared remainder_profile values must be positive integers: 0" + }, + { + "name": "declared_profile_boolean_value", + "reason": "declared remainder_profile values must be positive integers: True" + }, + { + "name": "declared_profile_noncanonical_key_01", + "reason": "declared remainder_profile keys must be canonical decimal rank strings: '01'" + }, + { + "name": "declared_profile_swapped_classes", + "reason": "declared remainder_profile disagrees with the recomputed census: declared {\"0\": 49770, \"1\": 1, \"2\": 4, \"48\": 8689}, census {\"0\": 49770, \"1\": 4, \"2\": 1, \"48\": 8689}" + }, + { + "name": "tampered_u_table_u2_14", + "reason": "signed-price table disagrees with the independent enumeration" + }, + { + "name": "wrong_replica_count_28", + "reason": "bin count identity: profile has 58464 bins, quotas give 56448" + }, + { + "name": "profile_off_by_one_rank1", + "reason": "bin count identity: profile has 58465 bins, quotas give 58464" + }, + { + "name": "profile_same_bins_same_mass_positive_slack", + "reason": "signed-price identity (zero slack) fails: sum u(r) n_r = -112843, actual total price = -112868" + }, + { + "name": "profile_same_bins_same_mass_negative_slack", + "reason": "profile violates the necessary signed-price inequality (slack -50)" + }, + { + "name": "tampered_source_pin", + "reason": "source pin mismatch: research/complex-t21-owner-bound/PROOF.md" + } + ], + "nonuniqueness": "two distinct checked realizations; no statement about any other count vector", + "patterns_with_different_counts": [ + "16:{8,8}", + "16:{9,7}", + "32:{8,8,8,8}", + "32:{9,9,4,4,4}", + "32:{9,9,7,7}", + "32:{9,9,8,4}", + "8:{4,4}", + "8:{8}" + ], + "prices": { + "4": -1, + "5": -20, + "7": -8, + "8": -2, + "9": 4 + }, + "profile": { + "0": 49770, + "1": 4, + "2": 1, + "48": 8689 + }, + "quotas": { + "16": 12992, + "32": 12992, + "48": 12992, + "8": 19488 + }, + "rank_mass": 417078, + "realizations_checked": 2, + "replicas": 29, + "scope": "Aggregate capacity-tagged whole-helper pattern feasibility only. No chronology, owner geometry, physical schedule, controller, invoice or kappa claim; the selected PR1042 supplier is outside scope.", + "second_witness": { + "bins": 58464, + "census": { + "0": 49770, + "1": 4, + "2": 1, + "48": 8689 + }, + "distinct_patterns": 10, + "patterns": [ + { + "capacity": 8, + "count": 11203, + "pattern": "8:{8}", + "remainder": 0 + }, + { + "capacity": 8, + "count": 8285, + "pattern": "8:{4,4}", + "remainder": 0 + }, + { + "capacity": 16, + "count": 8168, + "pattern": "16:{8,8}", + "remainder": 0 + }, + { + "capacity": 16, + "count": 4824, + "pattern": "16:{9,7}", + "remainder": 0 + }, + { + "capacity": 32, + "count": 4635, + "pattern": "32:{9,9,7,7}", + "remainder": 0 + }, + { + "capacity": 32, + "count": 8352, + "pattern": "32:{9,9,9,5}", + "remainder": 0 + }, + { + "capacity": 32, + "count": 4, + "pattern": "32:{9,9,9,4}", + "remainder": 1 + }, + { + "capacity": 32, + "count": 1, + "pattern": "32:{9,9,4,4,4}", + "remainder": 2 + }, + { + "capacity": 48, + "count": 8689, + "pattern": "48:{}", + "remainder": 48 + }, + { + "capacity": 48, + "count": 4303, + "pattern": "48:{9,9,9,9,8,4}", + "remainder": 0 + } + ], + "source": "REVIEW.md blind hand construction, transcribed as data", + "total_signed_price": -112868 + }, + "source_sha256": { + "research/complex-t21-owner-bound/PROOF.md": "2aa0aa6ec1d87402138564c38749b5ca0f058c16817efdf58a2685d2d90cb417", + "research/complex-t37-owners/ALL-T-PROOF.md": "4c0c71ccd0afb850538af1b467e5208b7eb3edd0260fded84e02a8c01dfc868b", + "research/t37-integrality-audit/EXPECTED.json": "17ffdeffab4ae2a843381ea1e87305608e4caac27cc15293b590c6313a2dd095", + "research/t37-integrality-audit/PROOF.md": "0dd18b2b486b98dc06e67b0b64e21dc18b6282af483f975e551b1f36dbc5d7ca", + "research/t37-integrality-audit/README.md": "5e90726de4069d8d19c1f3cf49e636578f46c1d150f1b8d7a7ca64c90b78ea1c" + }, + "status": "PASS_T29_CAPACITY_TAGGED_PATTERN_WITNESS", + "structure": { + "cap32_bins_free_for_rank0_without_fives": 4635, + "capacity16_nine_seven_bins_necessary_range": [ + 4824, + 12992 + ], + "capacity16_nine_seven_bins_range_is_necessary_only": true, + "forced_fives_bins_cap32_9995": 8352, + "forced_full_capacity48_bins": 4303, + "nines_in_forced_bins": 42282, + "nines_remaining_equals_sevens": 14094, + "tight_patterns_by_class": { + "0": [ + "8:{8}", + "8:{4,4}", + "16:{8,8}", + "16:{9,7}", + "16:{8,4,4}", + "16:{4,4,4,4}", + "32:{8,8,8,8}", + "32:{9,8,8,7}", + "32:{9,9,7,7}", + "32:{9,9,9,5}", + "32:{8,8,8,4,4}", + "32:{9,8,7,4,4}", + "32:{8,8,4,4,4,4}", + "32:{9,7,4,4,4,4}", + "32:{8,4,4,4,4,4,4}", + "32:{4,4,4,4,4,4,4,4}", + "48:{9,9,9,9,8,4}", + "48:{9,9,9,9,4,4,4}" + ], + "1": [ + "32:{9,9,9,4}" + ], + "2": [ + "32:{9,9,8,4}", + "32:{9,9,4,4,4}" + ], + "48": [ + "48:{}" + ] + } + }, + "tightness_lemma": "sum of bin prices equals the fixed total -3892*T and equals sum_r n_r u(r); each bin price <= u(r); hence every bin attains u(r)", + "total_signed_price": -112868, + "u": { + "0": 0, + "1": 19, + "10": 15, + "11": 9, + "12": 3, + "13": -3, + "14": 16, + "15": 10, + "16": 4, + "17": -2, + "18": -8, + "19": 11, + "2": 13, + "20": 5, + "21": -1, + "22": -7, + "23": 12, + "24": 6, + "25": 0, + "26": -6, + "27": -12, + "28": 7, + "29": -24, + "3": 7, + "30": -5, + "31": -11, + "32": 8, + "33": -23, + "34": -29, + "35": -10, + "36": -16, + "37": -22, + "38": -53, + "39": -9, + "4": 1, + "40": -15, + "41": -21, + "43": -33, + "44": -14, + "48": -13, + "5": 20, + "6": 14, + "7": 8, + "8": 2, + "9": -4 + }, + "widths": [ + 4, + 5, + 7, + 8, + 9 + ], + "witness": { + "bins": 58464, + "census": { + "0": 49770, + "1": 4, + "2": 1, + "48": 8689 + }, + "distinct_patterns": 10, + "patterns": [ + { + "capacity": 8, + "count": 11202, + "pattern": "8:{8}", + "remainder": 0 + }, + { + "capacity": 8, + "count": 8286, + "pattern": "8:{4,4}", + "remainder": 0 + }, + { + "capacity": 16, + "count": 12992, + "pattern": "16:{9,7}", + "remainder": 0 + }, + { + "capacity": 32, + "count": 4084, + "pattern": "32:{8,8,8,8}", + "remainder": 0 + }, + { + "capacity": 32, + "count": 551, + "pattern": "32:{9,9,7,7}", + "remainder": 0 + }, + { + "capacity": 32, + "count": 8352, + "pattern": "32:{9,9,9,5}", + "remainder": 0 + }, + { + "capacity": 32, + "count": 4, + "pattern": "32:{9,9,9,4}", + "remainder": 1 + }, + { + "capacity": 32, + "count": 1, + "pattern": "32:{9,9,8,4}", + "remainder": 2 + }, + { + "capacity": 48, + "count": 8689, + "pattern": "48:{}", + "remainder": 48 + }, + { + "capacity": 48, + "count": 4303, + "pattern": "48:{9,9,9,9,8,4}", + "remainder": 0 + } + ], + "total_signed_price": -112868 + }, + "witness_canonical_sha256": "9d205e9a1498ee99050ebbb9eb4c3b2dd5ba79ea78eb28053cc8b8b72368daf9", + "witness_file_sha256": "07f269952622b3cb562dd3988f1e5e55b491dc1fcc0c46f848208641b10aadbd" +} diff --git a/research/t29-capacity-audit/FINAL-REVIEW.json b/research/t29-capacity-audit/FINAL-REVIEW.json new file mode 100644 index 0000000000..06864f0f6e --- /dev/null +++ b/research/t29-capacity-audit/FINAL-REVIEW.json @@ -0,0 +1,331 @@ +{ + "base_commit": "ba82555c64e1879e4b7decce28186f208fcb8262", + "commands": [ + { + "command": [ + "/kmh-nfs-ssd-us-mount/code/hanhong/miniforge3/bin/python", + "-I", + "-O", + "-B", + "/kmh-nfs-ssd-us-mount/code/siri/math/integer-mult-bounds/research/t29-capacity-audit/review.py", + "--witness", + "/kmh-nfs-ssd-us-mount/code/siri/math/integer-mult-bounds/research/t29-capacity-audit/WITNESS.json" + ], + "cwd": "/tmp/t29-final-review-9rhqj5pl", + "exit_code": 0, + "name": "independent_final_witness", + "seconds": 0.8368272790685296, + "stdout_sha256": "809801ccd29e3a477427d7d0f24f3214d12e6895ab1b4217b0bb680887a70a85" + }, + { + "command": [ + "/kmh-nfs-ssd-us-mount/code/hanhong/miniforge3/bin/python", + "-I", + "-O", + "-B", + "/tmp/t29-final-review-9rhqj5pl/checkout with spaces/research/t29-capacity-audit/verify.py" + ], + "cwd": "/tmp/t29-final-review-9rhqj5pl", + "exit_code": 0, + "name": "relocated_default_root", + "seconds": 0.23715756693854928, + "stdout_sha256": "9eacbd8faa4e4661ba59bf4a49620fddcde1c43eb0db622d2b178f6785f9ca8f" + }, + { + "command": [ + "/kmh-nfs-ssd-us-mount/code/hanhong/miniforge3/bin/python", + "-I", + "-O", + "-B", + "/tmp/t29-final-review-9rhqj5pl/checkout with spaces/research/t29-capacity-audit/verify.py", + "--repository", + "/tmp/t29-final-review-9rhqj5pl/checkout with spaces" + ], + "cwd": "/tmp/t29-final-review-9rhqj5pl", + "exit_code": 0, + "name": "relocated_explicit_root", + "seconds": 0.2377452969085425, + "stdout_sha256": "9eacbd8faa4e4661ba59bf4a49620fddcde1c43eb0db622d2b178f6785f9ca8f" + }, + { + "command": [ + "/kmh-nfs-ssd-us-mount/code/hanhong/miniforge3/bin/python", + "-I", + "-O", + "-B", + "/tmp/t29-final-review-9rhqj5pl/checkout with spaces/research/t29-capacity-audit/verify.py", + "--write", + "/tmp/t29-final-review-9rhqj5pl/fresh certificate.json" + ], + "cwd": "/tmp/t29-final-review-9rhqj5pl", + "exit_code": 0, + "name": "fresh_write", + "seconds": 0.23863160703331232, + "stdout_sha256": "9eacbd8faa4e4661ba59bf4a49620fddcde1c43eb0db622d2b178f6785f9ca8f" + }, + { + "command": [ + "/kmh-nfs-ssd-us-mount/code/hanhong/miniforge3/bin/python", + "-I", + "-O", + "-B", + "/tmp/t29-final-review-9rhqj5pl/checkout with spaces/research/t29-capacity-audit/verify.py", + "--write", + "/tmp/t29-final-review-9rhqj5pl/fresh certificate.json" + ], + "cwd": "/tmp/t29-final-review-9rhqj5pl", + "exit_code": 1, + "name": "existing_write_refused", + "seconds": 0.23718175699468702, + "stdout_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855" + }, + { + "command": [ + "/kmh-nfs-ssd-us-mount/code/hanhong/miniforge3/bin/python", + "-I", + "-O", + "-B", + "/tmp/t29-final-review-9rhqj5pl/checkout with spaces/research/t29-capacity-audit/verify.py" + ], + "cwd": "/tmp/t29-final-review-9rhqj5pl", + "exit_code": 1, + "name": "stale_expected", + "seconds": 0.2438701270148158, + "stdout_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855" + }, + { + "command": [ + "/kmh-nfs-ssd-us-mount/code/hanhong/miniforge3/bin/python", + "-I", + "-O", + "-B", + "/tmp/t29-final-review-9rhqj5pl/checkout with spaces/research/t29-capacity-audit/verify.py" + ], + "cwd": "/tmp/t29-final-review-9rhqj5pl", + "exit_code": 1, + "name": "malformed_witness", + "seconds": 0.23427625698968768, + "stdout_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855" + }, + { + "command": [ + "/kmh-nfs-ssd-us-mount/code/hanhong/miniforge3/bin/python", + "-I", + "-O", + "-B", + "/tmp/t29-final-review-9rhqj5pl/checkout with spaces/research/t29-capacity-audit/verify.py" + ], + "cwd": "/tmp/t29-final-review-9rhqj5pl", + "exit_code": 1, + "name": "wrong_witness_count", + "seconds": 0.23194042698014528, + "stdout_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855" + }, + { + "command": [ + "/kmh-nfs-ssd-us-mount/code/hanhong/miniforge3/bin/python", + "-I", + "-O", + "-B", + "/tmp/t29-final-review-9rhqj5pl/checkout with spaces/research/t29-capacity-audit/verify.py" + ], + "cwd": "/tmp/t29-final-review-9rhqj5pl", + "exit_code": 1, + "name": "corrupt_source", + "seconds": 0.18387142196297646, + "stdout_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855" + }, + { + "command": [ + "/kmh-nfs-ssd-us-mount/code/hanhong/miniforge3/bin/python", + "-I", + "-O", + "-B", + "/tmp/t29-final-review-9rhqj5pl/checkout with spaces/research/t29-capacity-audit/verify.py" + ], + "cwd": "/tmp/t29-final-review-9rhqj5pl", + "exit_code": 1, + "name": "missing_source", + "seconds": 0.1839448120445013, + "stdout_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855" + }, + { + "command": [ + "/kmh-nfs-ssd-us-mount/code/hanhong/miniforge3/bin/python", + "-I", + "-O", + "-B", + "/tmp/t29-final-review-9rhqj5pl/checkout with spaces/research/t29-capacity-audit/verify.py" + ], + "cwd": "/tmp/t29-final-review-9rhqj5pl", + "exit_code": 1, + "name": "malformed_sources", + "seconds": 0.18505218205973506, + "stdout_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855" + }, + { + "command": [ + "/kmh-nfs-ssd-us-mount/code/hanhong/miniforge3/bin/python", + "-I", + "-O", + "-B", + "/tmp/t29-final-review-9rhqj5pl/checkout with spaces/research/t29-capacity-audit/verify.py" + ], + "cwd": "/tmp/t29-final-review-9rhqj5pl", + "exit_code": 1, + "name": "false_declared_profile_default", + "seconds": 0.23812790703959763, + "stdout_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855" + }, + { + "command": [ + "/kmh-nfs-ssd-us-mount/code/hanhong/miniforge3/bin/python", + "-I", + "-O", + "-B", + "/tmp/t29-final-review-9rhqj5pl/checkout with spaces/research/t29-capacity-audit/verify.py", + "--write", + "/tmp/t29-final-review-9rhqj5pl/false-profile receipt.json" + ], + "cwd": "/tmp/t29-final-review-9rhqj5pl", + "exit_code": 0, + "name": "false_declared_profile_regeneration", + "seconds": 0.23781593597959727, + "stdout_sha256": "9eacbd8faa4e4661ba59bf4a49620fddcde1c43eb0db622d2b178f6785f9ca8f" + } + ], + "control_invariant_audit": [ + { + "delta": { + "actual_signed": 0, + "bins": 0, + "dual_credit": 0, + "mass": 0 + }, + "name": "width_swap_16_9_7_to_16_8_8_same_rank_same_price" + }, + { + "delta": { + "actual_signed": 0, + "bins": 0, + "dual_credit": 0, + "mass": 0 + }, + "name": "width_swap_32_9995_to_32_9977_same_rank_same_price" + }, + { + "delta": { + "actual_signed": 0, + "bins": 0, + "dual_credit": 0, + "mass": 0 + }, + "name": "rank2_alternative_32_99444_same_rank_same_price" + }, + { + "delta": { + "actual_signed": 0, + "bins": 0, + "dual_credit": 0, + "mass": 0 + }, + "name": "retag_8_8_to_16_88_same_rank_same_price" + }, + { + "delta": { + "actual_signed": 13, + "bins": 0, + "dual_credit": 0, + "mass": -48 + }, + "name": "retag_empty_48_to_full_48_changes_profile" + }, + { + "delta": { + "actual_signed": -25, + "bins": 0, + "dual_credit": 0, + "mass": 0 + }, + "name": "rank1_untight_32_8887_same_mass" + }, + { + "delta": { + "actual_signed": 0, + "bins": -1, + "dual_credit": 0, + "mass": 0 + }, + "name": "one_bin_short" + } + ], + "excluded": [ + "physical scheduling", + "chronology", + "geometry", + "new kappa", + "current PR1042 supplier", + "all-size theorem", + "full repository replays" + ], + "findings": [ + { + "file": "PROOF.md", + "id": "R1", + "kind": "unsupported inference", + "line": 112, + "summary": "Necessary interval alone does not imply many feasible realizations. Narrow to nonuniqueness with two explicit witnesses or prove a feasible family." + }, + { + "file": "README.md", + "id": "R2", + "kind": "incorrect coverage description", + "line": 49, + "summary": "Empty cap48 -> full cap48 mutation changes residual mass by -48. Distinguish each preserved invariant; the control rejects correctly." + }, + { + "file": "verify.py", + "function": "certificate", + "id": "R3", + "kind": "metadata binding gap", + "summary": "Declared remainder_profile ignored. False zero-rank count is caught by stale hash in default mode but accepted by --write; validate declared profile semantically and add regression control." + }, + { + "file": "README.md", + "id": "R4", + "kind": "minor precision", + "line": 38, + "summary": "One Cartesian pattern enumeration plus independent price-table DP; not two enumerations of all patterns." + } + ], + "mathematical_checks": { + "bins": 58464, + "distinct_independent_witnesses": 2, + "helpers": 131544, + "legal_patterns": 1163, + "producer_witness_checked_with_independent_code": true, + "tight_target_support_patterns": 22, + "u_table_entries": 45, + "unit_slot_expansion": true + }, + "mathematical_hypothesis": "supports q_b6cf2a2ce15a43ed:e10", + "phase": "authorized post-blind integration review", + "publication_acceptance": false, + "recorded_at": "2026-10-13T19:02:41.357125+00:00", + "reviewed_sha256": { + "CLAIM.json": "3ad349f8546610e3efcf9c662dddb74739334d17cba4d2dbc10f8471f513dad8", + "EXPECTED.json": "6872f5675e51abd44949923dae619f543b6d1ef8d5ad6164b0692573368c1a90", + "PROOF.md": "e2434c69f19d9f224bd579fb5de4de3ceba77a3d60712fc1830e138047d34f6f", + "README.md": "e4acd490686ae9e213a2560c01f10d6e893ab0dbc3086474d133e6da263443de", + "REVIEW.md": "bc1afb4c1176b174973133f1092c757e6cefd0fae80bc254b50d0b97d473977b", + "SOURCES.json": "412117fd06d9f7b6f45ee394c5ad03f66ba20737a47ebb658f08719b37799695", + "WITNESS.json": "07f269952622b3cb562dd3988f1e5e55b491dc1fcc0c46f848208641b10aadbd", + "review.py": "344678eac3a3ddeef8ab91502ce33b375accfa4521c53107bbc40517f9a6f6df", + "verify.py": "6ca61a5ea3c274d8f10772c24658542f776d3b43c20d64a8a7d6b38b49e0b8d6" + }, + "reviewer": "Astra AI mathematical reviewer; not independent human peer review", + "scratch_directory": "/tmp/t29-final-review-9rhqj5pl", + "source_count": 5, + "source_pins_match_recorded_git_base": true, + "status": "ACTIONABLE_FINDINGS" +} diff --git a/research/t29-capacity-audit/OVERLAP.json b/research/t29-capacity-audit/OVERLAP.json new file mode 100644 index 0000000000..c0c7cd3c03 --- /dev/null +++ b/research/t29-capacity-audit/OVERLAP.json @@ -0,0 +1,46 @@ +{ + "checked_at": "2026-10-13T18:59:12.023727+00:00", + "queries": [ + { + "query": "repo:CrocSwap/integer-mult-bounds is:pr is:open T29", + "total_count": 0, + "incomplete_results": false, + "items": [] + }, + { + "query": "repo:CrocSwap/integer-mult-bounds is:pr is:open \"capacity\" \"bin\"", + "total_count": 5, + "incomplete_results": false, + "items": [ + { + "number": 649, + "title": "Conditional \u03ba = 0.001652528731617094: PR589 bit supplier and dissolved owner map on PR645's gauge44 construction", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/649" + }, + { + "number": 262, + "title": "Conditional \u03ba = 8.339545889388e-4 on #233's row: the bit word's own retained ledger banked a second time (B1 open, not a witness)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/262" + }, + { + "number": 1129, + "title": "Conditional \u03ba = 0.001674097969905390: an attaining T37 construction and fixed R480 owner optimum", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1129" + }, + { + "number": 522, + "title": "Conditional kappa 0.001402213284556683: rank-factor coordinate totals merge 56 recursive pairs", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/522" + }, + { + "number": 532, + "title": "Conditional kappa 0.001467978682990812: paid circuit retirement on the 112-port supplier", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/532" + } + ] + } + ], + "assessment": "No open T29 match found. PR1129 proves an optimum and physical T37 construction for changed seven-slot R480 inventory; this audit instead realizes historical fixed-U8 PR992 T29 profile under exact inventory constraints. Shared 1163-pattern domain and signed-price predecessors do not identify the claims.", + "limits": "Keyword/body review, not proof of novelty; differently named or unpublished work may be absent.", + "main_checked": "ce7ad1b6ab09452c3478723a2e96ed5ff212dc08" +} diff --git a/research/t29-capacity-audit/POSTFIX-REVIEW.json b/research/t29-capacity-audit/POSTFIX-REVIEW.json new file mode 100644 index 0000000000..5419a2de7f --- /dev/null +++ b/research/t29-capacity-audit/POSTFIX-REVIEW.json @@ -0,0 +1,241 @@ +{ + "claim_scope_review": "historical fixed-U8 PR992 T29 integer packing; no chronology/geometry/physical owner/new kappa/PR1042 claim", + "dispositions": { + "R1": "resolved: two explicit checked realizations, no claim all necessary-range values feasible", + "R2": "resolved: all seven aggregate and inventory deltas independently agree", + "R3": "resolved: semantic profile check before default and write; eight relocated malformed-profile CLI failures create no output", + "R4": "resolved: one Cartesian enumeration plus independent maximum-price DP" + }, + "evidence": { + "commands": [ + { + "command": [ + "/kmh-nfs-ssd-us-mount/code/hanhong/miniforge3/bin/python", + "-I", + "-O", + "-B", + "/tmp/t29-postfix-review-a6_slr_a/checkout with spaces/research/t29-capacity-audit/verify.py" + ], + "cwd": "/tmp/t29-postfix-review-a6_slr_a", + "exit_code": 0, + "name": "relocated_optimized_baseline", + "seconds": 0.23864785698242486, + "stderr": "", + "stdout": "PASS_T29_CAPACITY_TAGGED_PATTERN_WITNESS patterns=1163 witness_bins=58464 witness_patterns=10 realizations=2 controls=31 no_new_kappa" + }, + { + "command": [ + "/kmh-nfs-ssd-us-mount/code/hanhong/miniforge3/bin/python", + "-I", + "-O", + "-B", + "/tmp/t29-postfix-review-a6_slr_a/checkout with spaces/research/t29-capacity-audit/verify.py", + "--repository", + "/tmp/t29-postfix-review-a6_slr_a/checkout with spaces" + ], + "cwd": "/tmp/t29-postfix-review-a6_slr_a", + "exit_code": 0, + "name": "relocated_explicit_repository", + "seconds": 0.23966410697903484, + "stderr": "", + "stdout": "PASS_T29_CAPACITY_TAGGED_PATTERN_WITNESS patterns=1163 witness_bins=58464 witness_patterns=10 realizations=2 controls=31 no_new_kappa" + }, + { + "command": [ + "/kmh-nfs-ssd-us-mount/code/hanhong/miniforge3/bin/python", + "-I", + "-O", + "-B", + "/tmp/t29-postfix-review-a6_slr_a/checkout with spaces/research/t29-capacity-audit/verify.py", + "--write", + "/tmp/t29-postfix-review-a6_slr_a/fresh expected.json" + ], + "cwd": "/tmp/t29-postfix-review-a6_slr_a", + "exit_code": 0, + "name": "fresh_write", + "seconds": 0.24218948592897505, + "stderr": "", + "stdout": "PASS_T29_CAPACITY_TAGGED_PATTERN_WITNESS patterns=1163 witness_bins=58464 witness_patterns=10 realizations=2 controls=31 no_new_kappa" + }, + { + "command": [ + "/kmh-nfs-ssd-us-mount/code/hanhong/miniforge3/bin/python", + "-I", + "-O", + "-B", + "/tmp/t29-postfix-review-a6_slr_a/checkout with spaces/research/t29-capacity-audit/verify.py" + ], + "cwd": "/tmp/t29-postfix-review-a6_slr_a", + "exit_code": 1, + "name": "false_zero_count_default", + "seconds": 0.23152111703529954, + "stderr": "FAIL_T29_CAPACITY_TAGGED_PATTERN_WITNESS: declared remainder_profile disagrees with the recomputed census: declared {\"0\": 1, \"1\": 4, \"2\": 1, \"48\": 8689}, census {\"0\": 49770, \"1\": 4, \"2\": 1, \"48\": 8689}", + "stdout": "" + }, + { + "command": [ + "/kmh-nfs-ssd-us-mount/code/hanhong/miniforge3/bin/python", + "-I", + "-O", + "-B", + "/tmp/t29-postfix-review-a6_slr_a/checkout with spaces/research/t29-capacity-audit/verify.py", + "--write", + "/tmp/t29-postfix-review-a6_slr_a/false_zero_count output.json" + ], + "cwd": "/tmp/t29-postfix-review-a6_slr_a", + "exit_code": 1, + "name": "false_zero_count_write", + "seconds": 0.23133425798732787, + "stderr": "FAIL_T29_CAPACITY_TAGGED_PATTERN_WITNESS: declared remainder_profile disagrees with the recomputed census: declared {\"0\": 1, \"1\": 4, \"2\": 1, \"48\": 8689}, census {\"0\": 49770, \"1\": 4, \"2\": 1, \"48\": 8689}", + "stdout": "" + }, + { + "command": [ + "/kmh-nfs-ssd-us-mount/code/hanhong/miniforge3/bin/python", + "-I", + "-O", + "-B", + "/tmp/t29-postfix-review-a6_slr_a/checkout with spaces/research/t29-capacity-audit/verify.py" + ], + "cwd": "/tmp/t29-postfix-review-a6_slr_a", + "exit_code": 1, + "name": "missing_profile_default", + "seconds": 0.2383161160396412, + "stderr": "FAIL_T29_CAPACITY_TAGGED_PATTERN_WITNESS: witness must declare remainder_profile", + "stdout": "" + }, + { + "command": [ + "/kmh-nfs-ssd-us-mount/code/hanhong/miniforge3/bin/python", + "-I", + "-O", + "-B", + "/tmp/t29-postfix-review-a6_slr_a/checkout with spaces/research/t29-capacity-audit/verify.py", + "--write", + "/tmp/t29-postfix-review-a6_slr_a/missing_profile output.json" + ], + "cwd": "/tmp/t29-postfix-review-a6_slr_a", + "exit_code": 1, + "name": "missing_profile_write", + "seconds": 0.23912974703125656, + "stderr": "FAIL_T29_CAPACITY_TAGGED_PATTERN_WITNESS: witness must declare remainder_profile", + "stdout": "" + }, + { + "command": [ + "/kmh-nfs-ssd-us-mount/code/hanhong/miniforge3/bin/python", + "-I", + "-O", + "-B", + "/tmp/t29-postfix-review-a6_slr_a/checkout with spaces/research/t29-capacity-audit/verify.py" + ], + "cwd": "/tmp/t29-postfix-review-a6_slr_a", + "exit_code": 1, + "name": "boolean_count_default", + "seconds": 0.23741735704243183, + "stderr": "FAIL_T29_CAPACITY_TAGGED_PATTERN_WITNESS: declared remainder_profile values must be positive integers: True", + "stdout": "" + }, + { + "command": [ + "/kmh-nfs-ssd-us-mount/code/hanhong/miniforge3/bin/python", + "-I", + "-O", + "-B", + "/tmp/t29-postfix-review-a6_slr_a/checkout with spaces/research/t29-capacity-audit/verify.py", + "--write", + "/tmp/t29-postfix-review-a6_slr_a/boolean_count output.json" + ], + "cwd": "/tmp/t29-postfix-review-a6_slr_a", + "exit_code": 1, + "name": "boolean_count_write", + "seconds": 0.23003977804910392, + "stderr": "FAIL_T29_CAPACITY_TAGGED_PATTERN_WITNESS: declared remainder_profile values must be positive integers: True", + "stdout": "" + }, + { + "command": [ + "/kmh-nfs-ssd-us-mount/code/hanhong/miniforge3/bin/python", + "-I", + "-O", + "-B", + "/tmp/t29-postfix-review-a6_slr_a/checkout with spaces/research/t29-capacity-audit/verify.py" + ], + "cwd": "/tmp/t29-postfix-review-a6_slr_a", + "exit_code": 1, + "name": "noncanonical_key_default", + "seconds": 0.23194515809882432, + "stderr": "FAIL_T29_CAPACITY_TAGGED_PATTERN_WITNESS: declared remainder_profile keys must be canonical decimal rank strings: '01'", + "stdout": "" + }, + { + "command": [ + "/kmh-nfs-ssd-us-mount/code/hanhong/miniforge3/bin/python", + "-I", + "-O", + "-B", + "/tmp/t29-postfix-review-a6_slr_a/checkout with spaces/research/t29-capacity-audit/verify.py", + "--write", + "/tmp/t29-postfix-review-a6_slr_a/noncanonical_key output.json" + ], + "cwd": "/tmp/t29-postfix-review-a6_slr_a", + "exit_code": 1, + "name": "noncanonical_key_write", + "seconds": 0.23090198705904186, + "stderr": "FAIL_T29_CAPACITY_TAGGED_PATTERN_WITNESS: declared remainder_profile keys must be canonical decimal rank strings: '01'", + "stdout": "" + } + ], + "fresh_write_byte_equal_expected": true, + "frozen_files_match_original_review": { + "CLAIM.json": true, + "FINAL-REVIEW.json": true, + "REVIEW.md": true, + "SOURCES.json": true, + "WITNESS.json": true, + "review.py": true + }, + "independent_control_delta_and_inventory_comparison": 7, + "malformed_profiles_rejected_before_output": 8, + "producer_controls": 31, + "scratch_directory": "/tmp/t29-postfix-review-a6_slr_a", + "second_witness_exactly_matches_blind": true, + "source_pins_unchanged_and_valid": 5, + "unchanged_mathematical_fields": [ + "u", + "profile", + "quotas", + "demands", + "bins", + "rank_mass", + "total_signed_price", + "credit_slack", + "legal_patterns", + "legal_patterns_by_capacity", + "source_sha256", + "witness_file_sha256" + ] + }, + "findings": [], + "overlap_scope_review": "dated qualified keyword/body evidence; distinguishes changed R480 PR1129; no absolute novelty guarantee", + "phase": "narrow post-fix review; original blind and integration records preserved", + "publication_acceptance": true, + "recorded_at": "2026-10-13T19:17:47.438539+00:00", + "review_md_append_only": true, + "review_md_original_sha256": "bc1afb4c1176b174973133f1092c757e6cefd0fae80bc254b50d0b97d473977b", + "reviewed_sha256": { + "CLAIM.json": "3ad349f8546610e3efcf9c662dddb74739334d17cba4d2dbc10f8471f513dad8", + "EXPECTED.json": "2d6301982d58e9176b3d1fd2353803ef1e183d8f22bf3ee2c9d26af4ed069384", + "FINAL-REVIEW.json": "73c73cc89f822d90f30ff1cc88e1dcc8f21a405a9d0d380a0409640705c25027", + "OVERLAP.json": "56dc7882e699c89533526e9914ea221ba141a353ab29fc4eda8c3431a7bc5a13", + "PROOF.md": "9fc548c21d2d7ee8b23dcb67d9001b8bc604f1e2a7bea32f3303b12e5053a02e", + "README.md": "b1deef7889fb2d489508abe8c257ad1d209a638d05367e6f52054fdcc1b587ab", + "REVIEW.md": "fc922062470afcc0b6c03a7a5de8b66ba64b5777fc9eeb5ecdc140662e227d53", + "SOURCES.json": "412117fd06d9f7b6f45ee394c5ad03f66ba20737a47ebb658f08719b37799695", + "WITNESS.json": "07f269952622b3cb562dd3988f1e5e55b491dc1fcc0c46f848208641b10aadbd", + "review.py": "344678eac3a3ddeef8ab91502ce33b375accfa4521c53107bbc40517f9a6f6df", + "verify.py": "6c58b45b5633c7f619d03cca0337d213c87d1192041b4eb3e5ea1c11605b7430" + }, + "reviewer": "Astra AI mathematical reviewer; no independent human review claimed", + "status": "ACCEPTED" +} diff --git a/research/t29-capacity-audit/PROOF.md b/research/t29-capacity-audit/PROOF.md new file mode 100644 index 0000000000..9013468c52 --- /dev/null +++ b/research/t29-capacity-audit/PROOF.md @@ -0,0 +1,133 @@ +# Capacity-tagged realization of the sharp T=29 profile + +All statements concern the fixed U8 whole-helper family of PR795/PR890/PR942 +and the arithmetic relaxation of PR992. Nothing here concerns chronology, +owner geometry, the physical schedule, the controller invoice or kappa. + +## Setting + +Per replica there are 672 bins of capacity 8 and 448 bins of each capacity +16, 32 and 48, and nine calls supply 720, 288, 486, 1098 and 1944 whole helpers +of widths 4, 5, 7, 8 and 9. At `T=29` the quotas are + +``` +capacity: 8 16 32 48 +bins: 19488 12992 12992 12992 (58464 bins) +width: 4 5 7 8 9 +helpers: 20880 8352 14094 31842 56376 +``` + +Total capacity is `1403136`, total helper width is `986058`, so the residual +mass is `417078 = 14382*29`. PR992's sharp profile is + +``` +n = {0:49770, 1:4, 2:1, 48:8689}, +``` + +which has 58464 bins and mass `4 + 2 + 48*8689 = 417078`. + +A *legal pattern* is a capacity tag together with a multiset of whole helper +widths of total width at most that capacity; its remainder is the unused +capacity. There are 1163 legal patterns. With the inherited prices +`(-1,-20,-8,-2,4)` for widths `(4,5,7,8,9)` and bonuses `(2,4,8,-13)` for +capacities `(8,16,32,48)`, `u(r)` is the largest bonus plus helper price among +legal patterns of remainder `r`; in particular `u(0)=0`, `u(1)=19`, `u(2)=13` +and `u(48)=-13`. + +**Question (hypothesis q_b6cf2a2ce15a43ed:e10).** Do nonnegative integer +counts of legal patterns exist whose capacity tags meet the four quotas, whose +widths meet the five demands, and whose remainders give exactly `n`, +including all 49770 rank-zero bins? + +## Lemma 1 (zero slack forces tight bins) + +For any realization, the sum of all bin prices is fixed by the inventory: + +``` +sum_c quota_c * bonus_c + sum_w demand_w * price_w = 29*(896 - 4788) = -112868. +``` + +Each bin of remainder `r` has price at most `u(r)`, so the sum is at most +`sum_r n_r u(r) = 4*19 + 13 - 13*8689 = -112868`. Equality of the two sums +forces every bin to attain `u(r)`. The checker verifies both totals. + +## Lemma 2 (forced structure) + +Enumerating the tight patterns of the four remainder classes present in `n`: + +- rank 48: only the empty capacity-48 bin; +- rank 1: only `32:{9,9,9,4}`; +- rank 2: only `32:{9,9,8,4}` and `32:{9,9,4,4,4}`; +- rank 0: `8:{8}`, `8:{4,4}`; `16:{8,8}`, `16:{8,4,4}`, `16:{4,4,4,4}`, + `16:{9,7}`; `32:{8,8,8,8}`, `32:{8,8,8,4,4}`, `32:{8,8,4,4,4,4}`, + `32:{8,4,4,4,4,4,4}`, `32:{4^8}`, `32:{9,8,8,7}`, `32:{9,8,7,4,4}`, + `32:{9,7,4,4,4,4}`, `32:{9,9,7,7}`, `32:{9,9,9,5}`; `48:{9,9,9,9,8,4}`, + `48:{9,9,9,9,4,4,4}`. + +Consequences, each checked by the program: + +1. The only tight pattern containing a width-five helper is `32:{9,9,9,5}`, so + every realization has exactly 8352 such bins. +2. The 12992 capacity-48 bins split into 8689 empty bins and 4303 full bins, + and each full tight capacity-48 pattern holds four nines: 17212 nines. +3. With the 25056 nines of item 1 and the 14 nines of the rank-1 and rank-2 + bins, exactly `56376 - 17212 - 25056 - 14 = 14094` nines remain, which + equals the width-seven demand. Every remaining tight rank-zero pattern + pairs each nine with exactly one seven, so the width-nine demand is implied + by the width-seven demand. +4. Sevens live in `16:{9,7}` (one each) or in capacity-32 tight patterns (at + most two each). After items 1 and the rank-1/rank-2 bins, 4635 capacity-32 + bins remain, so at least `14094 - 2*4635 = 4824` and at most 12992 + capacity-16 bins are `16:{9,7}` in every realization. This is a necessary + range only; nothing is claimed about which of its values are attained. + +## Proposition (a compact witness exists) + +The following ten pattern counts realize `n` exactly: + +``` + 8:{8} 11202 32:{9,9,9,5} 8352 + 8:{4,4} 8286 32:{9,9,9,4} 4 (rank 1) +16:{9,7} 12992 32:{9,9,8,4} 1 (rank 2) + 32:{9,9,7,7} 551 + 32:{8,8,8,8} 4084 +48:{} 8689 48:{9,9,9,9,8,4} 4303 +``` + +Quotas: `11202+8286 = 19488`; `12992`; `8352+4+1+551+4084 = 12992`; +`8689+4303 = 12992`. Demands: fours `2*8286 + 4 + 1 + 4303 = 20880`; fives +`8352`; sevens `12992 + 2*551 = 14094`; eights `11202 + 1 + 4*4084 + 4303 = +31842`; nines `12992 + 3*8352 + 12 + 2 + 2*551 + 4*4303 = 56376`. Remainders: +`8689` of rank 48, `4` of rank 1, `1` of rank 2 and `58464 - 8694 = 49770` of +rank 0. Every pattern is tight, so the total price is `-112868`. + +The witness is reconstructed in closed form by `verify.py` from three explicit +choices (all capacity-16 bins are `16:{9,7}`, the free capacity-32 bins are +`32:{8,8,8,8}`, the full capacity-48 bins are `48:{9,9,9,9,8,4}`); the +remaining counts are then forced by the quotas and demands. + +## Second realization (nonuniqueness) + +The reviewer's blind hand construction (REVIEW.md) is a second realization, +transcribed into `verify.py` as data and checked by the same exact census: + +``` + 8:{8} 11203 32:{9,9,9,5} 8352 + 8:{4,4} 8285 32:{9,9,9,4} 4 (rank 1) +16:{9,7} 4824 32:{9,9,4,4,4} 1 (rank 2) +16:{8,8} 8168 32:{9,9,7,7} 4635 +48:{} 8689 48:{9,9,9,9,8,4} 4303 +``` + +It differs from the witness above in eight pattern counts, including the +rank-2 pattern. Two distinct checked realizations establish that the +realization is not unique; nothing is claimed about any other count vector. + +## Conclusion and limits + +PR992's sharp aggregate profile passes the capacity-tagged whole-helper +pattern constraint that its relaxation omits: there is no obstruction at this +level, and the realization is not unique, as the two checked realizations +show. Lemma 2, item 4, is a necessary range only. The result does not +construct owner windows, charts or a controller for `T=29`, does not bound any +supplier outside the fixed U8 family, and changes no kappa. diff --git a/research/t29-capacity-audit/README.md b/research/t29-capacity-audit/README.md new file mode 100644 index 0000000000..e06a0769b3 --- /dev/null +++ b/research/t29-capacity-audit/README.md @@ -0,0 +1,114 @@ +# Capacity-tagged pattern feasibility of PR992's sharp T=29 profile + +**Scoped adversarial audit; no new kappa.** woklerx's +[PR992](https://github.com/CrocSwap/integer-mult-bounds/pull/992) +(`research/t37-integrality-audit`) exhibits the aggregate remainder profile +`{1:4, 2:1, 48:8689}` at `T=29` as the sharp case of its integer penalty and +states that it constructs no owner assignment for it. This package checks the +next necessary condition that PR992's arithmetic relaxation omits: whether +nonnegative integer counts of legal, capacity-tagged whole-helper bin patterns +meet the fixed U8 capacity quotas `(672,448,448,448)*29`, the width demands +`(720,288,486,1098,1944)*29` for widths `(4,5,7,8,9)`, and that exact +remainder profile including all 49770 rank-zero bins. + +**Result: feasible, and not unique.** A ten-pattern integer witness exists +(`WITNESS.json`), reconstructed in closed form and checked exactly; a second +realization with eight different pattern counts, the reviewer's blind hand +construction from `REVIEW.md`, is checked by the same census. The zero credit +slack forces every bin of every realization to attain `u(r)`; this pins all +8352 fives into `32:{9,9,9,5}` bins, all 4303 full capacity-48 bins to +four-nine patterns, and makes the width-nine demand a consequence of the +width-seven demand. See [PROOF.md](PROOF.md). No obstruction arises at this +level; nothing is claimed about count vectors other than the two checked +realizations. Chronology, owner geometry, the physical schedule, the +controller invoice and the selected PR1042 supplier are outside scope. + +## Reproduce + +Standard-library Python 3.9+ only, no network, writes nothing: + +```sh +python3 -I -O -B research/t29-capacity-audit/verify.py +``` + +Expected final line: + +```text +PASS_T29_CAPACITY_TAGGED_PATTERN_WITNESS patterns=1163 witness_bins=58464 witness_patterns=10 realizations=2 controls=31 no_new_kappa +``` + +The checker pins the consumed predecessor files by sha256 (`SOURCES.json`, +base `ba82555c64e1879e4b7decce28186f208fcb8262`), enumerates all 1163 legal +patterns once by Cartesian product, recomputes the price table `u(r)` +independently by a maximum-price dynamic program over exact fills (the two +tables must agree), checks the bin-count, rank-mass and zero-slack identities, +verifies the forced structure, checks every quota, demand and remainder of +both realizations, validates the witness's declared `remainder_profile` +against the recomputed census (canonical decimal keys, positive integer +values, no booleans, no missing or extra classes) before any acceptance or +`--write`, and compares the complete certificate with `EXPECTED.json`. All +checks raise explicit exceptions and remain active under `python -O`. +`--json` prints the certificate; `--write NEW_PATH` writes a fresh +certificate only after every check has passed and refuses to overwrite; +`--repository ROOT` points at another checkout of the same base. + +## Negative controls (all 31 must be rejected) + +**Seven inventory mutations of the witness.** For each, `verify.py` recomputes +the change in bin count, residual mass, dual credit `sum (48u(r)+13r) n_r` and +actual signed price, and records which inventory the mutation violates; the +values below are copied from `EXPECTED.json`. + +| Mutation | bins | mass | dual credit | actual price | violates | rejected at | +| --- | ---: | ---: | ---: | ---: | --- | --- | +| `16:{9,7}` to `16:{8,8}` | 0 | 0 | 0 | 0 | widths 7,8,9 | width demand | +| `32:{9,9,9,5}` to `32:{9,9,7,7}` | 0 | 0 | 0 | 0 | widths 5,7,9 | width demand | +| `32:{9,9,8,4}` to `32:{9,9,4,4,4}` | 0 | 0 | 0 | 0 | widths 4,8 | width demand | +| `8:{8}` to `16:{8,8}` | 0 | 0 | 0 | 0 | quotas 8,16; width 8 | capacity quota | +| `48:{}` to `48:{9,9,9,9,8,4}` | 0 | −48 | 0 | +13 | profile 0,48; widths 4,8,9 | remainder profile | +| `32:{9,9,9,4}` to `32:{8,8,8,7}` | 0 | 0 | 0 | −25 | widths 4,7,8,9 | width demand | +| one `8:{8}` bin fewer | −1 | 0 | 0 | 0 | quota 8; profile 0; width 8 | capacity quota | + +Only the first four preserve all of bin count, mass, dual credit and actual +price while violating the inventory. The empty-to-full capacity-48 retag +preserves bin count and dual credit but changes mass by −48 and actual price +by +13; the untight rank-one swap preserves bins, mass and dual credit but +changes actual price by −25; the missing bin changes only the bin count. + +**Eighteen invalid-witness documents:** overfull pattern, negative, fractional +or boolean count, unknown width or capacity, duplicate entry, false +per-pattern remainder; header replicas given as float or boolean, wrong +hypothesis; declared `remainder_profile` missing, false rank-zero count, +missing class, extra zero-count class, boolean value, non-canonical key +`"01"`, swapped class counts. **Six tampered-proof controls:** altered +`u(2)`, wrong replica count, off-by-one profile, same-bin same-mass profiles +with positive and with negative slack, altered source pin. Each rejection +reason is recorded in `EXPECTED.json`. + +## Files and ownership + +- `verify.py`, `WITNESS.json`, `EXPECTED.json`, `SOURCES.json`, `PROOF.md`, + `README.md`: this audit (Claude Fable 5.1, implementation). +- `CLAIM.json`, `OVERLAP.json`, `ACCEPTANCE.json`: sprint leader coordination. + `review.py`, `REVIEW.md`, `FINAL-REVIEW.json`, `POSTFIX-REVIEW.json`: Astra's + independent review records. The original findings are preserved in + `FINAL-REVIEW.json`; all four are resolved by the accepted post-fix review + in `POSTFIX-REVIEW.json`. During + the blind phase the implementation read neither the review nor Gemini's + brainstorming notes; the corrections R1 to R4 listed in `FINAL-REVIEW.json` + were made after the review was released, and the second realization is + transcribed from `REVIEW.md`. Exploratory control notes are retained + separately by the coordinator and are not part of this certificate. + +## Attribution and scope + +Prices, bonuses and the fixed family are Chafik Boukhalfa's (PR795, PR890); +the all-replica relaxation is Jonathan Capalbo's (PR942); the integer slack +lattice and the sharp T=29 profile are woklerx's (PR992); the T16 owner lineage +is Hao Yan's (PR858). This package adds only the capacity-tagged feasibility +statement, its forced-structure lemma and the two checked realizations. +Prepared with substantial AI assistance (Anthropic Claude Fable 5.1 as +implementation lead, with separate AI review and control drafting); no +independent human peer review is claimed. Apache-2.0. Finite checks here are +not a proof of the multiplication theorem and do not change the selected +result. diff --git a/research/t29-capacity-audit/REVIEW.md b/research/t29-capacity-audit/REVIEW.md new file mode 100644 index 0000000000..df48f4e146 --- /dev/null +++ b/research/t29-capacity-audit/REVIEW.md @@ -0,0 +1,327 @@ +# Phase 2 independent mathematical review: T29 capacity realization + +**Outcome: supports hypothesis `q_b6cf2a2ce15a43ed:e10`.** An independently +derived ten-pattern integer witness realizes the proposed residual profile +with every capacity quota and helper demand exactly. This is an audit of the +historical fixed-U8 inventory relaxation, not a physical owner construction. +No defect in the predecessor claim was found: PR992 explicitly left this +realization question outside its scope. + +Reviewer: Astra mathematical/scope reviewer, with substantial OpenAI assistance. +New reviewer material is Apache-2.0. Base: +`ba82555c64e1879e4b7decce28186f208fcb8262`, branch +`contribution/seed69-adversarial-audit`. Only the leader's CLAIM, inherited +sources, and reviewer-owned files were read for this phase; the implementer's +code/artifacts and Gemini's output were not inspected. No solver, producer +module, native replay, or other package checker was imported. + +## Source interpretation + +- `research/complex-t37-owners/ALL-T-PROOF.md`, fixed-family section: each + replica has 672 bins of capacity 8 and 448 each of capacities 16, 32, 48; + each of its nine calls contributes helper counts `(80,32,54,122,216)` at + widths `(4,5,7,8,9)`. +- `research/complex-t21-owner-bound/PROOF.md`: the per-replica unused mass + is 14382 and total signed price is -3892. Whole helpers are the units; + signed dual constraints are necessary and are not asserted sufficient. +- `research/t37-integrality-audit/PROOF.md`, lines 76–80: at T29 the sharp + relaxation witness is `{1:4,2:1,48:8689}` with zero signed-price slack. + Its README explicitly excludes bin-type inventory realization. +- Restoring omitted zero ranks gives `2016*29 - (4+1+8689) = 49770`. + Rank-zero bins still consume a capacity quota. Width demands are multiplied + by `9*29`, not just by 29. These are bins indexed by an idle child and port, + not a count of distinct physical families throughout execution. + +The four exact source SHA-256 pins are embedded in `review.py` and checked +before calculation. No current selected certificate is used as a floating +input. The base selects PR1042, whose changed supplier is outside this audit. + +## Exact proof and independently derived witness + +For a bin of capacity C and width-count vector h, let +`sigma = bonus(C) + p.h`, `r = C - w.h`, with inherited +`p=(-1,-20,-8,-2,4)` and bonuses `(2,4,8,-13)`. +By definition `sigma <= u(r)`. The target satisfies + +``` +sum u(r)*n_r = 4*19 + 13 - 8689*13 = -112868 = -3892*29. +``` + +The capacity and helper quotas force the actual sum of sigma to the same +number. Consequently all nonnegative bin slacks `u(r)-sigma` must vanish. +This is a necessary equality condition, not an inference that arbitrary +aggregate witnesses are realizable. + +An independent reachable-state closure enumerates all 1163 legal patterns, +45 attained ranks, and 22 tight patterns with ranks in `{0,1,2,48}`. Adding +one helper at a time covers every legal vector: removing any present helper +strictly decreases its fill and leaves another legal vector. Duplicate states +are eliminated by their full five-component multiplicity vector. This is +neither the inherited Cartesian product enumeration nor its value-only +unbounded-knapsack recurrence. + +A useful elimination identity for hand construction is + +``` +25*(h9-h7-3*h5) = C-r + 4*(sigma-bonus(C)). +``` + +It is checked on every legal pattern. A full tight cap-48 bin can be chosen +as `4+8+4*9`; all 8689 rank-48 bins are empty cap-48 bins, leaving 4303 such +full bins. Place each of the 8352 width-5 helpers in a cap-32 bin with three +width-9 helpers. The four rank-one bins use `4+3*9`, and the rank-two bin +uses `3*4+2*9`. Fill the other 4635 cap-32 bins with `2*7+2*9`, leaving +4824 width-7 helpers for cap-16 bins of type `7+9`. The remaining widths +4 and 8 then give the following complete witness, without optimization: + +| Capacity | Bin count | h4 | h5 | h7 | h8 | h9 | Residual | +|---|---:|---:|---:|---:|---:|---:|---:| +| 8 | 8285 | 2 | 0 | 0 | 0 | 0 | 0 | +| 8 | 11203 | 0 | 0 | 0 | 1 | 0 | 0 | +| 16 | 4824 | 0 | 0 | 1 | 0 | 1 | 0 | +| 16 | 8168 | 0 | 0 | 0 | 2 | 0 | 0 | +| 32 | 8352 | 0 | 1 | 0 | 0 | 3 | 0 | +| 32 | 4635 | 0 | 0 | 2 | 0 | 2 | 0 | +| 32 | 4 | 1 | 0 | 0 | 0 | 3 | 1 | +| 32 | 1 | 3 | 0 | 0 | 0 | 2 | 2 | +| 48 | 4303 | 1 | 0 | 0 | 1 | 4 | 0 | +| 48 | 8689 | 0 | 0 | 0 | 0 | 0 | 48 | + +The exact checked totals are: + +- Capacities `(8,16,32,48)`: `(19488,12992,12992,12992)`; 58464 bins. +- Widths `(4,5,7,8,9)`: `(20880,8352,14094,31842,56376)`; 131544 helpers. +- Residuals `{0:49770,1:4,2:1,48:8689}`; mass 417078. +- Total capacity 1403136, used cells 986058, signed price -112868, + and sum of nonnegative price slacks zero. + +In addition to the weighted census, a separate unit-slot oracle expands every +bin and every indivisible helper, fills literal slots in each bin, and counts +unoccupied slots. All three inventories agree. This constructs a packing +in abstract bins only; the slot order has no controller or chart meaning. + +## Adversarial controls and executed evidence + +Eight invalid witness controls reject at their specified predicates: + +1. In one cap-16 bin replace `7+9` by `4+4+4+4`. Capacity, residual profile, + total bin count, fill and signed price all remain unchanged. The helper + census changes by `(4,0,-1,0,-1)` and is rejected. +2. Replace three full cap-16 bins, each containing two width-8 helpers, by + two cap-8 bins and one cap-32 bin, all filled with the same six width-8 + helpers. Residual profile, helper census, total capacity, total bin count, + mass and signed price remain unchanged. The capacity census changes by + `(2,-3,1,0)` and is rejected. +3. Omit the empty bins: rejected capacity census. +4. Put a width-9 helper in a cap-8 bin: rejected overflow. +5. Fractional helper: rejected whole-helper domain. +6. Negative multiplicity: rejected multiplicity domain. +7. Boolean multiplicity: rejected multiplicity domain. +8. Unknown capacity: rejected capacity domain. + +The first two deliberately pass the implemented weak aggregate checker. +These are invalid-witness controls; they do not prove their residual profile +infeasible, since the valid witness above has that same profile. Reversing +row order and splitting a multiplicity into duplicate rows both preserve +the full valid receipt. + +Executed on CPython 3.10.14 (conda-forge, GCC 12.3.0): + +``` +python -I -B research/t29-capacity-audit/review.py +python -I -O -B research/t29-capacity-audit/review.py +``` + +Both exited 0 with `PASS_INDEPENDENT_T29_CAPACITY_REVIEW`, all 1163 patterns, +22 target-support tight patterns, eight rejections and two positive controls. +Measured wall times were 0.3853 s and 0.4739 s; these are local observations, +not performance guarantees. Outputs were byte-identical, SHA-256 +`de43d59347fb46e60943a98a4d1180c8938ceda249a7fdd7f1f76563caca5e56`. +Temporary receipts were retained in +`/kmh-nfs-ssd-us-mount/code/siri/tmp/t29-astra-review-7to23a8l/`. +Reviewed script SHA-256: +`1bee1e2785567a7fa70d87c0d5a5ff7ca83616a0da2def3a88805b94a418f59c`. + +## Narrow overlap refresh and limits + +Public GitHub REST checks at 2026-10-13 18:46 UTC: + +- Open-PR searches for `T29` and `(8689 OR 49770 OR capacity-tagged)` returned + zero matches. Search indexing and unpublished work remain limitations. +- The `capacity` + `bin` open-PR search returned five results. The relevant + recent one was [PR1034](https://github.com/CrocSwap/integer-mult-bounds/pull/1034), + open at `a1aff126d9816cff75a5293675ae6e10f65377db`, a catalogue-scoped + mixed-provider separating dual. It does not supply this T29 integer lift. +- [PR992](https://github.com/CrocSwap/integer-mult-bounds/pull/992) is closed, + head `0efdfc28b1eb71c91c012ca1e1945baeeebce7bb`, and incorporated in the base + ledger. Its sharpness and credit lattice are predecessor results, not new + claims here. Credit remains with Chafik Boukhalfa (PR795/890 signed prices), + Jonathan Capalbo (PR942), and woklerx (PR992). +- The two open issues were #913 (all-size/compiler) and #650 (Discussions). + No open coordination/claim issue was identified; no pinned coordination + issue ID was found. No GitHub writes were made. + +Conditional on the inherited arithmetic lemma, the witness shows that its +sharp numerator penalty is also attained after imposing these four capacity +and five helper inventories. No logarithm/moment engine needed rerunning. +Chronology, invocation-specific matching, geometry, family nonaliasing, native +semantics, finite invoice, physical feasibility, a new kappa and the changed +PR1042 family remain excluded. This phase does not review the implementer's +final package; that review awaits explicit integration authorization. + +## Authorized integration review (after the blind phase) + +**Disposition: mathematical witness passes; actionable corrections required +before publication acceptance.** This section is post-hoc integration review, +not evidence that the reviewer or implementer remained blind after phase 2. +The preceding witness, commands and script hash retain their historical meaning. +The reviewer script now accepts `--witness PATH` for this separate phase. + +The producer's ten-pattern witness differs from the blind witness: all 12992 +cap-16 bins use `7+9`, versus 4824 in the blind construction. Passing that +actual JSON through the reviewer's independent census and full unit-slot +oracle gives exactly the same four capacity quotas, five helper demands, +four residual counts and zero signed-price slack. The full 45-entry `u` +table and every one of the 22 tight patterns match the independent reachable +closure. Consequently Lemmas 1 and 2 and the explicit existence proposition +are supported. The interval in Lemma 2 is a necessary interval only. + +### Required corrections + +1. **Unsupported inference, PROOF.md lines 112–113.** A necessary range of + 8169 integer values does not prove all or many of them feasible. Replace + the justification for "far from unique" with the two independently + checked explicit witnesses, claiming simply nonuniqueness, or supply + a construction for additional values. No such range construction was + established in this review. +2. **Incorrect control description, README.md lines 49–51 and the inventory + control comment in verify.py.** Of the seven inventory mutations, + `retag_empty_48_to_full_48_changes_profile` changes residual mass by -48; + it does not preserve aggregate rank mass. The first four preserve residual + mass, dual credit and actual signed price. The untight rank-one mutation + preserves mass and dual credit but changes actual signed price by -25. + The missing-bin mutation preserves mass and credit but reduces bin count. + Describe these separate controls accurately; asserting that all seven + preserve mass is false. The existing rejections themselves work. +3. **Unchecked witness metadata on regeneration, verify.py certificate().** + `WITNESS.json.remainder_profile` is not compared with `PROFILE` or the + counted witness. In an isolated copy I changed its rank-zero count to 1: + default verification rejected the stale file hash, but `--write NEW_PATH` + still returned PASS and generated a receipt containing the contradictory + witness hash. Add an explicit declared-profile check and a control that + reaches it. The actual packing is checked against the correct hardcoded + profile, so this is a semantic metadata binding gap, not a false packing + or a counterexample to H. +4. **Minor independence wording, README.md lines 38–39.** The producer uses + one Cartesian pattern enumeration and an independent maximum-price DP. + The DP reconstructs `u(r)`; it does not enumerate or count all 1163 + multiplicity vectors. State those two tasks precisely. The reviewer + separately does enumerate every vector by reachable-state closure. + +### Executed integration evidence + +``` +python -I -O -B research/t29-capacity-audit/review.py \ + --witness research/t29-capacity-audit/WITNESS.json +``` + +Independent witness, all-slot and tight-class comparison passed in 0.8368 s. +All five SOURCES pins match both working files and `git show` at the recorded +base. Source attribution in README is consistent with the predecessor roles; +no independent human review is claimed. + +A minimal checkout at `/tmp/t29-final-review-9rhqj5pl/checkout with spaces/` +contains only the six producer files and the five pinned predecessor files. +From an unrelated working directory, `python -I -O -B` passes with both +default root detection and explicit `--repository ROOT`; each reports all +21 producer controls. Fresh `--write` regenerates an equal EXPECTED object. +An existing output is refused and its bytes remain unchanged. Stale EXPECTED, +malformed witness JSON, changed witness count, corrupt/missing source files, +and malformed SOURCES all fail nonzero under `-O`. Malformed JSON produces +a traceback rather than a formatted Reject diagnostic, but fails closed. +The false-profile default/re-generation distinction is recorded above. + +Post-blind instrumentation captured the producer's actual seven inventory +mutations and independently recomputed their invariants using reviewer code: + +| Mutation | Delta bins | Delta residual mass | Delta dual credit | Delta actual signed price | +|---|---:|---:|---:|---:| +| cap16 7+9 to 8+8 | 0 | 0 | 0 | 0 | +| cap32 9+9+9+5 to 9+9+7+7 | 0 | 0 | 0 | 0 | +| rank2 alternative | 0 | 0 | 0 | 0 | +| full cap8 to full cap16 | 0 | 0 | 0 | 0 | +| empty cap48 to full cap48 | 0 | -48 | 0 | 13 | +| rank1 untight pattern | 0 | 0 | 0 | -25 | +| one bin short | -1 | 0 | 0 | 0 | + +Here dual credit means `sum (48*u(r)+13*r)*n_r`; it is distinct from +actual signed bin price. The positive- and negative-slack profile controls +also have the claimed common bin count and mass, with signed-price slacks ++25 and -50. These are deliberately rejected by the zero-slack theorem's +admission predicate, not assertions that every positive-slack profile is +physically infeasible. + +Commands, exit codes, timings, invariant deltas and reviewed producer hashes +are preserved in `FINAL-REVIEW.json`. Scratch logs are under the temporary +directory above. Only reviewer-owned files were changed. The feasibility +result remains accepted mathematically; publication acceptance awaits the +listed corrections and their focused recheck. + + +## Narrow post-fix review: R1–R4 resolved + +**ACCEPTED for publication of this scoped capacity-tagged packing audit.** +This section appends to, and does not replace, the original findings. The +original `FINAL-REVIEW.json` is preserved unchanged. This is AI review, +not an independent human review or a new physical-feasibility claim. + +- **R1 resolved.** PROOF and README now claim nonuniqueness from two explicit + checked realizations only. The necessary interval is labelled necessary; + no interpolation or full-range feasibility is claimed. `SECOND_WITNESS` + was compared entry for entry with the reviewer's original blind witness + and agrees exactly. The producer and blind realizations differ in eight + pattern counts, as stated. +- **R2 resolved.** The receipt and README now distinguish changes to bin + count, residual mass, dual credit and actual signed price. The actual + producer's seven mutations were captured and all four aggregate deltas, + as well as their capacity/helper/profile inventory differences, were + recomputed using reviewer code. Every recorded value agrees. In + particular, the empty cap-48 replacement changes mass by -48 and signed + price by +13; the untight rank-one replacement changes price by -25; + removing a full cap-8 bin changes bin count by -1. +- **R3 resolved.** `admit_document` checks the actual packing census and then + validates the declared profile before `certificate` returns, so both + default comparison and fresh `--write` require semantic agreement. The + profile requires canonical decimal keys and positive integer counts, + explicitly excluding booleans. An isolated checkout with spaces was + tested under `-I -O -B`: a false zero-rank count, missing profile, boolean + count and noncanonical key each reject in both modes with the specific + profile diagnostic, empty stdout, and no output file created by `--write`. +- **R4 resolved.** Documentation and code descriptions now correctly state + one Cartesian enumeration of legal patterns and an independent + maximum-price dynamic program reconstructing `u(r)`. + +The relocated baseline passes all **31** controls with two realizations, +1163 patterns and 58464 bins. Explicit `--repository` also passes. A fresh +write is byte-identical to the committed EXPECTED.json. Commands, exit codes, +diagnostics, timings and exact reviewed hashes are in `POSTFIX-REVIEW.json`; +scratch evidence is `/tmp/t29-postfix-review-a6_slr_a/`. Typical individual +CLI runs took 0.23–0.25 seconds on the same Python 3.10.14 interpreter. + +Before this append, WITNESS.json, SOURCES.json, review.py, REVIEW.md and +CLAIM.json matched their original reviewed hashes. All five predecessor +source pins still match. FINAL-REVIEW.json still has SHA-256 +`73c73cc89f822d90f30ff1cc88e1dcc8f21a405a9d0d380a0409640705c25027`. +The unchanged `u`, quotas, demands, profile, mass and other mathematical +receipt fields were compared with the earlier snapshot; the unchanged +full mathematical derivation was not rerun. + +CLAIM.json still scopes the result to the historical PR992/U8 capacity-tagged +integer realization and excludes chronology, geometry, physical scheduling, +new kappa and PR1042's changed supplier. OVERLAP.json is a dated keyword/body +review, explicitly limited rather than a guarantee of novelty; its PR1129 +comparison distinguishes the changed R480 supplier from this fixed-U8 +question. Those coordination records were reviewed, not modified. Attribution +and the distinction between blind derivation and later transcription are +retained. No remaining actionable finding was identified in this narrow +re-review. Only this append and POSTFIX-REVIEW.json were written. diff --git a/research/t29-capacity-audit/SOURCES.json b/research/t29-capacity-audit/SOURCES.json new file mode 100644 index 0000000000..591c10db65 --- /dev/null +++ b/research/t29-capacity-audit/SOURCES.json @@ -0,0 +1,18 @@ +{ + "base_commit": "ba82555c64e1879e4b7decce28186f208fcb8262", + "hypothesis": "q_b6cf2a2ce15a43ed:e10", + "consumed_statements": { + "research/complex-t21-owner-bound/PROOF.md": "per-replica idle stock 672 cap-8 and 448 each of cap-16/32/48; nine calls supply 720,288,486,1098,1944 helpers of widths 4,5,7,8,9; mass 14382*T; signed price -3892*T", + "research/t37-integrality-audit/PROOF.md": "T=29 profile {1:4,2:1,48:8689} has mass 417078 and signed price -112868 (zero credit slack); sharp penalty delta(2)", + "research/t37-integrality-audit/README.md": "sharpness statement and explicit disclaimer that no physical owner assignment is constructed", + "research/t37-integrality-audit/EXPECTED.json": "residue-29 certificate profile and signed-price table u(r); 1163 legal bin patterns", + "research/complex-t37-owners/ALL-T-PROOF.md": "PR795/PR890 integer prices (-1,-20,-8,-2,4) and bonuses (2,4,8,-13); u(0)=0, u(1)=19, u(48)=-13" + }, + "sha256": { + "research/t37-integrality-audit/PROOF.md": "0dd18b2b486b98dc06e67b0b64e21dc18b6282af483f975e551b1f36dbc5d7ca", + "research/t37-integrality-audit/README.md": "5e90726de4069d8d19c1f3cf49e636578f46c1d150f1b8d7a7ca64c90b78ea1c", + "research/t37-integrality-audit/EXPECTED.json": "17ffdeffab4ae2a843381ea1e87305608e4caac27cc15293b590c6313a2dd095", + "research/complex-t21-owner-bound/PROOF.md": "2aa0aa6ec1d87402138564c38749b5ca0f058c16817efdf58a2685d2d90cb417", + "research/complex-t37-owners/ALL-T-PROOF.md": "4c0c71ccd0afb850538af1b467e5208b7eb3edd0260fded84e02a8c01dfc868b" + } +} diff --git a/research/t29-capacity-audit/WITNESS.json b/research/t29-capacity-audit/WITNESS.json new file mode 100644 index 0000000000..50e46024fe --- /dev/null +++ b/research/t29-capacity-audit/WITNESS.json @@ -0,0 +1,18 @@ +{ + "hypothesis": "q_b6cf2a2ce15a43ed:e10", + "replicas": 29, + "remainder_profile": {"0": 49770, "1": 4, "2": 1, "48": 8689}, + "note": "Every bin is listed with its capacity tag, including all 49770 rank-zero bins and the 8689 empty capacity-48 bins. Widths are whole helpers. Counts are nonnegative integers; no solver output is trusted, verify.py rechecks every quota, width demand and remainder exactly.", + "patterns": [ + {"capacity": 8, "widths": [8], "count": 11202}, + {"capacity": 8, "widths": [4, 4], "count": 8286}, + {"capacity": 16, "widths": [9, 7], "count": 12992}, + {"capacity": 32, "widths": [9, 9, 9, 5], "count": 8352}, + {"capacity": 32, "widths": [9, 9, 9, 4], "count": 4}, + {"capacity": 32, "widths": [9, 9, 8, 4], "count": 1}, + {"capacity": 32, "widths": [9, 9, 7, 7], "count": 551}, + {"capacity": 32, "widths": [8, 8, 8, 8], "count": 4084}, + {"capacity": 48, "widths": [], "count": 8689}, + {"capacity": 48, "widths": [9, 9, 9, 9, 8, 4], "count": 4303} + ] +} diff --git a/research/t29-capacity-audit/review.py b/research/t29-capacity-audit/review.py new file mode 100644 index 0000000000..84af89bda0 --- /dev/null +++ b/research/t29-capacity-audit/review.py @@ -0,0 +1,227 @@ +#!/usr/bin/env python3 +"""Independent phase-2 T29 inventory audit; no imports from package workers. + +Written for the mathematical reviewer with OpenAI assistance, Apache-2.0. +The ten-pattern witness was derived by hand, independently of the producer. +This certifies capacity-tagged integer packing, not physical owner execution. +""" +from collections import Counter +from pathlib import Path +import argparse +import hashlib +import json + +ROOT = Path(__file__).resolve().parents[2] +PINS = { + "research/complex-t37-owners/ALL-T-PROOF.md": "4c0c71ccd0afb850538af1b467e5208b7eb3edd0260fded84e02a8c01dfc868b", + "research/complex-t21-owner-bound/PROOF.md": "2aa0aa6ec1d87402138564c38749b5ca0f058c16817efdf58a2685d2d90cb417", + "research/t37-integrality-audit/PROOF.md": "0dd18b2b486b98dc06e67b0b64e21dc18b6282af483f975e551b1f36dbc5d7ca", + "research/t37-integrality-audit/README.md": "5e90726de4069d8d19c1f3cf49e636578f46c1d150f1b8d7a7ca64c90b78ea1c", +} +WIDTHS = (4, 5, 7, 8, 9) +PRICES = (-1, -20, -8, -2, 4) +BONUSES = {8: 2, 16: 4, 32: 8, 48: -13} +CAPS = {8: 19488, 16: 12992, 32: 12992, 48: 12992} +HELPERS = {4: 20880, 5: 8352, 7: 14094, 8: 31842, 9: 56376} +RANKS = {0: 49770, 1: 4, 2: 1, 48: 8689} +# (capacity, multiplicity, counts at widths 4,5,7,8,9) +WITNESS = ( + (8, 8285, (2, 0, 0, 0, 0)), + (8, 11203, (0, 0, 0, 1, 0)), + (16, 4824, (0, 0, 1, 0, 1)), + (16, 8168, (0, 0, 0, 2, 0)), + (32, 8352, (0, 1, 0, 0, 3)), + (32, 4635, (0, 0, 2, 0, 2)), + (32, 4, (1, 0, 0, 0, 3)), + (32, 1, (3, 0, 0, 0, 2)), + (48, 4303, (1, 0, 0, 1, 4)), + (48, 8689, (0, 0, 0, 0, 0)), +) + + +def need(ok, reason): + if not ok: + raise ValueError(reason) + + +def legal_patterns(): + """Reachability closure by adding one helper; no Cartesian/DFS generator.""" + result = [] + for capacity in BONUSES: + seen = {(0, 0, 0, 0, 0)} + todo = list(seen) + while todo: + counts = todo.pop() + fill = sum(w * n for w, n in zip(WIDTHS, counts)) + result.append((capacity, counts, capacity - fill, + BONUSES[capacity] + sum(p * n for p, n in zip(PRICES, counts)))) + for i, width in enumerate(WIDTHS): + if fill + width <= capacity: + next_counts = list(counts) + next_counts[i] += 1 + next_counts = tuple(next_counts) + if next_counts not in seen: + seen.add(next_counts) + todo.append(next_counts) + return result + + +def tally(rows): + caps, helpers, ranks = Counter(), Counter(), Counter() + signed = 0 + for capacity, multiplicity, counts in rows: + need(type(capacity) is int and capacity in BONUSES, "capacity domain") + need(type(multiplicity) is int and multiplicity >= 0, "multiplicity domain") + need(len(counts) == 5 and all(type(x) is int and x >= 0 for x in counts), "whole-helper domain") + rank = capacity - sum(w * n for w, n in zip(WIDTHS, counts)) + need(rank >= 0, "capacity overflow") + caps[capacity] += multiplicity + ranks[rank] += multiplicity + for width, number in zip(WIDTHS, counts): + helpers[width] += multiplicity * number + signed += multiplicity * (BONUSES[capacity] + sum(p * n for p, n in zip(PRICES, counts))) + return caps, helpers, ranks, signed + + +def aggregate(rows): + """Deliberately weak: profile/count, mass and signed price, not type quotas.""" + caps, helpers, ranks, signed = tally(rows) + return (dict(ranks) == RANKS and sum(caps.values()) == 58464 + and sum(r * n for r, n in ranks.items()) == 417078 + and signed == -112868) + + +def check(rows, upper): + caps, helpers, ranks, signed = tally(rows) + need(caps == Counter(CAPS), "capacity census") + need(helpers == Counter(HELPERS), "helper census") + need(ranks == Counter(RANKS), "residual census") + need(signed == -3892 * 29, "signed price") + slack = 0 + for capacity, multiplicity, counts in rows: + rank = capacity - sum(w * n for w, n in zip(WIDTHS, counts)) + actual = BONUSES[capacity] + sum(p * n for p, n in zip(PRICES, counts)) + need(actual <= upper[rank], "bin dual inequality") + slack += multiplicity * (upper[rank] - actual) + need(slack == 0, "tight-price necessity") + return dict(capacities=dict(caps), helpers=dict(helpers), residuals=dict(ranks), + signed_price=signed, total_bins=sum(caps.values()), + total_helpers=sum(helpers.values()), residual_mass=417078, + used_cells=sum(w * n for w, n in helpers.items()), price_slack=slack) + + +def unit_slot_oracle(rows): + """Expand every bin and every indivisible helper; count literal unit slots.""" + caps, helpers, ranks = Counter(), Counter(), Counter() + for capacity, multiplicity, counts in rows: + for _ in range(multiplicity): + slots = [None] * capacity + cursor = 0 + for width, count in zip(WIDTHS, counts): + for _ in range(count): + helpers[width] += 1 + for _ in range(width): + need(cursor < len(slots), "slot overflow") + slots[cursor] = width + cursor += 1 + caps[len(slots)] += 1 + ranks[slots.count(None)] += 1 + need(caps == Counter(CAPS) and helpers == Counter(HELPERS) and ranks == Counter(RANKS), + "expanded unit-slot inventories") + + +def subtract_one(rows, index, number=1): + rows = list(rows) + capacity, multiplicity, counts = rows[index] + rows[index] = (capacity, multiplicity - number, counts) + return rows + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--witness', type=Path, help='Post-blind review: independently check a producer WITNESS.json and its sibling EXPECTED.json') + args = parser.parse_args() + for relative, digest in PINS.items(): + need(hashlib.sha256((ROOT / relative).read_bytes()).hexdigest() == digest, + "source drift: " + relative) + need(CAPS == {c: 29 * n for c, n in zip((8, 16, 32, 48), (672, 448, 448, 448))}, "capacity interpretation") + need(HELPERS == {w: 29 * 9 * n for w, n in zip(WIDTHS, (80, 32, 54, 122, 216))}, "nine-call interpretation") + need(RANKS[0] == sum(CAPS.values()) - sum(n for r, n in RANKS.items() if r), "rank-zero interpretation") + patterns = legal_patterns() + need(len(patterns) == 1163 and len({(c, h) for c, h, r, s in patterns}) == 1163, "complete pattern census") + upper = {} + for capacity, counts, rank, signed in patterns: + upper[rank] = max(upper.get(rank, signed), signed) + need(len(upper) == 45 and {r: upper[r] for r in RANKS} == {0: 0, 1: 19, 2: 13, 48: -13}, "source dual values") + tight = [p for p in patterns if p[2] in RANKS and p[3] == upper[p[2]]] + # Direct algebra: fill + 4 * price removes widths 4 and 8. + for capacity, counts, rank, signed in patterns: + x4, x5, x7, x8, x9 = counts + need(25 * (x9 - x7 - 3 * x5) == capacity - rank + 4 * (signed - BONUSES[capacity]), "elimination identity") + need(sum(upper[r] * n for r, n in RANKS.items()) == -3892 * 29, "global price equality") + certificate = check(WITNESS, upper) + unit_slot_oracle(WITNESS) + + controls = [] + # Four width-4 helpers replace width 7 + width 9 in one full cap-16 bin: + # fill 16 and price -4 are unchanged, but source helper demands are broken. + wrong_helpers = subtract_one(WITNESS, 2) + [(16, 1, (4, 0, 0, 0, 0))] + need(aggregate(wrong_helpers), "helper control must preserve weak aggregate certificate") + controls.append(("aggregate-preserving wrong helper census", wrong_helpers, "helper census")) + # Three full cap-16 bins (six width-8 helpers) become two cap-8 and one + # cap-32 bin. All helpers, ranks, total capacity, bin count and price agree. + wrong_caps = subtract_one(WITNESS, 3, 3) + [(8, 2, (0, 0, 0, 1, 0)), (32, 1, (0, 0, 0, 4, 0))] + need(aggregate(wrong_caps) and tally(wrong_caps)[1] == Counter(HELPERS), "capacity control must preserve aggregate and helper census") + controls.append(("aggregate-and-helper-preserving wrong capacity census", wrong_caps, "capacity census")) + controls.append(("omitted empty bins", WITNESS[:-1], "capacity census")) + controls.append(("overfilled bin", WITNESS + ((8, 1, (0, 0, 0, 0, 1)),), "capacity overflow")) + controls.append(("fractional helper", WITNESS + ((8, 1, (0.5, 0, 0, 0, 0)),), "whole-helper domain")) + controls.append(("negative multiplicity", WITNESS + ((8, -1, (0, 0, 0, 0, 0)),), "multiplicity domain")) + controls.append(("boolean multiplicity", WITNESS + ((8, True, (0, 0, 0, 0, 0)),), "multiplicity domain")) + controls.append(("unknown capacity", WITNESS + ((9, 1, (0, 0, 0, 0, 0)),), "capacity domain")) + rejected = [] + for name, rows, reason in controls: + try: + check(rows, upper) + except ValueError as error: + need(str(error) == reason, "wrong rejection for " + name) + rejected.append(dict(control=name, reason=reason)) + else: + raise ValueError("accepted invalid control: " + name) + # Legal row order and splitting a multiplicity must not affect admission. + need(check(tuple(reversed(WITNESS)), upper) == certificate, "order independence") + split = subtract_one(WITNESS, 0) + [(8, 1, (2, 0, 0, 0, 0))] + need(check(split, upper) == certificate, "split-row invariance") + result = dict(status="PASS_INDEPENDENT_T29_CAPACITY_REVIEW", outcome="supports H", + patterns=len(patterns), attained_ranks=len(upper), + tight_patterns_for_target_ranks=len(tight), + witness=WITNESS, certificate=certificate, + negative_controls=rejected, positive_controls=2, + source_sha256=PINS) + if args.witness: + document = json.loads(args.witness.read_text()) + need(document['hypothesis'] == 'q_b6cf2a2ce15a43ed:e10' and document['replicas'] == 29, 'producer header') + need(document['remainder_profile'] == {str(r): n for r, n in RANKS.items()}, 'producer declared profile') + rows = [] + for item in document['patterns']: + need(all(type(w) is int and w in WIDTHS for w in item['widths']), 'producer width domain') + rows.append((item['capacity'], item['count'], tuple(item['widths'].count(w) for w in WIDTHS))) + producer = check(rows, upper) + unit_slot_oracle(rows) + expected = json.loads(args.witness.with_name('EXPECTED.json').read_text()) + need(expected['u'] == {str(r): p for r, p in upper.items()}, 'producer full u table') + classes = {str(r): set() for r in RANKS} + for capacity, counts, rank, signed in tight: + widths = [w for w, n in zip(WIDTHS, counts) for _ in range(n)] + classes[str(rank)].add(str(capacity) + ':{' + ','.join(map(str, sorted(widths, reverse=True))) + '}') + claimed = expected['structure']['tight_patterns_by_class'] + need(set(claimed) == set(classes) and all(len(claimed[r]) == len(classes[r]) and set(claimed[r]) == classes[r] for r in classes), 'producer complete tight classes') + need(producer == certificate, 'independent witnesses have identical inventories') + result['integration'] = dict(witness_sha256=hashlib.sha256(args.witness.read_bytes()).hexdigest(), + producer_witness=producer, complete_tight_classes_match=True, + witness_differs_from_blind=sorted(rows) != sorted(WITNESS)) + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/t29-capacity-audit/verify.py b/research/t29-capacity-audit/verify.py new file mode 100644 index 0000000000..418e78ea60 --- /dev/null +++ b/research/t29-capacity-audit/verify.py @@ -0,0 +1,524 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Capacity-tagged whole-helper pattern feasibility of PR992's sharp T=29 profile. + +PR992 (research/t37-integrality-audit) exhibits the aggregate remainder profile +{1:4, 2:1, 48:8689} at T=29 as the sharp case of its integer penalty and states +that it constructs no physical owner assignment. This checker tests the next +necessary condition that PR992 omits: do nonnegative integer counts of legal, +capacity-tagged bin patterns exist that meet the fixed U8 family's capacity +quotas (672,448,448,448)*29, its whole-helper width demands +(720,288,486,1098,1944)*29 for widths (4,5,7,8,9), and that exact remainder +profile including all 49770 rank-zero bins? + +Everything is exact integer arithmetic in the standard library. No solver is +run and no floating point enters any decision. The checker + + 1. verifies the sha256 pins of the consumed predecessor statements; + 2. enumerates every legal bin count vector once, by Cartesian product, and + recomputes the signed-price table u(r) independently by a maximum-price + dynamic program over exact fills; the two tables must agree; + 3. checks the aggregate identities for T=29: bin count, rank mass and the + zero credit slack sum_r n_r*u(r) = -3892*29; + 4. proves the tightness lemma consequences: every bin of any realization + attains u(r), every width-five helper sits in a {9,9,9,5} capacity-32 bin, + the three nonzero remainder classes have the listed patterns only, and the + width-nine demand is implied by the width-seven demand; + 5. checks WITNESS.json pattern by pattern, validates its declared + remainder_profile against the recomputed census before any acceptance or + --write, reconstructs it in closed form, and checks a second realization + with different counts (the reviewer's blind construction in REVIEW.md), so + the realization is not unique; + 6. runs negative controls: inventory mutations whose preserved and changed + aggregate invariants (bin count, residual mass, dual credit, actual signed + price, quotas, demands, profile) are recomputed and recorded, invalid + witness documents, false declared profiles, and tampered proof data; + 7. compares the complete certificate with EXPECTED.json. + +All checks raise explicit exceptions and stay active under python -O. +No network access, no third-party module, no file is written unless --write, +and --write writes only after every check has passed. +""" +import argparse +import hashlib +import itertools +import json +import sys +from collections import Counter +from pathlib import Path + +HERE = Path(__file__).resolve().parent +HYPOTHESIS = 'q_b6cf2a2ce15a43ed:e10' +STATUS = 'PASS_T29_CAPACITY_TAGGED_PATTERN_WITNESS' +WIDTHS = (4, 5, 7, 8, 9) +PRICE = {4: -1, 5: -20, 7: -8, 8: -2, 9: 4} +# capacity -> (bins per replica, capacity bonus) +CAPACITY = {8: (672, 2), 16: (448, 4), 32: (448, 8), 48: (448, -13)} +PER_CALL = {4: 80, 5: 32, 7: 54, 8: 122, 9: 216} +CALLS_PER_REPLICA = 9 +T = 29 +PROFILE = {0: 49770, 1: 4, 2: 1, 48: 8689} +ZERO = (0, 0, 0, 0, 0) +# Count vectors are indexed by WIDTHS: (n4, n5, n7, n8, n9). +# Second realization, transcribed from the reviewer's blind hand construction +# (REVIEW.md, "Exact proof and independently derived witness"). It differs from +# WITNESS.json in eight pattern counts, including a different rank-2 pattern. +SECOND_WITNESS = { + (8, (2, 0, 0, 0, 0)): 8285, (8, (0, 0, 0, 1, 0)): 11203, + (16, (0, 0, 1, 0, 1)): 4824, (16, (0, 0, 0, 2, 0)): 8168, + (32, (0, 1, 0, 0, 3)): 8352, (32, (0, 0, 2, 0, 2)): 4635, + (32, (1, 0, 0, 0, 3)): 4, (32, (3, 0, 0, 0, 2)): 1, + (48, (1, 0, 0, 1, 4)): 4303, (48, ZERO): 8689, +} + + +class Reject(ValueError): + """Explicit failure; independent of the assert statement and python -O.""" + + +def require(condition, message): + if not condition: + raise Reject(message) + + +def sha256_bytes(data): + return hashlib.sha256(data).hexdigest() + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(',', ':')).encode() + + +def load_json(path, what): + try: + return json.loads(path.read_bytes()) + except (OSError, UnicodeDecodeError, ValueError) as error: + raise Reject('%s is missing or malformed: %s' % (what, error)) + + +def width(vec): + return sum(w * n for w, n in zip(WIDTHS, vec)) + + +def price(cap, vec): + return CAPACITY[cap][1] + sum(PRICE[w] * n for w, n in zip(WIDTHS, vec)) + + +def label(cap, vec): + widths = [w for w, n in zip(WIDTHS, vec) for _ in range(n)] + return '%d:{%s}' % (cap, ','.join(str(w) for w in sorted(widths, reverse=True))) + + +# ---------------------------------------------------------------- sources +def check_sources(root, pins): + require(isinstance(pins, dict) and pins, 'SOURCES.json must map relative paths to sha256 digests') + for relative, digest in sorted(pins.items()): + path = root / relative + require(path.is_file(), 'source pin missing: ' + relative) + require(sha256_bytes(path.read_bytes()) == digest, 'source pin mismatch: ' + relative) + return dict(sorted(pins.items())) + + +# -------------------------------------------------------------- patterns +def enumerate_patterns(): + """The one enumeration: every legal count vector per capacity by Cartesian product.""" + patterns = {} + for cap in CAPACITY: + patterns[cap] = [vec for vec in itertools.product(*(range(cap // w + 1) for w in WIDTHS)) + if width(vec) <= cap] + return patterns + + +def price_table(patterns): + upper = {} + for cap, vectors in patterns.items(): + for vec in vectors: + r = cap - width(vec) + p = price(cap, vec) + if r not in upper or p > upper[r]: + upper[r] = p + return upper + + +def price_table_recurrence(): + """Independent maximum-price dynamic program over exact fills; it recomputes + u(r) without enumerating or counting the legal count vectors.""" + upper = {} + for cap, (_, bonus) in CAPACITY.items(): + best = {0: 0} + for fill in range(1, cap + 1): + candidates = [best[fill - w] + PRICE[w] for w in WIDTHS if fill >= w and fill - w in best] + if candidates: + best[fill] = max(candidates) + for fill, p in best.items(): + r = cap - fill + if r not in upper or p + bonus > upper[r]: + upper[r] = p + bonus + return upper + + +# ------------------------------------------------------------- aggregate +def aggregate(replicas, profile, upper): + quotas = {cap: replicas * bins for cap, (bins, _) in CAPACITY.items()} + demands = {w: replicas * CALLS_PER_REPLICA * PER_CALL[w] for w in WIDTHS} + bins = sum(quotas.values()) + mass = sum(cap * n for cap, n in quotas.items()) - sum(w * n for w, n in demands.items()) + signed = sum(CAPACITY[cap][1] * n for cap, n in quotas.items()) + sum(PRICE[w] * n for w, n in demands.items()) + for r in profile: + require(r in upper, 'profile uses an unattainable remainder rank: %d' % r) + require(sum(profile.values()) == bins, 'bin count identity: profile has %d bins, quotas give %d' % (sum(profile.values()), bins)) + require(sum(r * n for r, n in profile.items()) == mass, 'rank mass identity: profile mass %d, inventory mass %d' % (sum(r * n for r, n in profile.items()), mass)) + dual = sum(upper[r] * n for r, n in profile.items()) + slack = dual - signed + require(slack >= 0, 'profile violates the necessary signed-price inequality (slack %d)' % slack) + require(slack == 0, 'signed-price identity (zero slack) fails: sum u(r) n_r = %d, actual total price = %d' % (dual, signed)) + return dict(replicas=replicas, quotas=quotas, demands=demands, bins=bins, mass=mass, + signed_price=signed, dual_price=dual, slack=slack) + + +# ------------------------------------------------------- tightness lemma +def tight_patterns(patterns, upper, profile): + """Patterns attaining u(r) in each remainder class present in the profile. + + Zero slack forces every bin of every realization into this set: each bin's + price is at most u(r) and the sum of all bin prices equals sum_r n_r u(r). + """ + classes = {} + for r, n in profile.items(): + if n: + classes[r] = sorted((cap, vec) for cap, vectors in patterns.items() for vec in vectors + if cap - width(vec) == r and price(cap, vec) == upper[r]) + return classes + + +def forced_structure(classes, agg): + quotas, demands = agg['quotas'], agg['demands'] + tight = [(r, cap, vec) for r, items in classes.items() for cap, vec in items] + fives = [(r, cap, vec) for r, cap, vec in tight if vec[1]] + require(fives == [(0, 32, (0, 1, 0, 0, 3))], 'width-five helpers must sit in capacity-32 {9,9,9,5} bins') + require(classes[48] == [(48, ZERO)], 'rank-48 tight pattern must be the empty capacity-48 bin') + require(classes[1] == [(32, (1, 0, 0, 0, 3))], 'rank-1 tight pattern must be capacity-32 {9,9,9,4}') + require(classes[2] == [(32, (1, 0, 0, 1, 2)), (32, (3, 0, 0, 0, 2))], 'rank-2 tight patterns must be capacity-32 {9,9,8,4} and {9,9,4,4,4}') + cap48_full = [vec for cap, vec in classes[0] if cap == 48] + require(cap48_full == [(1, 0, 0, 1, 4), (3, 0, 0, 0, 4)], 'full capacity-48 tight patterns must be {9,9,9,9,8,4} and {9,9,9,9,4,4,4}') + others = [(cap, vec) for cap, vec in classes[0] if cap != 48 and vec != (0, 1, 0, 0, 3)] + require(all(vec[4] == vec[2] for cap, vec in others), 'every other full tight pattern must pair each nine with one seven') + fives_bins = demands[5] + full48 = quotas[48] - PROFILE[48] + nines_fixed = 4 * full48 + 3 * fives_bins + 3 * PROFILE[1] + 2 * PROFILE[2] + require(demands[9] - nines_fixed == demands[7], 'width-nine demand is not implied by the width-seven demand') + cap32_free = quotas[32] - fives_bins - PROFILE[1] - PROFILE[2] + low = max(0, demands[7] - 2 * cap32_free) + high = min(quotas[16], demands[7]) + require(low <= high, 'no room for the width-seven helpers') + return dict(tight_patterns_by_class={str(r): [label(cap, vec) for cap, vec in items] for r, items in classes.items()}, + forced_fives_bins_cap32_9995=fives_bins, + forced_full_capacity48_bins=full48, + nines_in_forced_bins=nines_fixed, + nines_remaining_equals_sevens=demands[7], + capacity16_nine_seven_bins_necessary_range=[low, high], + capacity16_nine_seven_bins_range_is_necessary_only=True, + cap32_bins_free_for_rank0_without_fives=cap32_free) + + +# --------------------------------------------------------------- witness +def parse_witness(document): + require(isinstance(document, dict) and isinstance(document.get('patterns'), list), 'witness must list patterns') + entries = {} + for item in document['patterns']: + require(isinstance(item, dict), 'pattern entry must be an object') + cap, widths, count = item.get('capacity'), item.get('widths'), item.get('count') + require(type(cap) is int and cap in CAPACITY, 'unknown capacity: %r' % (cap,)) + require(isinstance(widths, list) and all(type(w) is int and w in WIDTHS for w in widths), 'unknown helper width in %r' % (widths,)) + require(type(count) is int and count >= 0, 'count must be a nonnegative integer: %r' % (count,)) + vec = tuple(widths.count(w) for w in WIDTHS) + require(width(vec) <= cap, 'illegal pattern: width %d exceeds capacity %d' % (width(vec), cap)) + if 'remainder' in item: + require(item['remainder'] == cap - width(vec), 'declared remainder disagrees with capacity minus width') + key = (cap, vec) + require(key not in entries, 'duplicate pattern entry: ' + label(cap, vec)) + entries[key] = count + return entries + + +def invariants(entries, upper): + """Aggregate quantities of a pattern-count vector; used for the control deltas.""" + quotas = Counter() + demands = Counter({w: 0 for w in WIDTHS}) + profile = Counter() + signed = dual = 0 + for (cap, vec), n in entries.items(): + r = cap - width(vec) + quotas[cap] += n + profile[r] += n + for w, k in zip(WIDTHS, vec): + demands[w] += k * n + signed += n * price(cap, vec) + dual += n * (48 * upper[r] + 13 * r) if r in upper else 0 + return dict(bins=sum(quotas.values()), mass=sum(r * n for r, n in profile.items()), dual_credit=dual, + signed_price=signed, quotas=dict(quotas), demands=dict(demands), profile={r: n for r, n in profile.items() if n}) + + +def check_witness(entries, agg, upper): + quotas, demands = agg['quotas'], agg['demands'] + for cap in CAPACITY: + have = sum(n for (c, _), n in entries.items() if c == cap) + require(have == quotas[cap], 'capacity quota mismatch: capacity %d has %d bins, quota %d' % (cap, have, quotas[cap])) + census = Counter() + for (cap, vec), n in entries.items(): + census[cap - width(vec)] += n + census = {r: n for r, n in census.items() if n} + require(census == {r: n for r, n in PROFILE.items() if n}, 'remainder profile mismatch: %s' % dict(sorted(census.items()))) + for i, w in enumerate(WIDTHS): + have = sum(vec[i] * n for (cap, vec), n in entries.items()) + require(have == demands[w], 'width demand mismatch: width %d used %d times, demand %d' % (w, have, demands[w])) + total = 0 + for (cap, vec), n in entries.items(): + if n: + require(price(cap, vec) == upper[cap - width(vec)], 'untight pattern ' + label(cap, vec)) + total += n * price(cap, vec) + require(total == agg['signed_price'], 'total signed price %d differs from %d' % (total, agg['signed_price'])) + used = sorted(((cap, vec), n) for (cap, vec), n in entries.items() if n) + return dict(distinct_patterns=len(used), bins=sum(n for _, n in used), total_signed_price=total, + census={str(r): n for r, n in sorted(census.items())}, + patterns=[dict(pattern=label(cap, vec), capacity=cap, remainder=cap - width(vec), count=n) for (cap, vec), n in used]) + + +def check_declared_profile(document, census): + """The declared remainder_profile must equal the recomputed census exactly: + canonical decimal rank keys, positive integer values (not booleans), no + missing or extra classes.""" + require('remainder_profile' in document, 'witness must declare remainder_profile') + declared = document['remainder_profile'] + require(isinstance(declared, dict) and declared, 'declared remainder_profile must be a nonempty object') + for key, value in declared.items(): + require(isinstance(key, str) and key.isdigit() and str(int(key)) == key, + 'declared remainder_profile keys must be canonical decimal rank strings: %r' % (key,)) + require(type(value) is int and value > 0, 'declared remainder_profile values must be positive integers: %r' % (value,)) + require(declared == census, 'declared remainder_profile disagrees with the recomputed census: declared %s, census %s' % ( + json.dumps(declared, sort_keys=True), json.dumps(census, sort_keys=True))) + + +def admit_document(document, agg, upper): + """Header, patterns, exact packing census and declared profile, in this order.""" + require(isinstance(document, dict), 'witness must be a JSON object') + require(document.get('hypothesis') == HYPOTHESIS, 'witness header hypothesis must be ' + HYPOTHESIS) + require(type(document.get('replicas')) is int and document['replicas'] == T, 'witness header replicas must be the integer %d' % T) + entries = parse_witness(document) + summary = check_witness(entries, agg, upper) + check_declared_profile(document, summary['census']) + return entries, summary + + +def construct_witness(agg): + """Closed-form realization; every step is forced or a free choice made explicit.""" + quotas, demands = agg['quotas'], agg['demands'] + fives = demands[5] # forced: all fives in 32:{9,9,9,5} + full48 = quotas[48] - PROFILE[48] # forced: remaining capacity-48 bins are full + y1 = quotas[16] # choice: every capacity-16 bin is 16:{9,7} + rest7 = demands[7] - y1 + require(rest7 >= 0 and rest7 % 2 == 0, 'sevens left for 32:{9,9,7,7} must be an even nonnegative number') + y5 = rest7 // 2 + c1 = quotas[32] - fives - PROFILE[1] - PROFILE[2] - y5 # choice: remaining capacity-32 bins are 32:{8,8,8,8} + require(c1 >= 0, 'capacity-32 quota exceeded') + f1 = full48 # choice: every full capacity-48 bin is 48:{9,9,9,9,8,4} + a1 = demands[8] - f1 - 1 - 4 * c1 # forced by the width-eight demand given the choices + a2 = quotas[8] - a1 + require(0 <= a1 <= quotas[8], 'capacity-8 split out of range') + fours = 2 * a2 + f1 + PROFILE[1] + PROFILE[2] + require(fours == demands[4], 'closed-form witness fails the width-four demand: %d vs %d' % (fours, demands[4])) + return {(8, (0, 0, 0, 1, 0)): a1, (8, (2, 0, 0, 0, 0)): a2, + (16, (0, 0, 1, 0, 1)): y1, + (32, (0, 1, 0, 0, 3)): fives, (32, (1, 0, 0, 0, 3)): PROFILE[1], (32, (1, 0, 0, 1, 2)): PROFILE[2], + (32, (0, 0, 2, 0, 2)): y5, (32, (0, 0, 0, 4, 0)): c1, + (48, ZERO): PROFILE[48], (48, (1, 0, 0, 1, 4)): f1} + + +# -------------------------------------------------------------- controls +def swap(entries, old, new, count=1): + bad = dict(entries) + require(bad.get(old, 0) >= count, 'control setup: pattern absent ' + label(*old)) + bad[old] -= count + bad[new] = bad.get(new, 0) + count + return bad + + +def control_deltas(entries, mutated, upper): + """Which aggregate invariants a mutated pattern-count vector preserves or changes.""" + before, after = invariants(entries, upper), invariants(mutated, upper) + delta = {k: after[k] - before[k] for k in ('bins', 'mass', 'dual_credit', 'signed_price')} + changed = {k: v for k, v in delta.items() if v} + inventory = {} + for name in ('quotas', 'demands', 'profile'): + diff = {str(k): after[name].get(k, 0) - before[name].get(k, 0) + for k in set(before[name]) | set(after[name]) if after[name].get(k, 0) != before[name].get(k, 0)} + if diff: + inventory[name] = dict(sorted(diff.items())) + return dict(delta=delta, preserved=[k for k in delta if not delta[k]], changed=sorted(changed), + violated_inventory=inventory) + + +def negative_controls(entries, document, agg, upper, root, pins, patterns): + cases = [] + + def witness_case(name, build, expected): + def run(): + mutated = build() + try: + check_witness(mutated, agg, upper) + except Reject as error: + raise Reject(str(error), control_deltas(entries, mutated, upper)) + cases.append((name, run, expected)) + + # Inventory mutations; their preserved/changed invariants are recomputed and recorded. + witness_case('width_swap_16_9_7_to_16_8_8', lambda: swap(entries, (16, (0, 0, 1, 0, 1)), (16, (0, 0, 0, 2, 0))), 'width demand mismatch') + witness_case('width_swap_32_9995_to_32_9977', lambda: swap(entries, (32, (0, 1, 0, 0, 3)), (32, (0, 0, 2, 0, 2))), 'width demand mismatch') + witness_case('rank2_alternative_32_9984_to_32_99444', lambda: swap(entries, (32, (1, 0, 0, 1, 2)), (32, (3, 0, 0, 0, 2))), 'width demand mismatch') + witness_case('retag_8_8_to_16_88', lambda: swap(entries, (8, (0, 0, 0, 1, 0)), (16, (0, 0, 0, 2, 0))), 'capacity quota mismatch') + witness_case('retag_empty_48_to_full_48_999984', lambda: swap(entries, (48, ZERO), (48, (1, 0, 0, 1, 4))), 'remainder profile mismatch') + witness_case('rank1_untight_32_9994_to_32_8887', lambda: swap(entries, (32, (1, 0, 0, 0, 3)), (32, (0, 0, 1, 3, 0))), 'width demand mismatch') + witness_case('one_bin_short_8_8', lambda: {**entries, (8, (0, 0, 0, 1, 0)): entries[(8, (0, 0, 0, 1, 0))] - 1}, 'capacity quota mismatch') + + # Invalid witness documents (header, patterns, declared profile). + def mutated_document(mutate): + copy = json.loads(json.dumps(document)) + mutate(copy) + return copy + + def doc_case(name, mutate, expected): + cases.append((name, lambda: admit_document(mutated_document(mutate), agg, upper), expected)) + + doc_case('overfull_pattern_48_999994', lambda d: d['patterns'].append(dict(capacity=48, widths=[9, 9, 9, 9, 9, 4], count=1)), 'illegal pattern') + doc_case('negative_count', lambda d: d['patterns'][0].__setitem__('count', -1), 'count must be a nonnegative integer') + doc_case('fractional_count', lambda d: d['patterns'][0].__setitem__('count', 0.5), 'count must be a nonnegative integer') + doc_case('boolean_count', lambda d: d['patterns'][0].__setitem__('count', True), 'count must be a nonnegative integer') + doc_case('unknown_width_6', lambda d: d['patterns'].append(dict(capacity=16, widths=[6, 6], count=1)), 'unknown helper width') + doc_case('unknown_capacity_24', lambda d: d['patterns'].append(dict(capacity=24, widths=[8, 8, 8], count=1)), 'unknown capacity') + doc_case('duplicate_pattern_entry', lambda d: d['patterns'].append(dict(d['patterns'][0])), 'duplicate pattern entry') + doc_case('false_declared_remainder', lambda d: d['patterns'][0].__setitem__('remainder', 5), 'declared remainder disagrees') + doc_case('header_replicas_float', lambda d: d.__setitem__('replicas', 29.0), 'witness header replicas must be the integer') + doc_case('header_replicas_boolean', lambda d: d.__setitem__('replicas', True), 'witness header replicas must be the integer') + doc_case('header_wrong_hypothesis', lambda d: d.__setitem__('hypothesis', 'q_b6cf2a2ce15a43ed:e11'), 'witness header hypothesis must be') + doc_case('declared_profile_missing', lambda d: d.pop('remainder_profile'), 'witness must declare remainder_profile') + doc_case('declared_profile_false_rank0_count', lambda d: d['remainder_profile'].__setitem__('0', 1), 'declared remainder_profile disagrees') + doc_case('declared_profile_missing_class_2', lambda d: d['remainder_profile'].pop('2'), 'declared remainder_profile disagrees') + doc_case('declared_profile_extra_zero_class_3', lambda d: d['remainder_profile'].__setitem__('3', 0), 'declared remainder_profile values must be positive integers') + doc_case('declared_profile_boolean_value', lambda d: d['remainder_profile'].__setitem__('1', True), 'declared remainder_profile values must be positive integers') + doc_case('declared_profile_noncanonical_key_01', lambda d: d['remainder_profile'].__setitem__('01', d['remainder_profile'].pop('1')), 'declared remainder_profile keys must be canonical') + doc_case('declared_profile_swapped_classes', lambda d: d['remainder_profile'].update({'1': 1, '2': 4}), 'declared remainder_profile disagrees') + + # Tampered proof data. + def tampered_table(): + bad = dict(upper) + bad[2] = 14 + require(bad == price_table(patterns), 'signed-price table disagrees with the independent enumeration') + cases.append(('tampered_u_table_u2_14', tampered_table, 'signed-price table disagrees')) + cases.append(('wrong_replica_count_28', lambda: aggregate(28, PROFILE, upper), 'bin count identity')) + cases.append(('profile_off_by_one_rank1', lambda: aggregate(T, {0: 49770, 1: 5, 2: 1, 48: 8689}, upper), 'bin count identity')) + # Same 58464 bins and same mass 417078 as the sharp profile, different credit. + cases.append(('profile_same_bins_same_mass_positive_slack', lambda: aggregate(T, {0: 49769, 1: 6, 48: 8689}, upper), 'signed-price identity (zero slack) fails')) + cases.append(('profile_same_bins_same_mass_negative_slack', lambda: aggregate(T, {0: 49772, 2: 3, 48: 8689}, upper), 'profile violates the necessary signed-price inequality')) + + def tampered_pin(): + bad = dict(pins) + first = sorted(bad)[0] + bad[first] = '0' * 64 + check_sources(root, bad) + cases.append(('tampered_source_pin', tampered_pin, 'source pin mismatch')) + + rejected = [] + for name, run, expected in cases: + try: + run() + except Reject as error: + require(str(error.args[0]).startswith(expected), 'control %s rejected for an unexpected reason: %s' % (name, error.args[0])) + record = dict(name=name, reason=str(error.args[0])) + if len(error.args) > 1: + record['invariants'] = error.args[1] + rejected.append(record) + else: + raise Reject('negative control was accepted: ' + name) + return rejected + + +# ------------------------------------------------------------------ main +def certificate(root, run_controls=True): + sources = load_json(HERE / 'SOURCES.json', 'SOURCES.json') + require(isinstance(sources, dict) and 'sha256' in sources and 'base_commit' in sources, 'SOURCES.json must record sha256 pins and the base commit') + pins = check_sources(root, sources['sha256']) + patterns = enumerate_patterns() + legal = sum(len(v) for v in patterns.values()) + upper = price_table(patterns) + require(upper == price_table_recurrence(), 'the maximum-price recurrence disagrees with the enumerated table u(r)') + require((upper[0], upper[1], upper[2], upper[48]) == (0, 19, 13, -13), 'anchor values of u(r)') + agg = aggregate(T, PROFILE, upper) + classes = tight_patterns(patterns, upper, PROFILE) + structure = forced_structure(classes, agg) + witness_path = HERE / 'WITNESS.json' + witness_bytes = witness_path.read_bytes() if witness_path.is_file() else b'' + document = load_json(witness_path, 'WITNESS.json') + entries, summary = admit_document(document, agg, upper) + require({k: v for k, v in entries.items() if v} == construct_witness(agg), 'closed-form reconstruction differs from WITNESS.json') + y1 = entries.get((16, (0, 0, 1, 0, 1)), 0) + low, high = structure['capacity16_nine_seven_bins_necessary_range'] + require(low <= y1 <= high, 'witness outside the derived capacity-16 range') + second = check_witness(SECOND_WITNESS, agg, upper) + first_counts = {k: v for k, v in entries.items() if v} + differing = sorted(label(cap, vec) for (cap, vec) in set(first_counts) | set(SECOND_WITNESS) + if first_counts.get((cap, vec), 0) != SECOND_WITNESS.get((cap, vec), 0)) + require(differing, 'the second realization must differ from WITNESS.json') + result = dict(status=STATUS, hypothesis=HYPOTHESIS, base_commit=sources['base_commit'], + replicas=T, widths=list(WIDTHS), prices={str(w): PRICE[w] for w in WIDTHS}, + capacities={str(c): dict(bins_per_replica=b, bonus=z) for c, (b, z) in CAPACITY.items()}, + helpers_per_call={str(w): PER_CALL[w] for w in WIDTHS}, calls_per_replica=CALLS_PER_REPLICA, + profile={str(r): n for r, n in PROFILE.items()}, + quotas={str(c): n for c, n in agg['quotas'].items()}, demands={str(w): n for w, n in agg['demands'].items()}, + bins=agg['bins'], rank_mass=agg['mass'], total_signed_price=agg['signed_price'], credit_slack=agg['slack'], + enumeration='one Cartesian product enumeration of all legal count vectors; u(r) recomputed independently by a maximum-price dynamic program over exact fills', + legal_patterns=legal, legal_patterns_by_capacity={str(c): len(v) for c, v in patterns.items()}, + u={str(r): u for r, u in sorted(upper.items())}, + tightness_lemma='sum of bin prices equals the fixed total -3892*T and equals sum_r n_r u(r); each bin price <= u(r); hence every bin attains u(r)', + structure=structure, + witness=summary, declared_profile_checked_against_census=True, + second_witness=dict(source='REVIEW.md blind hand construction, transcribed as data', **second), + realizations_checked=2, patterns_with_different_counts=differing, + nonuniqueness='two distinct checked realizations; no statement about any other count vector', + witness_file_sha256=sha256_bytes(witness_bytes), witness_canonical_sha256=sha256_bytes(canonical(document)), + source_sha256=pins, + scope='Aggregate capacity-tagged whole-helper pattern feasibility only. No chronology, owner geometry, physical schedule, controller, invoice or kappa claim; the selected PR1042 supplier is outside scope.') + if run_controls: + result['negative_controls'] = negative_controls(entries, document, agg, upper, root, pins, patterns) + return result + + +def main(): + parser = argparse.ArgumentParser(description=__doc__, formatter_class=argparse.RawDescriptionHelpFormatter) + parser.add_argument('--repository', type=Path, default=HERE.parents[1], help='checkout root holding the pinned source files') + parser.add_argument('--write', type=Path, help='write a fresh EXPECTED.json after all checks pass (refuses to overwrite)') + parser.add_argument('--json', action='store_true', help='print the full certificate') + parser.add_argument('--no-controls', action='store_true') + args = parser.parse_args() + result = certificate(args.repository.resolve(), run_controls=not args.no_controls) + normalized = json.loads(json.dumps(result, sort_keys=True)) + if args.write: + require(not args.write.exists(), 'refusing to overwrite ' + str(args.write)) + require(args.write.parent.is_dir(), 'output directory does not exist: ' + str(args.write.parent)) + args.write.write_text(json.dumps(normalized, indent=2, sort_keys=True) + '\n') + else: + expected = load_json(HERE / 'EXPECTED.json', 'EXPECTED.json') + if args.no_controls: + expected.pop('negative_controls', None) + require(normalized == expected, 'certificate differs from EXPECTED.json') + if args.json: + print(json.dumps(normalized, indent=2, sort_keys=True)) + print('%s patterns=%d witness_bins=%d witness_patterns=%d realizations=%d controls=%d no_new_kappa' % ( + STATUS, result['legal_patterns'], result['witness']['bins'], result['witness']['distinct_patterns'], + result['realizations_checked'], len(result.get('negative_controls', [])))) + + +if __name__ == '__main__': + try: + main() + except Reject as error: + print('FAIL_T29_CAPACITY_TAGGED_PATTERN_WITNESS: ' + str(error.args[0]), file=sys.stderr) + sys.exit(1)