From 6d0b0c5a0b8eec1e510a0575c05b05df6c7a09b0 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Thu, 15 Oct 2026 10:01:09 +0530 Subject: [PATCH 1/6] Add PR2265 supplier-admission audit traced into PR2260 Adversarial audit / research note (no new kappa). Inventories 15 supplier- admission premises of the #2265 substitution (PR1673 capped-fusion outer on the PR2260 selective-borrowing supplier) with file:line pins and checks the finite ones with independent stdlib code on pinned PR blobs: call closure of the 44 borrowed aliases, an exact free-group restoration replay of both orientations, owner hosting and residual recount, finite constants, bit and complex endpoint moments, rate ordering. 6 COVERED, 4 TRUE-unencoded, 5 INHERITED-traced, 0 MISSING-PROOF, 0 FALSE; 13 negative controls rejected. Prepared by thakrarsagar with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5). Co-Authored-By: Claude Opus 5.5 --- .../EXPECTED.json | 193 +++++ .../INVENTORY.json | 202 ++++++ .../pr2265-supplier-admission-audit/README.md | 155 ++++ .../SOURCES.json | 30 + .../pr2265-supplier-admission-audit/TASK.json | 72 ++ .../VERIFY.json | 21 + .../pr2265-supplier-admission-audit/verify.py | 680 ++++++++++++++++++ 7 files changed, 1353 insertions(+) create mode 100644 research/pr2265-supplier-admission-audit/EXPECTED.json create mode 100644 research/pr2265-supplier-admission-audit/INVENTORY.json create mode 100644 research/pr2265-supplier-admission-audit/README.md create mode 100644 research/pr2265-supplier-admission-audit/SOURCES.json create mode 100644 research/pr2265-supplier-admission-audit/TASK.json create mode 100644 research/pr2265-supplier-admission-audit/VERIFY.json create mode 100644 research/pr2265-supplier-admission-audit/verify.py diff --git a/research/pr2265-supplier-admission-audit/EXPECTED.json b/research/pr2265-supplier-admission-audit/EXPECTED.json new file mode 100644 index 0000000000..c5428832d9 --- /dev/null +++ b/research/pr2265-supplier-admission-audit/EXPECTED.json @@ -0,0 +1,193 @@ +{ + "A_alias_closure": { + "backward": { + "borrowed_from_data_inputs": [ + 73 + ], + "borrowed_from_helper_inputs": 43, + "distinct_borrowed_sources": 44, + "events": 21381, + "handoffs": 44, + "owned_private_arrays": 76 + }, + "forward": { + "borrowed_from_data_inputs": [ + 73 + ], + "borrowed_from_helper_inputs": 43, + "distinct_borrowed_sources": 44, + "events": 21065, + "handoffs": 44, + "owned_private_arrays": 76 + } + }, + "A_owner_hosting": { + "calls": 72, + "hosted": 254088, + "original_children": 16128, + "original_rank_mass": 387072, + "profile": { + "1": 176252, + "2": 30096, + "3": 30908, + "32": 11, + "39": 7, + "4": 10152, + "48": 2493, + "5": 4493, + "6": 18, + "7": 494, + "8": 576 + }, + "residual": { + "1": 1724, + "3": 20, + "32": 11, + "39": 7, + "48": 2493, + "5": 1469, + "6": 18, + "7": 494 + }, + "residual_mass": 132984, + "roles": 31392 + }, + "A_restoration_replay": { + "backward": { + "borrowed_sources_ending_as_shear_column": [ + 73 + ], + "borrowed_sources_returned_to_input": 43, + "private_arrays_zero": 76, + "public_columns": 660 + }, + "forward": { + "borrowed_sources_ending_as_shear_column": [], + "borrowed_sources_returned_to_input": 44, + "private_arrays_zero": 76, + "public_columns": 660 + } + }, + "B_constants": { + "group_bits": 2628, + "guard_coefficient": 244, + "literal_bits": 35282, + "physical": 7745, + "required_C0_bits": 200012, + "retained_fixed_bit_prefix": 248, + "row": 16467, + "row_lambda_max_if_payload_scaled": 4, + "stock_bits": 2641 + }, + "C_bit": { + "bit_conservative_minus_one": "-1.598690e-24", + "bit_live": 28416, + "bit_maxchild": 42 + }, + "D_endpoint": { + "C_decimal_40": "0.0016834125885426074623303197400000000000", + "a_minus_q": "5.000000e-281", + "b_minus_a": "1.500000e-280", + "c_minus_b": "5.001445e-05", + "conservative_minus_one": "-2.883591e-200", + "native_moment_minus_one": "-8.386920e-12", + "next_grid_conservative_minus_one": "3.157248e-202" + }, + "inventory_classes": { + "COVERED": 6, + "INHERITED-traced": 5, + "TRUE-unencoded": 4 + }, + "negative_controls": { + "alias_source_is_removed_alias": "every borrowed source is a live public input array of the same call", + "alias_source_outside_call": "every borrowed source is a live public input array of the same call", + "bit_endpoint_equal_to_b": "rate ordering q < a_eff < b < c", + "bit_endpoint_plus_1e_18": "conservative bit moment below one at c", + "endpoint_plus_one_grid_step": "moments below one at C", + "event_reads_removed_alias": "event add touches register 597 outside the call", + "halving_child_rank_52": "halving guard m^2 > 2 rmax^2", + "kappa_plus_1e_240": "kappa = C - 1e-246 - 1e-222", + "owner_block_overlap": "assigned blocks are disjoint and form an exact prefix", + "owner_on_active_data_family": "helper family is not an active data family of its call", + "replay_doubles_one_add_coefficient": "('endpoint column not restored/sheared', 115)", + "replay_drops_one_monomial_warp": "('endpoint column not restored/sheared', 22)", + "row_payload_scaled_beyond_lambda_max": "row guard 2*stock_bits + 9909 + 252 + 2*payload < 20161" + }, + "pr2260": "fde6b107e26a14da5bac5b66913c914708ea6901", + "pr2265": "49ce38fee91f33edb54645724e7be9530f5631f6", + "status": "PASS_PR2265_SUPPLIER_ADMISSION_AUDIT", + "trace": [ + { + "commit": "fde6b107", + "file": "PROOF.md", + "item": "A-restoration", + "line": 7 + }, + { + "commit": "fde6b107", + "file": "PROOF-LOCAL.md", + "item": "A-restoration", + "line": 45 + }, + { + "commit": "fde6b107", + "file": "PROOF.md", + "item": "A-serialize", + "line": 23 + }, + { + "commit": "fde6b107", + "file": "PROOF-OWNERS.md", + "item": "A-serialize", + "line": 88 + }, + { + "commit": "49ce38fe", + "file": "README.md", + "item": "A-completed-call", + "line": 42 + }, + { + "commit": "49ce38fe", + "file": "vendor/pr1673/capped-phase-fusion/frontier_fusion/INDEPENDENT-SUBSTITUTION-REVIEW.md", + "item": "A-pr1673-use", + "line": 53 + }, + { + "commit": "fde6b107", + "file": "PROOF-LOCAL.md", + "item": "B-guard", + "line": 132 + }, + { + "commit": "fde6b107", + "file": "PROOF.md", + "item": "B-guard", + "line": 40 + }, + { + "commit": "49ce38fe", + "file": "vendor/pr1673/capped-phase-fusion/frontier_fusion/INDEPENDENT-SUBSTITUTION-REVIEW.md", + "item": "B-pr1673-generic", + "line": 76 + }, + { + "commit": "49ce38fe", + "file": "vendor/pr1673/capped-phase-fusion/frontier_fusion/INDEPENDENT-SUBSTITUTION-REVIEW.md", + "item": "C-interchange", + "line": 82 + }, + { + "commit": "fde6b107", + "file": "PROOF.md", + "item": "C-interchange", + "line": 71 + }, + { + "commit": "49ce38fe", + "file": "vendor/pr1673/capped-phase-fusion/phase_fusion_note.tex", + "item": "C-theorem", + "line": 63 + } + ] +} diff --git a/research/pr2265-supplier-admission-audit/INVENTORY.json b/research/pr2265-supplier-admission-audit/INVENTORY.json new file mode 100644 index 0000000000..40ecdc80c8 --- /dev/null +++ b/research/pr2265-supplier-admission-audit/INVENTORY.json @@ -0,0 +1,202 @@ +{ + "schema": "pr2265-supplier-admission-inventory/1", + "audited": { + "pr2265": {"head": "49ce38fee91f33edb54645724e7be9530f5631f6", "package": "research/selective-borrowing-outer-retune"}, + "pr2260": {"head": "fde6b107e26a14da5bac5b66913c914708ea6901", "package": "research/selective-borrowing-kappa"}, + "base": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2" + }, + "classes": { + "COVERED": "the premise is consumed and checked by #2265's own ledger/assertions or by a PR2260 check that #2265 reruns", + "TRUE-unencoded": "true on the shipped data under an exact independent check here, but not a row of #2265's ledger", + "INHERITED-traced": "the statement is located in PR2260/PR1673 sources; it is an interface premise with no finite data check possible at this level, or one not rechecked here", + "MISSING-PROOF": "used, but no supporting statement or check located", + "FALSE": "contradicted by the shipped data" + }, + "line_pins_note": "Line numbers refer to the pinned heads. verify.py re-locates the quoted phrases (EXPECTED.json 'trace').", + "premises": [ + { + "id": "A1-call-closure", + "group": "A", + "statement": "PR2260's dirty borrowing is internal to the T8 parent call, and the supplier is used only as a completed global call with no ambient-p address permutations.", + "stated_in_2265": "README.md:42 (marked inherited, not re-derived); README.md:35", + "stated_in_2260": "PROOF.md:21-31; PROOF-OWNERS.md:84-89; PROOF-LOCAL.md:19-25", + "consumed_by_outer": "theorem hypothesis only: vendor/pr1673/capped-phase-fusion/phase_fusion_note.tex:63 and :443; INDEPENDENT-SUBSTITUTION-REVIEW.md:51-58, :80-81. No ledger row.", + "check_here": "verify.py check_alias_closure + check_owner_hosting", + "class": "TRUE-unencoded", + "finding": "Both orientations of the local word touch only the 660 public arrays of the call (224 data, 436 helpers) and the 76 owned private arrays. No event references a removed alias or any register outside the call. The 44 borrowed sources are 43 helper inputs plus one public data input: register 73, an X-side source for removed alias 653. Handoffs occur exactly at the 44 borrowed sources, and each has paid rank 0. Every one of the 31392 owner rows lies in an inherited pending child of the same hosted parent. Within each child the rows form disjoint exact prefixes, and no row uses an active data family of its own call.", + "residual_inheritance": "The all-size realization of this finite closure (lambda-fold lift, physical tape and route) is inherited from PR2260 PROOF.md:49-52." + }, + { + "id": "A2-restoration", + "group": "A", + "statement": "Arbitrary dirty helper and spectator coordinates are restored, together with the same normalized global transform, at each completed-call boundary.", + "stated_in_2265": "README.md:34; README.md:42", + "stated_in_2260": "PROOF.md:5-7; PROOF-LOCAL.md:27-46 (two replays: emitting replay and local/check_trace.py)", + "consumed_by_outer": "INDEPENDENT-SUBSTITUTION-REVIEW.md:51-58; phase_fusion_note.tex:443-444. No ledger row.", + "check_here": "verify.py replay_restoration: an independently written exact replay over a free group of reference-change symbols with rational coefficients, with GF(2) frames compared by reduced basis.", + "class": "TRUE-unencoded", + "finding": "All 660 public columns end at the declared endpoint in both orientations: forward Y_i += X_i, backward X_i -= Y_i, all other columns returned to their own input label with an empty word. All 76 owned private arrays end at zero. The paid transport profile equals {1:2424,2:418,3:429,4:141,5:42,8:8}. In the forward orientation all 44 borrowed sources return to their input. In the backward orientation 43 do, and register 73 ends as the declared shear column X_73 - Y_185.", + "independence_note": "The replay was written for this audit after reading PR2260's row-interpreter semantics (PROOF-LOCAL.md:27-46, local/check_trace.py). No PR2260 code is imported or executed, but the event semantics model is PR2260's. It is a third replay of the same model, not a different model.", + "residual_inheritance": "The lambda-fold tensor lift (PROOF-LOCAL.md:102-107) and native Clifford lowering (PROOF-LOCAL.md:70-100) are not rechecked." + }, + { + "id": "A3-whole-call-hosting", + "group": "A", + "statement": "There are exactly 72 x 436 owner rows, one per (call, helper), each with one bin and contiguous axes.", + "stated_in_2265": "README.md:28 (checked); README.md:43", + "stated_in_2260": "PROOF-OWNERS.md:1-6, :93-114; owners/EXPECTED.json", + "consumed_by_outer": "phase_fusion_note.tex:63 (whole-call row hosting hypothesis); SPEC.json geometry", + "check_here": "verify.py check_owner_hosting", + "class": "COVERED", + "finding": "Confirmed independently. The original pending children are reconstructed as the hosted parent's pooled blocks plus its idle residuals: 16128 children with rank mass 387072. The 436-helper owners host 254088. The residual 132984 has histogram {1:1724,3:20,5:1469,6:18,7:494,32:11,39:7,48:2493}, which equals PR2260 owners/EXPECTED.json and the factor partition quoted at PROOF.md:26-28." + }, + { + "id": "A4-serialization-windows", + "group": "A", + "statement": "Invocations serialize, and each helper lies inside its derived time window before the pending child.", + "stated_in_2265": "not stated separately (part of README.md:35 retained interfaces)", + "stated_in_2260": "PROOF.md:23-24; PROOF-OWNERS.md:24-57, :88-89", + "consumed_by_outer": "phase_fusion_note.tex:63 hypotheses", + "check_here": "phrase pins only", + "class": "INHERITED-traced", + "finding": "Located in PR2260 and checked there by owners/verify.py. The 160 derived windows were not re-derived in this audit." + }, + { + "id": "B1-semantic-guard", + "group": "B", + "statement": "The semantic guard and prefix allowance for PR2260 is the magnitude guard 244*lambda < 512*lambda.", + "stated_in_2265": "README.md:41 (inherited, not re-derived)", + "stated_in_2260": "PROOF.md:39-40; PROOF-LOCAL.md:125-135; local/data/finite-invoice.json exact_magnitude_guard, precision_units", + "consumed_by_outer": "No #2265 ledger row. PR1673 requires only a fixed supplier-dependent constant in O(g) (INDEPENDENT-SUBSTITUTION-REVIEW.md:73-78) under the C_1 = 1 semantic-guard hypothesis (phase_fusion_note.tex:63).", + "check_here": "verify.py check_constants", + "class": "INHERITED-traced", + "finding": "The arithmetic holds: 244 = 63 + 144 + 37, the inequality 207 + 37*lambda <= 244*lambda is equivalent to lambda >= 1 (tight at 1), and 244 < 512. The retained fixed-bit rule of direct-delivery504 (local + 37 + calls + bridges + 4) gives 248 < 512. The value 63 is PR2260's P_binary_upper and is taken from its precision receipts, not recomputed.", + "open_unit_question": "PR2260 declares payload 512 a per-lambda coefficient, but its row formula 2*stock_bits + 9909 + 252 + 2*payload counts 2*payload = 1024 as a fixed term, as in the fixed-bit predecessors. If that term scaled with lambda, the row guard < 20161 would hold only for lambda <= 4. Neither PR2260 nor #2265 says how the row allowance scales with lambda. This is recorded as an open interface question, not a counterexample." + }, + { + "id": "B2-C0", + "group": "B", + "statement": "PR2260's fresh constant satisfies C_0 < 2^210000.", + "stated_in_2265": "README.md:36, :41", + "stated_in_2260": "PROOF.md:38-39, :45-49; PROOF-LOCAL.md:137-150; finite-invoice.json", + "consumed_by_outer": "No #2265 ledger row. It changes a constant only (README.md:36; phase_fusion_note.tex:443).", + "check_here": "verify.py check_constants", + "class": "TRUE-unencoded", + "finding": "Recomputed with the retained formula: required_C0_bits = bit_length(32*73*(|O(73,2)|*73*7168 + 2^100000)^2) = 200012 < 210000, and the tape bound 2*total+18 < 2^210000.", + "residual_inheritance": "The retained formula and the active-depth recurrence (PROOF.md:45-49) are inherited conventions." + }, + { + "id": "B3-row-coefficient", + "group": "B", + "statement": "PR2260's new row coefficient satisfies 16467 < 20161.", + "stated_in_2265": "README.md:36", + "stated_in_2260": "PROOF.md:40; PROOF-LOCAL.md:198; finite-invoice.json finite", + "consumed_by_outer": "No #2265 ledger row. It changes a constant only.", + "check_here": "verify.py check_constants", + "class": "TRUE-unencoded", + "finding": "Recomputed: physical families 7168 + 492 + 75 + 8 + 2 = 7745, where 75 is the trace's zero-buffer count; stock bits 2641; row = 2*2641 + 9909 + 252 + 1024 = 16467. The value is identical to direct-delivery504's (PREFIX-AND-INVOICE.json) together with physical_stock_bits 2641 and required_C0_bits 200012. This is explained, not copied: both stocks have the same bit length because 7682 and 7745 both lie in [2^12, 2^13), and the C0 field is dominated by 2^100000.", + "group_order_check": "The formula 2^(k^2) prod_{j=1..k} (2^(2j)-1) for |O(2k+1,2)| matches brute force for n = 3 and 5." + }, + { + "id": "C1-bit-endpoint", + "group": "C", + "statement": "The retained bit endpoint is c = 1733427039589844234749/10^24.", + "stated_in_2265": "SPEC.json supplier.bit_lower; README.md:13", + "stated_in_2260": "PROOF.md:69-71; arithmetic/vendor/BIT-EXPECTED.json (vendored from base research/e8-bit-p111-tuned/tune/EXPECTED.json)", + "consumed_by_outer": "ledger strict row actual_bit_above_effective; #2265 verify.py:79 binding", + "check_here": "verify.py check_bit", + "class": "COVERED", + "finding": "SPEC equals PR2260 BIT-EXPECTED, which is byte-identical to the base-tree file (sha256 b9f0e5ca...). Independent checks: the conservative bit moment at c is 1 - 1.5987e-24 < 1; the deficit identity 64*BW - mass = 32*(8v - 9*sum(copy_ranks)) holds; and 64^2 > 2*42^2. Raising c by 1e-18 makes the moment exceed 1." + }, + { + "id": "C2-equal-chunk-interchange", + "group": "C", + "statement": "The retained bit supplier supplies the arbitrary-width equal-chunk interchange interface with more rate than the chosen a.", + "stated_in_2265": "README.md:44 (inherited, not re-derived)", + "stated_in_2260": "PROOF.md:69-71 ('Its circuit/realization assumptions remain inherited.')", + "consumed_by_outer": "phase_fusion_note.tex:63 theorem hypothesis ('Assume the paid equal-chunk interchange primitive ...'); INDEPENDENT-SUBSTITUTION-REVIEW.md:82-84", + "check_here": "phrase pins; rate part c - b = 5.0014e-5 > 0", + "class": "INHERITED-traced", + "finding": "This is an interface hypothesis of PR1673's theorem. PR2260 declares it inherited, and neither PR has a finite data check for it. Its rate part (c > a) is true and is covered by the ledger." + }, + { + "id": "C3-C1-retained-interfaces", + "group": "C", + "statement": "PR2260 uses the same retained interfaces with C_1 = 1.", + "stated_in_2265": "README.md:35", + "stated_in_2260": "PROOF.md:104-105 (stated for feeding the balanced-prefix outer); PROOF.md:112-114", + "consumed_by_outer": "phase_fusion_note.tex:63", + "check_here": "none", + "class": "INHERITED-traced", + "finding": "PR2260 states C_1 = 1 in the context of its own balanced-prefix outer. #2265 reuses the same retained interface name for the PR1673 hypothesis. Nothing in the data distinguishes the two uses." + }, + { + "id": "D1-halving", + "group": "D", + "statement": "73^2 > 2*48^2.", + "stated_in_2265": "README.md:33; certify_endpoint.py:22", + "stated_in_2260": "PROOF.md:63-64", + "consumed_by_outer": "certify_endpoint.py:22 assertion", + "check_here": "verify.py check_endpoint", + "class": "COVERED", + "finding": "5329 > 4608. The maximum residual child rank is 48, taken from the independent recount. A mass-preserving mutation 48 + 4 -> 52 is rejected." + }, + { + "id": "D2-stock-profile", + "group": "D", + "statement": "W = 7168, rank mass 520704 and deficit 2560 against the SPEC global profile.", + "stated_in_2265": "README.md:13; SPEC.json expected", + "stated_in_2260": "PROOF.md:56-63; PROOF-OWNERS.md:116-135", + "consumed_by_outer": "#2265 verify.py binding; certify_endpoint.py:21", + "check_here": "verify.py check_owner_hosting + check_endpoint", + "class": "COVERED", + "finding": "Independently recounted as 72 x local profile + residual, which equals SPEC = ENDPOINT = PR2260 owners/EXPECTED. W = 896*8. 73*7168 - 520704 = 2560." + }, + { + "id": "D3-rate-ordering", + "group": "D", + "statement": "q < a_eff < b < c at #2265's final point.", + "stated_in_2265": "README.md:37", + "stated_in_2260": "n/a (outer-side)", + "consumed_by_outer": "ledger strict rows q_below_effective, complex_above_effective, actual_bit_above_effective", + "check_here": "verify.py check_endpoint", + "class": "COVERED", + "finding": "a - q = 5e-281, b - a = 1.5e-280 and c - b = 5.0014e-5, all exact rationals from LEDGER.json and ENDPOINT.json. The control with c = b is rejected." + }, + { + "id": "D4-endpoint-and-kappa", + "group": "D", + "statement": "C is the 10^-200 floor of the conservative root, and kappa = C - 10^-246 - 10^-222.", + "stated_in_2265": "README.md:3-5; ENDPOINT.json; LEDGER.json", + "stated_in_2260": "n/a (PR2260 certified only 8417/5000000)", + "consumed_by_outer": "certify_endpoint.py; ledger", + "check_here": "verify.py check_endpoint (decimal, 320 digits, error < 1e-316)", + "class": "COVERED", + "finding": "Independent check. At C the native moment is 1 - 8.387e-12 and the conservative moment is 1 - 2.884e-200. At C + 1e-200 the conservative moment is 1 + 3.157e-202. The kappa identity is exact." + }, + { + "id": "D5-surcharge", + "group": "D", + "statement": "The conservative moment uses PR2260's retained bad-residue surcharge 32*m*sum(H)/(10^16*W)*m^b.", + "stated_in_2265": "certify_endpoint.py:5-6, :23; ENDPOINT.json surcharge_weight", + "stated_in_2260": "arithmetic/vendor/moment.py:61-65 (vendored from base research/frame-domain-ceiling/engines/moment.py)", + "consumed_by_outer": "certify_endpoint.py conservative moment", + "check_here": "verify.py check_endpoint", + "class": "INHERITED-traced", + "finding": "The weight is 32*73*255500/(10^16*7168) = 5329/640000000000000, and the arithmetic is true. The vendored engine's own comment calls this envelope 'only conditionally portable to the new cover'. Its portability to the PR2260 cover is therefore an inherited condition, and neither PR proves it." + } + ], + "summary": { + "FALSE": 0, + "MISSING-PROOF": 0, + "COVERED": 6, + "TRUE-unencoded": 4, + "INHERITED-traced": 5, + "new_observations": [ + "One of the 44 borrowed sources is the public data input X_73, not a helper. It is restored in the forward orientation and ends as the declared shear column in the backward orientation.", + "If payload were per-lambda, the row formula would need lambda <= 4 (unit question).", + "The row/C0/stock-bit fields identical to direct-delivery504 are explained by equal stock bit length.", + "The surcharge envelope is flagged 'only conditionally portable' in the vendored engine." + ] + } +} diff --git a/research/pr2265-supplier-admission-audit/README.md b/research/pr2265-supplier-admission-audit/README.md new file mode 100644 index 0000000000..61b23525ad --- /dev/null +++ b/research/pr2265-supplier-admission-audit/README.md @@ -0,0 +1,155 @@ +# Supplier-admission audit of the #2265 substitution, traced into PR2260 + +**Status: adversarial audit / research note. No new kappa, no construction.** +No FALSE or MISSING-PROOF premise was found. The finite premises were checked here +with independent code. The remaining premises are interface hypotheses located in +the sources but not provable from shipped data. + +## Question + +PR #2265 (DreamingOfClouds, head `49ce38fe`) applies the PR1673 capped phase-cell +fusion outer to the PR2260 selective-borrowing supplier (Dugongue, head `fde6b107`). +Its README marks three substitution items as "inherited from PR2260; not +re-derived": the completed-call/dirty-borrowing premise, the semantic guard, and +the equal-chunk bit interchange. The PR asks for an independent check. This audit +asks whether each supplier-admission premise of the substitution has a supporting +statement or data check in PR2260, and whether it holds on the shipped data at +#2265's final point. The audit covers four groups: + +- (A) Borrowing stays inside the call and is restored. +- (B) The guard, C_0 and row constants. +- (C) The retained bit endpoint and the interchange premise. +- (D) The numeric substitution facts. + +The stop-parameter relations are already #2265 ledger rows and were audited for +T74 in #2286, so they are excluded. + +## Result + +[INVENTORY.json](INVENTORY.json) lists 15 premises with file:line pins and one +class each: + +| Class | Count | Premises | +|---|---:|---| +| COVERED (checked by #2265 or a PR2260 check it reruns; independently re-confirmed here) | 6 | A3 hosting 72x436, C1 bit endpoint, D1 73²>2·48², D2 W/mass/deficit, D3 q PASS_PR2265_SUPPLIER_ADMISSION_AUDIT controls_rejected 13 of 13; INVENTORY.json: 15 premises, 6 COVERED, 4 TRUE-unencoded, 5 INHERITED-traced, 0 MISSING-PROOF, 0 FALSE.", + "author": "thakrarsagar", + "ai_assistance": "Prepared by thakrarsagar with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5) via Claude Code.", + "open_questions": [ + { + "question": "Is the retained row allowance 20161 per-lambda or absolute, given PR2260's per-lambda 512 payload?", + "why_it_matters": "PR2260's row formula counts 2*payload=1024 as fixed; under a per-lambda reading the row guard holds only for lambda<=4.", + "first_step": "Locate the retained definitions of lambda and of the row coefficient in the selected lineage (direct-delivery504 / PR523 invoice notes) and restate PR2260's row in matching units.", + "blocked_by": "The definition of lambda in the all-size compiler is spread over historical notes." + }, + { + "question": "Does the bad-residue surcharge envelope 32*m*sum(H)/(10^16*W)*m^b port to the PR2260 cover?", + "why_it_matters": "#2265's endpoint is certified against the conservative moment; the vendored engine itself labels the envelope only conditionally portable.", + "first_step": "Find the derivation of the envelope behind research/frame-domain-ceiling/engines/moment.py and list its cover-specific hypotheses.", + "blocked_by": "The derivation may exist only in older PR discussions." + }, + { + "question": "Should PR2260's prose record that one alias (removed 653) borrows the public data input X_73 rather than a helper?", + "why_it_matters": "The outer's interface text speaks of dirty helper/spectator coordinates; the data borrow is restored/sheared exactly but the prose should match the data.", + "first_step": "Propose a one-line note in PR2260 PROOF-LOCAL.", + "blocked_by": "None." + } + ] +} diff --git a/research/pr2265-supplier-admission-audit/VERIFY.json b/research/pr2265-supplier-admission-audit/VERIFY.json new file mode 100644 index 0000000000..8de7545031 --- /dev/null +++ b/research/pr2265-supplier-admission-audit/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/direct-delivery504-global/evidence/audit/PREFIX-AND-INVOICE.json", + "research/e8-bit-p111-tuned/tune/EXPECTED.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Reads 18 SHA-256 pinned blobs of PR2260 head fde6b107 and PR2265 head 49ce38fe (fetches the PR heads if absent) plus two pinned base files; call closure and borrowed-source containment, independent free-group restoration replay of both orientations, owner hosting and residual recount, finite constants, bit endpoint moment, endpoint moments and rate ordering, inventory consistency; 13 negative controls must be rejected; receipt compared with EXPECTED.json." + } + ] +} diff --git a/research/pr2265-supplier-admission-audit/verify.py b/research/pr2265-supplier-admission-audit/verify.py new file mode 100644 index 0000000000..d7ab670fc9 --- /dev/null +++ b/research/pr2265-supplier-admission-audit/verify.py @@ -0,0 +1,680 @@ +#!/usr/bin/env python3 +"""Independent supplier-admission audit of the PR2265 substitution, traced into PR2260. + +Reads pinned Git blobs of PR2260 (head fde6b107) and PR2265 (head 49ce38fe) plus two +files of the base checkout, checks their SHA-256 pins, and re-derives the +supplier-admission premises with independent stdlib code. It imports and executes no +code from either PR. All acceptance arithmetic is exact (int / Fraction) except the +moment signs, which use correctly rounded `decimal` ln/exp at 320 digits with an +explicit error bound (see `moment`). Negative controls must be rejected by the same +check functions. + +Prerequisite (once): git fetch origin pull/2260/head pull/2265/head +Run from the repository root: python3 -B research/pr2265-supplier-admission-audit/verify.py + +Prepared by thakrarsagar with substantial AI assistance from Claude (Anthropic, +Claude Opus 5.5). Apache-2.0. +""" +import collections +import copy +import decimal +import gzip +import hashlib +import json +import subprocess +import sys +from fractions import Fraction as Q +from pathlib import Path + +sys.set_int_max_str_digits(0) +PKG = Path(__file__).resolve().parent +ROOT = PKG.parent.parent +C2260 = 'fde6b107e26a14da5bac5b66913c914708ea6901' +C2265 = '49ce38fee91f33edb54645724e7be9530f5631f6' +PREFIX = {C2260: 'research/selective-borrowing-kappa/', C2265: 'research/selective-borrowing-outer-retune/'} +PINS = { + (C2260, 'local/data/forward.json'): 'a9d513bc1d85eb11184d73242a4016119f3968bb2a1ff9b365e78109778c17ee', + (C2260, 'local/data/backward.json'): 'fc965c4a041f26960268b78ba526b9cca13cd01d713a843f31fe4a82c4e08334', + (C2260, 'local/data/postludes.json'): 'e14aed87c976b66c17735c6c198a33024c590e7f183ddcea8725aa6514974235', + (C2260, 'local/inputs/WITNESS.json'): '0a696e6243ba611eec064d0a3bb28fa94ca263d97eec22830f83fabf2e96616b', + (C2260, 'owners/OWNERS.json.gz'): '892b49f97d4caa7e92918262ea3a8cfa8cbf273c92d574ae53bb89a61ee5e847', + (C2260, 'owners/inputs/HOSTED-PARENT.json.gz'): 'f713f8e66aaeaebb8202fe72bf36c7d23497152497342c27892e0fda3092f95b', + (C2260, 'owners/EXPECTED.json'): 'c4ad5debab3f3bd5cba68b91e28a6a8fa64febcbeb892b1fd1d27e3977a76cb1', + (C2260, 'local/data/finite-invoice.json'): '6c7d14c364bd5d98395826ea7bc208fe1ebf2e46c62621bd9f393c4c9b0eaf1e', + (C2260, 'arithmetic/vendor/BIT-EXPECTED.json'): 'b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4', + (C2260, 'PROOF.md'): '5b166115490a71e9ec406497a4177e4b681e96185d0fcee9ceda69020301b23b', + (C2260, 'PROOF-LOCAL.md'): 'eb8a083f2ef5348a24e9f8873092eecdc2f5a95b5e86f09d6fb10e2dcf398960', + (C2260, 'PROOF-OWNERS.md'): '268292c6cd87e7c1be15390506412c65fee363b92ea47f6ce7bb51eff9f084d7', + (C2265, 'SPEC.json'): 'c60d04a8d971d0e984aeeeda87ae613d712537b2623e57a2f315983245e8a280', + (C2265, 'ENDPOINT.json'): 'aefecb3ba73c417e6942fb440fb9f964e74a635dd4d73074ecc54e31768df5be', + (C2265, 'outer/LEDGER.json'): 'df357ddc0265bbad6edc8b9c44e882fc0f8c783030dc68619ff9c0be188a2167', + (C2265, 'README.md'): '82cff31a66becda1ea8e6f051308293148b8057a29af467aed6ae40f59c7dc43', + (C2265, 'vendor/pr1673/capped-phase-fusion/frontier_fusion/INDEPENDENT-SUBSTITUTION-REVIEW.md'): + 'b48d3e14083829db81336b639a6cfc698ac0dccc76fa2606d11b4be7a968ddeb', + (C2265, 'vendor/pr1673/capped-phase-fusion/phase_fusion_note.tex'): + 'b5957f38c98a68f2584a42cedf91d753180dab438129fdf749b441074f00d4e1', +} +LOCAL_PINS = { + 'research/e8-bit-p111-tuned/tune/EXPECTED.json': 'b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4', + 'research/direct-delivery504-global/evidence/audit/PREFIX-AND-INVOICE.json': + 'ce1bfa49be88ae67a404f606a11db2232b7e1f2610d4418058e39749d86d8478', +} + + +class Reject(Exception): + pass + + +def need(cond, label): + if not cond: + raise Reject(label) + + +def sha(data): + return hashlib.sha256(data).hexdigest() + + +def ensure_commits(): + """Fetch the two pinned PR heads once if they are absent (read-only network access).""" + def present(): + return all(subprocess.run(['git', '-C', str(ROOT), 'cat-file', '-e', c + '^{commit}'], + capture_output=True).returncode == 0 for c in (C2260, C2265)) + if not present(): + subprocess.run(['git', '-C', str(ROOT), 'fetch', '--no-tags', '--quiet', 'origin', + 'refs/pull/2260/head', 'refs/pull/2265/head'], capture_output=True) + if not present(): + raise SystemExit('pinned PR heads unavailable; run `git fetch origin pull/2260/head pull/2265/head`') + + +def blob(commit, path): + spec = f'{commit}:{PREFIX[commit]}{path}' + try: + data = subprocess.run(['git', '-C', str(ROOT), 'cat-file', 'blob', spec], + check=True, capture_output=True).stdout + except subprocess.CalledProcessError as exc: + raise SystemExit(f'missing pinned blob {spec}; run ' + '`git fetch origin pull/2260/head pull/2265/head` first') from exc + if sha(data) != PINS[commit, path]: + raise SystemExit(f'pin mismatch for {spec}') + return data + + +def local_file(path): + data = (ROOT / path).read_bytes() + if sha(data) != LOCAL_PINS[path]: + raise SystemExit(f'pin mismatch for {path}') + return json.loads(data) + + +def text_pin(text, phrase): + """Return the 1-indexed line where the whitespace-normalised phrase starts.""" + flat = ' '.join(text.split()) + pos = flat.find(' '.join(phrase.split())) + need(pos >= 0, f'phrase not found: {phrase!r}') + word_index = flat[:pos].count(' ') + seen = 0 + for number, line in enumerate(text.splitlines(), 1): + seen += len(line.split()) + if seen > word_index: + return number + return None + + +# ---------------------------------------------------------------- (A) call closure of the local word +REG_OPERANDS = {'scale': (1,), 'add': (1, 2), 'transport': (1,), 'copy': (1, 2), 'clear': (1,), + 'handoff': (1,), 'swap': (1, 2), 'zero_buffer': (1, 3), 'logical_monomial': (1,), + 'dual_monomial': (1,), 'dual_handoff': (1,), 'zero_reframe': (1,)} + + +def check_alias_closure(trace, witness, postlude): + """Borrowed aliases come from helper inputs of the same local call; no event leaves the call.""" + n0 = trace['original_register_count'] + active = set(trace['active_registers']) + helpers = set(map(int, trace['helper_widths'])) + zero = set(map(int, trace['zero_buffers'].values())) + partners = set(map(int, trace['zero_buffers'])) + copy_reg = trace['copy_register'] + warps = trace['warps'] + removed = [w['removed'] for w in warps] + borrowed = [w['borrow_from'] for w in warps] + need(len(warps) == 44 and len(set(removed)) == 44, 'exactly 44 distinct removed aliases') + need(all(0 <= r < n0 for r in removed), 'removed aliases lie in the original call namespace') + need(active == set(range(n0)) - set(removed), 'active registers = original namespace minus removed aliases') + need(len(active) == 660 and helpers <= active and len(helpers) == 436, '660 public = 224 data + 436 helpers') + need(active - helpers == set(range(224)), 'data arrays are 0..223') + need(all(b in active for b in borrowed), 'every borrowed source is a live public input array of the same call') + from_data = sorted(b for b in borrowed if b not in helpers) + need(not (zero | {copy_reg}) & set(range(n0)), 'owned private arrays are outside the public namespace') + need(partners <= active, 'zero-buffer partners are public registers of the call') + pairs = witness['pairs'] + need(len(pairs) == 44, 'witness has 44 pairs') + need(sorted((p['register'], p['borrow_from'], tuple(p['handoff_basis'])) for p in pairs) + == sorted((w['removed'], w['borrow_from'], tuple(w['to_basis'])) for w in warps), + 'warps equal WITNESS pairs (removed alias, borrowed source, handoff basis; emission order differs)') + need(all(p['handoff_paid_rank'] == 0 for p in pairs) and all(w['physical_handoff_rank'] == 0 for w in warps), + 'every handoff has paid rank zero') + allowed = active | zero | {copy_reg} + hand = collections.Counter() + for event in trace['events']: + kind = event[0] + need(kind in REG_OPERANDS, f'unknown event kind {kind}') + for i in REG_OPERANDS[kind]: + need(event[i] in allowed, f'event {kind} touches register {event[i]} outside the call') + if kind in ('handoff', 'dual_handoff'): + hand[event[1]] += 1 + need(hand == collections.Counter(borrowed), 'handoffs occur exactly on the borrowed helper sources') + need(set(map(int, trace['endpoints'])) == active, 'endpoint ABI covers exactly the 660 public arrays') + need({e[1] for e in postlude} == zero | {copy_reg} and len(postlude) == len(zero) + 1 + and all(e[0] == 'clear' for e in postlude), 'postlude clears exactly the 76 owned private arrays') + return dict(distinct_borrowed_sources=len(set(borrowed)), borrowed_from_helper_inputs=len(borrowed) - len(from_data), + borrowed_from_data_inputs=from_data, events=len(trace['events']), + handoffs=sum(hand.values()), owned_private_arrays=len(zero) + 1) + + +# ---------------------------------------------------------------- (A) restoration replay +def rref(vectors): + """Canonical reduced basis of the GF(2) span of integer bit-vectors (frame identity).""" + basis = {} + for v in vectors: + for top in sorted(basis, reverse=True): + if v >> top & 1: + v ^= basis[top] + if v: + top = v.bit_length() - 1 + for t in list(basis): + if basis[t] >> top & 1: + basis[t] ^= v + basis[top] = v + return tuple(sorted(basis.items())) + + +def replay_restoration(trace): + """Exact replay over a free group of reference-change symbols with rational coefficients. + + Each register holds {(input_label, reduced_word): Fraction}. Every public array starts + as its own independent label (arbitrary dirty content); owned private arrays start absent. + The endpoint must be the normalized shear (forward Y_i += X_i, backward X_i -= Y_i, + i < 112 the X side) with every other public array -- including every borrowed source -- + returned exactly to its own label, and every owned private array returned to zero. + """ + active = trace['active_registers'] + val = {r: {(r, ()): Q(1)} for r in active} + frame = {r: rref(trace['endpoints'][str(r)]['initial']) for r in active} + private = set() + paid = collections.Counter() + + def warp(r, symbol): + out = collections.defaultdict(Q) + for (label, word), c in val[r].items(): + word = word[1:] if word and word[0] == -symbol else (symbol,) + word + out[label, word] += c + val[r] = {k: c for k, c in out.items() if c} + + for i, e in enumerate(trace['events']): + kind = e[0] + if kind == 'transport': + _, r, old, new, gap = e + need(frame[r] == rref(old), ('transport source frame', i)) + grow, shrink = rref(old + new) == rref(new), rref(old + new) == rref(old) + need((grow and len(new) > len(old)) or (r in private and shrink and len(new) < len(old)), + ('nested transport', i)) + need(gap == abs(len(new) - len(old)), ('transport rank', i)) + frame[r] = rref(new) + paid[gap] += 1 + elif kind == 'add': + _, d, src, q, common = e + need(d != src and frame[d] == frame[src] == rref(common), ('ADD common frame', i)) + q = Q(q) + for k, c in list(val[src].items()): + v = val[d].get(k, 0) + q * c + if v: + val[d][k] = v + else: + val[d].pop(k, None) + elif kind == 'scale': + _, r, q, common = e + need(frame[r] == rref(common) and Q(q) != 0, ('SCALE', i)) + val[r] = {k: Q(q) * c for k, c in val[r].items()} + elif kind == 'swap': + _, a, b, common = e + need(frame[a] == frame[b] == rref(common), ('SWAP', i)) + val[a], val[b] = val[b], val[a] + elif kind in ('logical_monomial', 'dual_monomial'): + _, r, symbol, common = e + need(frame[r] == rref(common), ('monomial frame', i)) + warp(r, symbol) + elif kind in ('handoff', 'dual_handoff'): + _, r, old, new, symbol = e + need(frame[r] == rref(old) and len(old) == len(new), ('handoff frame', i)) + warp(r, symbol) + frame[r] = rref(new) + elif kind == 'copy': + _, r, src, common = e + need(not val.get(r) and frame[src] == rref(common), ('COPY guard', i)) + val[r], frame[r] = dict(val[src]), rref(common) + private.add(r) + elif kind == 'clear': + _, r, common = e + need(r in private and frame[r] == rref(common), ('CLEAR guard', i)) + val[r] = {} + elif kind == 'zero_buffer': + _, r, common, role = e + need(r not in val and role in frame, ('fresh zero buffer', i)) + val[r], frame[r] = {}, rref(common) + private.add(r) + elif kind == 'zero_reframe': + _, r, common = e + need(r in private and not val[r], ('zero reframe', i)) + frame[r] = rref(common) + else: + raise Reject(('unknown event', kind)) + backward = trace.get('orientation') == 'backward' + for r in active: + want = {(r, ()): Q(1)} + if backward and r < 112: + want[r + 112, ()] = Q(-1) + if not backward and 112 <= r < 224: + want[r - 112, ()] = Q(1) + need(val[r] == want, ('endpoint column not restored/sheared', r)) + need(frame[r] == rref(trace['endpoints'][str(r)]['final']), ('endpoint frame', r)) + need(private and all(not val[r] for r in private), 'owned private arrays return to zero') + need({str(k): v for k, v in paid.items()} == trace['local_profile'], 'paid transport profile') + borrowed = sorted({w['borrow_from'] for w in trace['warps']}) + identity = [b for b in borrowed if val[b] == {(b, ()): Q(1)}] + sheared = [b for b in borrowed if b not in identity] # already checked equal to the declared shear column + return dict(borrowed_sources_returned_to_input=len(identity), borrowed_sources_ending_as_shear_column=sheared, + private_arrays_zero=len(private), public_columns=len(active)) + + +# ---------------------------------------------------------------- (A) whole-call owner hosting +def check_owner_hosting(owners, parent, helper_widths, local_profile): + widths = {int(k): v for k, v in helper_widths.items()} + calls = collections.defaultdict(list) + for row in owners: + calls[row['stage'], row['replica']].append(row) + need(set(calls) == {(s, r) for s in range(9) for r in range(8)}, '72 actual (stage, replica) calls') + pair_of = {(int(c['stage']), int(c['replica'])): int(c['pair']) for c in parent['calls']} + need(set(pair_of) == set(calls), 'parent call list matches owner calls') + for (stage, replica), rows in calls.items(): + need(len(rows) == 436 and {r['helper'] for r in rows} == set(widths), 'one row per (call, helper)') + need(len({r['family'] for r in rows}) == 436, 'at most one helper per physical family per call') + pair = pair_of[stage, replica] + data = {replica * 896 + (2 * pair + side) * 112 + port for side in (0, 1) for port in range(112)} + need(not data & {r['family'] for r in rows}, 'helper family is not an active data family of its call') + for r in owners: + need(r['width'] == widths[r['helper']], 'owner width equals the helper residual width') + need(r['copy'] == r['owner_replica'] * 112 + r['port'], 'copy ABI') + need(r['family'] // 896 == r['owner_replica'] and r['family'] % 112 == r['port'], 'family ABI') + # Original pending children = old pooled blocks + old idle residuals of the hosted parent. + pooled = collections.Counter() + for r in parent['hosting']['pooled_slots']: + pooled[r['family'], r['child']] += r['width'] + original = collections.Counter(pooled) + for x in parent['idle_children']: + need(x['hosted'] == pooled.get((x['family'], x['child']), 0) == x['pending_offset'], + 'idle offset = pooled prefix') + original[x['family'], x['child']] += x['rank'] + blocks = collections.defaultdict(list) + for r in owners: + blocks[r['family'], r['child']].append((r['offset'], r['offset'] + r['width'])) + for key, iv in blocks.items(): + need(key in original, 'owner row targets an inherited pending child') + iv.sort() + pos = 0 + for lo, hi in iv: + need(lo == pos, 'assigned blocks are disjoint and form an exact prefix') + pos = hi + need(pos <= original[key], 'assigned prefix fits inside the inherited child rank') + residual = collections.Counter() + for key, rank in original.items(): + rest = rank - sum(hi - lo for lo, hi in blocks.get(key, [])) + if rest: + residual[rest] += 1 + hosted = sum(r['width'] for r in owners) + total = sum(original.values()) + profile = collections.Counter() + for r, n in local_profile.items(): + profile[int(r)] += 72 * n + profile.update(residual) + return dict(calls=len(calls), roles=len(owners), original_children=len(original), + original_rank_mass=total, hosted=hosted, residual_mass=total - hosted, + residual={str(k): v for k, v in sorted(residual.items())}, + profile={str(k): v for k, v in sorted(profile.items())}) + + +# ---------------------------------------------------------------- (B) finite constants +def orthogonal_count(n): + """Brute-force |O(n,2)| = #{A in GF(2)^(n x n): A A^T = I} by orthonormal row extension.""" + vecs = [v for v in range(1 << n) if bin(v).count('1') % 2 == 1] + + def extend(rows): + if len(rows) == n: + return 1 + return sum(extend(rows + [v]) for v in vecs + if v not in rows and all(bin(v & w).count('1') % 2 == 0 for w in rows)) + return extend([]) + + +def group_order(m): + k = m // 2 + g = 2 ** (k * k) + for j in range(1, k + 1): + g *= 2 ** (2 * j) - 1 + return g + + +def row_guard(stock_bits, payload_bits): + row = 2 * stock_bits + 9909 + 252 + 2 * payload_bits + need(row < 20161, 'row guard 2*stock_bits + 9909 + 252 + 2*payload < 20161') + return row + + +def check_constants(invoice, trace, old, payload=512): + need(orthogonal_count(3) == group_order(3) == 6 and orthogonal_count(5) == group_order(5) == 720, + '|O(n,2)| formula on brute-forced small cases') + m = 73 + live, reserve, cleanup, centres, work = 896 * 8, 492, len(trace['zero_buffers']), 8, 2 + physical = live + reserve + cleanup + centres + work + need(physical == invoice['physical_families'] == 7745, 'physical family identity 7168+492+75+8+2') + group = group_order(m) + stock = group * physical + row = 2 * stock.bit_length() + 9909 + 252 + 2 * payload + total_mass = group * m * live + 2 ** 100000 + c0_bits = (32 * m * total_mass * total_mass).bit_length() + literal = 2 * 2 ** 30000 * stock ** 2 + 8 * group * m * live + 4 * stock + 4 + 32 * m + fin = invoice['finite'] + need((group.bit_length(), stock.bit_length(), row, c0_bits, literal.bit_length()) + == (fin['group_bits'], fin['physical_stock_bits'], fin['physical_row_coefficient'], + fin['required_C0_bits'], fin['literal_bits']), 'recomputed finite fields equal the invoice') + need(fin['retained_row_coefficient'] == 20161, 'retained row allowance') + row_guard(stock.bit_length(), payload) + need(c0_bits < 210000 and 2 * total_mass + 18 < 2 ** 210000, 'C0 guards') + # Equal finite fields in the direct-delivery504 invoice are explained by equal stock bit length. + ofin = old['finite'] + need((group * old['physical']).bit_length() == stock.bit_length() + and (ofin['physical_stock_bits'], ofin['physical_row_coefficient'], ofin['required_C0_bits']) + == (fin['physical_stock_bits'], fin['physical_row_coefficient'], fin['required_C0_bits']), + 'identical finite fields are explained by equal stock bit length') + guard = invoice['exact_magnitude_guard'] + ideal = max(invoice['local'][o]['precision']['P_binary_upper'] for o in ('forward', 'backward')) + blocks = guard['completed_blocks'] + conv = (m + 1) // 2 + need((ideal, blocks, conv) == (guard['ideal_local_bits'], 144, guard['initial_sup_to_hilbert_per_lambda']), + 'guard ingredients 63, 144, 37') + coeff = ideal + blocks + conv + need(coeff == invoice['global_precision_guard_coefficient'] == 244 and coeff < payload, + 'per-lambda guard 244 < payload') + # (ideal+blocks) + conv*lam <= coeff*lam <=> (ideal+blocks)*(lam-1) >= 0, i.e. lam >= 1; tight at lam = 1. + need(ideal + blocks + conv == coeff, 'guard identity at lambda = 1') + retained_fixed = ideal + conv + 72 + 72 + 4 # direct-delivery504 code/invoice_final.py fixed-bit prefix rule + need(retained_fixed < payload, 'retained fixed-bit prefix rule also holds at lambda = 1') + # Unit question: if the row term 2*payload scaled with lambda, the row guard would hold only up to lam_max. + lam_max = max(k for k in range(1, 64) if not rejected(lambda: row_guard(stock.bit_length(), payload * k))) + return dict(physical=physical, group_bits=group.bit_length(), stock_bits=stock.bit_length(), row=row, + required_C0_bits=c0_bits, literal_bits=literal.bit_length(), guard_coefficient=coeff, + retained_fixed_bit_prefix=retained_fixed, row_lambda_max_if_payload_scaled=lam_max) + + +# ---------------------------------------------------------------- moments (decimal, bounded error) +PREC = 320 +TOL = decimal.Decimal(10) ** -300 + + +def moment(profile, m, W, b, surcharge): + """sum_r r H_r/(m W) (m/r)^b [+ 32 m sum(H)/(10^16 W) m^b] minus one. + + Each term uses <= 7 correctly rounded decimal operations (CPython's decimal ln and exp + are correctly rounded), each with relative error <= 5e-320; there are <= 13 terms of + size <= 2, so the absolute error is < 1e-316. Callers accept a sign only when + |result| > TOL = 1e-300. + """ + with decimal.localcontext() as ctx: + ctx.prec = PREC + D = decimal.Decimal + bb = D(b.numerator) / D(b.denominator) + terms = [(Q(r * n, m * W), Q(m, r)) for r, n in profile.items()] + if surcharge: + terms.append((Q(32 * m * sum(profile.values()), 10 ** 16 * W), Q(m))) + total = D(0) + for w, ratio in terms: + weight = D(w.numerator) / D(w.denominator) + total += weight * (bb * (D(ratio.numerator) / D(ratio.denominator)).ln()).exp() + return total - 1 + + +def sign_of(x): + need(abs(x) > TOL, 'moment within the decimal error tolerance') + return 1 if x > 0 else -1 + + +def check_endpoint(spec, endpoint, ledger, profile): + m, W = 73, 7168 + prof = {int(k): v for k, v in profile.items()} + need({int(k): v for k, v in spec['expected']['global_profile'].items()} == prof + == {int(k): v for k, v in endpoint['profile'].items()}, 'SPEC = ENDPOINT = recounted profile') + mass = sum(r * n for r, n in prof.items()) + need((spec['expected']['live'], endpoint['W'], spec['geometry']['dimension']) == (W, W, m), 'm and W') + need(mass == spec['expected']['rank_mass'] == 520704 and m * W - mass == spec['expected']['deficit'] == 2560, + 'rank mass and deficit') + need(m * m > 2 * max(prof) ** 2, 'halving guard m^2 > 2 rmax^2') + need(spec['geometry']['calls'] * spec['geometry']['helpers_per_call'] == 72 * 436, '72 x 436 owner rows') + need(Q(endpoint['surcharge_weight']) == Q(32 * m * sum(prof.values()), 10 ** 16 * W), 'surcharge weight') + C = Q(endpoint['complex_lower']) + need((C * 10 ** 200).denominator == 1, 'C on the 10^-200 grid') + need(Q(ledger['complex_lower_pinned']['rational']) == C, 'ledger uses the certified endpoint') + native = moment(prof, m, W, C, False) + cons = moment(prof, m, W, C, True) + nxt = moment(prof, m, W, C + Q(1, 10 ** 200), True) + need(sign_of(native) < 0 and sign_of(cons) < 0, 'moments below one at C') + need(sign_of(nxt) > 0, 'conservative moment above one at C + 10^-200') + row = ledger['rows']['struct_boundary_radix_union'] + q, a, kappa = (Q(row[k]['rational']) for k in ('q', 'a', 'kappa')) + c = Q(spec['supplier']['bit_lower']) + need(0 < q < a < C < c, 'rate ordering q < a_eff < b < c') + need(kappa == C - Q(1, 10 ** 246) - Q(1, 10 ** 222), 'kappa = C - 1e-246 - 1e-222') + return dict(C_decimal_40=f'{decimal.Decimal(C.numerator) / decimal.Decimal(C.denominator):.40f}', + native_moment_minus_one=f'{native:.6e}', conservative_minus_one=f'{cons:.6e}', + next_grid_conservative_minus_one=f'{nxt:.6e}', a_minus_q=f'{float(a - q):.6e}', + b_minus_a=f'{float(C - a):.6e}', c_minus_b=f'{float(c - C):.6e}') + + +# ---------------------------------------------------------------- (C) retained bit supplier +def check_bit(spec, bit_pr2260, bit_main, bit_override=None): + need(bit_pr2260 == bit_main, 'PR2260 BIT-EXPECTED equals the base-tree e8-bit-p111-tuned EXPECTED') + nine = bit_pr2260['nine'] + need(Q(spec['supplier']['bit_lower']) == Q(nine['bit_lower']), 'SPEC bit_lower is the retained bit endpoint') + c = Q(nine['bit_lower']) if bit_override is None else bit_override + H = {int(k): v for k, v in nine['profile'].items()} + BW = nine['bit']['live'] + word = bit_pr2260['word'] + need(64 * BW - sum(r * n for r, n in H.items()) == 32 * (8 * word['v'] - 9 * sum(word['copy_ranks'])), + 'bit deficit identity') + need(64 * 64 > 2 * max(H) ** 2, 'bit halving guard') + mom = moment(H, 64, BW, c, True) + need(sign_of(mom) < 0, 'conservative bit moment below one at c') + return dict(bit_conservative_minus_one=f'{mom:.6e}', bit_live=BW, bit_maxchild=max(H)) + + +# ---------------------------------------------------------------- inherited-statement trace +REVIEW = 'vendor/pr1673/capped-phase-fusion/frontier_fusion/INDEPENDENT-SUBSTITUTION-REVIEW.md' +TRACE = [ + ('A-restoration', C2260, 'PROOF.md', 'restore arbitrary dirty helpers, and return all owned private fields to zero'), + ('A-restoration', C2260, 'PROOF-LOCAL.md', 'Thus arbitrary dirty inputs and operator order, rather than only the all-zero helper assignment, are checked.'), + ('A-serialize', C2260, 'PROOF.md', 'Invocations serialize; each whole-helper operator restores all spectator coordinates.'), + ('A-serialize', C2260, 'PROOF-OWNERS.md', 'Each invocation completes before the next one begins.'), + ('A-completed-call', C2265, 'README.md', "PR2260's dirty borrowing is internal to the T8 parent call and is restored at its boundary"), + ('A-pr1673-use', C2265, REVIEW, 'acts as identity on arbitrary dirty helper/coarse/spectator coordinates at completed-call boundaries'), + ('B-guard', C2260, 'PROOF-LOCAL.md', '63 + 144 + 37*lambda <= 244*lambda < 512*lambda.'), + ('B-guard', C2260, 'PROOF.md', 'the new row coefficient 16467<20161'), + ('B-pr1673-generic', C2265, REVIEW, 'It does not require the former numeric prefix constant to remain512 or1024.'), + ('C-interchange', C2265, REVIEW, 'The retained bit supplier supplies the same arbitrary-width equal-chunk interchange interface'), + ('C-interchange', C2260, 'PROOF.md', 'Its circuit/realization assumptions remain inherited.'), + ('C-theorem', C2265, 'vendor/pr1673/capped-phase-fusion/phase_fusion_note.tex', 'Assume the paid equal-chunk interchange primitive used by the retained support router.'), +] + + +def check_trace(texts): + return [dict(item=item, commit=commit[:8], file=path, line=text_pin(texts[commit, path], phrase)) + for item, commit, path, phrase in TRACE] + + +# ---------------------------------------------------------------- driver +def rejected(fn): + try: + fn() + except Reject as exc: + return str(exc) + return False + + +def main(): + ensure_commits() + inp = {key: blob(*key) for key in PINS} + + def J(commit, path): + data = inp[commit, path] + return json.loads(gzip.decompress(data) if path.endswith('.gz') else data) + fwd, bwd = J(C2260, 'local/data/forward.json'), J(C2260, 'local/data/backward.json') + post = J(C2260, 'local/data/postludes.json') + witness = J(C2260, 'local/inputs/WITNESS.json') + owners, parent = J(C2260, 'owners/OWNERS.json.gz'), J(C2260, 'owners/inputs/HOSTED-PARENT.json.gz') + owners_expected, invoice = J(C2260, 'owners/EXPECTED.json'), J(C2260, 'local/data/finite-invoice.json') + bit2260 = J(C2260, 'arithmetic/vendor/BIT-EXPECTED.json') + spec, endpoint, ledger = J(C2265, 'SPEC.json'), J(C2265, 'ENDPOINT.json'), J(C2265, 'outer/LEDGER.json') + bit_main = local_file('research/e8-bit-p111-tuned/tune/EXPECTED.json') + old = local_file('research/direct-delivery504-global/evidence/audit/PREFIX-AND-INVOICE.json') + texts = {k: v.decode() for k, v in inp.items() if k[1].endswith(('.md', '.tex'))} + + out = dict(status=None, pr2260=C2260, pr2265=C2265) + out['A_alias_closure'] = {o: check_alias_closure(t, witness, post[o]) + for o, t in (('forward', fwd), ('backward', bwd))} + need(fwd['helper_widths'] == bwd['helper_widths'] and fwd['local_profile'] == bwd['local_profile'], + 'orientations agree') + out['A_restoration_replay'] = {o: replay_restoration(t) for o, t in (('forward', fwd), ('backward', bwd))} + need(all(v['borrowed_sources_returned_to_input'] + len(v['borrowed_sources_ending_as_shear_column']) == 44 + for v in out['A_restoration_replay'].values()), 'all 44 borrowed sources end at their endpoint column') + hosting = check_owner_hosting(owners, parent, fwd['helper_widths'], fwd['local_profile']) + need(hosting['residual'] == owners_expected['idle'] and hosting['profile'] == owners_expected['profile'], + 'independent residual recount equals PR2260 owners EXPECTED') + need((hosting['original_rank_mass'], hosting['hosted'], hosting['residual_mass']) == (387072, 254088, 132984), + 'factor partition 387072 = 254088 hosted + 132984 residual (PR2260 PROOF.md)') + out['A_owner_hosting'] = hosting + out['B_constants'] = check_constants(invoice, fwd, old) + out['C_bit'] = check_bit(spec, bit2260, bit_main) + out['D_endpoint'] = check_endpoint(spec, endpoint, ledger, hosting['profile']) + out['trace'] = check_trace(texts) + inventory = json.loads((PKG / 'INVENTORY.json').read_text()) + classes = collections.Counter(item['class'] for item in inventory['premises']) + need(all(inventory['summary'][k] == classes.get(k, 0) for k in inventory['classes']), + 'INVENTORY summary matches its premise classes') + out['inventory_classes'] = dict(sorted(classes.items())) + + # ------------------------------------------------------------ negative controls + removed = [w['removed'] for w in fwd['warps']] + + def alias_source_is_removed_alias(): + t = copy.deepcopy(fwd) + t['warps'][0]['borrow_from'] = removed[1] + w = copy.deepcopy(witness) + w['pairs'][0]['borrow_from'] = removed[1] + check_alias_closure(t, w, post['forward']) + + def alias_source_outside_call(): + t = copy.deepcopy(fwd) + t['warps'][0]['borrow_from'] = 2000 + w = copy.deepcopy(witness) + w['pairs'][0]['borrow_from'] = 2000 + check_alias_closure(t, w, post['forward']) + + def event_reads_removed_alias(): + t = copy.deepcopy(fwd) + i = next(i for i, e in enumerate(t['events']) if e[0] == 'add') + t['events'][i][2] = removed[0] + check_alias_closure(t, witness, post['forward']) + + def owner_block_overlap(): + o = copy.deepcopy(owners) + r = next(r for r in o if r['offset'] > 0) + r['offset'] -= 1 + check_owner_hosting(o, parent, fwd['helper_widths'], fwd['local_profile']) + + def owner_on_active_data_family(): + o = copy.deepcopy(owners) + r = o[0] + call = next(c for c in parent['calls'] if (int(c['stage']), int(c['replica'])) == (r['stage'], r['replica'])) + r['owner_replica'] = r['replica'] + r['family'] = r['replica'] * 896 + 2 * int(call['pair']) * 112 + r['port'] + r['copy'] = r['owner_replica'] * 112 + r['port'] + check_owner_hosting(o, parent, fwd['helper_widths'], fwd['local_profile']) + + def halving_child_rank_52(): + p = dict(hosting['profile']) # mass-preserving: 48 + 4 -> 52 + p['48'] -= 1 + p['4'] -= 1 + p['52'] = 1 + s = copy.deepcopy(spec) + e = copy.deepcopy(endpoint) + s['expected']['global_profile'] = p + e['profile'] = p + check_endpoint(s, e, ledger, p) + + def row_payload_scaled_beyond_lambda_max(): + lam = out['B_constants']['row_lambda_max_if_payload_scaled'] + 1 + row_guard(out['B_constants']['stock_bits'], 512 * lam) + + def endpoint_plus_one_grid_step(): + e = copy.deepcopy(endpoint) + e['complex_lower'] = str(Q(e['complex_lower']) + Q(1, 10 ** 200)) + led = copy.deepcopy(ledger) + led['complex_lower_pinned']['rational'] = e['complex_lower'] + check_endpoint(spec, e, led, hosting['profile']) + + def kappa_plus_1e_240(): + led = copy.deepcopy(ledger) + k = led['rows']['struct_boundary_radix_union']['kappa'] + k['rational'] = str(Q(k['rational']) + Q(1, 10 ** 240)) + check_endpoint(spec, endpoint, led, hosting['profile']) + + def bit_endpoint_equal_to_b(): + s = copy.deepcopy(spec) + s['supplier']['bit_lower'] = endpoint['complex_lower'] + check_endpoint(s, endpoint, ledger, hosting['profile']) + + def bit_endpoint_plus_1e_18(): + check_bit(spec, bit2260, bit_main, bit_override=Q(bit2260['nine']['bit_lower']) + Q(1, 10 ** 18)) + + def replay_drops_one_monomial_warp(): + t = copy.deepcopy(fwd) + i = next(i for i, e in enumerate(t['events']) if e[0] == 'logical_monomial') + del t['events'][i] + replay_restoration(t) + + def replay_doubles_one_add_coefficient(): + t = copy.deepcopy(fwd) + i = next(i for i, e in enumerate(t['events']) if e[0] == 'add' and str(e[1]) in t['helper_widths']) + t['events'][i][3] = str(2 * Q(t['events'][i][3])) + replay_restoration(t) + + controls = {} + for fn in (replay_drops_one_monomial_warp, replay_doubles_one_add_coefficient, alias_source_is_removed_alias, alias_source_outside_call, event_reads_removed_alias, + owner_block_overlap, owner_on_active_data_family, halving_child_rank_52, + row_payload_scaled_beyond_lambda_max, endpoint_plus_one_grid_step, kappa_plus_1e_240, + bit_endpoint_equal_to_b, bit_endpoint_plus_1e_18): + controls[fn.__name__] = rejected(fn) + out['negative_controls'] = controls + need(all(isinstance(v, str) for v in controls.values()), ('control accepted', [k for k, v in controls.items() if not v])) + out['status'] = 'PASS_PR2265_SUPPLIER_ADMISSION_AUDIT' + rendered = json.dumps(out, indent=1, sort_keys=True) + '\n' + expected_path = PKG / 'EXPECTED.json' + if '--write' in sys.argv[1:]: + expected_path.write_text(rendered) + else: + need(json.loads(expected_path.read_text()) == json.loads(rendered), 'receipt differs from EXPECTED.json') + print(out['status'], 'controls_rejected', sum(isinstance(v, str) for v in controls.values()), 'of', len(controls)) + + +if __name__ == '__main__': + try: + main() + except Reject as exc: + raise SystemExit(f'FAIL: {exc}') From 6226a8348b4069b6c1c8d66a3ff35526bf2c767a Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Thu, 15 Oct 2026 10:02:26 +0530 Subject: [PATCH 2/6] Record fixed-bit lambda threshold for the PR2260 guard units question The selected lineage charges a fixed 512-bit prefix allowance; PR2260's per-lambda guard 244*lambda fits it only for lambda <= 2, and under the per-lambda reading its row formula needs lambda <= 4. Recorded as an open interface question (not a counterexample) in the receipt, inventory and README. Co-Authored-By: Claude Opus 5.5 --- research/pr2265-supplier-admission-audit/EXPECTED.json | 1 + .../pr2265-supplier-admission-audit/INVENTORY.json | 2 +- research/pr2265-supplier-admission-audit/README.md | 10 ++++++---- research/pr2265-supplier-admission-audit/TASK.json | 2 +- research/pr2265-supplier-admission-audit/verify.py | 5 ++++- 5 files changed, 13 insertions(+), 7 deletions(-) diff --git a/research/pr2265-supplier-admission-audit/EXPECTED.json b/research/pr2265-supplier-admission-audit/EXPECTED.json index c5428832d9..ba9dc48463 100644 --- a/research/pr2265-supplier-admission-audit/EXPECTED.json +++ b/research/pr2265-supplier-admission-audit/EXPECTED.json @@ -71,6 +71,7 @@ "B_constants": { "group_bits": 2628, "guard_coefficient": 244, + "guard_lambda_max_if_payload_fixed_bits": 2, "literal_bits": 35282, "physical": 7745, "required_C0_bits": 200012, diff --git a/research/pr2265-supplier-admission-audit/INVENTORY.json b/research/pr2265-supplier-admission-audit/INVENTORY.json index 40ecdc80c8..fbccd759e3 100644 --- a/research/pr2265-supplier-admission-audit/INVENTORY.json +++ b/research/pr2265-supplier-admission-audit/INVENTORY.json @@ -71,7 +71,7 @@ "check_here": "verify.py check_constants", "class": "INHERITED-traced", "finding": "The arithmetic holds: 244 = 63 + 144 + 37, the inequality 207 + 37*lambda <= 244*lambda is equivalent to lambda >= 1 (tight at 1), and 244 < 512. The retained fixed-bit rule of direct-delivery504 (local + 37 + calls + bridges + 4) gives 248 < 512. The value 63 is PR2260's P_binary_upper and is taken from its precision receipts, not recomputed.", - "open_unit_question": "PR2260 declares payload 512 a per-lambda coefficient, but its row formula 2*stock_bits + 9909 + 252 + 2*payload counts 2*payload = 1024 as a fixed term, as in the fixed-bit predecessors. If that term scaled with lambda, the row guard < 20161 would hold only for lambda <= 4. Neither PR2260 nor #2265 says how the row allowance scales with lambda. This is recorded as an open interface question, not a counterexample." + "open_unit_question": "In the selected lineage the prefix allowance is a fixed 512-bit count, compared with a lambda-free prefix: docs/research/community-batch952-review.md:51-56, scripts/verify_frontier1094.py:94, research/direct-delivery504-global/code/invoice_final.py:238-241. PR2260 instead declares payload 512 a per-lambda coefficient, with guard 244*lambda. Under the fixed-bit reading, 244*lambda < 512 holds only for lambda <= 2. Under the per-lambda reading, PR2260's row formula 2*stock_bits + 9909 + 252 + 2*payload still counts 2*payload = 1024 as a fixed term; if it scaled, row < 20161 would hold only for lambda <= 4. Neither PR2260 nor #2265 defines lambda or says how the row allowance scales with it. This is an open interface question, not a counterexample. For #2265 the PR1673 outer only needs an O(g) supplier guard constant (review:73-78), so it bears more on PR2260's own balanced-prefix outer, whose degree gap uses 20161." }, { "id": "B2-C0", diff --git a/research/pr2265-supplier-admission-audit/README.md b/research/pr2265-supplier-admission-audit/README.md index 61b23525ad..55066ab8e5 100644 --- a/research/pr2265-supplier-admission-audit/README.md +++ b/research/pr2265-supplier-admission-audit/README.md @@ -64,9 +64,11 @@ What the independent checks establish: - In the forward orientation it is returned to its input. - In the backward orientation it ends as the declared shear column X_73 − Y_185. - So the "completed call" premise holds for this word, but a reader should not take "borrowed = helper" literally. -2. **Unit question for the guard (B1).** PR2260 declares the 512 payload a *per-lambda* coefficient (`finite-invoice.json` precision_units), with guard 244·lambda. Its row formula `2*stock_bits + 9909 + 252 + 2*payload` still counts `2*payload = 1024` as a fixed term, as in the fixed-bit predecessors. If that term scaled with lambda, row < 20161 would hold only for lambda ≤ 4. - - Neither PR states how the row allowance scales with lambda. - - For #2265 the PR1673 outer needs only an O(g) supplier constant (review, lines 73–78), so this is recorded as an open interface question, not a counterexample. +2. **Unit question for the guard (B1).** In the selected lineage the prefix allowance is a *fixed* 512-bit count, compared with a lambda-free prefix (`docs/research/community-batch952-review.md:51`, `scripts/verify_frontier1094.py:94`, `direct-delivery504-global/code/invoice_final.py:238-241`). PR2260 instead declares the 512 payload a *per-lambda* coefficient, with guard 244·lambda (`finite-invoice.json` precision_units). + - Under the fixed-bit reading, 244·lambda < 512 only for lambda ≤ 2. + - Under PR2260's per-lambda reading, its row formula `2*stock_bits + 9909 + 252 + 2*payload` still counts `2*payload = 1024` as fixed. If that term scaled, row < 20161 would need lambda ≤ 4. + - Neither PR defines lambda here or says how the row allowance scales with it. + - For #2265 the PR1673 outer needs only an O(g) supplier guard constant (review, lines 73–78). The question bears mainly on PR2260's own balanced-prefix outer, whose degree gap uses 20161. It is an open interface question, not a counterexample. 3. **Identical invoice fields are explained, not copied.** PR2260's physical_stock_bits 2641, row 16467 and required_C0_bits 200012 equal direct-delivery504's exactly. The reason is that both stocks (7682 and 7745 families) have the same bit length after multiplying by |O(73,2)|, and the C_0 field is dominated by 2^100000. 4. **Surcharge portability.** The conservative surcharge used by #2265's endpoint comes from the vendored `moment.py`. Its own comment calls the envelope "only conditionally portable to the new cover". Neither PR proves that portability; it is inherited. @@ -123,7 +125,7 @@ Each control must be rejected by the named check: 1. **Guard units (B1).** - *Question:* is the retained row allowance 20161 per-lambda or absolute, given PR2260's per-lambda payload? - - *Why it matters:* under a per-lambda reading of `2*payload`, the row guard holds only for lambda ≤ 4. + - *Why it matters:* under the lineage's fixed-bit reading, PR2260's 244·lambda guard fits 512 only for lambda ≤ 2. Under a per-lambda reading of `2*payload`, the row guard holds only for lambda ≤ 4. - *First step:* locate the retained interface's definition of lambda and of the row coefficient in the selected lineage (direct-delivery504 / PR523 invoice notes), then restate PR2260's row in matching units. - *Blocker:* the definition of lambda in the all-size compiler is spread over historical notes. 2. **Surcharge portability (D5).** diff --git a/research/pr2265-supplier-admission-audit/TASK.json b/research/pr2265-supplier-admission-audit/TASK.json index 5d1ede1a24..aa01c5dd0d 100644 --- a/research/pr2265-supplier-admission-audit/TASK.json +++ b/research/pr2265-supplier-admission-audit/TASK.json @@ -52,7 +52,7 @@ "open_questions": [ { "question": "Is the retained row allowance 20161 per-lambda or absolute, given PR2260's per-lambda 512 payload?", - "why_it_matters": "PR2260's row formula counts 2*payload=1024 as fixed; under a per-lambda reading the row guard holds only for lambda<=4.", + "why_it_matters": "In the selected lineage the 512 prefix allowance is a fixed bit count; PR2260's 244*lambda guard fits it only for lambda<=2, while under PR2260's per-lambda reading its row formula (2*payload fixed) holds only for lambda<=4.", "first_step": "Locate the retained definitions of lambda and of the row coefficient in the selected lineage (direct-delivery504 / PR523 invoice notes) and restate PR2260's row in matching units.", "blocked_by": "The definition of lambda in the all-size compiler is spread over historical notes." }, diff --git a/research/pr2265-supplier-admission-audit/verify.py b/research/pr2265-supplier-admission-audit/verify.py index d7ab670fc9..682882017a 100644 --- a/research/pr2265-supplier-admission-audit/verify.py +++ b/research/pr2265-supplier-admission-audit/verify.py @@ -410,7 +410,10 @@ def check_constants(invoice, trace, old, payload=512): need(retained_fixed < payload, 'retained fixed-bit prefix rule also holds at lambda = 1') # Unit question: if the row term 2*payload scaled with lambda, the row guard would hold only up to lam_max. lam_max = max(k for k in range(1, 64) if not rejected(lambda: row_guard(stock.bit_length(), payload * k))) - return dict(physical=physical, group_bits=group.bit_length(), stock_bits=stock.bit_length(), row=row, + # Fixed-bit reading of the retained allowance (selected lineage: 512 bits, e.g. verify_frontier1094.py:94): + # the per-lambda guard coeff*lambda fits a fixed 512-bit payload only up to lam_fixed. + lam_fixed = max(k for k in range(1, 64) if coeff * k < payload) + return dict(guard_lambda_max_if_payload_fixed_bits=lam_fixed,physical=physical, group_bits=group.bit_length(), stock_bits=stock.bit_length(), row=row, required_C0_bits=c0_bits, literal_bits=literal.bit_length(), guard_coefficient=coeff, retained_fixed_bit_prefix=retained_fixed, row_lambda_max_if_payload_scaled=lam_max) From c4b4e63afde3a822ac716a7995b72b6e7a43affd Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Thu, 15 Oct 2026 10:03:05 +0530 Subject: [PATCH 3/6] Note why the PR2284 modern-outer point is out of scope Co-Authored-By: Claude Opus 5.5 --- research/pr2265-supplier-admission-audit/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/research/pr2265-supplier-admission-audit/README.md b/research/pr2265-supplier-admission-audit/README.md index 55066ab8e5..e36918f577 100644 --- a/research/pr2265-supplier-admission-audit/README.md +++ b/research/pr2265-supplier-admission-audit/README.md @@ -113,7 +113,7 @@ Each control must be rejected by the named check: ## Scope, inherited assumptions, unresolved obligations -- This is a finite data audit at one point: #2265's final point and PR2260's shipped word. It is not a proof of the capped-fusion theorem, of the all-size compiler, or of any multiplication theorem. #2284's "modern outer" point was not audited. +- This is a finite data audit at one point: #2265's final point and PR2260's shipped word. It is not a proof of the capped-fusion theorem, of the all-size compiler, or of any multiplication theorem. #2284's "modern outer" point was not audited. Its `outer/ENDPOINT.json` at head `e71574b9` has a different schema (an 8-digit endpoint with no surcharge_weight) and a different profile (93-row owner delta, a rank-40 child), so the keys are not identical. - The replay is limited to PR2260's event model: - It checks the literal events under PR2260's documented semantics: free reference-change symbols, GF(2) frames, destructive COPY/CLEAR. It was written after reading PR2260's description and its row interpreter, so it is an independent *implementation* of the same model, not an independent model. - The native Clifford lowering, phases, the lambda-fold lift and the physical charts are not rechecked. From 14ab4ccc3f3f6cd49001586c2de715636dd97efb Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Thu, 15 Oct 2026 10:03:20 +0530 Subject: [PATCH 4/6] Require zero buffers to serve public roles in the restoration replay Co-Authored-By: Claude Opus 5.5 --- research/pr2265-supplier-admission-audit/verify.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/research/pr2265-supplier-admission-audit/verify.py b/research/pr2265-supplier-admission-audit/verify.py index 682882017a..3bb333c8c4 100644 --- a/research/pr2265-supplier-admission-audit/verify.py +++ b/research/pr2265-supplier-admission-audit/verify.py @@ -198,6 +198,7 @@ def replay_restoration(trace): returned exactly to its own label, and every owned private array returned to zero. """ active = trace['active_registers'] + public = set(active) val = {r: {(r, ()): Q(1)} for r in active} frame = {r: rref(trace['endpoints'][str(r)]['initial']) for r in active} private = set() @@ -259,7 +260,7 @@ def warp(r, symbol): val[r] = {} elif kind == 'zero_buffer': _, r, common, role = e - need(r not in val and role in frame, ('fresh zero buffer', i)) + need(r not in val and role in public, ('fresh zero buffer for a public role', i)) val[r], frame[r] = {}, rref(common) private.add(r) elif kind == 'zero_reframe': From 6ee781ae149149596b2809d88db5fb836a21fbe1 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Thu, 15 Oct 2026 10:18:15 +0530 Subject: [PATCH 5/6] Address review: rescope guard units, reclassify covered premises, harden controls - B1: report the literal-prefix threshold (lambda <= 8), state that both self-consistent readings pass, and check that the same mixed-reading thresholds bind the selected #1094 (pinned verify_frontier1094.py). - A2/B2/B3 reclassified COVERED (#2265 reruns PR2260 local/verify.py and local/invoice.py); D5 restated as a disjunction with the PR559 license. - Credit PR2226's witness for the X_73 borrow; cite PROOF-LOCAL:22. - Replace the tautological lambda control with two invoice-data mutations; add a backward-orientation replay control (15 controls). - Fall back to fetching pinned SHAs if a PR head moves; author credits. Co-Authored-By: Claude Opus 5.5 --- .../EXPECTED.json | 13 +++- .../INVENTORY.json | 53 +++++++------ .../pr2265-supplier-admission-audit/README.md | 78 +++++++++++-------- .../SOURCES.json | 6 ++ .../VERIFY.json | 5 +- .../pr2265-supplier-admission-audit/verify.py | 65 ++++++++++++---- 6 files changed, 144 insertions(+), 76 deletions(-) diff --git a/research/pr2265-supplier-admission-audit/EXPECTED.json b/research/pr2265-supplier-admission-audit/EXPECTED.json index ba9dc48463..71b5348d4f 100644 --- a/research/pr2265-supplier-admission-audit/EXPECTED.json +++ b/research/pr2265-supplier-admission-audit/EXPECTED.json @@ -72,12 +72,15 @@ "group_bits": 2628, "guard_coefficient": 244, "guard_lambda_max_if_payload_fixed_bits": 2, + "guard_lambda_max_literal_prefix_fixed_bits": 8, "literal_bits": 35282, "physical": 7745, "required_C0_bits": 200012, "retained_fixed_bit_prefix": 248, "row": 16467, "row_lambda_max_if_payload_scaled": 4, + "selected1094_prefix_lambda_max_if_conversion_scaled": 4, + "selected1094_row_lambda_max_if_payload_scaled": 4, "stock_bits": 2641 }, "C_bit": { @@ -95,24 +98,26 @@ "next_grid_conservative_minus_one": "3.157248e-202" }, "inventory_classes": { - "COVERED": 6, + "COVERED": 9, "INHERITED-traced": 5, - "TRUE-unencoded": 4 + "TRUE-unencoded": 1 }, "negative_controls": { "alias_source_is_removed_alias": "every borrowed source is a live public input array of the same call", "alias_source_outside_call": "every borrowed source is a live public input array of the same call", + "backward_replay_inverts_one_dual_monomial_symbol": "('endpoint column not restored/sheared', 70)", "bit_endpoint_equal_to_b": "rate ordering q < a_eff < b < c", "bit_endpoint_plus_1e_18": "conservative bit moment below one at c", "endpoint_plus_one_grid_step": "moments below one at C", "event_reads_removed_alias": "event add touches register 597 outside the call", "halving_child_rank_52": "halving guard m^2 > 2 rmax^2", + "invoice_guard_coefficient_245": "per-lambda guard 244 < payload", + "invoice_row_coefficient_16466": "recomputed finite fields equal the invoice", "kappa_plus_1e_240": "kappa = C - 1e-246 - 1e-222", "owner_block_overlap": "assigned blocks are disjoint and form an exact prefix", "owner_on_active_data_family": "helper family is not an active data family of its call", "replay_doubles_one_add_coefficient": "('endpoint column not restored/sheared', 115)", - "replay_drops_one_monomial_warp": "('endpoint column not restored/sheared', 22)", - "row_payload_scaled_beyond_lambda_max": "row guard 2*stock_bits + 9909 + 252 + 2*payload < 20161" + "replay_drops_one_monomial_warp": "('endpoint column not restored/sheared', 22)" }, "pr2260": "fde6b107e26a14da5bac5b66913c914708ea6901", "pr2265": "49ce38fee91f33edb54645724e7be9530f5631f6", diff --git a/research/pr2265-supplier-admission-audit/INVENTORY.json b/research/pr2265-supplier-admission-audit/INVENTORY.json index fbccd759e3..13c2be619a 100644 --- a/research/pr2265-supplier-admission-audit/INVENTORY.json +++ b/research/pr2265-supplier-admission-audit/INVENTORY.json @@ -1,8 +1,14 @@ { "schema": "pr2265-supplier-admission-inventory/1", "audited": { - "pr2265": {"head": "49ce38fee91f33edb54645724e7be9530f5631f6", "package": "research/selective-borrowing-outer-retune"}, - "pr2260": {"head": "fde6b107e26a14da5bac5b66913c914708ea6901", "package": "research/selective-borrowing-kappa"}, + "pr2265": { + "head": "49ce38fee91f33edb54645724e7be9530f5631f6", + "package": "research/selective-borrowing-outer-retune" + }, + "pr2260": { + "head": "fde6b107e26a14da5bac5b66913c914708ea6901", + "package": "research/selective-borrowing-kappa" + }, "base": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2" }, "classes": { @@ -23,7 +29,7 @@ "consumed_by_outer": "theorem hypothesis only: vendor/pr1673/capped-phase-fusion/phase_fusion_note.tex:63 and :443; INDEPENDENT-SUBSTITUTION-REVIEW.md:51-58, :80-81. No ledger row.", "check_here": "verify.py check_alias_closure + check_owner_hosting", "class": "TRUE-unencoded", - "finding": "Both orientations of the local word touch only the 660 public arrays of the call (224 data, 436 helpers) and the 76 owned private arrays. No event references a removed alias or any register outside the call. The 44 borrowed sources are 43 helper inputs plus one public data input: register 73, an X-side source for removed alias 653. Handoffs occur exactly at the 44 borrowed sources, and each has paid rank 0. Every one of the 31392 owner rows lies in an inherited pending child of the same hosted parent. Within each child the rows form disjoint exact prefixes, and no row uses an active data family of its own call.", + "finding": "Both orientations of the local word touch only the 660 public arrays of the call (224 data, 436 helpers) and the 76 owned private arrays. No event references a removed alias or any register outside the call. The 44 borrowed sources are 43 helper inputs plus one public data input: register 73, an X-side source for removed alias 653. Handoffs occur exactly at the 44 borrowed sources, and each has paid rank 0. Every one of the 31392 owner rows lies in an inherited pending child of the same hosted parent. Within each child the rows form disjoint exact prefixes, and no row uses an active data family of its own call. The data-input borrow (removed alias 653 <- source 73) originates in PR2226's 80-alias WITNESS (head dacaf3d8, research/anticipatory-dirty-borrowing/WITNESS.json) and is carried into PR2260. PR2260 PROOF-LOCAL.md:22 already treats all 660 public/data/helper inputs as arbitrary, so this is covered by PR2260's stated model; only helper-specific wording elsewhere is imprecise. It is a precision note, not a gap.", "residual_inheritance": "The all-size realization of this finite closure (lambda-fold lift, physical tape and route) is inherited from PR2260 PROOF.md:49-52." }, { @@ -32,12 +38,13 @@ "statement": "Arbitrary dirty helper and spectator coordinates are restored, together with the same normalized global transform, at each completed-call boundary.", "stated_in_2265": "README.md:34; README.md:42", "stated_in_2260": "PROOF.md:5-7; PROOF-LOCAL.md:27-46 (two replays: emitting replay and local/check_trace.py)", - "consumed_by_outer": "INDEPENDENT-SUBSTITUTION-REVIEW.md:51-58; phase_fusion_note.tex:443-444. No ledger row.", + "consumed_by_outer": "INDEPENDENT-SUBSTITUTION-REVIEW.md:51-58; phase_fusion_note.tex:443-444. No ledger row; covered by the PR2260 check that #2265 reruns.", "check_here": "verify.py replay_restoration: an independently written exact replay over a free group of reference-change symbols with rational coefficients, with GF(2) frames compared by reduced basis.", - "class": "TRUE-unencoded", + "class": "COVERED", "finding": "All 660 public columns end at the declared endpoint in both orientations: forward Y_i += X_i, backward X_i -= Y_i, all other columns returned to their own input label with an empty word. All 76 owned private arrays end at zero. The paid transport profile equals {1:2424,2:418,3:429,4:141,5:42,8:8}. In the forward orientation all 44 borrowed sources return to their input. In the backward orientation 43 do, and register 73 ends as the declared shear column X_73 - Y_185.", "independence_note": "The replay was written for this audit after reading PR2260's row-interpreter semantics (PROOF-LOCAL.md:27-46, local/check_trace.py). No PR2260 code is imported or executed, but the event semantics model is PR2260's. It is a third replay of the same model, not a different model.", - "residual_inheritance": "The lambda-fold tensor lift (PROOF-LOCAL.md:102-107) and native Clifford lowering (PROOF-LOCAL.md:70-100) are not rechecked." + "residual_inheritance": "The lambda-fold tensor lift (PROOF-LOCAL.md:102-107) and native Clifford lowering (PROOF-LOCAL.md:70-100) are not rechecked.", + "class_note": "#2265 verify.py reruns PR2260's local/verify.py (both restoration replays) (#2265 verify.py:43, :68-69); re-confirmed here by independent code." }, { "id": "A3-whole-call-hosting", @@ -70,8 +77,8 @@ "consumed_by_outer": "No #2265 ledger row. PR1673 requires only a fixed supplier-dependent constant in O(g) (INDEPENDENT-SUBSTITUTION-REVIEW.md:73-78) under the C_1 = 1 semantic-guard hypothesis (phase_fusion_note.tex:63).", "check_here": "verify.py check_constants", "class": "INHERITED-traced", - "finding": "The arithmetic holds: 244 = 63 + 144 + 37, the inequality 207 + 37*lambda <= 244*lambda is equivalent to lambda >= 1 (tight at 1), and 244 < 512. The retained fixed-bit rule of direct-delivery504 (local + 37 + calls + bridges + 4) gives 248 < 512. The value 63 is PR2260's P_binary_upper and is taken from its precision receipts, not recomputed.", - "open_unit_question": "In the selected lineage the prefix allowance is a fixed 512-bit count, compared with a lambda-free prefix: docs/research/community-batch952-review.md:51-56, scripts/verify_frontier1094.py:94, research/direct-delivery504-global/code/invoice_final.py:238-241. PR2260 instead declares payload 512 a per-lambda coefficient, with guard 244*lambda. Under the fixed-bit reading, 244*lambda < 512 holds only for lambda <= 2. Under the per-lambda reading, PR2260's row formula 2*stock_bits + 9909 + 252 + 2*payload still counts 2*payload = 1024 as a fixed term; if it scaled, row < 20161 would hold only for lambda <= 4. Neither PR2260 nor #2265 defines lambda or says how the row allowance scales with it. This is an open interface question, not a counterexample. For #2265 the PR1673 outer only needs an O(g) supplier guard constant (review:73-78), so it bears more on PR2260's own balanced-prefix outer, whose degree gap uses 20161." + "finding": "The arithmetic holds: 244 = 63 + 144 + 37, the literal prefix 207 + 37*lambda <= 244*lambda is equivalent to lambda >= 1 (tight at 1), and 244 < 512. The retained fixed-bit rule of direct-delivery504 (local + 37 + calls + bridges + 4) gives 248 < 512. Both self-consistent readings therefore pass: fixed-bit 248 < 512 and per-lambda 244*lambda < 512*lambda. The value 63 is PR2260's P_binary_upper and is taken from its precision receipts, not recomputed.", + "open_unit_question": "Lineage-wide unit question, not a PR2260 guard gap. In the selected lineage the prefix allowance is a fixed 512-bit count compared with a lambda-free prefix (docs/research/community-batch952-review.md:51-56, scripts/verify_frontier1094.py:94-96, research/direct-delivery504-global/code/invoice_final.py:238-241). PR2260 states 'Payload512 is a per-lambda magnitude coefficient, not a fixed bit count' (finite-invoice.json precision_units) with no located retained-lineage source for that convention; this is the only PR2260-specific point. Mixed readings only: against a fixed 512, PR2260's literal prefix 207 + 37*lambda fits for lambda <= 8 (its relaxed bound 244*lambda for lambda <= 2); if the row term 2*payload scaled with lambda, row < 20161 would need lambda <= 4. The same mixed readings bind the selected #1094 equally or more tightly: its row 16469 would need lambda <= 4, and its 397-bit prefix with the 37 conversion scaled would need lambda <= 4. The outer consumes 20161 as a fixed degree gap (PR2260 PROOF.md:104-105). For #2265 the PR1673 outer needs only an O(g) supplier guard constant (review:73-78)." }, { "id": "B2-C0", @@ -79,11 +86,12 @@ "statement": "PR2260's fresh constant satisfies C_0 < 2^210000.", "stated_in_2265": "README.md:36, :41", "stated_in_2260": "PROOF.md:38-39, :45-49; PROOF-LOCAL.md:137-150; finite-invoice.json", - "consumed_by_outer": "No #2265 ledger row. It changes a constant only (README.md:36; phase_fusion_note.tex:443).", + "consumed_by_outer": "No #2265 ledger row; covered by the PR2260 check that #2265 reruns. It changes a constant only (README.md:36; phase_fusion_note.tex:443).", "check_here": "verify.py check_constants", - "class": "TRUE-unencoded", + "class": "COVERED", "finding": "Recomputed with the retained formula: required_C0_bits = bit_length(32*73*(|O(73,2)|*73*7168 + 2^100000)^2) = 200012 < 210000, and the tape bound 2*total+18 < 2^210000.", - "residual_inheritance": "The retained formula and the active-depth recurrence (PROOF.md:45-49) are inherited conventions." + "residual_inheritance": "The retained formula and the active-depth recurrence (PROOF.md:45-49) are inherited conventions.", + "class_note": "#2265 verify.py reruns PR2260's local/invoice.py and requires equality with finite-invoice.json (#2265 verify.py:43, :68-69); re-confirmed here by independent code." }, { "id": "B3-row-coefficient", @@ -91,11 +99,12 @@ "statement": "PR2260's new row coefficient satisfies 16467 < 20161.", "stated_in_2265": "README.md:36", "stated_in_2260": "PROOF.md:40; PROOF-LOCAL.md:198; finite-invoice.json finite", - "consumed_by_outer": "No #2265 ledger row. It changes a constant only.", + "consumed_by_outer": "No #2265 ledger row; covered by the PR2260 check that #2265 reruns. It changes a constant only.", "check_here": "verify.py check_constants", - "class": "TRUE-unencoded", + "class": "COVERED", "finding": "Recomputed: physical families 7168 + 492 + 75 + 8 + 2 = 7745, where 75 is the trace's zero-buffer count; stock bits 2641; row = 2*2641 + 9909 + 252 + 1024 = 16467. The value is identical to direct-delivery504's (PREFIX-AND-INVOICE.json) together with physical_stock_bits 2641 and required_C0_bits 200012. This is explained, not copied: both stocks have the same bit length because 7682 and 7745 both lie in [2^12, 2^13), and the C0 field is dominated by 2^100000.", - "group_order_check": "The formula 2^(k^2) prod_{j=1..k} (2^(2j)-1) for |O(2k+1,2)| matches brute force for n = 3 and 5." + "group_order_check": "The formula 2^(k^2) prod_{j=1..k} (2^(2j)-1) for |O(2k+1,2)| matches brute force for n = 3 and 5.", + "class_note": "#2265 verify.py reruns PR2260's local/invoice.py and requires equality with finite-invoice.json (#2265 verify.py:43, :68-69); re-confirmed here by independent code." }, { "id": "C1-bit-endpoint", @@ -177,26 +186,26 @@ { "id": "D5-surcharge", "group": "D", - "statement": "The conservative moment uses PR2260's retained bad-residue surcharge 32*m*sum(H)/(10^16*W)*m^b.", + "statement": "The endpoint C is admissible for the PR2260 cover: either the retained bad-residue surcharge 32*m*sum(H)/(10^16*W)*m^b is an adequate bound for that cover, or the PR559 native-complex license (surcharge omitted) applies to it.", "stated_in_2265": "certify_endpoint.py:5-6, :23; ENDPOINT.json surcharge_weight", - "stated_in_2260": "arithmetic/vendor/moment.py:61-65 (vendored from base research/frame-domain-ceiling/engines/moment.py)", + "stated_in_2260": "arithmetic/vendor/moment.py:61-65, vendored verbatim from base research/frame-domain-ceiling/engines/moment.py:62", "consumed_by_outer": "certify_endpoint.py conservative moment", "check_here": "verify.py check_endpoint", "class": "INHERITED-traced", - "finding": "The weight is 32*73*255500/(10^16*7168) = 5329/640000000000000, and the arithmetic is true. The vendored engine's own comment calls this envelope 'only conditionally portable to the new cover'. Its portability to the PR2260 cover is therefore an inherited condition, and neither PR proves it." + "finding": "The weight is 32*73*255500/(10^16*7168) = 5329/640000000000000, and the arithmetic is true. The surcharge only lowers C, and #2265 also certifies the native moment below one at C (1 - 8.39e-12), so C is valid under either disjunct: the envelope is adequate for the PR2260 cover, or the PR559 native-complex license applies to it (the selected lineage uses that license; cf. research/audit-frontier890-endpoint-seed73/AUDIT.md F3-F5). The comment 'only conditionally portable to the new cover' sits in the base-tree frame-domain-ceiling engine and refers to that package's cover, not to PR2260's. Neither PR proves either disjunct for the PR2260 cover; it is inherited." } ], "summary": { "FALSE": 0, "MISSING-PROOF": 0, - "COVERED": 6, - "TRUE-unencoded": 4, + "COVERED": 9, + "TRUE-unencoded": 1, "INHERITED-traced": 5, "new_observations": [ - "One of the 44 borrowed sources is the public data input X_73, not a helper. It is restored in the forward orientation and ends as the declared shear column in the backward orientation.", - "If payload were per-lambda, the row formula would need lambda <= 4 (unit question).", + "One of the 44 borrowed sources is the public data input X_73 (removed alias 653), not a helper. It is restored in the forward orientation and ends as the declared shear column in the backward orientation. The pair originates in PR2226's WITNESS and is within PR2260's stated model (PROOF-LOCAL.md:22); precision note on helper-specific prose only.", + "Guard units: both self-consistent readings pass (fixed 248 < 512; per-lambda 244*lambda < 512*lambda). Mixed readings give lambda thresholds 8 (literal prefix), 2 (relaxed 244*lambda) and 4 (scaled row) for PR2260, and 4 and 4 for the selected #1094, so this is a lineage-wide question. PR2260's per-lambda payload convention has no located retained source.", "The row/C0/stock-bit fields identical to direct-delivery504 are explained by equal stock bit length.", - "The surcharge envelope is flagged 'only conditionally portable' in the vendored engine." + "Endpoint admissibility is a disjunction: surcharge envelope adequate for the PR2260 cover, or the PR559 native-complex license applies; neither is proved for this cover." ] } } diff --git a/research/pr2265-supplier-admission-audit/README.md b/research/pr2265-supplier-admission-audit/README.md index e36918f577..5c0091bd16 100644 --- a/research/pr2265-supplier-admission-audit/README.md +++ b/research/pr2265-supplier-admission-audit/README.md @@ -31,9 +31,13 @@ class each: | Class | Count | Premises | |---|---:|---| -| COVERED (checked by #2265 or a PR2260 check it reruns; independently re-confirmed here) | 6 | A3 hosting 72x436, C1 bit endpoint, D1 73²>2·48², D2 W/mass/deficit, D3 q2·48², D2 W/mass/deficit, D3 q ) Run from the repository root: python3 -B research/pr2265-supplier-admission-audit/verify.py Prepared by thakrarsagar with substantial AI assistance from Claude (Anthropic, @@ -58,6 +59,7 @@ 'research/e8-bit-p111-tuned/tune/EXPECTED.json': 'b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4', 'research/direct-delivery504-global/evidence/audit/PREFIX-AND-INVOICE.json': 'ce1bfa49be88ae67a404f606a11db2232b7e1f2610d4418058e39749d86d8478', + 'scripts/verify_frontier1094.py': 'c7e20f59968ed5736fb859735de4de207de3418083e37012310ebcded946b949', } @@ -82,6 +84,10 @@ def present(): if not present(): subprocess.run(['git', '-C', str(ROOT), 'fetch', '--no-tags', '--quiet', 'origin', 'refs/pull/2260/head', 'refs/pull/2265/head'], capture_output=True) + if not present(): + # Fallback if a PR head has moved: GitHub serves PR-network commits by SHA. + subprocess.run(['git', '-C', str(ROOT), 'fetch', '--no-tags', '--quiet', 'origin', C2260, C2265], + capture_output=True) if not present(): raise SystemExit('pinned PR heads unavailable; run `git fetch origin pull/2260/head pull/2265/head`') @@ -99,11 +105,11 @@ def blob(commit, path): return data -def local_file(path): +def local_file(path, raw=False): data = (ROOT / path).read_bytes() if sha(data) != LOCAL_PINS[path]: raise SystemExit(f'pin mismatch for {path}') - return json.loads(data) + return data.decode() if raw else json.loads(data) def text_pin(text, phrase): @@ -370,7 +376,7 @@ def row_guard(stock_bits, payload_bits): return row -def check_constants(invoice, trace, old, payload=512): +def check_constants(invoice, trace, old, lineage1094, payload=512): need(orthogonal_count(3) == group_order(3) == 6 and orthogonal_count(5) == group_order(5) == 720, '|O(n,2)| formula on brute-forced small cases') m = 73 @@ -409,14 +415,26 @@ def check_constants(invoice, trace, old, payload=512): need(ideal + blocks + conv == coeff, 'guard identity at lambda = 1') retained_fixed = ideal + conv + 72 + 72 + 4 # direct-delivery504 code/invoice_final.py fixed-bit prefix rule need(retained_fixed < payload, 'retained fixed-bit prefix rule also holds at lambda = 1') - # Unit question: if the row term 2*payload scaled with lambda, the row guard would hold only up to lam_max. + # Unit question (lineage-wide, not a PR2260 gap). Both self-consistent readings pass at the + # supplier: fixed rule 248 < 512, per-lambda rule 244*lambda < 512*lambda. The thresholds below + # only matter for mixed readings, and they bind the selected #1094 equally or more tightly. lam_max = max(k for k in range(1, 64) if not rejected(lambda: row_guard(stock.bit_length(), payload * k))) - # Fixed-bit reading of the retained allowance (selected lineage: 512 bits, e.g. verify_frontier1094.py:94): - # the per-lambda guard coeff*lambda fits a fixed 512-bit payload only up to lam_fixed. - lam_fixed = max(k for k in range(1, 64) if coeff * k < payload) + lam_fixed = max(k for k in range(1, 64) if coeff * k < payload) # relaxed bound 244*lambda + lam_literal = max(k for k in range(1, 64) if ideal + blocks + conv * k < payload) # literal 207 + 37*lambda + need((lam_max, lam_fixed, lam_literal) == (4, 2, 8), 'PR2260 mixed-reading lambda thresholds 4, 2, 8') + # Selected #1094 (scripts/verify_frontier1094.py:94-96): prefix 397 (fixed 37 conversion), charged 512, row 16469. + for phrase in ("final['prefix_bits'] == 397", "final['charged_prefix_bits'] == 512", + "final['physical_row_coefficient'] == 16469"): + need(phrase in lineage1094, ('#1094 constant', phrase)) + lam_1094_row = max(k for k in range(1, 64) if 16469 - 2 * payload + 2 * payload * k < 20161) + lam_1094_prefix = max(k for k in range(1, 64) if 397 - conv + conv * k < payload) + need((lam_1094_row, lam_1094_prefix) == (4, 4), '#1094 mixed-reading lambda thresholds 4, 4') return dict(guard_lambda_max_if_payload_fixed_bits=lam_fixed,physical=physical, group_bits=group.bit_length(), stock_bits=stock.bit_length(), row=row, required_C0_bits=c0_bits, literal_bits=literal.bit_length(), guard_coefficient=coeff, - retained_fixed_bit_prefix=retained_fixed, row_lambda_max_if_payload_scaled=lam_max) + retained_fixed_bit_prefix=retained_fixed, row_lambda_max_if_payload_scaled=lam_max, + guard_lambda_max_literal_prefix_fixed_bits=lam_literal, + selected1094_row_lambda_max_if_payload_scaled=lam_1094_row, + selected1094_prefix_lambda_max_if_conversion_scaled=lam_1094_prefix) # ---------------------------------------------------------------- moments (decimal, bounded error) @@ -547,6 +565,7 @@ def J(commit, path): spec, endpoint, ledger = J(C2265, 'SPEC.json'), J(C2265, 'ENDPOINT.json'), J(C2265, 'outer/LEDGER.json') bit_main = local_file('research/e8-bit-p111-tuned/tune/EXPECTED.json') old = local_file('research/direct-delivery504-global/evidence/audit/PREFIX-AND-INVOICE.json') + lineage1094 = local_file('scripts/verify_frontier1094.py', raw=True) texts = {k: v.decode() for k, v in inp.items() if k[1].endswith(('.md', '.tex'))} out = dict(status=None, pr2260=C2260, pr2265=C2265) @@ -563,7 +582,7 @@ def J(commit, path): need((hosting['original_rank_mass'], hosting['hosted'], hosting['residual_mass']) == (387072, 254088, 132984), 'factor partition 387072 = 254088 hosted + 132984 residual (PR2260 PROOF.md)') out['A_owner_hosting'] = hosting - out['B_constants'] = check_constants(invoice, fwd, old) + out['B_constants'] = check_constants(invoice, fwd, old, lineage1094) out['C_bit'] = check_bit(spec, bit2260, bit_main) out['D_endpoint'] = check_endpoint(spec, endpoint, ledger, hosting['profile']) out['trace'] = check_trace(texts) @@ -622,9 +641,15 @@ def halving_child_rank_52(): e['profile'] = p check_endpoint(s, e, ledger, p) - def row_payload_scaled_beyond_lambda_max(): - lam = out['B_constants']['row_lambda_max_if_payload_scaled'] + 1 - row_guard(out['B_constants']['stock_bits'], 512 * lam) + def invoice_guard_coefficient_245(): + inv = copy.deepcopy(invoice) + inv['global_precision_guard_coefficient'] = 245 + check_constants(inv, fwd, old, lineage1094) + + def invoice_row_coefficient_16466(): + inv = copy.deepcopy(invoice) + inv['finite']['physical_row_coefficient'] = 16466 + check_constants(inv, fwd, old, lineage1094) def endpoint_plus_one_grid_step(): e = copy.deepcopy(endpoint) @@ -653,6 +678,12 @@ def replay_drops_one_monomial_warp(): del t['events'][i] replay_restoration(t) + def backward_replay_inverts_one_dual_monomial_symbol(): + t = copy.deepcopy(bwd) + i = next(i for i, e in enumerate(t['events']) if e[0] == 'dual_monomial') + t['events'][i][2] = -t['events'][i][2] + replay_restoration(t) + def replay_doubles_one_add_coefficient(): t = copy.deepcopy(fwd) i = next(i for i, e in enumerate(t['events']) if e[0] == 'add' and str(e[1]) in t['helper_widths']) @@ -660,9 +691,11 @@ def replay_doubles_one_add_coefficient(): replay_restoration(t) controls = {} - for fn in (replay_drops_one_monomial_warp, replay_doubles_one_add_coefficient, alias_source_is_removed_alias, alias_source_outside_call, event_reads_removed_alias, + for fn in (replay_drops_one_monomial_warp, replay_doubles_one_add_coefficient, + backward_replay_inverts_one_dual_monomial_symbol, alias_source_is_removed_alias, + alias_source_outside_call, event_reads_removed_alias, owner_block_overlap, owner_on_active_data_family, halving_child_rank_52, - row_payload_scaled_beyond_lambda_max, endpoint_plus_one_grid_step, kappa_plus_1e_240, + invoice_guard_coefficient_245, invoice_row_coefficient_16466, endpoint_plus_one_grid_step, kappa_plus_1e_240, bit_endpoint_equal_to_b, bit_endpoint_plus_1e_18): controls[fn.__name__] = rejected(fn) out['negative_controls'] = controls From 00de1b48c3155846ee340993eeb9e9d7daf157af Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Thu, 15 Oct 2026 23:24:26 +0530 Subject: [PATCH 6/6] Narrow A1 TRUE-unencoded label and refresh stale TASK.json Independent re-audit: PR2260's local/check_trace.py (run by local/verify.py) and owners/verify.py, both rerun by #2265 (verify.py:43-44), already enforce event closure and the owner-row facts. Limit A1's TRUE-unencoded label to the namespace/metadata sub-facts (warps = WITNESS pairs, active = namespace minus removed aliases, owned arrays outside the namespace, handoffs exactly on the borrowed sources) and move the owner-row facts to A3. Align the INVENTORY class definition with the README. Update TASK.json evidence (15 of 15, 9/1/5) and replace its pre-review open questions with the README's. Move the orphaned MISSING-PROOF/FALSE row into the Result table and correct the provenance of the D5 engine comment (PR361 / e8-r740 lineage, predates PR2260). Counts, verify.py and EXPECTED.json are unchanged. Co-Authored-By: Claude Opus 5.5 --- .../INVENTORY.json | 15 +++++---- .../pr2265-supplier-admission-audit/README.md | 31 ++++++++++++++----- .../pr2265-supplier-admission-audit/TASK.json | 24 +++++++------- 3 files changed, 45 insertions(+), 25 deletions(-) diff --git a/research/pr2265-supplier-admission-audit/INVENTORY.json b/research/pr2265-supplier-admission-audit/INVENTORY.json index 13c2be619a..e8bfe0a698 100644 --- a/research/pr2265-supplier-admission-audit/INVENTORY.json +++ b/research/pr2265-supplier-admission-audit/INVENTORY.json @@ -13,7 +13,7 @@ }, "classes": { "COVERED": "the premise is consumed and checked by #2265's own ledger/assertions or by a PR2260 check that #2265 reruns", - "TRUE-unencoded": "true on the shipped data under an exact independent check here, but not a row of #2265's ledger", + "TRUE-unencoded": "true on the shipped data under an exact independent check here, but not checked by #2265's own ledger/assertions or by a PR2260 check that #2265 reruns", "INHERITED-traced": "the statement is located in PR2260/PR1673 sources; it is an interface premise with no finite data check possible at this level, or one not rechecked here", "MISSING-PROOF": "used, but no supporting statement or check located", "FALSE": "contradicted by the shipped data" @@ -27,9 +27,11 @@ "stated_in_2265": "README.md:42 (marked inherited, not re-derived); README.md:35", "stated_in_2260": "PROOF.md:21-31; PROOF-OWNERS.md:84-89; PROOF-LOCAL.md:19-25", "consumed_by_outer": "theorem hypothesis only: vendor/pr1673/capped-phase-fusion/phase_fusion_note.tex:63 and :443; INDEPENDENT-SUBSTITUTION-REVIEW.md:51-58, :80-81. No ledger row.", - "check_here": "verify.py check_alias_closure + check_owner_hosting", + "check_here": "verify.py check_alias_closure (the owner-row facts formerly listed here are under A3)", "class": "TRUE-unencoded", - "finding": "Both orientations of the local word touch only the 660 public arrays of the call (224 data, 436 helpers) and the 76 owned private arrays. No event references a removed alias or any register outside the call. The 44 borrowed sources are 43 helper inputs plus one public data input: register 73, an X-side source for removed alias 653. Handoffs occur exactly at the 44 borrowed sources, and each has paid rank 0. Every one of the 31392 owner rows lies in an inherited pending child of the same hosted parent. Within each child the rows form disjoint exact prefixes, and no row uses an active data family of its own call. The data-input borrow (removed alias 653 <- source 73) originates in PR2226's 80-alias WITNESS (head dacaf3d8, research/anticipatory-dirty-borrowing/WITNESS.json) and is carried into PR2260. PR2260 PROOF-LOCAL.md:22 already treats all 660 public/data/helper inputs as arbitrary, so this is covered by PR2260's stated model; only helper-specific wording elsewhere is imprecise. It is a precision note, not a gap.", + "class_scope": "The TRUE-unencoded label applies only to four namespace/metadata sub-facts: (i) the trace's 44 warps equal the 44 pairs of PR2260 local/inputs/WITNESS.json (a selected 44-alias subset of PR2226's 80-alias witness) as (removed alias, borrowed source, handoff basis); (ii) active_registers equals the original 704-register call namespace minus the 44 removed aliases; (iii) the 76 owned private arrays lie outside that namespace, so none is a removed alias; (iv) the 44 borrowed sources named in the warps are public arrays of the call, and the handoff events occur exactly once on each of them. No check that #2265 reruns binds these: PR2260 local/check_trace.py takes active_registers as given, and its unmodified run() accepts, for example, the forward trace with COPY register 1364 renamed to removed alias 597 (probe in the 2026-10-15 re-audit; the shipped trace is hash-pinned, so this concerns what the replay checks, not the shipped data).", + "covered_part": "Event closure is already enforced by a PR2260 check that #2265 reruns. PR2260 local/check_trace.py keeps state only for active_registers (:22-24) and for the arrays its own COPY/zero_buffer events create (:78-94), so an event on any other register raises and fails local/verify.py; local/verify.py:91-92 requires exactly 76 such private arrays, all cleared by the postlude, and expected-local.json pins independent_input_columns 660 and private_fields 76 in both orientations. Handoffs are dimension-preserving (paid rank 0) by check_trace.py:75. #2265 reruns local/verify.py with check=True (#2265 verify.py:43). In the 2026-10-15 re-audit the unmodified check_trace.run rejected an ADD reading removed alias 597 or register 2000, an ADD writing 597, and a handoff on 597. The owner-row facts are checked by PR2260 owners/verify.py, rerun at #2265 verify.py:44; they are listed under A3.", + "finding": "Re-confirmed by independent code: both orientations of the local word (21065 forward and 21381 backward events) touch only the 660 public arrays of the call (224 data, 436 helpers) and the 76 owned private arrays; PR2260's replay already enforces this (covered_part). Checked only here (class_scope): the 44 warps equal the WITNESS pairs; the public arrays are exactly the original 704-register namespace minus the 44 removed aliases; the 76 owned private arrays lie outside that namespace, so no event references a removed alias; the 44 borrowed sources are public arrays of the call and the handoffs occur exactly once on each of them, with paid rank 0 in the WITNESS and warp metadata. The 44 borrowed sources are 43 helper inputs plus one public data input: register 73, an X-side source for removed alias 653. The data-input borrow (removed alias 653 <- source 73) originates in PR2226's 80-alias WITNESS (head dacaf3d8, research/anticipatory-dirty-borrowing/WITNESS.json) and is carried into PR2260. PR2260 PROOF-LOCAL.md:22 already treats all 660 public/data/helper inputs as arbitrary, so this is covered by PR2260's stated model; only helper-specific wording elsewhere is imprecise. It is a precision note, not a gap.", "residual_inheritance": "The all-size realization of this finite closure (lambda-fold lift, physical tape and route) is inherited from PR2260 PROOF.md:49-52." }, { @@ -55,7 +57,8 @@ "consumed_by_outer": "phase_fusion_note.tex:63 (whole-call row hosting hypothesis); SPEC.json geometry", "check_here": "verify.py check_owner_hosting", "class": "COVERED", - "finding": "Confirmed independently. The original pending children are reconstructed as the hosted parent's pooled blocks plus its idle residuals: 16128 children with rank mass 387072. The 436-helper owners host 254088. The residual 132984 has histogram {1:1724,3:20,5:1469,6:18,7:494,32:11,39:7,48:2493}, which equals PR2260 owners/EXPECTED.json and the factor partition quoted at PROOF.md:26-28." + "finding": "Confirmed independently. The original pending children are reconstructed as the hosted parent's pooled blocks plus its idle residuals: 16128 children with rank mass 387072. The 436-helper owners host 254088. The residual 132984 has histogram {1:1724,3:20,5:1469,6:18,7:494,32:11,39:7,48:2493}, which equals PR2260 owners/EXPECTED.json and the factor partition quoted at PROOF.md:26-28. Every one of the 31392 owner rows lies in an inherited pending child of the same hosted parent; within each child the rows form disjoint exact prefixes, and no row uses an active data family of its own call (listed under A1 before the 2026-10-15 correction).", + "class_note": "#2265 verify.py:44 reruns PR2260's owners/verify.py, which checks the owner rows: one row per (call, helper) (:78-82, :100-101), no row on its call's active source/target data families (:87), each block inside the pending child's axes (:88-89), disjoint physical blocks (:95), exact occupied prefixes (:106), and mass 520704 / deficit 2560 (:113). Re-confirmed here by independent code." }, { "id": "A4-serialization-windows", @@ -188,11 +191,11 @@ "group": "D", "statement": "The endpoint C is admissible for the PR2260 cover: either the retained bad-residue surcharge 32*m*sum(H)/(10^16*W)*m^b is an adequate bound for that cover, or the PR559 native-complex license (surcharge omitted) applies to it.", "stated_in_2265": "certify_endpoint.py:5-6, :23; ENDPOINT.json surcharge_weight", - "stated_in_2260": "arithmetic/vendor/moment.py:61-65, vendored verbatim from base research/frame-domain-ceiling/engines/moment.py:62", + "stated_in_2260": "arithmetic/vendor/moment.py:61-65, vendored verbatim from base research/frame-domain-ceiling/engines/moment.py:62 (itself a byte-identical copy of the older PR361 / e8-r740-lineage engine)", "consumed_by_outer": "certify_endpoint.py conservative moment", "check_here": "verify.py check_endpoint", "class": "INHERITED-traced", - "finding": "The weight is 32*73*255500/(10^16*7168) = 5329/640000000000000, and the arithmetic is true. The surcharge only lowers C, and #2265 also certifies the native moment below one at C (1 - 8.39e-12), so C is valid under either disjunct: the envelope is adequate for the PR2260 cover, or the PR559 native-complex license applies to it (the selected lineage uses that license; cf. research/audit-frontier890-endpoint-seed73/AUDIT.md F3-F5). The comment 'only conditionally portable to the new cover' sits in the base-tree frame-domain-ceiling engine and refers to that package's cover, not to PR2260's. Neither PR proves either disjunct for the PR2260 cover; it is inherited." + "finding": "The weight is 32*73*255500/(10^16*7168) = 5329/640000000000000, and the arithmetic is true. The surcharge only lowers C, and #2265 also certifies the native moment below one at C (1 - 8.39e-12), so C is valid under either disjunct: the envelope is adequate for the PR2260 cover, or the PR559 native-complex license applies to it (the selected lineage uses that license; cf. research/audit-frontier890-endpoint-seed73/AUDIT.md F3-F5). The comment 'only conditionally portable to the new cover' is inherited verbatim from the long-vendored PR361 / e8-r740-lineage engine (byte-identical copies, sha256 81cbc864..., include research/direct-delivery504-global/inputs/data-base/work/pr361/code/engines/moment.py and research/e8-bit-carrier-skeleton/code/hub/e8-r740-replica32/code/engines/moment.py), which PR2260 vendored via frame-domain-ceiling. It predates PR2260, so it does not refer to PR2260's cover. Neither PR proves either disjunct for the PR2260 cover; it is inherited." } ], "summary": { diff --git a/research/pr2265-supplier-admission-audit/README.md b/research/pr2265-supplier-admission-audit/README.md index 5c0091bd16..bc4f8496cf 100644 --- a/research/pr2265-supplier-admission-audit/README.md +++ b/research/pr2265-supplier-admission-audit/README.md @@ -31,20 +31,34 @@ class each: | Class | Count | Premises | |---|---:|---| -| COVERED (checked by #2265 or a PR2260 check it reruns; independently re-confirmed here) | 9 | A2 restoration replay, A3 hosting 72x436, B2 C_0<2^210000, B3 row 16467<20161, C1 bit endpoint, D1 73²>2·48², D2 W/mass/deficit, D3 q2·48², D2 W/mass/deficit, D3 q PASS_PR2265_SUPPLIER_ADMISSION_AUDIT controls_rejected 13 of 13; INVENTORY.json: 15 premises, 6 COVERED, 4 TRUE-unencoded, 5 INHERITED-traced, 0 MISSING-PROOF, 0 FALSE.", + "evidence": "python3 -B research/pr2265-supplier-admission-audit/verify.py -> PASS_PR2265_SUPPLIER_ADMISSION_AUDIT controls_rejected 15 of 15; INVENTORY.json: 15 premises, 9 COVERED, 1 TRUE-unencoded (A1, namespace/metadata sub-facts only; its event closure and the owner-row facts are covered by PR2260 checks that #2265 reruns), 5 INHERITED-traced, 0 MISSING-PROOF, 0 FALSE.", "author": "thakrarsagar", "ai_assistance": "Prepared by thakrarsagar with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5) via Claude Code.", "open_questions": [ { - "question": "Is the retained row allowance 20161 per-lambda or absolute, given PR2260's per-lambda 512 payload?", - "why_it_matters": "In the selected lineage the 512 prefix allowance is a fixed bit count; PR2260's 244*lambda guard fits it only for lambda<=2, while under PR2260's per-lambda reading its row formula (2*payload fixed) holds only for lambda<=4.", - "first_step": "Locate the retained definitions of lambda and of the row coefficient in the selected lineage (direct-delivery504 / PR523 invoice notes) and restate PR2260's row in matching units.", - "blocked_by": "The definition of lambda in the all-size compiler is spread over historical notes." + "question": "Where does the retained lineage define whether the 512-bit payload and the 20161 row allowance scale with lambda? PR2260 asserts a per-lambda payload without a located source.", + "why_it_matters": "Both self-consistent readings pass (fixed-bit 248 < 512; per-lambda 244*lambda < 512*lambda). Mixed readings give lambda <= 4 thresholds for PR2260 and for the selected #1094 alike (lambda <= 8 or <= 2 for PR2260's literal or relaxed prefix against a fixed 512), so this is a lineage-wide question, not a PR2260 gap.", + "first_step": "Locate the all-size compiler's definition of lambda and of the row coefficient (direct-delivery504 / PR523 invoice notes), then restate both rows in matching units.", + "blocked_by": "The definition of lambda is spread over historical notes." }, { - "question": "Does the bad-residue surcharge envelope 32*m*sum(H)/(10^16*W)*m^b port to the PR2260 cover?", - "why_it_matters": "#2265's endpoint is certified against the conservative moment; the vendored engine itself labels the envelope only conditionally portable.", - "first_step": "Find the derivation of the envelope behind research/frame-domain-ceiling/engines/moment.py and list its cover-specific hypotheses.", - "blocked_by": "The derivation may exist only in older PR discussions." + "question": "Does either disjunct hold for the PR2260 cover: the bad-residue envelope 32*m*sum(H)/(10^16*W) is adequate, or the PR559 native-complex license applies?", + "why_it_matters": "#2265 certifies C under both the native and the conservative moment, and the surcharge only lowers C, so one of the two disjuncts is needed. The engine comment 'only conditionally portable to the new cover' predates PR2260 and does not refer to its cover.", + "first_step": "List the cover-specific hypotheses of the PR559 exact-cover argument (research/complex-multicold/vendor/pr559/PROOF.md) and of the envelope derivation, and test them against PR2260's cover.", + "blocked_by": "The envelope derivation may only be in older PR discussions." }, { - "question": "Should PR2260's prose record that one alias (removed 653) borrows the public data input X_73 rather than a helper?", - "why_it_matters": "The outer's interface text speaks of dirty helper/spectator coordinates; the data borrow is restored/sheared exactly but the prose should match the data.", - "first_step": "Propose a one-line note in PR2260 PROOF-LOCAL.", + "question": "Should the helper-specific prose in PR2226/PR2260 say that one alias (653, from PR2226's witness) borrows the public X_73 input?", + "why_it_matters": "PR2260's model (PROOF-LOCAL.md:22) already covers it and data borrowing is invisible at the call boundary, but helper-only wording elsewhere does not match the data.", + "first_step": "A one-line note next to the helper-borrowing sentences.", "blocked_by": "None." } ]