From b859f7791a6d2dad68652d5a54e266cb020a1302 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Sat, 17 Oct 2026 15:10:57 +0100 Subject: [PATCH 1/2] feat(research): exclude five ten-piece P112 beta profiles --- research/p112-ten-piece-simplex/CHECKS.json | 66 ++ research/p112-ten-piece-simplex/DECISIONS.tsv | 4 + .../p112-ten-piece-simplex/ENGINEERING.md | 62 ++ research/p112-ten-piece-simplex/PROOF.md | 203 ++++ research/p112-ten-piece-simplex/README.md | 99 ++ research/p112-ten-piece-simplex/RESULT.json | 863 ++++++++++++++++++ research/p112-ten-piece-simplex/SOURCES.json | 85 ++ research/p112-ten-piece-simplex/TASK.json | 66 ++ research/p112-ten-piece-simplex/VERIFY.json | 34 + research/p112-ten-piece-simplex/beta.py | 145 +++ research/p112-ten-piece-simplex/geometry.py | 188 ++++ .../p112-ten-piece-simplex/test_verify.py | 155 ++++ research/p112-ten-piece-simplex/verify.py | 85 ++ 13 files changed, 2055 insertions(+) create mode 100644 research/p112-ten-piece-simplex/CHECKS.json create mode 100644 research/p112-ten-piece-simplex/DECISIONS.tsv create mode 100644 research/p112-ten-piece-simplex/ENGINEERING.md create mode 100644 research/p112-ten-piece-simplex/PROOF.md create mode 100644 research/p112-ten-piece-simplex/README.md create mode 100644 research/p112-ten-piece-simplex/RESULT.json create mode 100644 research/p112-ten-piece-simplex/SOURCES.json create mode 100644 research/p112-ten-piece-simplex/TASK.json create mode 100644 research/p112-ten-piece-simplex/VERIFY.json create mode 100644 research/p112-ten-piece-simplex/beta.py create mode 100644 research/p112-ten-piece-simplex/geometry.py create mode 100644 research/p112-ten-piece-simplex/test_verify.py create mode 100644 research/p112-ten-piece-simplex/verify.py diff --git a/research/p112-ten-piece-simplex/CHECKS.json b/research/p112-ten-piece-simplex/CHECKS.json new file mode 100644 index 0000000000..59d39acdca --- /dev/null +++ b/research/p112-ten-piece-simplex/CHECKS.json @@ -0,0 +1,66 @@ +{ + "schema": "p112-ten-piece-simplex-checks/v1", + "checked_at_utc": "2026-10-17T14:10:01.656746+00:00", + "upstream_commit": "997e6a9ca7b4f95d50e366f61412fd640d72a88a", + "priority_revision": 6, + "environments": { + "3.12": "3.12.15 (main, Oct 14 2026, 00:55:37) [Clang 23.1.3 ]\nmacOS-27.0.1-arm64-arm-64bit", + "3.13": "3.13.16 (main, Oct 14 2026, 00:55:38) [Clang 23.1.3 ]\nmacOS-27.0.1-arm64-arm-64bit-Mach-O" + }, + "checks": [ + { + "command": "TMPDIR=SESSION uv run --python 3.12 --no-project python -W error -B scripts/research_package.py --package research/p112-ten-piece-simplex", + "result": "PASS_REGISTERED_RESEARCH_PACKAGE; full receipt equality; sixteen optimized behavioral groups" + }, + { + "command": "TMPDIR=SESSION uv run --python 3.13 --no-project python -O -W error -B EXPORT/research/p112-ten-piece-simplex/verify.py", + "result": "PASS; identical receipt from read-only Git-free source export" + }, + { + "command": "TMPDIR=SESSION uv run --python 3.13 --no-project python -O -W error -B EXPORT/research/p112-ten-piece-simplex/test_verify.py", + "result": "sixteen groups pass from read-only Git-free source export" + }, + { + "command": "Run both exact pinned PR3154 TWOSIDE bk1b.py and bk2b.py sources", + "result": "both reproduce 38 survivors for (5,5); interpretation of their deficit columns differs, so no deficit statistic is used" + }, + { + "command": "Compile all four package Python sources in memory with warnings as errors; inspect every function via ast", + "result": "syntax passes; all functions below 60 physical lines; Ruff/Mypy/Pyright unavailable" + }, + { + "command": "Compare geometry.py bytes with pinned PR3164 Git blob", + "result": "identical" + }, + { + "command": "Invoke verify.py --output on an in-checkout path and an existing external path", + "result": "both reject; no in-checkout file created; existing receipt is not overwritten" + } + ], + "coverage": { + "label_flat_kernels": 4097782, + "root_line_pairs": 7140, + "simple_reflections": 960, + "behavioral_groups": 16, + "all_endpoint_patterns": 117649, + "new_exclusion_margins": [ + 11, + 11, + 27, + 27, + 27 + ] + }, + "review": { + "mathematics": "Read-only internal review independently corroborated the endpoint inequality, quotient argument and five support budgets.", + "overlap": "Separate exhaustive enumeration corroborated all five prior-cover minima and the rank-four-anchor control.", + "limits": "Internal review is not independent human or proof-kernel review. Weyl-chamber theorem, full TWOSIDE reduction, all other decoder cases and supplier admission remain separate obligations." + }, + "publication": "Run scripts/check_research_commit.py after committing and inspect GitHub head before final handoff.", + "not_run": [ + "Lean/proof-assistant build", + "full supplier cold replay", + "historical long predecessor suites", + "hosted CI" + ] +} diff --git a/research/p112-ten-piece-simplex/DECISIONS.tsv b/research/p112-ten-piece-simplex/DECISIONS.tsv new file mode 100644 index 0000000000..a7df51a441 --- /dev/null +++ b/research/p112-ten-piece-simplex/DECISIONS.tsv @@ -0,0 +1,4 @@ +timestamp attempt hypothesis change before after correctness_check verdict note +2026-10-17T14:08:22.379991+00:00 1 four small pieces preserve the six-vertex simplex ten-piece quotient in dimension five 0 new exclusions 2 new exclusions full geometry and prior-cover checks keep original count margins one and one +2026-10-17T14:08:22.379991+00:00 2 3^3,4,6^6 is another new application alternative quotient basis audit claimed new candidate covered by PR3167 all quotient bases and independent covers reject novelty retained as an overlap control +2026-10-17T14:08:22.379991+00:00 3 finite coordinate count strengthens the endpoint charge unequal pairs at most 4k+1 2 new exclusions 5 new exclusions complete endpoint patterns; full geometry; internal proof review keep exact margins 11,11,27,27,27; no runtime metric diff --git a/research/p112-ten-piece-simplex/ENGINEERING.md b/research/p112-ten-piece-simplex/ENGINEERING.md new file mode 100644 index 0000000000..3b1e99699b --- /dev/null +++ b/research/p112-ten-piece-simplex/ENGINEERING.md @@ -0,0 +1,62 @@ +# Verification bounds and decisions + +Build the Lever changed the work from a larger deletion census to a reusable +checker for one counting lemma and its actual weight applications. Prove It +Works required complete receipt equality, losing controls, a separately coded +cover oracle and publication-byte checks. Power of Ten kept loops finite, +checks active under optimization, and generated output outside the checkout. + +The code is isolated in this package. `geometry.py` is byte-identical to the +pinned PR3164 source. `beta.py` contains the new inequality, application and +overlap logic. `verify.py` reconstructs data and compares the receipt. +`test_verify.py` tests mathematical inequalities and failure conditions. +No selected result, shared verifier or frozen predecessor changes. + +All control flow is structured and nonrecursive. Flat enumeration has exactly +3,309,747 and 788,035 kernels. There are 7,140 root pairs and 120 third-root +candidates per pair; 960 reflection checks; eight-dimensional elimination; +and weight multisets of lengths five through ten over six possible weights. +Quotient covers have at most C(10,5)=252 index choices and 3^5=243 bin +assignments. The independent cover oracle uses at most 2^5 * 2^5 pairs of +subsets. The endpoint-pattern control uses 7^6=117,649 patterns. Registered +commands run sequentially with 120-second bounds. There is no recursive +search, retry loop or background process. + +Rule 3 deviation, managed-runtime allocation. Python creates integers, tuples +and Fraction objects during these bounded computations. Avoiding allocation +would require replacing the standard-library implementation. Live geometry is +bounded by 120 eight-dimensional roots, a 120-by-120 Gram table, 512 masks of +112 bits, at most four collections of at most 64 row masks, and 113 histogram +counters. Kernels are processed and discarded. The input has a 2 MB size cap; +the pinned input is 971,985 bytes. New live application data are at most 38 +weight tuples of length ten, five result rows and 252 quotient-index choices +streamed from an iterator. Tests use scoped temporary directories. Full replay +and mutation tests exercise the bounds and cleanup. Reconsider a fixed-memory +native implementation only if the fixed problem dimensions grow. + +Functions stay below 60 physical lines. Meaningful guards check dimensions, +source bytes, rank inventories, kernel counts, quotient and root thresholds, +original survivors and prior coverage. They use `require` rather than Python +assertions, so optimization does not disable them. Test assertions use unittest. +State is local except read-only module lookup tables. No dynamic evaluation or runtime +code generation is used. Every subprocess used for development is checked; +the retained verifier launches none. Output creation uses exclusive mode. + +Rule 9 runtime limitation. Python exposes no C pointer-dereference discipline. +The nearest inspected mechanisms are bounded tuple/list access and direct +function calls; there is no application callback chain or dynamic dispatch. +The unittest framework has a fixed set of sixteen local test methods. + +Rule 10 diagnostics limitation. Mathematical and behavioral commands run with +`-W error`; optimization controls retain their guards. Bytecode compilation +checks syntax without writing into the checkout. The registered manifest makes +the real replay recurring. No Ruff, Mypy or Pyright executable is installed; +adding a repository-wide lint policy would exceed this isolated research task. +The follow-up is to include these files in such a policy when adopted. +CHECKS.json records the exact supported diagnostics and environments. + +The metric is the number of additional pinned beta shapes excluded, rather +than runtime. All acceptance values are exact integers. DECISIONS.tsv records +the rejected overlap and the original-count versus coordinate-budget attempts. +No noisy timing result or benchmark speedup is claimed. The best remaining +question requires a different quotient-independence argument for `4,5^9`. diff --git a/research/p112-ten-piece-simplex/PROOF.md b/research/p112-ten-piece-simplex/PROOF.md new file mode 100644 index 0000000000..278072bdaf --- /dev/null +++ b/research/p112-ten-piece-simplex/PROOF.md @@ -0,0 +1,203 @@ +# A coordinate budget strengthens the P112 root-simplex obstruction + +## Statement + +Let K be a characteristic-zero field. Use the 112 live E8 root lines and +their binary labels ell(t) from the pinned P112 input. Put + +``` +C = {c_h : c_h(t) = , h in K^8}, +w(q) = rank_F2 {ell(t) : q(t) != 0}. +``` + +The root representatives r_t in the replay are doubled roots. Scaling the +representatives does not change supports. Ten linearly independent pieces +spanning T with dim(T intersect C) >= 5 cannot have weights bounded by any +of these five multisets: + +``` +2,2,4,5,6,6,6,6,6,6 +2,2,5,5,5,6,6,6,6,6 +2,3,4,4,6,6,6,6,6,6 +2,3,4,5,5,6,6,6,6,6 +2,4,4,4,5,6,6,6,6,6. +``` + +All five are actual survivors of the pinned TWOSIDE `(b,t)=(5,5)` BK/BK7 +weight filters. This is a theorem about these explicit piece hypotheses. +Its application to the decoder reduction inherits that reduction's other +conditions. It does not settle C5, the decoder floor or a supplier. + +## Geometry and finite dependencies + +We use the following P112 facts, replayed rather than assumed from a receipt: + +1. Supports of weight d=2,3,4,5,6 have cardinality at most 2,4,8,12,20. +2. Every nonzero element of C has support at least 53. +3. A nonzero element of C with support below 70 is a root direction. +4. The evaluation map h -> c_h is injective. + +The first three dimensions follow from the labels' leading-one coordinate: +a binary d-flat meets that affine hyperplane in at most 2^(d-1) points. +For dimensions five and six, `geometry.py` enumerates every annihilator in +unique reverse row-echelon form: 3,309,747 and 788,035 subspaces. Their +kernel intersections with the 112 distinct labels have maxima 12 and 20. +A support of smaller rank extends to a flat of the stated dimension. + +For facts 2 and 3, use the standard Weyl-chamber theorem for the real E8 +root system. A real direction with support below 70 is perpendicular to at +least 43 live root lines. In a closed chamber the perpendicular root system +is generated by the simple roots that vanish on the direction. The replay +checks that all six-node parabolics have at most 36 root lines. The eight +seven-node parabolics have counts `42,28,22,14,16,23,37,63`; only the last +can contain 43 perpendicular lines, and its normal is a root direction. +Root directions have live supports 53 or 56, so the same argument also +rules out support below 53. The replay checks all 960 simple reflections, +simple-system positivity, parabolic counts and root supports. The chamber +theorem itself is a mathematical dependency, not a program-proved result. + +These facts extend to K. Rational roots perpendicular to a nonzero +K-valued direction span a rational subspace of dimension at most seven. +If this dimension were at most six, choose a generic real normal to that +span. Its perpendicular roots are exactly the roots in that span; the +six-node parabolic bound allows at most 36 lines, contradicting 43. +Consequently, at support below 70 the perpendicular span has dimension +seven. Its rational kernel is one-dimensional, and the K-valued direction +is proportional to its rational generator. Apply the real argument to +that generator. Finally, the live-root Gram sum is 112 times the identity +in doubled coordinates, proving injectivity over K. + +The geometry code is unchanged from Nick Petalas's PR3164. Its exact +source pin and the preceding E8/P112 lineage are in SOURCES.json. + +## Four small pieces leave a root A5 simplex + +Choose the four smallest pieces s_1,...,s_4. Write S for the union of their +supports and s=|S|. The remaining pieces are q_0,...,q_5; put +U=sum_i |supp(q_i)|. For every proposed shape, the support-cap sum for S +plus any one q_i is at most 48, strictly below 53. + +Let D=T intersect C and lambda:T -> T/D. Since dim T=10 and dim D>=5, +the quotient has dimension at most five. The four small images together +with each q_i image are independent. A dependence would give a nonzero +codeword supported on fewer than 53 coordinates, contrary to fact 2. +Thus dim(T/D)=5, dim D=5, and the four small images are independent. + +Modulo their span, the six q_i images are nonzero in one dimension. +Rescale each q_i to give it the same image there. The supports do not change. +For i=1,...,5 there is a unique small-piece combination a_i with + +``` +c_i = q_i - q_0 - a_i in D. +``` + +Set c_0=a_0=0. The five c_i are independent, since their coefficients on +q_1,...,q_5 in the original piece basis are distinct unit vectors. Every +edge c_i-c_j is nonzero and supported on S union supp(q_i) union supp(q_j). +The largest edge-support cap in the five applications is 68, below 70. +By facts 3 and 4, c_i=c_{h_i} for five independent directions, and every +difference among 0,h_1,...,h_5 is a scalar root direction. + +Here is the root-simplex argument from PR3164 with its hypotheses retained. +Normalize roots to norm squared two. In the plane of two independent +rational E8 roots, a third root line exists only in an A2 subsystem, with +coefficient ratio +1 or -1. The replay verifies this for all 7,140 root-line +pairs and all 120 possible third roots. The same statement holds over K: +a rational vector in the K-span of two rational independent vectors is +already in their rational span, by an invertible rational coordinate minor. + +Write h_i=b_i alpha_i for roots alpha_i. Every h_i-h_j is a third root line, +so b_i/b_j is +1 or -1. Absorb these signs to write h_i=b alpha_i with one +common b!=0. Then =1 and alpha_i-alpha_j is a root. Thus +0,alpha_1,...,alpha_5 form a root A5 simplex. + +Each live coordinate r evaluates on its vertices in six integer levels, +all pairwise differences in {-2,-1,0,1,2}. If a difference has absolute +value two, equality in Cauchy-Schwarz makes r the corresponding edge root. +The value multiplicities are 1,1,4, with nine unequal pairs. Otherwise the +levels occupy at most two consecutive integers, with at most 3*3=9 unequal +pairs. Therefore each coordinate lies in at most nine of the fifteen edge +supports. The common nonzero field scalar changes no zeros. This is a +universal proof; the replay's sharp A5 fixture is a calibration only. + +## The new coordinate-budget inequality + +At a coordinate outside S, the edge values are exactly q_i(t)-q_j(t). +Suppose k of the six endpoint values are nonzero. There are at most + +``` +k(6-k) + k(k-1)/2 = k(11-k)/2 +``` + +unequal pairs. For every integer k=0,...,6, this is at most 4k+1, since +(k-1)(k-2)>=0. It is also at most 5k. This statement works for arbitrary +field-valued endpoints and needs no root-system assumption. + +There are exactly 112-s coordinates outside S. Summing the new bound gives + +``` +outside edge incidences <= 4 U_outside + 112-s <= 4U + 112-s. +``` + +Using the nine-incidence bound inside S, and the distance 53 on all fifteen +edges, yields + +``` +795 = 15*53 <= 9s + 4U + 112-s = 112 + 8s + 4U. (*) +``` + +The original endpoint count gives the additional bound `795 <= 9s+5U`. +Both right sides increase with s and U, so replacing them with their +support-cap sums is valid even when small supports overlap, when some +q_i support lies in S, or when the actual supports are smaller. + +| Ten-piece weights | Four small weights | s cap | U cap | New upper | Margin | Old margin | +|---|---|---:|---:|---:|---:|---:| +| `2,2,4,5,6^6` | `2,2,4,5` | 24 | 120 | 784 | 11 | -21 | +| `2,2,5^3,6^5` | `2,2,5,5` | 28 | 112 | 784 | 11 | -17 | +| `2,3,4^2,6^6` | `2,3,4,4` | 22 | 120 | 768 | 27 | -3 | +| `2,3,4,5^2,6^5` | `2,3,4,5` | 26 | 112 | 768 | 27 | 1 | +| `2,4^3,5,6^5` | `2,4,4,4` | 26 | 112 | 768 | 27 | 1 | + +Each row contradicts (*). The first three exclusions specifically require +the stronger coordinate budget; the original count cannot establish them. + +## Bind the applications and distinguish earlier coverage + +`beta.py` reproduces all 38 original `(5,5)` BK/BK7 survivors over all +weight multisets of lengths five through ten with weights two through seven. +The filters follow the two pinned TWOSIDE implementations. Their full +decoder-level derivation and generalized distances are inherited; the five +new exclusions themselves only need the explicit hypotheses stated above. +Replacing weights zero or one by two is conservative for support bounds. + +For every proposed shape, the replay examines every support-certified +five-piece quotient basis and every weight-certified cover by two six-flats +plus individual deleted supports. It checks the earlier eight-cut span-three, +ten-cut span-four and twelve-cut rank-four-anchor theorems. A nonbasis +weight-seven piece is conservatively charged one extra independent direction. +Minimum cut allowances in the five rows are `12,16,12,14,16`, all above ten. +The first three rows admit no weight-four anchor in a support-certified +quotient cover. The last two need at least eighteen cuts with such an anchor. + +This is an audit of those weight-certified rules. It does not exclude better +covers exploiting overlaps in actual supports, or prove that every other +research route was tried. A separate subset-cover oracle corroborates the +enumeration without its ternary-assignment implementation. + +The superficially similar shape `3,3,3,4,6^6` is deliberately excluded from +the new-result count. PR3167 already excludes it: use quotient basis +`3,3,3,6,6`, support cap 52, and twelve common extra lines. The nonbasis +weight-four piece supplies the rank-four anchor. This overlap control is +checked on every replay. A nine-piece PR3164 exclusion does not directly +cover a ten-piece configuration: deleting one piece only guarantees an +intersection of dimension four, rather than the required five. + +## Verification limits + +The proof uses the standard Weyl-chamber theorem and exact finite label/root +facts. It is not proof-kernel verified. Internal mathematical review and +separate enumeration methods are not independent human review. Other beta +shapes, full C5, the C1-C7 reduction and supplier admission remain separate +obligations. The selected exponent is unchanged. No full supplier replay, +Lean build or historical long suite is required or claimed for this result. diff --git a/research/p112-ten-piece-simplex/README.md b/research/p112-ten-piece-simplex/README.md new file mode 100644 index 0000000000..06d5a006a3 --- /dev/null +++ b/research/p112-ten-piece-simplex/README.md @@ -0,0 +1,99 @@ +# Five ten-piece P112 beta exclusions from a coordinate budget + +Ten independent P112 pieces with code intersection dimension at least five +cannot have any of these weight profiles: + +``` +2,2,4,5,6^6 +2,2,5^3,6^5 +2,3,4^2,6^6 +2,3,4,5^2,6^5 +2,4^3,5,6^5. +``` + +The theorem holds over every characteristic-zero field. These profiles occur +in the pinned TWOSIDE `(b,t)=(5,5)` residue. They are not excluded by the +weight-certified eight-cut, ten-cut or twelve-cut rank-four-anchor rules +audited here. No claim of a complete current residue count is made. + +Four small pieces leave six affine root-simplex vertices. The new step counts +the 112 available coordinates: six endpoint values with k nonzero entries +have at most 4k+1 unequal pairs. The required incidence inequality becomes + +``` +795 <= 112 + 8s + 4U, +``` + +where s is the small-support union size and U is the sum of the six remaining +support sizes. The five profile bounds give right sides 784,784,768,768,768, +with contradiction margins 11,11,27,27,27. The original endpoint-only count +fails on the first three profiles. [PROOF.md](PROOF.md) gives all hypotheses, +the characteristic-zero argument and the exact relationship to predecessors. + +[RESULT.json](RESULT.json) records the complete 4,097,782-flat replay, +7,140 root-plane checks, 960 reflections, original 38-shape weight residue, +five applications and an explicit overlap control. Sixteen behavioral groups +include an independently coded cover oracle, all endpoint equality patterns, +input mutations and valid support budgets where the contradiction fails. +The third initial candidate `3^3,4,6^6` was rejected as already covered by +PR3167 and remains a required control. + +This advances five finite decoder-floor cases. Full C5, `C(P112)>=64`, +supplier admission and an improved kappa remain open. The selected conditional +kappa remains `0.001672660197076918`. + +## Reproduce + +Requires Python 3.12 or later, standard library only. From the repository root: + +```sh +RUN="$HOME/.cache/integer-mult-bounds-runs/p112-ten-piece-replay" +mkdir -p "$RUN" +TMPDIR="$RUN" uv run --python 3.12 --no-project python -W error -B \ + scripts/research_package.py --package research/p112-ten-piece-simplex +``` + +An existing Python 3.12 executable can replace the `uv run` prefix. The +registered replay checks exact sources, reconstructs the mathematical receipt, +compares it to the committed JSON, and runs the behavioral controls with +optimization enabled. Both commands are bounded to 120 seconds and run +sequentially. Direct Git-free replay uses `verify.py` and `test_verify.py` +with this package and the single declared P112 input at its repository path. +`verify.py --output NEW_PATH` writes a new external receipt and refuses to +overwrite an existing path. No build, network or native dependency is needed +for the direct replay. [CHECKS.json](CHECKS.json) records environments and limits. + +## Open next questions + +Can the same coordinate accounting exclude `4,5^9`, another pinned ten-piece +survivor? The present four-small-piece support allowance is 44, and adding one +remaining weight-five support gives 56, above the distance 53. First find a +valid quotient normalization using the actual supports or prove a replacement +for that independence step. The current argument cannot assume that step. + +Can the root-simplex and endpoint-count lemmas be kernel-verified separately +from the finite E8 input? Start with six endpoint values and the root inner +products, then bind a verified label-capacity receipt. This package supplies +no proof-assistant environment. Structured questions are in [TASK.json](TASK.json). + +## Credit and scope + +Nick Petalas contributed the coordinate-budget strengthening and these five +ten-piece applications. DreamingOfClouds's [PR3154](https://github.com/CrocSwap/integer-mult-bounds/pull/3154) +supplies TWOSIDE and the open conjecture map. Nick Petalas's +[PR3164](https://github.com/CrocSwap/integer-mult-bounds/pull/3164) supplies the +root-simplex argument, geometry code and earlier nine-piece exclusions; +[PR3161](https://github.com/CrocSwap/integer-mult-bounds/pull/3161), +[PR3162](https://github.com/CrocSwap/integer-mult-bounds/pull/3162) and +[PR3167](https://github.com/CrocSwap/integer-mult-bounds/pull/3167) supply the +audited prior cover contracts. Geometry and label reconstruction retain the +E8/P112 and one-sided decoder lineage, including DreamingOfClouds's source +packages and joaqcoo's original decoder model. Exact heads, paths, Git blobs, +hashes and code origins are in [SOURCES.json](SOURCES.json). Predecessor files +are unchanged. New work and reused code are Apache-2.0. + +Internal read-only mathematical review corroborated the counting argument and +separately enumerated the prior covers. Independent human review, proof-kernel +verification and hosted CI are separate; none is claimed here. The Weyl-chamber +theorem is an explicit mathematical dependency. [ENGINEERING.md](ENGINEERING.md) +records implementation bounds and the decisions shaped by the engineering skills. diff --git a/research/p112-ten-piece-simplex/RESULT.json b/research/p112-ten-piece-simplex/RESULT.json new file mode 100644 index 0000000000..e12cc5acab --- /dev/null +++ b/research/p112-ten-piece-simplex/RESULT.json @@ -0,0 +1,863 @@ +{ + "schema": "p112-ten-piece-simplex/v1", + "input_sha256": "ac4a48851b922f2a433684b60c74768ae3bb4fc5e8990ffe63e3942bb3c2ea34", + "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 + } + } + ], + "simplex_control": { + "vertices": [ + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -2, + 2, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -2, + 0, + 2, + 0, + 0, + 0, + 0, + 0 + ], + [ + -2, + 0, + 0, + 2, + 0, + 0, + 0, + 0 + ], + [ + -2, + 0, + 0, + 0, + 2, + 0, + 0, + 0 + ], + [ + -2, + 0, + 0, + 0, + 0, + 2, + 0, + 0 + ] + ], + "histogram": [ + 2, + 0, + 0, + 0, + 0, + 36, + 0, + 0, + 42, + 32, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "beta": { + "multisets_examined": 7798, + "pinned_survivors": [ + [ + 2, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 3, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 4, + 5, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 2, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 2, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 2, + 3, + 5, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 3, + 5, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 2, + 3, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 4, + 4, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 4, + 4, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 2, + 4, + 5, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 5, + 5, + 5, + 6, + 6, + 6, + 6, + 6 + ], + [ + 3, + 3, + 5, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 3, + 4, + 4, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 2, + 2, + 2, + 6, + 7, + 7, + 7, + 7, + 7 + ], + [ + 2, + 2, + 2, + 3, + 5, + 7, + 7, + 7, + 7, + 7 + ], + [ + 2, + 2, + 2, + 4, + 4, + 7, + 7, + 7, + 7, + 7 + ], + [ + 2, + 2, + 2, + 5, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 2, + 2, + 5, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 2, + 2, + 2, + 5, + 6, + 6, + 6, + 6, + 7, + 7 + ], + [ + 2, + 2, + 2, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 2, + 2, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 2, + 2, + 3, + 5, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 2, + 3, + 5, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 2, + 2, + 3, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 2, + 4, + 4, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 2, + 4, + 4, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 2, + 2, + 4, + 5, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 2, + 5, + 5, + 5, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 3, + 3, + 4, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 3, + 3, + 4, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 2, + 3, + 3, + 5, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 3, + 4, + 4, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 3, + 4, + 5, + 5, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 4, + 4, + 4, + 5, + 6, + 6, + 6, + 6, + 6 + ], + [ + 3, + 3, + 3, + 4, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 4, + 5, + 5, + 5, + 5, + 5, + 5, + 5, + 5, + 5 + ] + ], + "new_exclusions": [ + { + "weights": [ + 2, + 2, + 4, + 5, + 6, + 6, + 6, + 6, + 6, + 6 + ], + "small_weights": [ + 2, + 2, + 4, + 5 + ], + "large_weights": [ + 6, + 6, + 6, + 6, + 6, + 6 + ], + "small_support_cap": 24, + "large_support_sum_cap": 120, + "quotient_support_cap": 44, + "edge_support_cap": 64, + "edge_incidence_lower": 795, + "original_incidence_upper": 816, + "coordinate_incidence_upper": 784, + "original_margin": -21, + "margin": 11, + "excluded": true, + "prior_cover_audit": { + "minimum_cuts": 12, + "minimum_anchor_cuts": null, + "quotient_weight_bases": 2, + "prior_exclusions": [] + } + }, + { + "weights": [ + 2, + 2, + 5, + 5, + 5, + 6, + 6, + 6, + 6, + 6 + ], + "small_weights": [ + 2, + 2, + 5, + 5 + ], + "large_weights": [ + 5, + 6, + 6, + 6, + 6, + 6 + ], + "small_support_cap": 28, + "large_support_sum_cap": 112, + "quotient_support_cap": 48, + "edge_support_cap": 68, + "edge_incidence_lower": 795, + "original_incidence_upper": 812, + "coordinate_incidence_upper": 784, + "original_margin": -17, + "margin": 11, + "excluded": true, + "prior_cover_audit": { + "minimum_cuts": 16, + "minimum_anchor_cuts": null, + "quotient_weight_bases": 2, + "prior_exclusions": [] + } + }, + { + "weights": [ + 2, + 3, + 4, + 4, + 6, + 6, + 6, + 6, + 6, + 6 + ], + "small_weights": [ + 2, + 3, + 4, + 4 + ], + "large_weights": [ + 6, + 6, + 6, + 6, + 6, + 6 + ], + "small_support_cap": 22, + "large_support_sum_cap": 120, + "quotient_support_cap": 42, + "edge_support_cap": 62, + "edge_incidence_lower": 795, + "original_incidence_upper": 798, + "coordinate_incidence_upper": 768, + "original_margin": -3, + "margin": 27, + "excluded": true, + "prior_cover_audit": { + "minimum_cuts": 12, + "minimum_anchor_cuts": null, + "quotient_weight_bases": 1, + "prior_exclusions": [] + } + }, + { + "weights": [ + 2, + 3, + 4, + 5, + 5, + 6, + 6, + 6, + 6, + 6 + ], + "small_weights": [ + 2, + 3, + 4, + 5 + ], + "large_weights": [ + 5, + 6, + 6, + 6, + 6, + 6 + ], + "small_support_cap": 26, + "large_support_sum_cap": 112, + "quotient_support_cap": 46, + "edge_support_cap": 66, + "edge_incidence_lower": 795, + "original_incidence_upper": 794, + "coordinate_incidence_upper": 768, + "original_margin": 1, + "margin": 27, + "excluded": true, + "prior_cover_audit": { + "minimum_cuts": 14, + "minimum_anchor_cuts": 18, + "quotient_weight_bases": 3, + "prior_exclusions": [] + } + }, + { + "weights": [ + 2, + 4, + 4, + 4, + 5, + 6, + 6, + 6, + 6, + 6 + ], + "small_weights": [ + 2, + 4, + 4, + 4 + ], + "large_weights": [ + 5, + 6, + 6, + 6, + 6, + 6 + ], + "small_support_cap": 26, + "large_support_sum_cap": 112, + "quotient_support_cap": 46, + "edge_support_cap": 66, + "edge_incidence_lower": 795, + "original_incidence_upper": 794, + "coordinate_incidence_upper": 768, + "original_margin": 1, + "margin": 27, + "excluded": true, + "prior_cover_audit": { + "minimum_cuts": 16, + "minimum_anchor_cuts": 18, + "quotient_weight_bases": 3, + "prior_exclusions": [] + } + } + ], + "overlap_control": { + "weights": [ + 3, + 3, + 3, + 4, + 6, + 6, + 6, + 6, + 6, + 6 + ], + "minimum_cuts": 12, + "minimum_anchor_cuts": 12, + "quotient_weight_bases": 2, + "prior_exclusions": [ + "PR3167:H4-p12" + ] + } + } +} diff --git a/research/p112-ten-piece-simplex/SOURCES.json b/research/p112-ten-piece-simplex/SOURCES.json new file mode 100644 index 0000000000..954f7f1aac --- /dev/null +++ b/research/p112-ten-piece-simplex/SOURCES.json @@ -0,0 +1,85 @@ +{ + "schema_version": 1, + "base_commit": "997e6a9ca7b4f95d50e366f61412fd640d72a88a", + "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-reduction-to-conjectures/checks/TWOSIDE/NOTES.md", + "usage": "provenance", + "pin": "head:708f0ad8928c383de8294aea3c126e9461d2066d:research/p112-reduction-to-conjectures/checks/TWOSIDE/NOTES.md", + "git_blob": "e3fd3f2b1dfd77b597f000b38ec2dbec3dbca931", + "sha256": "226cd59ccc6bc065319e5e4c4768c889206169ff58f74ef4053eeadc5b2e03c8" + }, + { + "path": "research/p112-reduction-to-conjectures/checks/TWOSIDE/bk1b.py", + "usage": "provenance", + "pin": "head:708f0ad8928c383de8294aea3c126e9461d2066d:research/p112-reduction-to-conjectures/checks/TWOSIDE/bk1b.py", + "git_blob": "7e73f346afb284ab9f4d08efc26c8006acb6da3a", + "sha256": "a045b1927675a59275e53008ea2de00b495f986ca95651e25052d85454ec19cf" + }, + { + "path": "research/p112-reduction-to-conjectures/checks/TWOSIDE/bk2b.py", + "usage": "provenance", + "pin": "head:708f0ad8928c383de8294aea3c126e9461d2066d:research/p112-reduction-to-conjectures/checks/TWOSIDE/bk2b.py", + "git_blob": "3394029014bb13f16225587a153fa7b70016de6d", + "sha256": "dff16eff255c883db372a587cf3f34e6f35c08f75c60af9d11952be5a5838807" + }, + { + "path": "research/p112-root-simplex-exclusion/PROOF.md", + "usage": "provenance", + "pin": "head:857384079ab640a949fb7618b7909664d3e737e5:research/p112-root-simplex-exclusion/PROOF.md", + "git_blob": "ccae08212784114e732da1192b336e47fc6a2091", + "sha256": "2b5d70570e3a13d2ccc71c1fc7eef113f0d049993cb9bb24007166223ac7b734" + }, + { + "path": "research/p112-root-simplex-exclusion/geometry.py", + "usage": "provenance", + "pin": "head:857384079ab640a949fb7618b7909664d3e737e5:research/p112-root-simplex-exclusion/geometry.py", + "git_blob": "222ea556faf2b275f73815c4e7d0d5f1e3294f2f", + "sha256": "b8ac379e41f5ad83bdb6c7f7c55129fc3d9c07801ea61591478f25d72ff0b021" + }, + { + "path": "research/p112-root-simplex-exclusion/simplex.py", + "usage": "provenance", + "pin": "head:857384079ab640a949fb7618b7909664d3e737e5:research/p112-root-simplex-exclusion/simplex.py", + "git_blob": "9cf0651b02f0e6b0ca9110f40b03c14715608185", + "sha256": "b50fb12f89fbc84e57a350d2398228e7e5a02d68ce8adf9eb5576869350c22b9" + }, + { + "path": "research/p112-ten-deletion-span/PROOF.md", + "usage": "provenance", + "pin": "head:ebd7fd275288e4a9f658e77fa77a0119a8322e74:research/p112-ten-deletion-span/PROOF.md", + "git_blob": "fb45b45d0ced71d3c9ed0b6523f8edaef28ded35", + "sha256": "6978f53d37a8e262bd9a443425441922c13508e19cb564e37f369f690ef4bfe8" + }, + { + "path": "research/p112-mixed-rank-anchor/PROOF.md", + "usage": "provenance", + "pin": "head:c2c7508f2d731feea550f1628601aebd35c6e147:research/p112-mixed-rank-anchor/PROOF.md", + "git_blob": "230c852f7e2033d50e3c1133c32cc1cf6efaaedb", + "sha256": "53bcf6a09b9a4119c1270c2a2d5d3339d97e3e3727e53917cb6a0684d49673f4" + } + ], + "code_origins": { + "geometry.py": "Byte-identical copy of PR3164 geometry.py", + "beta.py": "New ten-piece application and cover audit; filters from PR3154, incidence arithmetic adapted from PR3164 simplex.py", + "verify.py": "Data binding and sharp fixture adapted from PR3164 verify.py/simplex.py" + } +} diff --git a/research/p112-ten-piece-simplex/TASK.json b/research/p112-ten-piece-simplex/TASK.json new file mode 100644 index 0000000000..f86fb583e3 --- /dev/null +++ b/research/p112-ten-piece-simplex/TASK.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 6, + "base_commit": "997e6a9ca7b4f95d50e366f61412fd640d72a88a", + "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": "Prove a strengthened coordinate-budget root-simplex inequality and exclude five ten-piece TWOSIDE (5,5) beta profiles over characteristic-zero fields.", + "scope_change_reason": "The live C5 handoff requests finite decoder-floor progress. This session supplies an exact combinatorial proof and rerunnable finite dependencies, rather than a proof-assistant formalization. No Lean claim is made.", + "bottleneck_link": "Closes five explicit cases in the P112 decoder-floor reduction by a new coordinate count; does not admit a supplier or change kappa.", + "budget_minutes": 60, + "stop_rule": "Stop after verifying at least one new shape exclusion or falsifying the incidence premise; do not expand beyond the pinned (5,5) ten-piece cell. Target met with five exclusions.", + "outcome": "completed", + "evidence": "PROOF.md and RESULT.json; complete P112 flat/root replay, sixteen behavioral groups, independent subset-cover oracle and read-only internal mathematical review.", + "author": "Nick Petalas", + "ai_assistance": "Internal computational checks; independent human and proof-kernel review remain open.", + "open_questions": [ + { + "question": "Can the remaining ten-piece profile 4,5^9 be excluded with a valid quotient normalization?", + "why_it_matters": "It is another original (5,5) survivor for which this proof cannot establish quotient independence.", + "first_step": "Pin actual support hypotheses and derive a replacement for the 44+12<53 independence test, which fails.", + "blocked_by": "The existing distance/support-cap argument only gives 56, above 53." + }, + { + "question": "Can the endpoint-count and root-simplex lemmas be kernel-verified with exact input bindings?", + "why_it_matters": "Separates universal algebra from finite E8 quantities and reduces proof-audit obligations.", + "first_step": "Formalize six endpoint equality classes, then the A2 coefficient-ratio implication.", + "blocked_by": "No proof-assistant environment or checked finite-input import is supplied." + } + ] +} diff --git a/research/p112-ten-piece-simplex/VERIFY.json b/research/p112-ten-piece-simplex/VERIFY.json new file mode 100644 index 0000000000..46688d9e95 --- /dev/null +++ b/research/p112-ten-piece-simplex/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/one-sided-six-multisets/data/data.txt" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Full geometry and label binding; complete flat counts; five exclusions; exact committed-receipt equality and prior-cover overlap control." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 120, + "checks": "Sixteen behavioral groups, all endpoint equality patterns, independent subset-cover oracle, losing budgets and changed input controls under optimization." + } + ] +} diff --git a/research/p112-ten-piece-simplex/beta.py b/research/p112-ten-piece-simplex/beta.py new file mode 100644 index 0000000000..960c9a0398 --- /dev/null +++ b/research/p112-ten-piece-simplex/beta.py @@ -0,0 +1,145 @@ +"""Ten-piece applications and a bounded audit of earlier weight-cover rules. + +The filters follow DreamingOfClouds's PR3154 TWOSIDE. The incidence argument +extends Nick Petalas's PR3164; earlier cover theorems are PR3161/3162/3167. +Apache-2.0. Exact source heads are recorded in SOURCES.json. +""" + +from itertools import combinations, combinations_with_replacement, product + +from geometry import require + +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) +NEW_SHAPES = ((2, 2, 4, 5, 6, 6, 6, 6, 6, 6), + (2, 2, 5, 5, 5, 6, 6, 6, 6, 6), + (2, 3, 4, 4, 6, 6, 6, 6, 6, 6), + (2, 3, 4, 5, 5, 6, 6, 6, 6, 6), + (2, 4, 4, 4, 5, 6, 6, 6, 6, 6)) +ANCHOR_CONTROL = (3, 3, 3, 4, 6, 6, 6, 6, 6, 6) + + +def validate_weights(weights): + require(5 <= len(weights) <= 10 + and all(type(w) is int and w in CAP for w in weights) + and tuple(sorted(weights)) == tuple(weights), "invalid weight multiset") + + +def two_flat_cuts(weights): + """Minimum cardinality allowance outside two bins of dimension six.""" + require(len(weights) <= 5 and all(type(w) is int and w in CAP for w in weights), + "cover input") + best = sum(CAP[w] for w in weights) + for assignment in product(range(3), repeat=len(weights)): + if any(sum(w for w, a in zip(weights, assignment, strict=True) if a == k) > 6 + for k in (0, 1)): + continue + cuts = sum(CAP[w] for w, a in zip(weights, assignment, strict=True) if a == 2) + best = min(best, cuts) + return best + + +def original_survivor(weights): + """Exactly the pinned BK/BK7 necessary filters for b=5, t<=5.""" + validate_weights(weights) + if sum(w - 2 for w in weights) >= 30: + return False + for level in range(1, 6): + retained = weights[:len(weights) - (5 - level)] + global_cap = sum(CAP[w] for w in retained) + target_cap = sum(TARGET_CAP[w] for w in retained) + if level == 1 and target_cap < 53 and global_cap < 73: + return False + if level == 2 and target_cap < 78 and global_cap < 82: + return False + if level >= 3 and global_cap < DISTANCE[level]: + return False + basis = weights[:len(weights) - 5] + if sum(CAP[w] for w in basis) < 53: + if sum(basis) <= 7 or two_flat_cuts(basis) == 0: + return False + return True + + +def prior_cover_audit(weights): + """Search every quotient basis, including bases other than the smallest.""" + validate_weights(weights) + rho = len(weights) - 5 + best, best_anchor = 113, 113 + exclusions = set() + bases = set() + for indices in combinations(range(len(weights)), rho): + basis = tuple(weights[i] for i in indices) + if basis in bases or sum(CAP[w] for w in basis) >= 53: + continue + bases.add(basis) + complement = tuple(w for i, w in enumerate(weights) if i not in indices) + cuts = two_flat_cuts(basis) + best = min(best, cuts) + sevens = complement.count(7) + if cuts <= 8 and 3 + sevens < 5: + exclusions.add("PR3161:p8") + if cuts <= 10 and 4 + sevens < 5: + exclusions.add("PR3162:p10") + if any(w <= 4 for w in complement): + best_anchor = min(best_anchor, cuts) + if cuts <= 12 and 3 + sevens < 5: + exclusions.add("PR3167:H4-p12") + return {"minimum_cuts": None if best == 113 else best, + "minimum_anchor_cuts": None if best_anchor == 113 else best_anchor, + "quotient_weight_bases": len(bases), "prior_exclusions": sorted(exclusions)} + + +def incidence(small_cap, large_caps): + require(type(small_cap) is int and 0 <= small_cap <= 112 + and len(large_caps) == 6 + and all(type(n) is int and 0 <= n <= 112 for n in large_caps), + "invalid support bounds") + ordered = sorted(large_caps, reverse=True) + require(small_cap + ordered[0] < 53, "quotient independence is uncertified") + require(small_cap + sum(ordered[:2]) < 70, "root-edge hypothesis is uncertified") + large_sum = sum(large_caps) + original_upper = 9 * small_cap + 5 * large_sum + coordinate_upper = 112 + 8 * small_cap + 4 * large_sum + upper = min(original_upper, coordinate_upper) + return {"small_support_cap": small_cap, "large_support_sum_cap": sum(large_caps), + "quotient_support_cap": small_cap + ordered[0], + "edge_support_cap": small_cap + sum(ordered[:2]), + "edge_incidence_lower": 15 * 53, + "original_incidence_upper": original_upper, + "coordinate_incidence_upper": coordinate_upper, + "original_margin": 15 * 53 - original_upper, + "margin": 15 * 53 - upper, "excluded": 15 * 53 > upper} + + +def ten_piece_obstruction(weights): + validate_weights(weights) + require(len(weights) == 10 and max(weights) <= 6, "ten bounded pieces required") + return {"weights": list(weights), "small_weights": list(weights[:4]), + "large_weights": list(weights[4:]), + **incidence(sum(CAP[w] for w in weights[:4]), + [CAP[w] for w in weights[4:]])} + + +def beta_receipt(): + examined, survivors = 0, [] + for size in range(5, 11): + for weights in combinations_with_replacement(range(2, 8), size): + examined += 1 + if original_survivor(weights): + survivors.append(weights) + require(len(survivors) == 38, "pinned (5,5) survivor count") + applications = [] + for shape in NEW_SHAPES: + require(shape in survivors, "new shape is absent from the original residue") + audit = prior_cover_audit(shape) + require(not audit["prior_exclusions"], "proposed exclusion is already covered") + row = {**ten_piece_obstruction(shape), "prior_cover_audit": audit} + require(row["excluded"], "new exclusion margin") + applications.append(row) + overlap = prior_cover_audit(ANCHOR_CONTROL) + require("PR3167:H4-p12" in overlap["prior_exclusions"], "missed anchor overlap") + return {"multisets_examined": examined, "pinned_survivors": [list(w) for w in survivors], + "new_exclusions": applications, + "overlap_control": {"weights": list(ANCHOR_CONTROL), **overlap}} diff --git a/research/p112-ten-piece-simplex/geometry.py b/research/p112-ten-piece-simplex/geometry.py new file mode 100644 index 0000000000..222ea556fa --- /dev/null +++ b/research/p112-ten-piece-simplex/geometry.py @@ -0,0 +1,188 @@ +"""Exact E8/P112 geometry; coordinates follow PR3162's retained convention. + +Root and label reconstruction derive from Nick Petalas's PR3161/PR3162, +with the E8/P112 lineage retained in SOURCES.json. Apache-2.0. +""" + +from fractions import Fraction +from itertools import combinations, product +from math import gcd, lcm + +SIMPLE = ( + (1, -1, -1, -1, -1, -1, -1, 1), + (2, 2, 0, 0, 0, 0, 0, 0), + (-2, 2, 0, 0, 0, 0, 0, 0), + (0, -2, 2, 0, 0, 0, 0, 0), + (0, 0, -2, 2, 0, 0, 0, 0), + (0, 0, 0, -2, 2, 0, 0, 0), + (0, 0, 0, 0, -2, 2, 0, 0), + (0, 0, 0, 0, 0, -2, 2, 0), +) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def dot(a, b): + return sum(x * y for x, y in zip(a, b, strict=True)) + + +def canonical(row): + return max(tuple(row), tuple(-x for x in row)) + + +def primitive(row): + denominator = lcm(*(x.denominator for x in row)) + integers = tuple(int(x * denominator) for x in row) + divisor = gcd(*integers) + require(divisor != 0, "zero projective direction") + return canonical(tuple(x // divisor for x in integers)) + + +def root_lines(): + roots = set() + for i, j in combinations(range(8), 2): + for sign in (-2, 2): + row = [0] * 8 + row[i], row[j] = 2, sign + roots.add(canonical(row)) + for row in product((-1, 1), repeat=8): + if sum(x == -1 for x in row) % 2 == 0: + roots.add(canonical(row)) + require(len(roots) == 120, "E8 root-line count") + return tuple(sorted(roots)) + + +def frame_lines(): + frame = [] + for i in range(0, 8, 2): + for sign in (-2, 2): + row = [0] * 8 + row[i], row[i + 1] = 2, sign + frame.append(canonical(row)) + return tuple(frame) + + +def solve(matrix, rhs): + """Exact eight-dimensional elimination, also used by the chamber check.""" + require(len(matrix) == len(rhs) == 8, "linear-system dimension") + rows = [[Fraction(x) for x in row] + [Fraction(y)] + for row, y in zip(matrix, rhs, strict=True)] + require(all(len(row) == 9 for row in rows), "linear-system row dimension") + for col in range(8): + pivot = next((i for i in range(col, 8) if rows[i][col]), None) + require(pivot is not None, "singular linear system") + rows[col], rows[pivot] = rows[pivot], rows[col] + scale = rows[col][col] + rows[col] = [x / scale for x in rows[col]] + for i in range(8): + if i != col: + scale = rows[i][col] + rows[i] = [x - scale * y + for x, y in zip(rows[i], rows[col], strict=True)] + return tuple(row[8] for row in rows) + + +def root_data(): + roots, frame = root_lines(), frame_lines() + points = tuple(row for row in roots if row not in frame) + matrix = tuple(zip(*SIMPLE, strict=True)) + coordinates = tuple(solve(matrix, row) for row in roots) + require(all(x.denominator == 1 for row in coordinates for x in row), + "nonintegral simple-root coordinates") + by_root = dict(zip(roots, coordinates, strict=True)) + labels = tuple(1 | sum((int(x) % 2) << (i + 1) + for i, x in enumerate(by_root[row])) for row in points) + require(len(points) == len(set(labels)) == 112, "P112 inventory") + require(all(0 < x < 512 and x & 1 for x in labels), "odd binary labels") + require(all(sum(r[i] * r[j] for r in points) == 112 * (i == j) + for i in range(8) for j in range(8)), "P112 spans eight dimensions") + return roots, points, labels, coordinates + + +def chamber_receipt(roots, points, coordinates): + for root in roots: + for simple in SIMPLE: + pairing = dot(root, simple) + require(dot(simple, simple) == 8 and pairing % 4 == 0, + "simple reflection normalization") + reflected = canonical(tuple(x - (pairing // 4) * y + for x, y in zip(root, simple, strict=True))) + require(reflected in roots, "root system is not reflection closed") + require(all(all(x >= 0 for x in c) or all(x <= 0 for x in c) + for c in coordinates), "simple system positivity") + six_counts = [sum(all(c[i] == 0 for i in omitted) for c in coordinates) + for omitted in combinations(range(8), 2)] + rays = [primitive(solve(SIMPLE, [int(i == j) for i in range(8)])) + for j in range(8)] + ray_zeros = [sum(dot(h, r) == 0 for r in roots) for h in rays] + require(max(six_counts) == 36, "rank-six parabolic cap") + require(ray_zeros == [42, 28, 22, 14, 16, 23, 37, 63], "chamber rays") + root_directions = {primitive(tuple(map(Fraction, r))) for r in roots} + require(rays[7] in root_directions, "qualifying ray is not a root") + support_sizes = [sum(dot(r, t) != 0 for t in points) for r in roots] + require(sorted(support_sizes) == [53] * 112 + [56] * 8, "root support sizes") + # These finite facts support the Weyl-chamber proof in PROOF.md. + return {"simple_reflection_checks": 960, + "rank_six_parabolic_counts": six_counts, "ray_zero_counts": ray_zeros, + "root_support_histogram": {"53": 112, "56": 8}} + + +def root_plane_receipt(roots): + """Every third root line in a root plane is the A2 sum/difference.""" + require(len(roots) == len(set(roots)) == 120 + and all(len(r) == 8 and dot(r, r) == 8 for r in roots), + "normalized root-plane input") + gram = tuple(tuple(dot(a, b) for b in roots) for a in roots) + histogram = {2: 0, 3: 0} + for i, j in combinations(range(120), 2): + d = gram[i][j] + require(d in (-4, 0, 4), "nonparallel root inner product") + in_plane = [] + for k in range(120): + x, y = gram[i][k], gram[j][k] + determinant = 512 + 2 * d * x * y - 8 * (d*d + x*x + y*y) + if determinant == 0: + in_plane.append(k) + expected = {i, j} + if d: + third = canonical(tuple(a - (d // 4) * b + for a, b in zip(roots[i], roots[j], strict=True))) + require(third in roots, "missing A2 root") + expected.add(roots.index(third)) + require(set(in_plane) == expected, "unexpected third root line") + histogram[len(in_plane)] += 1 + return {str(k): v for k, v in histogram.items()} + + +def flat_capacity(labels, dimension): + require(dimension in (5, 6), "only five/six-flat capacities are supported") + require(len(labels) == len(set(labels)) == 112 + and all(type(x) is int and 0 < x < 512 and x & 1 for x in labels), + "invalid P112 labels") + all_lines = (1 << 112) - 1 + kernels = tuple(all_lines ^ sum(1 << i for i, label in enumerate(labels) + if (label & x).bit_count() & 1) for x in range(512)) + histogram = [0] * 113 + annihilator_dimension = 9 - dimension + for pivots in combinations(range(9), annihilator_dimension): + row_kernels = [] + for pivot in pivots: + free = tuple(c for c in range(pivot) if c not in pivots) + rows = tuple((1 << pivot) | sum(((code >> i) & 1) << col + for i, col in enumerate(free)) + for code in range(1 << len(free))) + row_kernels.append(tuple(kernels[row] for row in rows)) + for chosen in product(*row_kernels): + mask = all_lines + for row in chosen: + mask &= row + histogram[mask.bit_count()] += 1 + expected = {5: (3309747, 12), 6: (788035, 20)}[dimension] + require(sum(histogram) == expected[0], "incomplete annihilator census") + maximum = max(i for i, n in enumerate(histogram) if n) + require(maximum == expected[1], "flat capacity changed") + return {"dimension": dimension, "subspaces": sum(histogram), "maximum": maximum, + "histogram": {str(i): n for i, n in enumerate(histogram) if n}} diff --git a/research/p112-ten-piece-simplex/test_verify.py b/research/p112-ten-piece-simplex/test_verify.py new file mode 100644 index 0000000000..96c5bede65 --- /dev/null +++ b/research/p112-ten-piece-simplex/test_verify.py @@ -0,0 +1,155 @@ +"""Behavioral and mathematical controls; safe under Python optimization.""" + +from itertools import combinations, product +from pathlib import Path +import tempfile +import unittest + +from beta import (CAP, NEW_SHAPES, beta_receipt, incidence, + original_survivor, prior_cover_audit, ten_piece_obstruction, + two_flat_cuts) +from geometry import canonical, dot, require, root_data, root_plane_receipt +from verify import DATA, ROOT, bind_data, simplex_control + + +def subset_cut_oracle(weights): + """Independent cover formulation by disjoint subsets, no ternary assignment.""" + best = sum(CAP[w] for w in weights) + for left in range(1 << len(weights)): + if sum(w for i, w in enumerate(weights) if left >> i & 1) > 6: + continue + for right in range(1 << len(weights)): + if left & right or sum(w for i, w in enumerate(weights) if right >> i & 1) > 6: + continue + uncovered = sum(CAP[w] for i, w in enumerate(weights) + if not (left | right) >> i & 1) + best = min(best, uncovered) + return best + + +class MathematicalControls(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.roots, cls.points, cls.labels, _ = root_data() + + def test_five_new_shapes(self): + for shape, margin in zip(NEW_SHAPES, (11, 11, 27, 27, 27), strict=True): + self.assertTrue(original_survivor(shape)) + row = ten_piece_obstruction(shape) + self.assertEqual(row["margin"], margin) + self.assertTrue(row["excluded"]) + + def test_small_support_boundary_loses_the_contradiction(self): + self.assertEqual(incidence(25, [20]*6)["margin"], 3) + row = incidence(26, [20]*6) + self.assertEqual(row["margin"], -5) + self.assertFalse(row["excluded"]) + + def test_large_support_boundary_loses_the_contradiction(self): + self.assertEqual(incidence(26, [18, 20, 20, 20, 20, 20])["margin"], 3) + row = incidence(26, [19, 20, 20, 20, 20, 20]) + self.assertEqual(row["margin"], -1) + self.assertFalse(row["excluded"]) + + def test_original_count_does_not_prove_three_of_the_exclusions(self): + margins = [ten_piece_obstruction(shape)["original_margin"] for shape in NEW_SHAPES] + self.assertEqual(margins, [-21, -17, -3, 1, 1]) + + def test_quotient_and_root_thresholds_are_strict(self): + with self.assertRaisesRegex(ValueError, "quotient"): + incidence(33, [20] * 6) + with self.assertRaisesRegex(ValueError, "root-edge"): + incidence(30, [20] * 6) + + def test_invalid_support_inputs(self): + for small, large in ((-1, [20]*6), (True, [20]*6), (26, [20]*5), + (26, [20]*5 + [False]), (26, [113]*6)): + with self.assertRaises(ValueError): + incidence(small, large) + + def test_invalid_weights(self): + for weights in ((2, 3), (7,)*11, (6, 5, 4, 3, 2), (2, 3, 4, 5, 8)): + with self.assertRaises(ValueError): + original_survivor(weights) + with self.assertRaises(ValueError): + ten_piece_obstruction((2, 3, 4, 5, 6)) + + def test_original_residue_and_overlap_control(self): + result = beta_receipt() + self.assertEqual(len(result["pinned_survivors"]), 38) + self.assertEqual(result["overlap_control"]["minimum_anchor_cuts"], 12) + self.assertIn("PR3167:H4-p12", result["overlap_control"]["prior_exclusions"]) + + def test_all_alternative_quotient_bases(self): + for shape, minimum, anchor_minimum in zip(NEW_SHAPES, (12, 16, 12, 14, 16), + (None, None, None, 18, 18), strict=True): + answer = prior_cover_audit(shape) + self.assertEqual(answer["minimum_cuts"], minimum) + self.assertEqual(answer["minimum_anchor_cuts"], anchor_minimum) + self.assertEqual(answer["prior_exclusions"], []) + independent, anchor = 113, 113 + for indices in combinations(range(10), 5): + basis = tuple(shape[i] for i in indices) + if sum(CAP[w] for w in basis) >= 53: + continue + cuts = subset_cut_oracle(basis) + independent = min(independent, cuts) + if any(w <= 4 for i, w in enumerate(shape) if i not in indices): + anchor = min(anchor, cuts) + self.assertEqual((independent, None if anchor == 113 else anchor), + (minimum, anchor_minimum)) + + def test_cover_oracle_matches_independent_subsets(self): + for weights in product((2, 3, 4, 5, 6), repeat=3): + self.assertEqual(two_flat_cuts(weights), subset_cut_oracle(weights)) + + def test_two_level_and_edge_coordinate_incidence(self): + maximum = 0 + for values in product((0, 1), repeat=6): + count = sum(a != b for a, b in combinations(values, 2)) + maximum = max(maximum, count) + self.assertLessEqual(count, 9) + self.assertEqual(maximum, 9) + self.assertEqual(sum(a != b for a, b in combinations((-1, 1, 0, 0, 0, 0), 2)), 9) + + def test_outside_charge_for_arbitrary_endpoint_values(self): + for values in product((-1, 0, 1, 2), repeat=6): + unequal = sum(a != b for a, b in combinations(values, 2)) + nonzero = sum(v != 0 for v in values) + self.assertLessEqual(unequal, 5 * nonzero) + self.assertLessEqual(unequal, 4 * nonzero + 1) + + def test_charge_bound_for_all_zero_and_equality_patterns(self): + # Every possible equality relation among six endpoint values is + # represented using zero and at most six distinct nonzero values. + for values in product(range(7), repeat=6): + unequal = sum(a != b for a, b in combinations(values, 2)) + self.assertLessEqual(unequal, 4 * sum(v != 0 for v in values) + 1) + + def test_sharp_root_simplex(self): + result = simplex_control(self.roots, self.points) + self.assertGreater(result["histogram"][9], 0) + changed = list(self.roots) + changed[0] = changed[1] + with self.assertRaises(ValueError): + root_plane_receipt(changed) + + def test_bound_input_and_byte_mutation(self): + path = ROOT / DATA + self.assertEqual(len(bind_data(path, self.points, self.labels)), 64) + with tempfile.TemporaryDirectory() as temporary: + changed = Path(temporary) / "changed.txt" + changed.write_bytes(path.read_bytes() + b"\n") + with self.assertRaisesRegex(ValueError, "changed P112"): + bind_data(changed, self.points, self.labels) + + def test_root_evaluation_span_and_distance(self): + self.assertEqual({sum(dot(root, point) != 0 for point in self.points) + for root in self.roots}, {53, 56}) + self.assertEqual(len({canonical(row) for row in self.roots}), 120) + with self.assertRaises(ValueError): + require(False, "optimized Python must retain this guard") + + +if __name__ == "__main__": + unittest.main() diff --git a/research/p112-ten-piece-simplex/verify.py b/research/p112-ten-piece-simplex/verify.py new file mode 100644 index 0000000000..5d00d3d1f7 --- /dev/null +++ b/research/p112-ten-piece-simplex/verify.py @@ -0,0 +1,85 @@ +"""Replay the finite geometry, five ten-piece exclusions and overlap controls.""" + +import argparse +import hashlib +import json +from itertools import combinations +from pathlib import Path + +from beta import beta_receipt +from geometry import (canonical, chamber_receipt, dot, flat_capacity, require, + root_data, root_plane_receipt) + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parent.parent +DATA = "research/one-sided-six-multisets/data/data.txt" + + +def bind_data(path, points, labels): + require(path.is_file() and path.stat().st_size <= 2_000_000, "missing/large P112 input") + raw = path.read_bytes() + sources = json.loads((PACKAGE / "SOURCES.json").read_text()) + pins = [row for row in sources["files"] if row["usage"] == "input"] + require(len(pins) == 1 and pins[0]["path"] == DATA, "live-input inventory") + digest = hashlib.sha256(raw).hexdigest() + require(digest == pins[0]["sha256"], "changed P112 input") + rows = raw.decode("utf-8").splitlines() + require(len(rows) >= 114, "truncated P112 input") + require(tuple(map(int, rows[0].split())) == labels, "P112 label binding") + require(tuple(tuple(map(int, row.split())) for row in rows[2:114]) == points, + "P112 root binding") + return digest + + +def simplex_control(roots, points): + """Sharp fixture, supplementary to the universal proof in PROOF.md.""" + vertices = [(0,) * 8] + for i in range(1, 6): + vertex = [0] * 8 + vertex[0], vertex[i] = -2, 2 + vertices.append(tuple(vertex)) + edges = [canonical(tuple(x - y for x, y in zip(a, b, strict=True))) + for a, b in combinations(vertices, 2)] + require(len(set(edges)) == 15 and all(edge in roots for edge in edges), "A5 fixture") + histogram = [0] * 16 + for point in points: + values = [dot(point, vertex) for vertex in vertices] + count = sum(a != b for a, b in combinations(values, 2)) + histogram[count] += 1 + require(max(i for i, n in enumerate(histogram) if n) == 9, "nine-edge sharpness") + return {"vertices": vertices, "histogram": histogram} + + +def receipt(): + roots, points, labels, coordinates = root_data() + return {"schema": "p112-ten-piece-simplex/v1", + "input_sha256": bind_data(ROOT / DATA, points, labels), + "chamber": chamber_receipt(roots, points, coordinates), + "root_planes": root_plane_receipt(roots), + "flat_capacities": [flat_capacity(labels, d) for d in (5, 6)], + "simplex_control": simplex_control(roots, points), "beta": beta_receipt()} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, help="write a new external receipt") + args = parser.parse_args() + result = receipt() + serialized = json.dumps(result, indent=2) + "\n" + if args.output is None: + expected = json.loads((PACKAGE / "RESULT.json").read_text()) + require(json.loads(serialized) == expected, "committed receipt differs") + else: + output = args.output.expanduser().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) + rows = result["beta"]["new_exclusions"] + margins = ",".join(str(row["margin"]) for row in rows) + flats = sum(row["subspaces"] for row in result["flat_capacities"]) + print(f"PASS_P112_TEN_PIECE_SIMPLEX new_exclusions={len(rows)} " + f"margins={margins} flats={flats} errors=0") + + +if __name__ == "__main__": + main() From 2dbbd3004b70772cef200e341037c7c05b094fbc Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Sat, 17 Oct 2026 15:13:03 +0100 Subject: [PATCH 2/2] fix(research): make ten-piece source metadata portable --- research/p112-ten-piece-simplex/CHECKS.json | 4 ++ research/p112-ten-piece-simplex/README.md | 7 +++- research/p112-ten-piece-simplex/SOURCES.json | 39 +++++++++++++------- 3 files changed, 34 insertions(+), 16 deletions(-) diff --git a/research/p112-ten-piece-simplex/CHECKS.json b/research/p112-ten-piece-simplex/CHECKS.json index 59d39acdca..0ee38099bf 100644 --- a/research/p112-ten-piece-simplex/CHECKS.json +++ b/research/p112-ten-piece-simplex/CHECKS.json @@ -35,6 +35,10 @@ { "command": "Invoke verify.py --output on an in-checkout path and an existing external path", "result": "both reject; no in-checkout file created; existing receipt is not overwritten" + }, + { + "command": "Validate all historical source heads with the initial registered replay; retain their exact heads/blobs/hashes as historical citations, outside required replay pins", + "result": "historical source records verified locally; required replay provenance uses canonical main only and does not depend on unrelated PR commits or the contribution merge strategy" } ], "coverage": { diff --git a/research/p112-ten-piece-simplex/README.md b/research/p112-ten-piece-simplex/README.md index 06d5a006a3..bbf54f9488 100644 --- a/research/p112-ten-piece-simplex/README.md +++ b/research/p112-ten-piece-simplex/README.md @@ -89,8 +89,11 @@ root-simplex argument, geometry code and earlier nine-piece exclusions; audited prior cover contracts. Geometry and label reconstruction retain the E8/P112 and one-sided decoder lineage, including DreamingOfClouds's source packages and joaqcoo's original decoder model. Exact heads, paths, Git blobs, -hashes and code origins are in [SOURCES.json](SOURCES.json). Predecessor files -are unchanged. New work and reused code are Apache-2.0. +hashes and code origins are in [SOURCES.json](SOURCES.json). Historical source +records were checked locally; the replay uses the self-contained proof/code +and declared P112 input. Required provenance uses canonical main only, so +fresh CI needs no unrelated unmerged PR commits or preserved merge strategy. +Predecessor files are unchanged. New work and reused code are Apache-2.0. Internal read-only mathematical review corroborated the counting argument and separately enumerated the prior covers. Independent human review, proof-kernel diff --git a/research/p112-ten-piece-simplex/SOURCES.json b/research/p112-ten-piece-simplex/SOURCES.json index 954f7f1aac..3734af7a86 100644 --- a/research/p112-ten-piece-simplex/SOURCES.json +++ b/research/p112-ten-piece-simplex/SOURCES.json @@ -19,67 +19,78 @@ "usage": "input", "git_blob": "dc591a4e0252bac096e6c63c51058f6caee66bfe", "sha256": "ac4a48851b922f2a433684b60c74768ae3bb4fc5e8990ffe63e3942bb3c2ea34" - }, + } + ], + "code_origins": { + "geometry.py": "Byte-identical copy of PR3164 geometry.py", + "beta.py": "New ten-piece application and cover audit; filters from PR3154, incidence arithmetic adapted from PR3164 simplex.py", + "verify.py": "Data binding and sharp fixture adapted from PR3164 verify.py/simplex.py" + }, + "historical_sources": [ { "path": "research/p112-reduction-to-conjectures/checks/TWOSIDE/NOTES.md", "usage": "provenance", "pin": "head:708f0ad8928c383de8294aea3c126e9461d2066d:research/p112-reduction-to-conjectures/checks/TWOSIDE/NOTES.md", "git_blob": "e3fd3f2b1dfd77b597f000b38ec2dbec3dbca931", - "sha256": "226cd59ccc6bc065319e5e4c4768c889206169ff58f74ef4053eeadc5b2e03c8" + "sha256": "226cd59ccc6bc065319e5e4c4768c889206169ff58f74ef4053eeadc5b2e03c8", + "checked": "Git blob and SHA256 matched locally before publication; historical citation, not a replay dependency." }, { "path": "research/p112-reduction-to-conjectures/checks/TWOSIDE/bk1b.py", "usage": "provenance", "pin": "head:708f0ad8928c383de8294aea3c126e9461d2066d:research/p112-reduction-to-conjectures/checks/TWOSIDE/bk1b.py", "git_blob": "7e73f346afb284ab9f4d08efc26c8006acb6da3a", - "sha256": "a045b1927675a59275e53008ea2de00b495f986ca95651e25052d85454ec19cf" + "sha256": "a045b1927675a59275e53008ea2de00b495f986ca95651e25052d85454ec19cf", + "checked": "Git blob and SHA256 matched locally before publication; historical citation, not a replay dependency." }, { "path": "research/p112-reduction-to-conjectures/checks/TWOSIDE/bk2b.py", "usage": "provenance", "pin": "head:708f0ad8928c383de8294aea3c126e9461d2066d:research/p112-reduction-to-conjectures/checks/TWOSIDE/bk2b.py", "git_blob": "3394029014bb13f16225587a153fa7b70016de6d", - "sha256": "dff16eff255c883db372a587cf3f34e6f35c08f75c60af9d11952be5a5838807" + "sha256": "dff16eff255c883db372a587cf3f34e6f35c08f75c60af9d11952be5a5838807", + "checked": "Git blob and SHA256 matched locally before publication; historical citation, not a replay dependency." }, { "path": "research/p112-root-simplex-exclusion/PROOF.md", "usage": "provenance", "pin": "head:857384079ab640a949fb7618b7909664d3e737e5:research/p112-root-simplex-exclusion/PROOF.md", "git_blob": "ccae08212784114e732da1192b336e47fc6a2091", - "sha256": "2b5d70570e3a13d2ccc71c1fc7eef113f0d049993cb9bb24007166223ac7b734" + "sha256": "2b5d70570e3a13d2ccc71c1fc7eef113f0d049993cb9bb24007166223ac7b734", + "checked": "Git blob and SHA256 matched locally before publication; historical citation, not a replay dependency." }, { "path": "research/p112-root-simplex-exclusion/geometry.py", "usage": "provenance", "pin": "head:857384079ab640a949fb7618b7909664d3e737e5:research/p112-root-simplex-exclusion/geometry.py", "git_blob": "222ea556faf2b275f73815c4e7d0d5f1e3294f2f", - "sha256": "b8ac379e41f5ad83bdb6c7f7c55129fc3d9c07801ea61591478f25d72ff0b021" + "sha256": "b8ac379e41f5ad83bdb6c7f7c55129fc3d9c07801ea61591478f25d72ff0b021", + "checked": "Git blob and SHA256 matched locally before publication; historical citation, not a replay dependency." }, { "path": "research/p112-root-simplex-exclusion/simplex.py", "usage": "provenance", "pin": "head:857384079ab640a949fb7618b7909664d3e737e5:research/p112-root-simplex-exclusion/simplex.py", "git_blob": "9cf0651b02f0e6b0ca9110f40b03c14715608185", - "sha256": "b50fb12f89fbc84e57a350d2398228e7e5a02d68ce8adf9eb5576869350c22b9" + "sha256": "b50fb12f89fbc84e57a350d2398228e7e5a02d68ce8adf9eb5576869350c22b9", + "checked": "Git blob and SHA256 matched locally before publication; historical citation, not a replay dependency." }, { "path": "research/p112-ten-deletion-span/PROOF.md", "usage": "provenance", "pin": "head:ebd7fd275288e4a9f658e77fa77a0119a8322e74:research/p112-ten-deletion-span/PROOF.md", "git_blob": "fb45b45d0ced71d3c9ed0b6523f8edaef28ded35", - "sha256": "6978f53d37a8e262bd9a443425441922c13508e19cb564e37f369f690ef4bfe8" + "sha256": "6978f53d37a8e262bd9a443425441922c13508e19cb564e37f369f690ef4bfe8", + "checked": "Git blob and SHA256 matched locally before publication; historical citation, not a replay dependency." }, { "path": "research/p112-mixed-rank-anchor/PROOF.md", "usage": "provenance", "pin": "head:c2c7508f2d731feea550f1628601aebd35c6e147:research/p112-mixed-rank-anchor/PROOF.md", "git_blob": "230c852f7e2033d50e3c1133c32cc1cf6efaaedb", - "sha256": "53bcf6a09b9a4119c1270c2a2d5d3339d97e3e3727e53917cb6a0684d49673f4" + "sha256": "53bcf6a09b9a4119c1270c2a2d5d3339d97e3e3727e53917cb6a0684d49673f4", + "checked": "Git blob and SHA256 matched locally before publication; historical citation, not a replay dependency." } ], - "code_origins": { - "geometry.py": "Byte-identical copy of PR3164 geometry.py", - "beta.py": "New ten-piece application and cover audit; filters from PR3154, incidence arithmetic adapted from PR3164 simplex.py", - "verify.py": "Data binding and sharp fixture adapted from PR3164 verify.py/simplex.py" - } + "historical_source_contract": "Exact predecessor heads, blobs and hashes were validated locally. They are citations only; replay uses this package code/proof and the sole declared P112 input. Fresh CI needs only canonical-base provenance, so unrelated unmerged PR heads and later squash merges do not affect replay." }