diff --git a/research/p112-unequal-endpoint-deletion/CHECKS.json b/research/p112-unequal-endpoint-deletion/CHECKS.json new file mode 100644 index 0000000000..33f4f87a6f --- /dev/null +++ b/research/p112-unequal-endpoint-deletion/CHECKS.json @@ -0,0 +1,101 @@ +{ + "schema": "p112-unequal-endpoint-checks/v1", + "environment": { + "os": "Linux-6.6.87.2-microsoft-standard-WSL2-x86_64-with-glibc2.41", + "python": [ + "3.12.15", + "3.13.5" + ], + "dependencies": "standard library only", + "ruff": "0.17.1" + }, + "checks": [ + { + "command": "python3.12 -B scripts/research_package.py --package research/p112-unequal-endpoint-deletion", + "result": "PASS_REGISTERED_RESEARCH_PACKAGE outcome=partial; exact replay and 12 optimized behavioral groups pass" + }, + { + "command": "python3.13 -W error -OO -B research/p112-unequal-endpoint-deletion/verify.py", + "result": "PASS_P112_UNEQUAL_ENDPOINT_DELETION profiles=2 margin=11 errors=0" + }, + { + "command": "python3.13 -W error -OO -B research/p112-unequal-endpoint-deletion/test_verify.py", + "result": "12 tests pass" + }, + { + "command": "same Python 3.13 commands from a read-only source-only export with exactly the four declared inputs", + "result": "both pass; no Git metadata or extra predecessor imports" + }, + { + "command": "ruff check --no-cache --select E4,E7,E9,F,B,C4,ICN,PIE,PGH,RUF,UP,SIM,I research/p112-unequal-endpoint-deletion/*.py", + "result": "all checks pass" + }, + { + "command": "in-memory compile plus AST inspection of all three new Python files", + "result": "26 functions; longest 24 physical lines; no bytecode emitted" + } + ], + "semantic_mutants": [ + { + "mutant": "dimension-loss", + "result": "rejected", + "observed_test": "test_sharp_dimension_loss" + }, + { + "mutant": "small-support-charge", + "result": "rejected", + "observed_test": "test_both_actual_profiles" + }, + { + "mutant": "strict-root-boundary", + "result": "rejected", + "observed_test": "test_strict_support_cutoffs" + }, + { + "mutant": "rank-five-capacity", + "result": "rejected", + "observed_test": "test_both_actual_profiles" + } + ], + "failure_controls": [ + "uniform endpoint charge does not exclude", + "old incidence upper bound does not exclude", + "strict 53/70 cutoffs", + "dimension deletion is not free", + "invalid support/weight/dimension inputs", + "each of four changed input files is rejected", + "wrong expected receipt is rejected", + "relative/in-checkout/overwrite output is rejected" + ], + "scope": { + "geometric_premises": "re-executed retained engine, not independent reimplementation", + "independent_components": "subset-cover oracle, sharp coordinate-subspace dimension examples, rational quotient fixture and elementary endpoint count", + "unrun": [ + "proof-kernel formalization", + "independent human review", + "hosted CI", + "native or complete supplier replay" + ] + }, + "upstream_checkpoint": { + "commit": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "priority_revision": 6, + "relevant_guidance_changed": false, + "overlap_checked_at": "2026-10-17T17:10:54.688803+00:00", + "coverage": { + "open_prs": { + "fetched_at": "2026-10-17T17:10:26.456052+00:00", + "complete_pagination": true, + "records": 245 + }, + "discussions": { + "fetched_at": "2026-10-17T17:10:54.622748+00:00", + "complete_pagination": true, + "records": 1987 + } + }, + "warnings": [], + "exact_profile_hits": "own claim and local package only; not a novelty guarantee" + }, + "publication_checks": "Exact committed export and raw Git-byte preflight are performed after committing; their receipts will be linked in the PR/Discussion." +} diff --git a/research/p112-unequal-endpoint-deletion/ENGINEERING.md b/research/p112-unequal-endpoint-deletion/ENGINEERING.md new file mode 100644 index 0000000000..d14cdd5e79 --- /dev/null +++ b/research/p112-unequal-endpoint-deletion/ENGINEERING.md @@ -0,0 +1,71 @@ +# Bounded implementation and checks + +The kept change is one isolated research package. It calls an unchanged, +SHA256-bound geometry module rather than copying or editing predecessor code. +The real result is the written characteristic-zero implication in PROOF.md; +the finite replay checks its declared premises and arithmetic, not the whole +multiplication theorem. No subagent or independent human review was available. + +## Power-of-ten inspection + +1. All new paths use structured loops, exceptions and context-managed files. + There is no recursion. Input/proof failures propagate as nonzero exits; + output files are closed on success or failure. +2. Weights have length at most ten, support invoices have exactly six + endpoints, and dimensions are at most sixteen. Historical enumeration + checks 7,546 multisets. Prior covers inspect at most 210 index quartets + and 81 assignments per quartet. Endpoint enumeration has `7^6` assignments. + The inherited geometry has fixed dimensions and exactly 4,097,782 flat + iterations. Each registered command has a 120-second bound; the historical + subprocess has a 30-second bound. The test subprocess emits 24 lines. +3. Python allocates managed objects during execution. Direct fixed-memory + compliance is unavailable in this runtime. Live state is bounded by those + input sizes: the geometry keeps small histograms and at most 120 roots, + not a stored list of millions of flats; the historical list has 69 rows. + Each input is limited to two megabytes before reading. The interpreter and + standard-library internals were not allocation-instrumented. +4. AST inspection finds maximum new function lengths of 24, 19 and 15 lines + in ledger.py, test_verify.py and verify.py, respectively. +5. Explicit `require` contracts remain active with `-OO`. They check dimensions, + strict support cutoffs, exact input inventories/hashes, profile inclusion, + arithmetic margins and receipt equality. Tests use unittest checks rather + than removable Python assertions. No density-only assertions were added. +6. Mutable evidence is function-local. The only import-path change is scoped + with `finally` and undone immediately. No shared cache or frontier record + is modified. Test patches are scoped and disposable copies are private. +7. Source reads, exclusive writes and the historical child process either + return checked results or raise. The child is SHA-bound, uses no shell, + has a timeout and checks its exit code, stderr and exact row count. +8. No generated code, decorators or evaluation of input text is introduced. + The one late ordinary module import is necessary to authenticate the + retained source first. The registered runner supplies private bytecode + isolation. Direct execution assumes a trusted interpreter/import cache. +9. Calls are direct and data access is shallow. unittest dispatch and scoped + mock patches are bounded standard-library test mechanisms, not production + plug-ins. The input module name and location are fixed in the driver. +10. The registered interpreter uses `-W error`; tests also use `-OO`. Applicable + Ruff checks cover E4,E7,E9,F,B,C4,ICN,PIE,PGH,RUF,UP,SIM,I. Compilation uses + `compile` in memory and AST function-length inspection, leaving no bytecode. + CHECKS.json records the exact commands. The replay manifest makes behavior + and warning checks recur when the package or a declared input changes. + +Rules 3 and 9 use managed-runtime/framework deviations. Their scope is this +bounded one-shot Python replay and unittest suite; collection bounds, timeout +checks, cross-version execution and disposable-copy cleanup are the compensating +controls. A future port to a fixed-memory runtime must implement fixed-capacity +buffers before claiming direct compliance. No such port is needed for this +mathematical contribution. + +An exploratory Ruff ALL scan also suggested converting unittest to pytest, +adding namespace-package markers and forbidding CLI output/late imports, plus +project-wide annotation/docstring style. Those policies do not apply to this +standard-library standalone verifier. Applicable complexity, import ordering, +tuple construction and comparison findings were resolved. No suppression is +added to source. The applicable check set above passes; a clean ALL result is +not claimed. + +The registered replay, independent subset oracle, failure controls, mutation +checks and source-only export are verification evidence. The geometric engine +is re-executed, not independently reimplemented. Standard Weyl theory and the +original decoder reduction remain written dependencies. No Lean, Docker, +physical implementation, native supplier or full selected replay was run. diff --git a/research/p112-unequal-endpoint-deletion/PROOF.md b/research/p112-unequal-endpoint-deletion/PROOF.md new file mode 100644 index 0000000000..33505b88e7 --- /dev/null +++ b/research/p112-unequal-endpoint-deletion/PROOF.md @@ -0,0 +1,183 @@ +# Two unequal-endpoint P112 exclusions + +## Statement and exact change + +Use the fixed 112 nonframe E8 root lines `r_t`, their nine-bit binary labels +`ell(t)`, and the code + +``` +C = {c_h : c_h(t)=, h in K^8}, +w(q) = rank_F2 {ell(t) : q(t) != 0}. +``` + +The field `K` has characteristic zero. All intersections and independence +below are over `K`; only support weights use binary rank. + +**Nine-piece theorem.** Nine independent pieces with weight bounds either +`3,5,5,5,6,6,6,6,6` or `4,4,5,5,6,6,6,6,6` span a space `T0` with +`dim(T0 intersect C)<=4`. + +**Ten-piece consequence.** Ten independent pieces with code intersection +of dimension at least six cannot have either TWOSIDE profile +`3,5^3,6^5,7` or `4^2,5^2,6^5,7`. The last piece can actually be unrestricted. + +This applies Nick Petalas/PR3169's existing A5 coordinate inequality after +the dimension-deletion step of PR3197. The new callers have six unequal +endpoint capacities `12,20,20,20,20,20`, rather than six twenties. No new +geometric inequality, full C5 result, decoder floor, supplier or exponent +is claimed. + +## Replayed geometric premises and written dependency + +The unchanged, declared `geometry.py` input reconstructs the roots and +labels and binds them to the declared P112 data. It checks the following +finite premises, inherited from PR3164/3169 and PR3161/3162. + +* Weight-three and weight-four supports have at most four and eight + coordinates. The labels are distinct and odd, so a binary `d`-space + contains at most `2^(d-1)` of them. Weight-five and weight-six supports + have capacities twelve and twenty. The replay enumerates all 3,309,747 + five-flats and 788,035 six-flats in the nine-dimensional label space. +* A nonzero codeword has at least 53 live coordinates. A codeword supported + on fewer than seventy coordinates is proportional to a root codeword. +* The Gram sum in doubled root coordinates is `112 I`, so evaluation from + `K^8` into `C` is injective. +* A plane containing three distinct E8 root lines is A2. Relative to the + first two roots, the third has coefficient ratio `+1` or `-1`. + +The support classification uses the standard Weyl-chamber theorem, not a +short-vector enumeration. In a closed chamber, perpendicular roots are +generated by vanishing simple roots. The 28 six-node parabolics have at +most 36 root lines. The eight seven-node faces have counts +`42,28,22,14,16,23,37,63`; only the last admits 43 perpendicular live lines, +and its normal is a root. Root directions have live support 53 or 56. +This proves the distance and the below-seventy classification over the +reals. Reflection closure, simple-root positivity, the face counts and +all 7,140 root-line planes are replayed exactly. + +For an arbitrary characteristic-zero field, the rational roots perpendicular +to a field-valued direction have rational rank at most seven. If their rank +were at most six while there were at least 43 of them, a generic real normal +to their span would contradict the rank-six parabolic bound. Their rational +kernel is therefore one-dimensional. The field-valued direction is a field +scalar times its rational generator, to which the real classification +applies. This includes complex coefficients without a positive-definite +field-valued norm. The standard Weyl-chamber theorem and the original +decoder reduction remain written dependencies, not proof-kernel results. + +## Nine pieces and six root-simplex vertices + +Suppose `dim(T0 intersect C)>=5`. In either weight profile take the first +three pieces as `s1,s2,s3`, and call the other six `q0,...,q5`. Put + +``` +S = supp(s1) union supp(s2) union supp(s3), s=|S|<=28, +U = sum_i |supp(q_i)| <= 12+5*20 = 112, +D0 = T0 intersect C. +``` + +For the first profile, the small-support bound is `4+12+12=28`. For the +second it is `8+8+12=28`. Their endpoint capacities are identical. + +The quotient `T0/D0` has dimension at most four. For every `i`, the four +images of `s1,s2,s3,q_i` are independent: a dependence would give a nonzero +codeword supported on at most `28+20=48<53` coordinates. Nonzero follows +from independence of the original pieces. Consequently the quotient has +exact dimension four, and `dim D0=5`. + +After quotienting by the three small images, all six endpoint images are +nonzero in one dimension. Rescale them to agree. Their supports and +independence do not change. For suitable small-piece combinations `a_i`, + +``` +c0=0, c_i=q_i-q0-a_i in D0, i=1,...,5. +``` + +The five codewords are independent, as witnessed by their distinct nonzero +coefficients on `q1,...,q5`. Every nonzero edge `c_i-c_j` has support at most +`28+20+20=68<70`, and hence is a root direction. Injectivity gives five +independent direction vectors. + +Normalize real E8 roots to squared norm two. Write those vectors as +`h_i=b_i alpha_i`. Every difference is also a root direction, so the A2 +plane fact forces `b_i/b_j` to be `+1` or `-1`. Absorb signs into the roots. +There is one common nonzero scalar `b`, and all distinct +`=1`. Thus the six vertices `0,alpha_1,...,alpha_5` form +an affine root A5 simplex. This argument remains valid over `K`: a rational +root in the field span of two independent rational roots lies in their +rational span, by a nonsingular rational coordinate minor. + +## The inherited coordinate inequality, with the correct endpoint bill + +At any root coordinate the six simplex values lie on at most two adjacent +integer levels, except when that coordinate is an edge root. In the latter +case their equality multiplicities are `1,1,4`. In either case at most nine +of the fifteen pairs have unequal values. The common field scalar changes +no equalities. + +Outside `S`, edge values are exactly `q_i(t)-q_j(t)`. If `k` of the six +endpoint values are nonzero, their number of unequal pairs is at most + +``` +k(6-k) + k(k-1)/2 = k(11-k)/2 <= 4k+1, 0<=k<=6. +``` + +This last inequality follows from `(k-1)(k-2)>=0` for integer `k`. It needs +no restrictions on the nonzero field values. Summing inside and outside +`S`, and using the distance 53 on all fifteen edges, gives PR3169's bound + +``` +795 = 15*53 <= 9s + 4U + (112-s) = 112+8s+4U. +``` + +The present endpoints give + +``` +795 <= 112+8*28+4*112 = 784, +``` + +a contradiction of eleven. This proves both nine-piece statements. The +older `9s+5U` bound gives 812 and is insufficient. Charging six twenties +instead gives 816 even in the coordinate bound. Both losing controls are +retained; neither is an exclusion. The replay also enumerates all `7^6` +assignments of six values with zero distinguished, representing every +possible equality pattern. + +## Delete the unrestricted piece + +Let `T` be the span of ten independent pieces and `T0` the span after +removing the last one. Its codimension is one. Restricting the map +`T intersect C -> T/T0` shows + +``` +dim(T0 intersect C) >= dim(T intersect C)-1 >= 5. +``` + +Either retained profile contradicts the nine-piece theorem. No weight or +support assumption on the removed piece is used. Removing two pieces +would guarantee only four code dimensions, not five. + +## Original residue and prior coverage + +Both targets pass DreamingOfClouds/PR3154's original TWOSIDE `(6,4)` +filters, with excess `35<36`. A direct transcription reproduces all 69 +historical survivors; the unchanged declared `bk2b.py` corroborates the +count. This is not a claim that 69 profiles remain open today. + +All 210 four-piece index subsets and all `3^4` assignments to two six-flat +groups plus paid cuts are checked. For `3,5^3,6^5,7`, support-certified basis +types are `3,5,5,5` and `3,5,5,6`, each needing at least sixteen paid cuts. +For `4^2,5^2,6^5,7`, the basis types are `4,4,5,5`, `4,4,5,6` and +`4,5,5,6`, with minima sixteen, sixteen and twenty. Thus none of the +weight-certified covers reaches the earlier fourteen-cut rule, or the +smaller eight/ten-cut rules. The only nonbasis weight-four anchor occurs +in the twenty-cut case, outside the twelve-cut anchor theorem. +These are comparisons of named sufficient routes, not exclusions of +unknown actual support overlaps or every possible earlier proof. + +The targets are not componentwise consequences of PR3197's +`4^3,6^6,7` caller, nor PR3195's shorter `5^2,6^6,7` caller. The unequal +endpoint bill is essential for this particular application. No full C5, +`C(P112)>=64`, physical realization, supplier admission, multiplication +theorem or new kappa is established. Evidence is author-checked; independent +human review, hosted CI and proof-kernel verification are separate. diff --git a/research/p112-unequal-endpoint-deletion/README.md b/research/p112-unequal-endpoint-deletion/README.md new file mode 100644 index 0000000000..f4d459d00a --- /dev/null +++ b/research/p112-unequal-endpoint-deletion/README.md @@ -0,0 +1,85 @@ +# Two P112 weight-seven profiles close with unequal endpoints + +Nick Petalas. Apache-2.0. + +Ten independent P112 pieces with code-intersection dimension at least six +cannot have either actual TWOSIDE `(b,t)=(6,4)` profile +`3,5^3,6^5,7` or `4^2,5^2,6^5,7`, over any characteristic-zero field. +[PROOF.md](PROOF.md) gives the complete scoped argument. + +Deleting the last piece retains five code dimensions on nine independent +pieces. Three small pieces have support at most 28. The remaining six +endpoints have capacities `12,20,20,20,20,20`, so Nick Petalas/PR3169's +coordinate inequality requires `795<=784`, a contradiction of eleven. +The older incidence bound gives 812; replacing the unequal endpoints by +six twenties gives 816. Neither losing bound proves the exclusion. + +The new result is this unequal-endpoint application and its source-bound +checks, not a new A5 inequality or geometry census. It follows the released +[PR3197 handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/3156#discussioncomment-19001119). +It does not close full C5, prove `C(P112)>=64`, admit a supplier or improve +kappa. The selected frontier stays unchanged. Evidence is author-checked, +not independent human or proof-kernel review; hosted CI is separate. + +## Reproduce + +Python 3.12 or later, standard library only. From the repository root: + +```sh +RUN="$HOME/.cache/integer-mult-bounds-runs/p112-unequal-endpoint-replay" +mkdir -p "$RUN" +TMPDIR="$RUN" python3.12 -B scripts/research_package.py \ + --package research/p112-unequal-endpoint-deletion +``` + +The two bounded commands print `PASS_P112_UNEQUAL_ENDPOINT_DELETION` and +`Ran 12 tests ... OK`. They authenticate all four declared inputs, replay +all 4,097,782 inherited five/six-flats and all root planes, check 117,649 +endpoint equality assignments, reproduce historical inclusion, and audit +every weight-certified four-piece quotient basis. A separate subset oracle +checks the two-flat cover minima; twelve behavioral groups include four +input mutations and strict/losing controls. [RESULT.json](RESULT.json) is +the expected mathematical receipt; [CHECKS.json](CHECKS.json) records checks. + +No output is generated in the checkout. Direct replay is +`python3.12 -B research/p112-unequal-endpoint-deletion/verify.py` followed by +`test_verify.py` there. An optional `--output NEW_ABSOLUTE_EXTERNAL_PATH` +creates an exclusive external receipt. Git-free exports need this package +and exactly the four inputs listed in [VERIFY.json](VERIFY.json), preserving +their relative paths. The registered runner additionally validates Git +provenance and isolates bytecode caches. Direct execution assumes a trusted +Python runtime and import cache. [ENGINEERING.md](ENGINEERING.md) records +implementation bounds and verification limits. + +## Sources and limits + +Base main is `463113d675af7410ac91d53a4fed51ec6494eb9a`, priority revision 6. +[TASK.json](TASK.json) records the changed scope from formalization to the +live C5 handoff, success/stop test and remaining obligations. +[SOURCES.json](SOURCES.json) binds all live inputs at that base and records +exact predecessor heads. No frozen package is changed or copied. + +DreamingOfClouds/PR3154 supplied the TWOSIDE filters and original reduction. +Nick Petalas/PR3169 supplied the coordinate inequality, with PR3164 and +PR3161/3162's retained root geometry. PR3197 supplied the dimension-deletion +application for a different ten-piece profile; PR3195 supplied the adjacent, +shorter deletion caller. The retained E8/P112 decoder lineage, including +joaqcoo's model, remains credited in the declared predecessor proof and +sources. Development and local checks used substantial automated assistance. + +Both new profiles have excess `35<36` and occur among the 69 historical +`(6,4)` survivors. That number is not a current unresolved count. Their best +weight-only two-six-flat covers need sixteen paid cuts, beyond the earlier +fourteen-cut rule. Actual support overlaps and other profiles are not ruled +out by that comparison. The proof inherits the standard Weyl-chamber theorem +and original decoder reduction; no native, physical or full supplier replay +was run. + +## Open next questions + +Before another census, bind one actual still-open profile to its surviving +code dimension, support caps and current exclusions. First refresh +Discussion3156 and apply the existing deletion and cover rules. The blocker +is a missing current disposition, not another seed. This package does not +justify expanding a construction family. The structured question is in +[TASK.json](TASK.json). diff --git a/research/p112-unequal-endpoint-deletion/RESULT.json b/research/p112-unequal-endpoint-deletion/RESULT.json new file mode 100644 index 0000000000..263d17d56a --- /dev/null +++ b/research/p112-unequal-endpoint-deletion/RESULT.json @@ -0,0 +1,334 @@ +{ + "schema": "p112-unequal-endpoint-deletion/v1", + "input_sha256": { + "research/one-sided-six-multisets/data/data.txt": "ac4a48851b922f2a433684b60c74768ae3bb4fc5e8990ffe63e3942bb3c2ea34", + "research/p112-weight-seven-deletion/geometry.py": "b8ac379e41f5ad83bdb6c7f7c55129fc3d9c07801ea61591478f25d72ff0b021", + "research/p112-weight-seven-deletion/vendor/COORDINATE-PROOF.md": "21cd2f726865241c65641fb3e966c5ab3ae51694e47169d491b077ca73f547a2", + "research/p112-weight-seven-deletion/vendor/bk2b.py": "dff16eff255c883db372a587cf3f34e6f35c08f75c60af9d11952be5a5838807" + }, + "geometry": { + "chamber": { + "simple_reflection_checks": 960, + "rank_six_parabolic_counts": [ + 21, + 21, + 12, + 12, + 15, + 21, + 30, + 16, + 13, + 12, + 13, + 16, + 21, + 12, + 10, + 10, + 12, + 16, + 10, + 8, + 8, + 10, + 13, + 12, + 13, + 21, + 21, + 36 + ], + "ray_zero_counts": [ + 42, + 28, + 22, + 14, + 16, + 23, + 37, + 63 + ], + "root_support_histogram": { + "53": 112, + "56": 8 + } + }, + "root_planes": { + "2": 3780, + "3": 3360 + }, + "flat_capacities": [ + { + "dimension": 5, + "subspaces": 3309747, + "maximum": 12, + "histogram": { + "0": 99593, + "2": 6720, + "3": 71680, + "4": 300076, + "5": 258048, + "6": 729344, + "7": 442368, + "8": 826770, + "9": 200704, + "10": 287168, + "11": 43008, + "12": 44268 + } + }, + { + "dimension": 6, + "subspaces": 788035, + "maximum": 20, + "histogram": { + "0": 10796, + "4": 56, + "6": 896, + "7": 4096, + "8": 8148, + "10": 56448, + "11": 86016, + "12": 124040, + "14": 131712, + "15": 143360, + "16": 141491, + "18": 33152, + "19": 28672, + "20": 19152 + } + } + ] + }, + "endpoints": { + "equality_assignments": 117649, + "nonzero_histogram": { + "0": 1, + "1": 36, + "2": 540, + "3": 4320, + "4": 19440, + "5": 46656, + "6": 46656 + }, + "uniform_endpoint_control": { + "small_support_cap": 28, + "endpoint_caps": [ + 20, + 20, + 20, + 20, + 20, + 20 + ], + "endpoint_sum_cap": 120, + "quotient_support_cap": 48, + "edge_support_cap": 68, + "edge_incidence_lower": 795, + "coordinate_incidence_upper": 816, + "old_incidence_upper": 852, + "margin": -21, + "excluded": false + } + }, + "historical_inventory": { + "cell": [ + 6, + 4 + ], + "multisets_examined": 7546, + "survivor_count": 69, + "applications": [ + { + "weights": [ + 3, + 5, + 5, + 5, + 6, + 6, + 6, + 6, + 6, + 7 + ], + "retained_weights": [ + 3, + 5, + 5, + 5, + 6, + 6, + 6, + 6, + 6 + ], + "intersection_before": 6, + "intersection_after_lower": 5, + "quotient_dimension": 4, + "prior_cover_rows": [ + { + "basis": [ + 3, + 5, + 5, + 5 + ], + "complement": [ + 6, + 6, + 6, + 6, + 6, + 7 + ], + "support_cap": 40, + "minimum_two_flat_cuts": 16, + "rank_four_anchor": false + }, + { + "basis": [ + 3, + 5, + 5, + 6 + ], + "complement": [ + 5, + 6, + 6, + 6, + 6, + 7 + ], + "support_cap": 48, + "minimum_two_flat_cuts": 16, + "rank_four_anchor": false + } + ], + "small_support_cap": 28, + "endpoint_caps": [ + 12, + 20, + 20, + 20, + 20, + 20 + ], + "endpoint_sum_cap": 112, + "quotient_support_cap": 48, + "edge_support_cap": 68, + "edge_incidence_lower": 795, + "coordinate_incidence_upper": 784, + "old_incidence_upper": 812, + "margin": 11, + "excluded": true + }, + { + "weights": [ + 4, + 4, + 5, + 5, + 6, + 6, + 6, + 6, + 6, + 7 + ], + "retained_weights": [ + 4, + 4, + 5, + 5, + 6, + 6, + 6, + 6, + 6 + ], + "intersection_before": 6, + "intersection_after_lower": 5, + "quotient_dimension": 4, + "prior_cover_rows": [ + { + "basis": [ + 4, + 4, + 5, + 5 + ], + "complement": [ + 6, + 6, + 6, + 6, + 6, + 7 + ], + "support_cap": 40, + "minimum_two_flat_cuts": 16, + "rank_four_anchor": false + }, + { + "basis": [ + 4, + 4, + 5, + 6 + ], + "complement": [ + 5, + 6, + 6, + 6, + 6, + 7 + ], + "support_cap": 48, + "minimum_two_flat_cuts": 16, + "rank_four_anchor": false + }, + { + "basis": [ + 4, + 5, + 5, + 6 + ], + "complement": [ + 4, + 6, + 6, + 6, + 6, + 7 + ], + "support_cap": 52, + "minimum_two_flat_cuts": 20, + "rank_four_anchor": true + } + ], + "small_support_cap": 28, + "endpoint_caps": [ + 12, + 20, + 20, + 20, + 20, + 20 + ], + "endpoint_sum_cap": 112, + "quotient_support_cap": 48, + "edge_support_cap": 68, + "edge_incidence_lower": 795, + "coordinate_incidence_upper": 784, + "old_incidence_upper": 812, + "margin": 11, + "excluded": true + } + ] + } +} diff --git a/research/p112-unequal-endpoint-deletion/SOURCES.json b/research/p112-unequal-endpoint-deletion/SOURCES.json new file mode 100644 index 0000000000..498167ea8b --- /dev/null +++ b/research/p112-unequal-endpoint-deletion/SOURCES.json @@ -0,0 +1,73 @@ +{ + "schema_version": 1, + "base_commit": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/one-sided-six-multisets/data/data.txt", + "usage": "input", + "git_blob": "dc591a4e0252bac096e6c63c51058f6caee66bfe", + "sha256": "ac4a48851b922f2a433684b60c74768ae3bb4fc5e8990ffe63e3942bb3c2ea34" + }, + { + "path": "research/p112-weight-seven-deletion/geometry.py", + "usage": "input", + "git_blob": "222ea556faf2b275f73815c4e7d0d5f1e3294f2f", + "sha256": "b8ac379e41f5ad83bdb6c7f7c55129fc3d9c07801ea61591478f25d72ff0b021" + }, + { + "path": "research/p112-weight-seven-deletion/vendor/COORDINATE-PROOF.md", + "usage": "input", + "git_blob": "278072bdaf6e0f067655491a61317f115f38160f", + "sha256": "21cd2f726865241c65641fb3e966c5ab3ae51694e47169d491b077ca73f547a2" + }, + { + "path": "research/p112-weight-seven-deletion/vendor/bk2b.py", + "usage": "input", + "git_blob": "3394029014bb13f16225587a153fa7b70016de6d", + "sha256": "dff16eff255c883db372a587cf3f34e6f35c08f75c60af9d11952be5a5838807" + } + ], + "predecessors": [ + { + "pr": 3154, + "author": "DreamingOfClouds", + "head": "708f0ad8928c383de8294aea3c126e9461d2066d", + "contribution": "Original TWOSIDE filters and decoder reduction; retained bk2b bytes are a declared input." + }, + { + "pr": 3169, + "author": "Nick Petalas", + "head": "2dbbd3004b70772cef200e341037c7c05b094fbc", + "contribution": "A5 coordinate inequality and retained geometry from PR3164/3161/3162; unchanged proof and geometry are declared inputs." + }, + { + "pr": 3197, + "author": "Nick Petalas", + "head": "3949cc17a4fa4f108a044f532a5d58323c6cb6d2", + "contribution": "Codimension-one deletion application for the distinct uniform-endpoint profile 4^3,6^6,7." + }, + { + "pr": 3195, + "author": "Nick Petalas", + "head": "22f1479db213b1ed0de68cbc61ba15f6352d3276", + "contribution": "Adjacent shorter 5^2,6^6,7 deletion caller, not a new result here." + } + ], + "code_origins": { + "ledger.py": "New unequal-endpoint applications and prior-cover audit; original BK/BK7 filters transcribed from DreamingOfClouds/PR3154. Dimension and invoice formulas follow Nick Petalas/PR3197 and PR3169.", + "verify.py": "New input-bound driver calling the unchanged declared PR3169 geometry module retained by PR3197. No geometry source copied.", + "test_verify.py": "New profile/support/source controls; quotient fixture and subset-cover oracle adapted from Nick Petalas/PR3197." + } +} diff --git a/research/p112-unequal-endpoint-deletion/TASK.json b/research/p112-unequal-endpoint-deletion/TASK.json new file mode 100644 index 0000000000..e212e8e09e --- /dev/null +++ b/research/p112-unequal-endpoint-deletion/TASK.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 6, + "base_commit": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one small, precisely scoped interface lemma be formalized with its actual hypotheses?", + "starting_points": [ + "certificates/selected-result.json", + "research/hyperplane-end-lean/PROOF.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the exact hypotheses in the hyperplane-end proof and distinguish Lean theorems from finite supplier assumptions.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "State one missing boundary lemma in full before starting a proof-assistant build.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding" + ] + }, + "scope_status": "changed", + "actual_scope": "Exclude the actual TWOSIDE (6,4) profiles 3,5^3,6^5,7 and 4^2,5^2,6^5,7 by deleting one unrestricted piece and charging unequal A5 endpoint capacities.", + "scope_change_reason": "Took the live weight-seven C5 handoff in Discussion3156 before using the generic card. This is a written characteristic-zero consequence of the retained coordinate inequality with exact finite replay, not Lean formalization. The unequal endpoint invoice supplies coverage beyond the published uniform-endpoint deletion application.", + "bottleneck_link": "Closes two specific missing implications in the P112 decoder-floor reduction on the binding complex side. It does not prove full C5, the decoder floor, supplier admission or a new exponent.", + "budget_minutes": 60, + "stop_rule": "Stop after these two source-bound applications, a failed quotient/support premise or the sixty-minute session; do not extend the census without another actual caller.", + "outcome": "partial", + "evidence": "PROOF.md gives the nine-piece statements and codimension-one transfer. RESULT.json records both exact invoices, historical inclusion, prior-cover audit, all five/six-flat capacities and endpoint patterns. CHECKS.json records commands and limits.", + "author": "Nick Petalas", + "ai_assistance": "Substantial automated assistance in derivation, implementation and local checks. No independent human review or proof-kernel verification is claimed.", + "open_questions": [ + { + "question": "Does an actual remaining weight-seven profile require a genuinely stronger support or quotient argument after all existing deletion consequences are applied?", + "why_it_matters": "A historical survivor count is not the current C5 frontier, and another seed or adjacent profile alone does not justify a new geometry census.", + "first_step": "Refresh Discussion3156, bind one still-open profile to exact predecessor heads, and check surviving code dimension plus all existing sufficient cover rules before computing.", + "blocked_by": "The complete C5 disposition and other decoder-floor conjectures remain unresolved; no full supplier cost or physical realization is supplied here." + } + ] +} diff --git a/research/p112-unequal-endpoint-deletion/VERIFY.json b/research/p112-unequal-endpoint-deletion/VERIFY.json new file mode 100644 index 0000000000..565c2a9771 --- /dev/null +++ b/research/p112-unequal-endpoint-deletion/VERIFY.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/one-sided-six-multisets/data/data.txt", + "research/p112-weight-seven-deletion/geometry.py", + "research/p112-weight-seven-deletion/vendor/COORDINATE-PROOF.md", + "research/p112-weight-seven-deletion/vendor/bk2b.py" + ], + "commands": [ + { + "argv": ["{python}", "-W", "error", "-B", "{package}/verify.py"], + "timeout_seconds": 120, + "checks": "All four input pins, complete inherited five/six-flat and root geometry replay, endpoint patterns, two exact invoices and historical/prior-cover inventory." + }, + { + "argv": ["{python}", "-W", "error", "-OO", "-B", "{package}/test_verify.py"], + "timeout_seconds": 120, + "checks": "Twelve behavioral groups with dimension/quotient fixtures, losing invoices, strict cutoffs, independent subset-cover oracle, original checker, four input mutations and exclusive external output." + } + ] +} diff --git a/research/p112-unequal-endpoint-deletion/ledger.py b/research/p112-unequal-endpoint-deletion/ledger.py new file mode 100644 index 0000000000..254626d547 --- /dev/null +++ b/research/p112-unequal-endpoint-deletion/ledger.py @@ -0,0 +1,134 @@ +"""Unequal-endpoint applications of Nick Petalas/PR3169's A5 inequality. + +Historical BK/BK7 filters follow DreamingOfClouds/PR3154. Apache-2.0. +""" + +# Copyright 2026 Nick Petalas + +from itertools import combinations, combinations_with_replacement, product + +CAP = {2: 2, 3: 4, 4: 8, 5: 12, 6: 20, 7: 36} +TARGET_CAP = {**CAP, 7: 32} +DISTANCE = (0, 53, 78, 92, 100, 106, 109) +TARGETS = ((3, 5, 5, 5, 6, 6, 6, 6, 6, 7), + (4, 4, 5, 5, 6, 6, 6, 6, 6, 7)) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def validate_weights(weights): + require(isinstance(weights, tuple) and 6 <= len(weights) <= 10 + and all(type(w) is int and w in CAP for w in weights) + and weights == tuple(sorted(weights)), "invalid weight multiset") + + +def surviving_dimension(dimension, intersection, removed): + require(all(type(x) is int for x in (dimension, intersection, removed)) + and 0 <= intersection <= dimension <= 16 + and 0 <= removed <= dimension, "invalid dimension ledger") + return max(0, intersection - removed) + + +def coordinate_invoice(small, endpoints): + """Needs independent pieces, five code dimensions and three small pieces.""" + require(type(small) is int and 0 <= small <= 112 + and isinstance(endpoints, tuple) and len(endpoints) == 6 + and all(type(x) is int and 0 <= x <= 112 for x in endpoints), + "invalid support ledger") + ordered = sorted(endpoints, reverse=True) + require(small + ordered[0] < 53, "uncertified quotient independence") + require(small + sum(ordered[:2]) < 70, "uncertified root edges") + total = sum(endpoints) + upper = 112 + 8 * small + 4 * total + return {"small_support_cap": small, "endpoint_caps": list(endpoints), + "endpoint_sum_cap": total, "quotient_support_cap": small + ordered[0], + "edge_support_cap": small + sum(ordered[:2]), + "edge_incidence_lower": 795, "coordinate_incidence_upper": upper, + "old_incidence_upper": 9 * small + 5 * total, + "margin": 795 - upper, "excluded": upper < 795} + + +def historical_survivor(weights): + """Original (b,t)=(6,4) necessary filters, not a current disposition ledger.""" + validate_weights(weights) + if sum(w - 2 for w in weights) >= 36: + return False + for level in range(1, 7): + kept = weights[:len(weights) - (6 - level)] + global_cap = sum(CAP[w] for w in kept) + target_cap = sum(TARGET_CAP[w] for w in kept) + target_min, global_min = ((53, 73) if level == 1 else + (78, 82) if level == 2 else + (DISTANCE[level], DISTANCE[level])) + if global_cap < global_min and (level >= 3 or target_cap < target_min): + return False + basis = weights[:len(weights) - 6] + if sum(CAP[w] for w in basis) >= 53: + return True + if sum(basis) <= 7: + return False + for assignment in product((0, 1), repeat=len(basis)): + if all(sum(w for w, a in zip(basis, assignment, strict=True) if a == group) + <= 6 for group in (0, 1)): + return False + return True + + +def prior_cover_rows(weights): + """Every support-certified four-piece basis and weight-only two-flat cover.""" + validate_weights(weights) + require(len(weights) == 10, "prior cover needs ten pieces") + rows = {} + for indices in combinations(range(10), 4): + basis = tuple(weights[i] for i in indices) + if basis in rows or sum(CAP[w] for w in basis) >= 53: + continue + complement = tuple(w for i, w in enumerate(weights) if i not in indices) + paid = sum(CAP[w] for w in basis) + for assignment in product(range(3), repeat=4): + if all(sum(w for w, a in zip(basis, assignment, strict=True) if a == k) + <= 6 for k in (0, 1)): + paid = min(paid, sum(CAP[w] for w, a in + zip(basis, assignment, strict=True) if a == 2)) + rows[basis] = {"basis": list(basis), "complement": list(complement), + "support_cap": sum(CAP[w] for w in basis), + "minimum_two_flat_cuts": paid, + "rank_four_anchor": any(w <= 4 for w in complement)} + return [rows[basis] for basis in sorted(rows)] + + +def application(weights): + validate_weights(weights) + require(weights in TARGETS, "outside the two-profile application") + retained = weights[:-1] + small = sum(CAP[w] for w in retained[:3]) + endpoints = tuple(CAP[w] for w in retained[3:]) + invoice = coordinate_invoice(small, endpoints) + dimension = surviving_dimension(10, 6, 1) + require(dimension == 5 and invoice["excluded"] and invoice["margin"] == 11, + "failed dimension or support invoice") + covers = prior_cover_rows(weights) + require(covers and min(row["minimum_two_flat_cuts"] for row in covers) == 16 + and all(row["minimum_two_flat_cuts"] > 14 for row in covers), + "earlier cut route applies") + return {"weights": list(weights), "retained_weights": list(retained), + "intersection_before": 6, "intersection_after_lower": dimension, + "quotient_dimension": 4, "prior_cover_rows": covers, **invoice} + + +def historical_inventory(): + survivors = [] + examined = 0 + for size in range(6, 11): + for weights in combinations_with_replacement(range(2, 8), size): + examined += 1 + if historical_survivor(weights): + survivors.append(weights) + require(len(survivors) == 69 and all(w in survivors for w in TARGETS), + "historical inventory differs") + return {"cell": [6, 4], "multisets_examined": examined, + "survivor_count": len(survivors), + "applications": [application(w) for w in TARGETS]} diff --git a/research/p112-unequal-endpoint-deletion/test_verify.py b/research/p112-unequal-endpoint-deletion/test_verify.py new file mode 100644 index 0000000000..933db0f6ec --- /dev/null +++ b/research/p112-unequal-endpoint-deletion/test_verify.py @@ -0,0 +1,178 @@ +"""Independent finite controls and failure cases for the two applications.""" + +# Copyright 2026 Nick Petalas + +import json +import shutil +import subprocess +import sys +import tempfile +import unittest +from fractions import Fraction +from itertools import combinations, product +from pathlib import Path +from unittest.mock import patch + +import verify +from ledger import ( + CAP, + TARGETS, + application, + coordinate_invoice, + historical_inventory, + historical_survivor, + prior_cover_rows, + surviving_dimension, +) + + +class DeletionTests(unittest.TestCase): + def test_both_actual_profiles(self): + inventory = historical_inventory() + self.assertEqual(inventory["survivor_count"], 69) + for weights in TARGETS: + row = application(weights) + self.assertEqual(row["intersection_after_lower"], 5) + self.assertEqual(row["quotient_dimension"], 4) + self.assertEqual(row["small_support_cap"], 28) + self.assertEqual(row["endpoint_caps"], [12, 20, 20, 20, 20, 20]) + self.assertEqual(row["coordinate_incidence_upper"], 784) + self.assertEqual(row["margin"], 11) + self.assertTrue(historical_survivor(weights)) + self.assertEqual(sum(w - 2 for w in weights), 35) + + def test_sharp_dimension_loss(self): + for dimension in range(1, 11): + for code in range(dimension + 1): + for removed in range(dimension + 1): + actual = len(set(range(code)) & set(range(removed, dimension))) + self.assertEqual(actual, surviving_dimension(dimension, code, removed)) + self.assertEqual(surviving_dimension(10, 6, 2), 4) + self.assertNotEqual(surviving_dimension(10, 6, 1), 6) + + def test_invalid_dimension_ledger(self): + for values in ((10, 11, 1), (10, 6, -1), (10, 6, 11), + (17, 6, 1), (10, True, 1), (10, 6, 1.0)): + with self.subTest(values=values), self.assertRaises(ValueError): + surviving_dimension(*values) + + def test_nonuniform_endpoint_is_essential_for_this_invoice(self): + row = coordinate_invoice(28, (12,) + (20,) * 5) + self.assertEqual(row["old_incidence_upper"], 812) + self.assertGreaterEqual(row["old_incidence_upper"], 795) + uniform = coordinate_invoice(28, (20,) * 6) + self.assertEqual(uniform["coordinate_incidence_upper"], 816) + self.assertFalse(uniform["excluded"]) + self.assertFalse(coordinate_invoice(30, (19,) * 6)["excluded"]) + + def test_strict_support_cutoffs(self): + # First fails 53, second hits 70 while keeping quotient support below 53. + for small, caps in ((33, (20,) * 6), (30, (20,) * 6), + (28, (36,) + (20,) * 5)): + with self.subTest(small=small, caps=caps), self.assertRaises(ValueError): + coordinate_invoice(small, caps) + + def test_invalid_support_and_weight_inputs(self): + for small, caps in ((-1, (20,) * 6), (True, (20,) * 6), + (28, (20,) * 5), (28, (20,) * 5 + (-1,)), + (28, (20,) * 5 + (20.0,))): + with self.subTest(small=small, caps=caps), self.assertRaises(ValueError): + coordinate_invoice(small, caps) + for weights in (TARGETS[0][::-1], (*TARGETS[0][:-1], 8), (2,) * 11): + with self.assertRaises(ValueError): + historical_survivor(weights) + self.assertFalse(historical_survivor((6,) * 9)) + with self.assertRaises(ValueError): + application((4, 4, 4, 6, 6, 6, 6, 6, 6, 7)) + + def test_quotient_normalization_and_independent_codewords(self): + images = [(1, 0, 0, 0), (0, 1, 0, 0), (0, 0, 1, 0)] + images += [(i, i * i, i ** 3, i + 1) for i in range(6)] + circuits = [] + for i in range(1, 6): + row = [Fraction(0)] * 9 + row[i + 3], row[3] = Fraction(1, i + 1), -1 + for j in range(3): + row[j] = -Fraction(i ** (j + 1), i + 1) + self.assertEqual(tuple(sum(row[j] * images[j][k] for j in range(9)) + for k in range(4)), (0, 0, 0, 0)) + circuits.append(row) + for i, row in enumerate(circuits): + self.assertEqual(row[4:], [Fraction(1, i + 2) if i == j else 0 + for j in range(5)]) + + def test_independent_two_flat_subset_oracle(self): + expected = [2, 3] + for weights, count in zip(TARGETS, expected, strict=True): + rows = prior_cover_rows(weights) + self.assertEqual(len(rows), count) + for row in rows: + basis = row["basis"] + costs = [] + for paid in product((False, True), repeat=4): + unpaid = [w for w, p in zip(basis, paid, strict=True) if not p] + for left in product((False, True), repeat=len(unpaid)): + totals = [sum(w for w, side in zip(unpaid, left, strict=True) + if side == value) for value in (False, True)] + if max(totals) <= 6: + costs.append(sum(CAP[w] for w, p in + zip(basis, paid, strict=True) if p)) + self.assertEqual(min(costs), row["minimum_two_flat_cuts"]) + self.assertGreater(min(costs), 14) + self.assertEqual(min(row["minimum_two_flat_cuts"] for row in rows), 16) + + def test_unmodified_historical_checker(self): + verify.bound_inputs() + command = [sys.executable, "-B", str(verify.ROOT / verify.INPUTS[3])] + result = subprocess.run(command, check=True, capture_output=True, + text=True, timeout=30) + rows = [tuple(map(int, line.split())) for line in result.stdout.splitlines()] + self.assertEqual(len(rows), 24) + self.assertIn((6, 4, 69, 1), rows) + self.assertEqual(result.stderr, "") + + def test_endpoint_patterns_and_root_hypothesis_control(self): + self.assertEqual(verify.endpoint_receipt()["equality_assignments"], 7 ** 6) + # Arbitrary six values can have 15 unequal pairs. Nine is root-specific. + self.assertEqual(sum(a != b for a, b in combinations(range(6), 2)), 15) + # Independent arithmetic checks all possible nonzero endpoint counts. + for k in range(7): + self.assertLessEqual(k * (6 - k) + k * (k - 1) // 2, 4 * k + 1) + + def test_every_input_is_authenticated(self): + self.assertEqual(set(verify.bound_inputs()), set(verify.INPUTS)) + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + for name in verify.INPUTS: + target = root / name + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(verify.ROOT / name, target) + for name in verify.INPUTS: + target = root / name + raw = target.read_bytes() + target.write_bytes(raw + b"\n") + with patch.object(verify, "ROOT", root), self.assertRaisesRegex( + ValueError, "input hash differs"): + verify.bound_inputs() + target.write_bytes(raw) + + def test_external_exclusive_output_and_receipt_comparison(self): + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + output = root / "receipt.json" + verify.publish({"control": True}, output) + self.assertEqual(json.loads(output.read_text()), {"control": True}) + with self.assertRaises(FileExistsError): + verify.publish({}, output) + (root / "RESULT.json").write_text('{"expected": true}\n') + with patch.object(verify, "PACKAGE", root), self.assertRaisesRegex( + ValueError, "committed receipt differs"): + verify.publish({}, None) + with self.assertRaisesRegex(ValueError, "outside checkout"): + verify.publish({}, verify.PACKAGE / "forbidden.json") + with self.assertRaisesRegex(ValueError, "absolute"): + verify.publish({}, Path("relative.json")) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/p112-unequal-endpoint-deletion/verify.py b/research/p112-unequal-endpoint-deletion/verify.py new file mode 100644 index 0000000000..af58216bde --- /dev/null +++ b/research/p112-unequal-endpoint-deletion/verify.py @@ -0,0 +1,102 @@ +#!/usr/bin/env python3 +"""Source-bound P112 unequal-endpoint deletion replay. Apache-2.0.""" + +# Copyright 2026 Nick Petalas + +import argparse +import hashlib +import json +import sys +from collections import Counter +from itertools import combinations, product +from pathlib import Path + +from ledger import coordinate_invoice, historical_inventory, require + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parent.parent +PREDECESSOR = "research/p112-weight-seven-deletion" +INPUTS = ("research/one-sided-six-multisets/data/data.txt", + f"{PREDECESSOR}/geometry.py", + f"{PREDECESSOR}/vendor/COORDINATE-PROOF.md", + f"{PREDECESSOR}/vendor/bk2b.py") + + +def bound_inputs(): + pins = json.loads((PACKAGE / "SOURCES.json").read_text(encoding="utf-8")) + rows = [row for row in pins["files"] if row["usage"] == "input"] + require(tuple(row["path"] for row in rows) == INPUTS, "input inventory differs") + result = {} + for row in rows: + path = ROOT / row["path"] + require(path.is_file() and not path.is_symlink() + and path.stat().st_size <= 2_000_000, "missing/large input") + digest = hashlib.sha256(path.read_bytes()).hexdigest() + require(digest == row["sha256"], "input hash differs") + result[row["path"]] = digest + return result + + +def geometric_receipt(): + """Reuse the unchanged, authenticated module, not a new geometry census.""" + sys.path.insert(0, str(ROOT / PREDECESSOR)) + try: + import geometry + finally: + sys.path.pop(0) + roots, points, labels, coordinates = geometry.root_data() + raw = (ROOT / INPUTS[0]).read_text(encoding="utf-8").splitlines() + require(tuple(map(int, raw[0].split())) == labels, "P112 label binding") + require(tuple(tuple(map(int, row.split())) for row in raw[2:114]) == points, + "P112 coordinate binding") + return {"chamber": geometry.chamber_receipt(roots, points, coordinates), + "root_planes": geometry.root_plane_receipt(roots), + "flat_capacities": [geometry.flat_capacity(labels, d) for d in (5, 6)]} + + +def endpoint_receipt(): + """Seven symbols realize every equality pattern of six values and zero.""" + histogram = Counter() + for values in product(range(7), repeat=6): + nonzero = sum(value != 0 for value in values) + unequal = sum(a != b for a, b in combinations(values, 2)) + require(unequal <= 4 * nonzero + 1, "endpoint inequality") + histogram[nonzero] += 1 + losing = coordinate_invoice(28, (20,) * 6) + require(not losing["excluded"] and losing["margin"] == -21, + "uniform-endpoint losing control") + return {"equality_assignments": sum(histogram.values()), + "nonzero_histogram": {str(k): v for k, v in sorted(histogram.items())}, + "uniform_endpoint_control": losing} + + +def receipt(): + pins = bound_inputs() + return {"schema": "p112-unequal-endpoint-deletion/v1", "input_sha256": pins, + "geometry": geometric_receipt(), "endpoints": endpoint_receipt(), + "historical_inventory": historical_inventory()} + + +def publish(result, output): + serialized = json.dumps(result, indent=2) + "\n" + if output is None: + expected = json.loads((PACKAGE / "RESULT.json").read_text(encoding="utf-8")) + require(result == expected, "committed receipt differs") + return + require(output.is_absolute(), "output must be absolute") + output = output.resolve() + require(not output.is_relative_to(ROOT), "output must be outside checkout") + with output.open("x", encoding="utf-8") as stream: + stream.write(serialized) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, help="new absolute external receipt") + args = parser.parse_args() + publish(receipt(), args.output) + print("PASS_P112_UNEQUAL_ENDPOINT_DELETION profiles=2 margin=11 errors=0") + + +if __name__ == "__main__": + main()