diff --git a/research/three-base-paid-census/README.md b/research/three-base-paid-census/README.md new file mode 100644 index 0000000000..2fd9ccd73d --- /dev/null +++ b/research/three-base-paid-census/README.md @@ -0,0 +1,162 @@ +# THREE-base supplier: independent paid-event census + +**Finite accounting audit; no new kappa.** The supplier-census question left by +[Ryanson Jonathan's #4426](https://github.com/CrocSwap/integer-mult-bounds/pull/4426) +is answered for its pinned THREE-base word. Separate standard-library code +recovers the unsplit paid histogram + +```text +{1:2487, 2:713, 3:224, 4:102, 5:20, 8:8} +``` + +in both orientations: **3,554 paid calls, rank mass 5,157**. The 408 nested +helper frame increments give `{5:28, 6:18, 7:56, 8:93, 9:213}`, rank mass +**3,301**. These agree exactly with the supplier receipt used by #4426. + +This closes its finite census handoff, not the supplier's operator or physical +correctness obligations. Evidence is an author-executed, separately implemented +check; no independent human or proof-assistant review is claimed. + +## What is reconstructed + +The native input actually contains the **split** centers, with 22,633 events +and paid profile `{1:2487, 2:713, 3:232, 4:102, 5:28}` in each direction. +Its 16 center events form eight consecutive pairs. Their frame dimensions are +`8 -> 3 -> 0` forward and `0 -> 3 -> 8` backward. Coalescing each pair recovers +the unsplit program's 22,625 events without changing any scalar or warp event. + +The resulting paid census, identical in the two orientations, is: + +| Phase | Rank 1 | Rank 2 | Rank 3 | Rank 4 | Rank 5 | Rank 8 | Calls | Rank mass | +| --- | ---: | ---: | ---: | ---: | ---: | ---: | ---: | ---: | +| A | 950 | 12 | 20 | 38 | 0 | 0 | 1,020 | 1,186 | +| Centers | 0 | 0 | 0 | 0 | 0 | 8 | 8 | 64 | +| B | 1,161 | 571 | 150 | 64 | 20 | 0 | 1,966 | 3,109 | +| Cleanup tail | 72 | 53 | 0 | 0 | 0 | 0 | 125 | 178 | +| Final | 304 | 77 | 54 | 0 | 0 | 0 | 435 | 620 | +| **Total** | **2,487** | **713** | **224** | **102** | **20** | **8** | **3,554** | **5,157** | + +For the 15 native invocations inherited from Cinna Davis's #4416, the supplier +part alone is `{1:37305, 2:10695, 3:3360, 4:1530, 5:300, 8:120}`, rank mass +77,355. Controller idles are additional. This multiplication by 15 is arithmetic; +#4426 retains credit for reconstructing the controller, its targets and idles. + +## Method and proof boundary + +1. Authenticate exactly three inputs against [SOURCES.json](SOURCES.json), then + require the supplier receipt's artifact hashes to name those actual native + and canonical bytes. They are already retained on the pinned main branch; + no unpublished Git object or network fetch is needed for this package. +2. Independently eliminate all 1,159 nine-bit frame bases over F2. Every basis + must be independent. For each paid transition, compute containment by the + rank of the concatenated bases and derive the rank difference. The event's + declared rank is only a comparison target, never the rank calculation. +3. Trace frames on 632 persistent fields and the owned C0 field. Check paid + entrances, warp entrances, scalar operands, final persistent frames, and + the final explicit center clear. `adapter`, `residual_adapter` and `phase` + are markers in the inherited event format; the paid moves they annotate + appear explicitly as `climb` or `center` events. Scalar and warp costs are + outside this recursive-child histogram. +4. Verify both literal split programs and coalesce their adjacent center + pairs. Under the inherited common-frame convention, if + `T(a,b) = F_b F_a^-1`, then + `T(b,c) T(a,b) = F_c F_b^-1 F_b F_a^-1 = T(a,c)`. + Complex conjugation preserves this identity. The shared middle reference, + immediate adjacency, dimensions and nesting are checked; a scalar inserted + between the two pieces is rejected. This is telescoping of frame symbols, + not a fresh check of serialized Clifford phases or a regeneration of the + original unsplit word from its ancestor. +5. For each helper `L224` through `L631`, independently verify the nested + entry/exit spaces and count their dimension difference. C0 receives no + productive credit. Compare the full distributions, not only rank masses, + to the receipt. Recheck frames and counts on the coalesced programs too. + +The verifier imports no repository module and executes no predecessor +interpreter. The source interpreter was read to identify the native format +and tariff. The elimination algorithm, census, center reconstruction, controls +and receipt are separately written. The selected construction already had +native replays; this package supplies additional independent accounting +coverage requested by #4426, not a first proof of the supplier. + +## Verification + +From the repository root, Python 3.12, standard library only: + +```sh +python -B scripts/research_package.py --package research/three-base-paid-census --check-only +python -B scripts/research_package.py --package research/three-base-paid-census +python -O -B research/three-base-paid-census/verify.py +``` + +The direct verifier recomputes and compares [RESULT.json](RESULT.json). +`--write` regenerates only that package-local result. All assertions use explicit +exceptions and remain active under `-O`. + +There are **16 rejecting controls**: source corruption, artifact misbinding, +wrong paid rank, a deleted climb, a same-dimension nonnested edge, stale warp +entrance, wrong scalar frame, borrowed-field clearing, missing/interrupted +center pairs, a dependent basis, wrong final frame, unknown event, two +rank-mass-preserving paid-profile changes, and a helper-distribution change +preserving both count and rank mass. All 512 ordered triples in F2^3 additionally +cross-check elimination against enumerated spans, including dependent triples. + +An explicit **coverage probe** changes an ADD sign in memory and obtains the +same census. It demonstrates why these checks cannot certify the operator +identity. Actual input-file changes are separately rejected by SHA256 binding. + +## Sources, overlap and limitations + +Base: canonical main `2a13eb1827784206202db90e5dc8327cf8a250db`, priority revision +7, selected conditional kappa `23/10000`. Exact input blobs and SHA256 values +are in [SOURCES.json](SOURCES.json); scope and freshness are in [TASK.json](TASK.json). +Coordination: [discussion #4445](https://github.com/CrocSwap/integer-mult-bounds/discussions/4445), +with a pointer replying to the [handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19103994). + +The overlap refresh covered all 5,731 tracked local package notes/ledger entries, +301 open PR bodies and 3,290 Discussion records, with complete pagination at +21:05/21:06 UTC on October 21. It surfaced #4426's explicit missing census and +no separate competing census. Closed work was covered through local notes and +the ledger, not a fresh scan of every closed PR body; code diffs are outside +the helper's search. A submission refresh at 21:16/21:17 UTC covered 303 open +PRs and 3,294 Discussion records, with complete pagination and no warnings or +new competing census. Canonical main, guidance and the inputs were unchanged. +The older `t360-local-rewrite-census` searches rewrites of prior words, rather +than reconstructing this full-identity receipt. This is not proof of novelty. +#4441's changed helper word is a different input; this frozen audit does not +certify its invoice. + +Not rerun: arbitrary-input operator equality, exact Clifford phases, scalar +primitive pricing/prefix norms, helper physical normalization, the p7 controller, +121-axis admission, tensor/strictification arguments, compiler, precision/stock, +fixed-tape and outer/analytic obligations. The source baseline command was +attempted but could not complete with omitted source-closure directories in +this sparse checkout (`Invalid package root: research/kappa-accounted-composition`). +It is not reported as passing. The targeted inputs are all materialized and +authenticated. The complete `frontier4359-verify` replay was not run. + +## Open next questions + +No further census question is justified for these exact bytes: both orientations +and the full distributions match, with the stated rejection controls. The +physical/operator, phase and downstream boundaries listed above remain inherited +in this audit. Their absence here does not mean the repository lacks evidence +for them. Consult the selected proof review and live handoffs before proposing +any additional independent check; a changed native word needs its own census. + +## Credit + +- **Ryanson (Ryan) Jonathan / pinterbanget**, #4426 at + `6f918e2658c727007611d98ffb8d3c7336e2290c`, for the independent p7 controller + invoice reconstruction and this explicit handoff; #4420 for the arithmetic audit. +- **Cinna Davis / 1337isnot1337**, #4416 at + `e9058860b5c850760fdf970e796a96aefcdb1d98`, for the p7 construction and invoice. +- **zxv**, #4359's retained source closure at + `da637c87c89482bc4c86be36bd0071b3d400dbed`, for the full-identity supplier, + center split and productive-helper construction. Jacob Alan Sussman supplies + the mixed-target recursion; David Ganz, Rohan Arun, Cinna Davis, Jeremy Kothe, + Marius-Paul Dumitrean, Erwan Secousses and the retained native/frame contributors + are credited in the [checkpoint contributor map](../../docs/research/community-productive4359-contributors.md). + +Prepared for **mihir-s-05** with substantial **OpenAI Codex** assistance in +research, implementation, verification and writing. Apache-2.0. Frozen sources +and their attribution are unchanged. diff --git a/research/three-base-paid-census/RESULT.json b/research/three-base-paid-census/RESULT.json new file mode 100644 index 0000000000..e4114d00e7 --- /dev/null +++ b/research/three-base-paid-census/RESULT.json @@ -0,0 +1,582 @@ +{ + "claim": "Finite native-event accounting and nested helper widths; no new kappa.", + "controls": { + "rank_cross_check_ordered_triples": 512, + "rejected": { + "borrowed_clear": "borrowed field overwritten", + "corrupted_source_bytes": "source hash: research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz", + "deleted_climb": "chronological frame mismatch", + "dependent_basis": "dependent frame basis", + "equal_dimension_nonnested_edge": "non-nested paid edge", + "interrupted_center_pair": "adjacent center chain", + "mass_and_count_preserving_helper_drift": "helper inventory", + "mass_preserving_canonical_drift": "canonical split profile", + "mass_preserving_receipt_drift": "receipt paid profile", + "missing_center_piece": "chronological frame mismatch", + "stale_warp_entrance": "chronological frame mismatch", + "unknown_event": "unknown native event: unpaid_jump", + "wrong_artifact": "receipt artifact binding", + "wrong_declared_rank": "declared paid rank", + "wrong_final_frame": "final persistent frames", + "wrong_scalar_frame": "chronological frame mismatch" + }, + "scope_probe": "An in-memory ADD sign flip preserves this census; no operator identity is certified." + }, + "result": { + "fifteen_call_scaling": { + "helper_widths": { + "5": 420, + "6": 270, + "7": 840, + "8": 1395, + "9": 3195 + }, + "paid_profile": { + "1": 37305, + "2": 10695, + "3": 3360, + "4": 1530, + "5": 300, + "8": 120 + }, + "paid_rank_mass": 77355, + "scope": "Arithmetic scaling by #4416's inherited 15 calls; controller not replayed." + }, + "frame_count": 1159, + "helper_count": 408, + "helper_rank_mass": 3301, + "helper_widths": { + "5": 28, + "6": 18, + "7": 56, + "8": 93, + "9": 213 + }, + "orientations": { + "backward": { + "center_pairs": [ + { + "coalesced_rank": 8, + "event_indices": [ + 11794, + 11795 + ], + "frames": [ + 0, + 1155, + 254 + ], + "piece_ranks": [ + 3, + 5 + ] + }, + { + "coalesced_rank": 8, + "event_indices": [ + 11821, + 11822 + ], + "frames": [ + 0, + 1155, + 274 + ], + "piece_ranks": [ + 3, + 5 + ] + }, + { + "coalesced_rank": 8, + "event_indices": [ + 11848, + 11849 + ], + "frames": [ + 0, + 1155, + 619 + ], + "piece_ranks": [ + 3, + 5 + ] + }, + { + "coalesced_rank": 8, + "event_indices": [ + 11875, + 11876 + ], + "frames": [ + 0, + 1155, + 279 + ], + "piece_ranks": [ + 3, + 5 + ] + }, + { + "coalesced_rank": 8, + "event_indices": [ + 11902, + 11903 + ], + "frames": [ + 0, + 1156, + 621 + ], + "piece_ranks": [ + 3, + 5 + ] + }, + { + "coalesced_rank": 8, + "event_indices": [ + 11929, + 11930 + ], + "frames": [ + 0, + 1157, + 280 + ], + "piece_ranks": [ + 3, + 5 + ] + }, + { + "coalesced_rank": 8, + "event_indices": [ + 11956, + 11957 + ], + "frames": [ + 0, + 1157, + 624 + ], + "piece_ranks": [ + 3, + 5 + ] + }, + { + "coalesced_rank": 8, + "event_indices": [ + 11983, + 11984 + ], + "frames": [ + 0, + 1158, + 281 + ], + "piece_ranks": [ + 3, + 5 + ] + } + ], + "split": { + "checked_scalar_operands": 33710, + "event_counts": { + "adapter": 978, + "center": 16, + "climb": 3546, + "phase": 10, + "residual_adapter": 390, + "scalar": 17453, + "warp": 240 + }, + "events": 22633, + "final_frames_match": true, + "paid_by_kind": { + "center": { + "3": 8, + "5": 8 + }, + "climb": { + "1": 2487, + "2": 713, + "3": 224, + "4": 102, + "5": 20 + } + }, + "paid_by_phase": { + "A": { + "1": 950, + "2": 12, + "3": 20, + "4": 38 + }, + "B": { + "1": 1161, + "2": 571, + "3": 150, + "4": 64, + "5": 20 + }, + "centers": { + "3": 8, + "5": 8 + }, + "cleanup_tail": { + "1": 72, + "2": 53 + }, + "final": { + "1": 304, + "2": 77, + "3": 54 + } + }, + "paid_calls": 3562, + "paid_profile": { + "1": 2487, + "2": 713, + "3": 232, + "4": 102, + "5": 28 + }, + "paid_rank_mass": 5157 + }, + "unsplit": { + "checked_scalar_operands": 33710, + "event_counts": { + "adapter": 978, + "center": 8, + "climb": 3546, + "phase": 10, + "residual_adapter": 390, + "scalar": 17453, + "warp": 240 + }, + "events": 22625, + "final_frames_match": true, + "paid_by_kind": { + "center": { + "8": 8 + }, + "climb": { + "1": 2487, + "2": 713, + "3": 224, + "4": 102, + "5": 20 + } + }, + "paid_by_phase": { + "A": { + "1": 950, + "2": 12, + "3": 20, + "4": 38 + }, + "B": { + "1": 1161, + "2": 571, + "3": 150, + "4": 64, + "5": 20 + }, + "centers": { + "8": 8 + }, + "cleanup_tail": { + "1": 72, + "2": 53 + }, + "final": { + "1": 304, + "2": 77, + "3": 54 + } + }, + "paid_calls": 3554, + "paid_profile": { + "1": 2487, + "2": 713, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "paid_rank_mass": 5157 + } + }, + "forward": { + "center_pairs": [ + { + "coalesced_rank": 8, + "event_indices": [ + 11773, + 11774 + ], + "frames": [ + 254, + 1155, + 0 + ], + "piece_ranks": [ + 5, + 3 + ] + }, + { + "coalesced_rank": 8, + "event_indices": [ + 11800, + 11801 + ], + "frames": [ + 274, + 1155, + 0 + ], + "piece_ranks": [ + 5, + 3 + ] + }, + { + "coalesced_rank": 8, + "event_indices": [ + 11827, + 11828 + ], + "frames": [ + 619, + 1155, + 0 + ], + "piece_ranks": [ + 5, + 3 + ] + }, + { + "coalesced_rank": 8, + "event_indices": [ + 11854, + 11855 + ], + "frames": [ + 279, + 1155, + 0 + ], + "piece_ranks": [ + 5, + 3 + ] + }, + { + "coalesced_rank": 8, + "event_indices": [ + 11881, + 11882 + ], + "frames": [ + 621, + 1156, + 0 + ], + "piece_ranks": [ + 5, + 3 + ] + }, + { + "coalesced_rank": 8, + "event_indices": [ + 11908, + 11909 + ], + "frames": [ + 280, + 1157, + 0 + ], + "piece_ranks": [ + 5, + 3 + ] + }, + { + "coalesced_rank": 8, + "event_indices": [ + 11935, + 11936 + ], + "frames": [ + 624, + 1157, + 0 + ], + "piece_ranks": [ + 5, + 3 + ] + }, + { + "coalesced_rank": 8, + "event_indices": [ + 11962, + 11963 + ], + "frames": [ + 281, + 1158, + 0 + ], + "piece_ranks": [ + 5, + 3 + ] + } + ], + "split": { + "checked_scalar_operands": 33710, + "event_counts": { + "adapter": 978, + "center": 16, + "climb": 3546, + "phase": 10, + "residual_adapter": 390, + "scalar": 17453, + "warp": 240 + }, + "events": 22633, + "final_frames_match": true, + "paid_by_kind": { + "center": { + "3": 8, + "5": 8 + }, + "climb": { + "1": 2487, + "2": 713, + "3": 224, + "4": 102, + "5": 20 + } + }, + "paid_by_phase": { + "A": { + "1": 950, + "2": 12, + "3": 20, + "4": 38 + }, + "B": { + "1": 1161, + "2": 571, + "3": 150, + "4": 64, + "5": 20 + }, + "centers": { + "3": 8, + "5": 8 + }, + "cleanup_tail": { + "1": 72, + "2": 53 + }, + "final": { + "1": 304, + "2": 77, + "3": 54 + } + }, + "paid_calls": 3562, + "paid_profile": { + "1": 2487, + "2": 713, + "3": 232, + "4": 102, + "5": 28 + }, + "paid_rank_mass": 5157 + }, + "unsplit": { + "checked_scalar_operands": 33710, + "event_counts": { + "adapter": 978, + "center": 8, + "climb": 3546, + "phase": 10, + "residual_adapter": 390, + "scalar": 17453, + "warp": 240 + }, + "events": 22625, + "final_frames_match": true, + "paid_by_kind": { + "center": { + "8": 8 + }, + "climb": { + "1": 2487, + "2": 713, + "3": 224, + "4": 102, + "5": 20 + } + }, + "paid_by_phase": { + "A": { + "1": 950, + "2": 12, + "3": 20, + "4": 38 + }, + "B": { + "1": 1161, + "2": 571, + "3": 150, + "4": 64, + "5": 20 + }, + "centers": { + "8": 8 + }, + "cleanup_tail": { + "1": 72, + "2": 53 + }, + "final": { + "1": 304, + "2": 77, + "3": 54 + } + }, + "paid_calls": 3554, + "paid_profile": { + "1": 2487, + "2": 713, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "paid_rank_mass": 5157 + } + } + } + }, + "source_sha256": { + "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-CANONICAL.json.gz": "6418ec3da24d548a57f5c3fe5b9062c26c9478e638504a61c387f5cfb5f4ed61", + "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz": "c54b0a3e129d28e6dbf74fa731fc3bb70fe3c6705f07256750fbecddcc842d39", + "research/pr4416-invoice-rebuild/vendor/SUPPLIER-RESULT.json": "943d5fad2fc529f470df05a35446e07ecaef7344abfce450d2c2eb2c9b3798f6" + }, + "status": "PASS_THREE_BASE_PAID_CENSUS" +} diff --git a/research/three-base-paid-census/SOURCES.json b/research/three-base-paid-census/SOURCES.json new file mode 100644 index 0000000000..ac43594017 --- /dev/null +++ b/research/three-base-paid-census/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "2a13eb1827784206202db90e5dc8327cf8a250db", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40", + "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-CANONICAL.json.gz", + "usage": "input", + "git_blob": "4a8c4ed26e53a72362d571c972e65aff546be784", + "sha256": "6418ec3da24d548a57f5c3fe5b9062c26c9478e638504a61c387f5cfb5f4ed61" + }, + { + "path": "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz", + "usage": "input", + "git_blob": "b46d44c6ee624968dd57be928b0c15d9d45f3b2c", + "sha256": "c54b0a3e129d28e6dbf74fa731fc3bb70fe3c6705f07256750fbecddcc842d39" + }, + { + "path": "research/pr4416-invoice-rebuild/vendor/SUPPLIER-RESULT.json", + "usage": "input", + "git_blob": "c6edcbdc43bf36bb11201235027d0ec170d07fc8", + "sha256": "943d5fad2fc529f470df05a35446e07ecaef7344abfce450d2c2eb2c9b3798f6" + } + ] +} diff --git a/research/three-base-paid-census/TASK.json b/research/three-base-paid-census/TASK.json new file mode 100644 index 0000000000..5486623b40 --- /dev/null +++ b/research/three-base-paid-census/TASK.json @@ -0,0 +1,170 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 7, + "base_commit": "2a13eb1827784206202db90e5dc8327cf8a250db", + "original_card": { + "id": "independent-moment", + "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/staged544-mixed-fourth-entry/README.md", + "research/staged-fourth-mixture-ceiling/README.md", + "research/r437-two-window-carrier/README.md" + ], + "methods": [ + "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.", + "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Calling an aggregate histogram or source archive an independently accepted physical supplier." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering", + "4088", + "4091", + "4067", + "staged544-mixed-fourth-entry", + "staged-fourth-mixture-ceiling", + "r437-two-window-carrier" + ], + "existing_checks": [ + { + "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.", + "evidence": "research/staged-fourth-mixture-ceiling/README.md", + "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.", + "status": "author-checked", + "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.", + "evidence": "research/r437-two-window-carrier/README.md", + "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.", + "status": "author-checked", + "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Close #4426's finite supplier-census handoff: independently derive the THREE-base paid rank histogram and nested helper frame increments from its literal native events in both orientations, including reconstruction of the unsplit centers.", + "scope_change_reason": "Handoff-first selection: #4426 already rebuilds the p7 controller but explicitly inherits the supplier receipt. Current selected #4359 and the later #4416 lineage make the exact native bill the useful missing accounting check; no new moment digits or supplier admission are proposed.", + "bottleneck_link": "The supplier contributes 15*2487 rank-one calls to #4416. #4420 reports a much smaller margin than a one-call accounting error. This audit checks the inherited bill itself.", + "budget_minutes": 60, + "stop_rule": "Stop after reconstructing the fixed supplier distributions in both orientations with source binding and rejection controls, or reporting an exact discrepancy. No search, whole-supplier adoption or changed frontier.", + "outcome": "completed", + "evidence": "RESULT.json and verify.py: 22,633 native events per orientation; 3,562 split paid calls, 3,554 coalesced paid calls, rank mass 5,157; 408 helpers, rank mass 3,301. All receipt distributions match. Sixteen rejecting controls, 512 small-space rank checks, and an explicit accounting-only sign-flip probe.", + "author": "mihir-s-05, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in source reading, independent checker implementation, verification and writing. No subagents; no independent human or proof-kernel review claimed.", + "open_questions": [], + "coordination_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4445", + "predecessors": [ + { + "pr": 4426, + "author": "Ryanson (Ryan) Jonathan / pinterbanget", + "head": "6f918e2658c727007611d98ffb8d3c7336e2290c", + "scope": "Controller invoice reconstruction and supplier-census handoff." + }, + { + "pr": 4416, + "author": "Cinna Davis / 1337isnot1337", + "head": "e9058860b5c850760fdf970e796a96aefcdb1d98", + "scope": "p7 construction and invoice; supplier receipt is retained by #4426." + }, + { + "pr": 4359, + "author": "zxv", + "head": "da637c87c89482bc4c86be36bd0071b3d400dbed", + "scope": "Selected source closure, full-identity native supplier and center split." + } + ], + "overlap": { + "initial_upstream_commit": "2a13eb1827784206202db90e5dc8327cf8a250db", + "priority_revision": 7, + "local_notes": 5731, + "local_complete_head_inventory": true, + "open_prs": { + "fetched_at": "2026-10-21T21:05:34.201272+00:00", + "records": 301, + "complete_pagination": true + }, + "discussions": { + "fetched_at": "2026-10-21T21:06:50.573062+00:00", + "records": 3290, + "complete_pagination": true + }, + "nearest_overlap": "#4426 explicitly leaves this supplier census open; #4420/#4428 check arithmetic; #4441 changes the helper word, outside these frozen inputs. No distinct competing census found. No novelty guarantee.", + "limitations": "Closed PRs covered by local notes and ledger only; no code-diff search.", + "submission_refresh": { + "searched_at": "2026-10-21T21:17:33.920532+00:00", + "coverage": { + "local": { + "head": "2a13eb1827784206202db90e5dc8327cf8a250db", + "records": 5733, + "head_records": 5731, + "complete_head_inventory": true, + "unsearched_head_paths": [] + }, + "open_prs": { + "fetched_at": "2026-10-21T21:16:20.946893+00:00", + "complete_pagination": true, + "records": 303 + }, + "discussions": { + "fetched_at": "2026-10-21T21:17:33.644805+00:00", + "complete_pagination": true, + "records": 3294 + } + }, + "warnings": [], + "upstream_commit": "2a13eb1827784206202db90e5dc8327cf8a250db", + "upstream_checked_at": "2026-10-21T21:15:26Z", + "guidance_and_inputs_changed": false, + "relevant_matches": "#4426 and our #4445 claim; t360-local-rewrite-census searches prior word rewrites rather than reconstructing this full-identity receipt. No new competing census found." + } + }, + "orientation_limitations": [ + "research_baseline.py attempted but failed at omitted sparse source-closure root research/kappa-accounted-composition; not a passing baseline.", + "No complete selected cold replay, physical/operator/phase audit, or new kappa acceptance." + ], + "no_open_questions_reason": "The exact finite supplier census requested by #4426 is complete and matches. This audit leaves physical/operator, phase and downstream evidence inherited, not newly absent from the repository. No additional fixed-word census or speculative follow-up is justified; consult current handoffs before assigning a separate audit.", + "validation": { + "environment": "Windows, CPython 3.12.0, standard library only", + "registered_replay": "passed", + "optimized_python": "passed with all 16 controls active", + "scope": "Local author execution, not hosted CI, independent human review or formal proof." + } +} diff --git a/research/three-base-paid-census/VERIFY.json b/research/three-base-paid-census/VERIFY.json new file mode 100644 index 0000000000..5be1fa3af8 --- /dev/null +++ b/research/three-base-paid-census/VERIFY.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-CANONICAL.json.gz", + "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz", + "research/pr4416-invoice-rebuild/vendor/SUPPLIER-RESULT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact three-input source and receipt binding; both native orientations; F2 frame containment/rank census; adjacent center coalescence; 408 nested helper increments; full receipt distributions; 16 rejecting controls; 512 F2^3 rank checks; accounting-only sign-flip probe; deterministic RESULT.json." + } + ] +} diff --git a/research/three-base-paid-census/verify.py b/research/three-base-paid-census/verify.py new file mode 100644 index 0000000000..c3ba433ff9 --- /dev/null +++ b/research/three-base-paid-census/verify.py @@ -0,0 +1,386 @@ +#!/usr/bin/env python3 +"""Independent finite accounting audit of the THREE-base native certificate. + +No predecessor code is imported. The native event tariff and frame convention +are inherited; operator identities, phases and physical admission are not proved. +Prepared for mihir-s-05 with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +from collections import Counter, defaultdict +from copy import deepcopy +from fractions import Fraction +import gzip +import hashlib +from itertools import product +import json +from pathlib import Path + + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PREFIX = "research/kappa-rebuild/complex/full-identity-certificates/" +CANONICAL = PREFIX + "THREE-base-FULL-IDENTITY-CANONICAL.json.gz" +NATIVE = PREFIX + "THREE-base-FULL-IDENTITY-NATIVE.json.gz" +RECEIPT = "research/pr4416-invoice-rebuild/vendor/SUPPLIER-RESULT.json" +PHASES = ["zero_frame_precondition", "entry_adapters", "A", "centers", "B", + "cleanup_tail", "final", "exit_adapters", "full_frame_cleanup", "done"] + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def rank(vectors): + """Gaussian elimination over F_2, independent of the source's span census.""" + pivots = {} + for value in vectors: + while value: + leading = value.bit_length() - 1 + if leading not in pivots: + pivots[leading] = value + break + value ^= pivots[leading] + return len(pivots) + + +def contained(small, large): + return rank([*large, *small]) == rank(large) + + +def histogram(counter): + return {str(k): v for k, v in sorted(counter.items()) if v} + + +def mass(counter): + return sum(int(k) * v for k, v in counter.items()) + + +def authenticate(data, expected, label): + need(hashlib.sha256(data).hexdigest() == expected, "source hash: " + label) + + +def load_inputs(): + pins = json.loads((HERE / "SOURCES.json").read_bytes()) + inputs = {row["path"]: row for row in pins["files"] if row["usage"] == "input"} + need(set(inputs) == {CANONICAL, NATIVE, RECEIPT}, "exact three-input closure") + decoded, hashes = {}, {} + for name, pin in inputs.items(): + raw = (ROOT / name).read_bytes() + authenticate(raw, pin["sha256"], name) + hashes[name] = pin["sha256"] + decoded[name] = json.loads(gzip.decompress(raw) if name.endswith(".gz") else raw) + return decoded[CANONICAL], decoded[NATIVE], decoded[RECEIPT], hashes + + +def frame_data(canonical): + need((canonical["h"], canonical["v"], canonical["R"]) == (9, 112, 408), + "fixed nine-bit THREE-base domain") + need(not canonical["zero_buffers"], "no external cleanup bank") + frames = canonical["frames"] + dimensions = [] + for vectors in frames: + need(all(type(x) is int and 0 < x < 512 for x in vectors), "frame vector domain") + dimension = rank(vectors) + need(dimension == len(vectors), "dependent frame basis") + dimensions.append(dimension) + need(dimensions[0] == 0 and dimensions[1] == 9, "zero/full frame anchors") + for key in ("start", "final"): + need(len(canonical[key]) == 632, "632 persistent fields") + need(all(type(i) is int and 0 <= i < len(frames) for i in canonical[key]), + "persistent frame index") + return frames, dimensions + + +def census(canonical, program): + frames, dimensions = frame_data(canonical) + current = {("L", i): f for i, f in enumerate(canonical["start"])} + current["C", 0] = None + counts, paid = Counter(), Counter() + by_phase, by_kind = defaultdict(Counter), defaultdict(Counter) + phases, phase = [], None + scalar_operands = 0 + center_cleared = False + + def frame(index): + need(type(index) is int and 0 <= index < len(frames), "event frame index") + return index + + def role(value): + need(isinstance(value, list) and len(value) == 2, "role shape") + result = tuple(value) + need(result in current, "unknown or unowned field") + return result + + def at(field, index): + need(current[field] == frame(index), "chronological frame mismatch") + + for event in program: + need(isinstance(event, list) and event, "event shape") + kind = event[0] + counts[kind] += 1 + if kind == "phase": + need(len(event) == 2 and event[1] in PHASES, "phase marker") + phase = event[1] + phases.append(phase) + elif kind in ("climb", "center"): + if kind == "climb": + need(len(event) == 6 and event[1] in ("A", "B", "cleanup_tail", "final"), "climb shape") + _, _, index, old, new, declared = event + field = role(["L", index]) + else: + need(len(event) == 5, "center shape") + _, index, old, new, declared = event + field = role(["C", index]) + at(field, old) + frame(new) + up = dimensions[old] < dimensions[new] and contained(frames[old], frames[new]) + down = dimensions[new] < dimensions[old] and contained(frames[new], frames[old]) + need(up if kind == "climb" else up or down, "non-nested paid edge") + actual = abs(dimensions[new] - dimensions[old]) + need(type(declared) is int and declared == actual, "declared paid rank") + paid[actual] += 1 + by_phase[phase][actual] += 1 + by_kind[kind][actual] += 1 + current[field] = new + elif kind == "warp": + need(len(event) == 5 and type(event[2]) is int, "warp shape") + field = role(event[1]) + at(field, event[3]) + current[field] = frame(event[4]) + elif kind == "scalar": + need(len(event) == 3 and isinstance(event[1], list), "scalar shape") + op, f = event[1], frame(event[2]) + need(op and op[0] in ("add", "copy", "clear", "scale"), "scalar opcode") + opcode = op[0] + need(len(op) == {"add": 5, "copy": 3, "clear": 2, "scale": 4}[opcode], + "scalar operand count") + target = role(op[1]) + if opcode == "clear": + need(target == ("C", 0), "borrowed field overwritten") + current[target] = f + center_cleared = True + continue + at(target, f) + scalar_operands += 1 + if opcode in ("add", "copy"): + source = role(op[2]) + at(source, f) + scalar_operands += 1 + need(target != source, "self scalar operation") + if opcode == "copy": + need(target == ("C", 0), "borrowed field overwritten") + center_cleared = False + continue + if target == ("C", 0): + center_cleared = False + numerator, denominator = op[-2:] + need(type(numerator) is int and type(denominator) is int and denominator != 0, + "scalar rational encoding") + value = Fraction(numerator, denominator) + need(value and value.denominator & (value.denominator - 1) == 0, "dyadic scalar") + if opcode == "scale": + need(abs(value.numerator) & (abs(value.numerator) - 1) == 0, "unit dyadic scale") + elif kind == "adapter": + need(len(event) == 4 and event[1] in ("old_to_new", "new_to_old"), "adapter marker") + role(["L", event[2]]) + frame(event[3]) + elif kind == "residual_adapter": + need(len(event) in (4, 5) and event[1] in ("pre", "post"), "residual adapter marker") + role(["L", event[2]]) + frame(event[3]) + if len(event) == 5: + frame(event[4]) + else: + raise ValueError("unknown native event: " + str(kind)) + need(phases == PHASES, "complete ordered phase sequence") + need([current["L", i] for i in range(632)] == canonical["final"], "final persistent frames") + need(center_cleared, "final owned-center clear") + return {"events": len(program), "event_counts": dict(sorted(counts.items())), + "paid_profile": histogram(paid), "paid_calls": sum(paid.values()), + "paid_rank_mass": mass(paid), "paid_by_phase": {k: histogram(v) for k, v in by_phase.items()}, + "paid_by_kind": {k: histogram(v) for k, v in sorted(by_kind.items())}, + "checked_scalar_operands": scalar_operands, "final_frames_match": True} + + +def coalesce_centers(canonical, program): + """Cancel the common frame in adjacent U_a^* U_b, U_b^* U_c factors. + + This also applies after complex conjugation. It is an abstract telescoping + argument under the inherited canonical-frame convention, not a phase replay. + """ + frames, dimensions = frame_data(canonical) + output, pairs = [], [] + i = 0 + while i < len(program): + first = program[i] + if first[0] != "center": + output.append(first) + i += 1 + continue + need(i + 1 < len(program), "missing second center piece") + second = program[i + 1] + need(second[0] == "center" and first[1] == second[1] == 0 and first[3] == second[2], + "adjacent center chain") + old, mid, new = first[2], first[3], second[3] + need([dimensions[old], dimensions[mid], dimensions[new]] in ([8, 3, 0], [0, 3, 8]), + "center 8/3/0 chain") + high = old if dimensions[old] == 8 else new + need(contained(frames[mid], frames[high]), "center intermediate containment") + pairs.append({"event_indices": [i, i + 1], "frames": [old, mid, new], + "piece_ranks": [abs(dimensions[old] - dimensions[mid]), + abs(dimensions[mid] - dimensions[new])], "coalesced_rank": 8}) + output.append(["center", 0, old, new, 8]) + i += 2 + need(len(pairs) == 8, "eight center pairs") + high_frames = [p["frames"][0] if dimensions[p["frames"][0]] == 8 else p["frames"][2] for p in pairs] + need(high_frames == canonical["center_frames"], "original ordered center frames") + return output, pairs + + +def audit(canonical, words, receipt, hashes): + provider = receipt["providers"]["THREE-base"] + for name in (CANONICAL, NATIVE): + need(provider["artifacts"][Path(name).name] == hashes[name], "receipt artifact binding") + need(set(words) == {"forward", "backward"}, "both orientations") + frames, dimensions = frame_data(canonical) + helpers = Counter() + for i in range(224, 632): + a, b = canonical["start"][i], canonical["final"][i] + need(dimensions[a] < dimensions[b] and contained(frames[a], frames[b]), "nested helper endpoint") + helpers[dimensions[b] - dimensions[a]] += 1 + boundary = provider["helper_boundary"] + need(histogram(helpers) == boundary["widths"] and sum(helpers.values()) == boundary["count"] + and mass(helpers) == boundary["total_width"], "helper inventory") + directions = {} + for direction, program in words.items(): + split = census(canonical, program) + need(split["paid_profile"] == canonical["local_profile"], "canonical split profile") + unsplit_word, pairs = coalesce_centers(canonical, program) + unsplit = census(canonical, unsplit_word) + for result, expected in ( + (split, provider["split_replays"][direction]["independent_native_replay"]), + (unsplit, provider["unsplit_replays"][direction]), + ): + need(result["paid_profile"] == expected["paid_profile"], "receipt paid profile") + need(result["paid_rank_mass"] == expected["paid_rank_mass"], "receipt rank mass") + need(result["event_counts"] == expected["event_counts"], "receipt event counts") + need(split["paid_rank_mass"] == unsplit["paid_rank_mass"], "coalescence rank mass") + directions[direction] = {"split": split, "unsplit": unsplit, "center_pairs": pairs} + need(directions["forward"]["unsplit"]["paid_profile"] == + directions["backward"]["unsplit"]["paid_profile"], "orientation invoice equality") + p = directions["forward"]["unsplit"]["paid_profile"] + return {"frame_count": len(frames), "helper_count": sum(helpers.values()), + "helper_widths": histogram(helpers), "helper_rank_mass": mass(helpers), + "orientations": directions, + "fifteen_call_scaling": {"paid_profile": {k: 15 * n for k, n in p.items()}, + "paid_rank_mass": 15 * mass(p), + "helper_widths": {k: 15 * n for k, n in histogram(helpers).items()}, + "scope": "Arithmetic scaling by #4416's inherited 15 calls; controller not replayed."}} + + +def controls(canonical, words, receipt, hashes): + rejected = {} + + def reject(name, expected_message, change): + c, w, r = deepcopy(canonical), deepcopy(words), deepcopy(receipt) + change(c, w, r) + try: + audit(c, w, r, hashes) + except ValueError as exc: + need(expected_message in str(exc), name + ": failed at an unintended check: " + str(exc)) + rejected[name] = str(exc) + else: + raise ValueError("control unexpectedly accepted: " + name) + + word = words["forward"] + climb = next(i for i, e in enumerate(word) if e[0] == "climb") + center = next(i for i, e in enumerate(word) if e[0] == "center") + warp = next(i for i, e in enumerate(word) if e[0] == "warp") + scalar = next(i for i, e in enumerate(word) if e[0] == "scalar" and e[1][0] == "add") + reject("wrong_declared_rank", "declared paid rank", + lambda c, w, r: w["forward"][climb].__setitem__(-1, word[climb][-1] + 1)) + reject("deleted_climb", "chronological frame mismatch", lambda c, w, r: w["forward"].pop(climb)) + reject("stale_warp_entrance", "chronological frame mismatch", + lambda c, w, r: w["forward"][warp].__setitem__(3, 1 if word[warp][3] != 1 else 0)) + reject("wrong_scalar_frame", "chronological frame mismatch", + lambda c, w, r: w["forward"][scalar].__setitem__(2, 1 if word[scalar][2] != 1 else 0)) + reject("borrowed_clear", "borrowed field overwritten", + lambda c, w, r: w["forward"][scalar].__setitem__(1, ["clear", ["L", 0]])) + reject("missing_center_piece", "chronological frame mismatch", lambda c, w, r: w["forward"].pop(center)) + reject("interrupted_center_pair", "adjacent center chain", + lambda c, w, r: w["forward"].insert(center + 1, + ["scalar", ["scale", ["C", 0], 2, 1], word[center][3]])) + reject("dependent_basis", "dependent frame basis", lambda c, w, r: c["frames"][1].append(256)) + reject("wrong_final_frame", "final persistent frames", lambda c, w, r: c["final"].__setitem__(0, 0)) + reject("unknown_event", "unknown native event", lambda c, w, r: w["forward"].insert(1, ["unpaid_jump"])) + reject("wrong_artifact", "receipt artifact binding", + lambda c, w, r: r["providers"]["THREE-base"]["artifacts"].__setitem__(Path(NATIVE).name, "0" * 64)) + + def drift(profile): + profile["1"] += 2 + profile["2"] -= 1 # Equal rank mass is deliberately insufficient. + + reject("mass_preserving_canonical_drift", "canonical split profile", lambda c, w, r: drift(c["local_profile"])) + reject("mass_preserving_receipt_drift", "receipt paid profile", + lambda c, w, r: drift(r["providers"]["THREE-base"]["unsplit_replays"]["forward"]["paid_profile"])) + + def helper_drift(c, w, r): + h = r["providers"]["THREE-base"]["helper_boundary"]["widths"] + h["5"] += 1 + h["6"] -= 2 + h["7"] += 1 # Preserves both helper count and total rank mass. + + reject("mass_and_count_preserving_helper_drift", "helper inventory", helper_drift) + frames, dims = frame_data(canonical) + nonnested = next((i, j) for i, e in enumerate(word) if e[0] == "climb" and dims[e[3]] > 0 + for j, f in enumerate(frames) if dims[j] == dims[e[4]] and not contained(frames[e[3]], f)) + reject("equal_dimension_nonnested_edge", "non-nested paid edge", + lambda c, w, r: w["forward"][nonnested[0]].__setitem__(4, nonnested[1])) + + # Independent finite cross-check of the elimination routine, including + # dependent vectors and zeros: all 512 ordered triples in F_2^3. + for vectors in product(range(8), repeat=3): + span = {0} + for vector in vectors: + span |= {x ^ vector for x in span} + need(1 << rank(vectors) == len(span), "small-space rank cross-check") + + raw = (ROOT / NATIVE).read_bytes() + try: + authenticate(raw + b"corruption", hashes[NATIVE], NATIVE) + except ValueError as exc: + rejected["corrupted_source_bytes"] = str(exc) + else: + raise ValueError("source corruption unexpectedly accepted") + + # A scoped census must not be presented as an operator proof. Changing an + # ADD sign keeps frames and prices; the hash guard catches file changes, + # but the accounting layer intentionally cannot detect this algebraic error. + altered = deepcopy(words) + altered["forward"][scalar][1][3] *= -1 + need(audit(canonical, altered, receipt, hashes) == audit(canonical, words, receipt, hashes), + "accounting-only scope probe") + return {"rejected": rejected, "rank_cross_check_ordered_triples": 512, + "scope_probe": "An in-memory ADD sign flip preserves this census; no operator identity is certified."} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", action="store_true", help="write the deterministic RESULT.json after all checks") + args = parser.parse_args() + canonical, words, receipt, hashes = load_inputs() + report = {"status": "PASS_THREE_BASE_PAID_CENSUS", "source_sha256": hashes, + "claim": "Finite native-event accounting and nested helper widths; no new kappa.", + "result": audit(canonical, words, receipt, hashes), + "controls": controls(canonical, words, receipt, hashes)} + target = HERE / "RESULT.json" + if args.write: + target.write_text(json.dumps(report, indent=2, sort_keys=True) + "\n", encoding="utf-8", newline="\n") + else: + need(json.loads(target.read_bytes()) == report, "committed RESULT.json differs from fresh census") + print(report["status"], "orientations=2 controls=" + str(len(report["controls"]["rejected"]))) + + +if __name__ == "__main__": + main()