From fd3c969f4d69cfd53e6057451a4b287c6263fc7f Mon Sep 17 00:00:00 2001 From: Chris R Date: Mon, 19 Oct 2026 18:01:00 +1100 Subject: [PATCH 1/2] Prove common24 P112 direction bound and exclude two literal C5 callers Check the complete root-normal cut domain by two implementations and bind the exact characteristic-zero quotients. Retain predecessor credit and all frozen inputs. --- research/p112-common24-caller/CHECKS.json | 44 ++++ .../p112-common24-caller/PREDECESSORS.json | 82 +++++++ research/p112-common24-caller/PROOF.md | 201 +++++++++++++++ research/p112-common24-caller/README.md | 101 ++++++++ research/p112-common24-caller/RESULT.json | 230 ++++++++++++++++++ research/p112-common24-caller/SOURCES.json | 42 ++++ research/p112-common24-caller/TASK.json | 88 +++++++ research/p112-common24-caller/VERIFY.json | 50 ++++ research/p112-common24-caller/independent.py | 215 ++++++++++++++++ research/p112-common24-caller/model.py | 124 ++++++++++ .../p112-common24-caller/test_controls.py | 133 ++++++++++ research/p112-common24-caller/verify.py | 230 ++++++++++++++++++ 12 files changed, 1540 insertions(+) create mode 100644 research/p112-common24-caller/CHECKS.json create mode 100644 research/p112-common24-caller/PREDECESSORS.json create mode 100644 research/p112-common24-caller/PROOF.md create mode 100644 research/p112-common24-caller/README.md create mode 100644 research/p112-common24-caller/RESULT.json create mode 100644 research/p112-common24-caller/SOURCES.json create mode 100644 research/p112-common24-caller/TASK.json create mode 100644 research/p112-common24-caller/VERIFY.json create mode 100644 research/p112-common24-caller/independent.py create mode 100644 research/p112-common24-caller/model.py create mode 100644 research/p112-common24-caller/test_controls.py create mode 100644 research/p112-common24-caller/verify.py diff --git a/research/p112-common24-caller/CHECKS.json b/research/p112-common24-caller/CHECKS.json new file mode 100644 index 0000000000..9b5d0b7baf --- /dev/null +++ b/research/p112-common24-caller/CHECKS.json @@ -0,0 +1,44 @@ +{ + "schema_version": 1, + "environment": "CPython3.12.3 / Linux x86-64; standard library only", + "scientific_base": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "prior_PR3951": { + "head": "9aacf01037f6e19cabb95ccbea15fcc2965dcd4d", + "CI": "https://github.com/CrocSwap/integer-mult-bounds/actions/runs/39210345012", + "CI_conclusion": "success", + "completed_UTC": "2026-10-19 06:34:09", + "entry_feedback": { + "comments": 0, + "submitted_reviews": 0, + "inline_threads": 0 + } + }, + "discovery": { + "primary_receipt_seconds": 19.749, + "final_receipt_seconds": 15.92, + "independent_finite_core": "PASS: Cramer/Bareiss labels, affine sections, record/candidate/admission digests agree", + "controls": "PASS:67 subspaces,12166 original filter multisets,77 historical survivors, separate21 minimum common44,2 semantic rejections,3 actual optimized CLI rejections" + }, + "timing_limit": "Single-run timings, not benchmarks.", + "development_corrections": [ + "Before final validation: fixed a proof-note line-join typo; changed literal witness verification to check all live residual sites before asserting completion containment.", + "Added all462 six-piece capacity-sum checks per caller; regenerated the receipt. No numerical bound changed." + ], + "verification_status": "PASS final complete registered replay: primary, separate finite-core checker and all behavioral/actual optimized CLI controls. PASS syntax, JSON, whitespace and metadata/source pins. Committed-byte/history, official committed export and hosted CI are post-commit obligations and will be reported with the exact publication head.", + "limits": [ + "No independent human or formal-kernel acceptance", + "No full C5, complete (5,6) cell, decoder floor, supplier, physical/native/restoration/consumer/all-size or multiplication theorem", + "No selected cold replay, Lean or Docker run", + "No lint pass claimed; syntax/JSON/whitespace checked", + "Snapshot overlap is partial for Discussions, closed/diff/private work" + ], + "frozen_inputs_unchanged": true, + "selected_frontier_unchanged": true, + "registered_command": "python3.12 -I -Werror -B scripts/research_package.py --package research/p112-common24-caller", + "registered_markers": [ + "PASS_COMMON24_CALLER spaces7=43435 cuts=6188 candidates=8540 directions<=2 callers=2", + "PASS_COMMON24_INDEPENDENT affine_spaces=43180 leading_zero=255 Cramer_roots=120 subset_join_candidates=8540", + "PASS_COMMON24_CONTROLS spaces4=67 original_multisets=12166 survivors=77 separate21_minimum_common=44 semantic_rejections=2 CLI_rejections=3", + "PASS_REGISTERED_RESEARCH_PACKAGE research/p112-common24-caller outcome=completed" + ] +} diff --git a/research/p112-common24-caller/PREDECESSORS.json b/research/p112-common24-caller/PREDECESSORS.json new file mode 100644 index 0000000000..04a5af294e --- /dev/null +++ b/research/p112-common24-caller/PREDECESSORS.json @@ -0,0 +1,82 @@ +{ + "schema_version": 1, + "pins": [ + { + "number": 3154, + "head": "708f0ad8928c383de8294aea3c126e9461d2066d", + "title": "C(P112) >= 64: complete reduction to stated conjectures", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3154", + "state": "open", + "merged": false, + "author": "DreamingOfClouds", + "role": "Original TWOSIDE/C5 and necessary filter, retained by PR3282; original author DreamingOfClouds." + }, + { + "number": 3163, + "head": "89419106cd86896c366e853795978f1bc85f9112", + "title": "test(research): certify a complete P112 common-deletion slice", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3163", + "state": "closed", + "merged": true, + "author": "petalas", + "role": "Complete fixed-first-space shared-four-deletion predecessor; retains the common-set quantifier and full-direction coverage." + }, + { + "number": 3269, + "head": "ebe02d33157dc6c6d3b35df204e4a39242b7429e", + "title": "Prove analytic E8 binary-support capacities 12 and 20", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3269", + "state": "closed", + "merged": true, + "author": "petalas", + "role": "Prior global binary support capacities12/20; rank-five12 is rechecked here." + }, + { + "number": 3282, + "head": "9607079de93907d87e6430d6de154f21a66c03e4", + "title": "Certify source-bound P112 caller coverage for the (6,4) cell", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3282", + "state": "closed", + "merged": true, + "author": "petalas", + "role": "Canonical retention of original filter and TWOSIDE note; conditional caller-inventory predecessor." + }, + { + "number": 3289, + "head": "e8570c50f9591c9ca653a527ed9626aaa703c3bc", + "title": "Reconcile original P112 cover contracts for three caller rows", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3289", + "state": "closed", + "merged": true, + "author": "petalas", + "role": "Original cover and quotient-composition predecessor, not a claim about the present public frontier." + }, + { + "number": 3931, + "head": "33b6be488be1e9e38f2f3f9bcfc4a7db0e8a332d", + "title": "Exclude a historical C5 caller with a common-cut23 bound", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3931", + "state": "open", + "merged": false, + "author": "Clear1nsight", + "role": "Same donor's prior common23 bound and different caller. Adjacent ten-piece cut22 reuse is credited, not a new geometric result." + }, + { + "number": 3951, + "head": "9aacf01037f6e19cabb95ccbea15fcc2965dcd4d", + "title": "Independently audit inherited P112 support and A2 bounds", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3951", + "state": "open", + "merged": false, + "author": "Clear1nsight", + "role": "Same donor's preceding dependency audit and chamber/field argument. model.py is explicitly adapted from its table model; the new core is separate." + } + ], + "geometry": { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3164", + "head": "857384079ab640a949fb7618b7909664d3e737e5", + "author": "Nick Petalas", + "role": "Root-simplex/geometry lineage, literal simple-system definition retained in canonical main." + }, + "runtime": "All executable inputs resolve at canonical main20ecf289. No pending predecessor Git object or executable is required by primary/independent replay; controls explicitly execute only authenticated original filter definitions." +} diff --git a/research/p112-common24-caller/PROOF.md b/research/p112-common24-caller/PROOF.md new file mode 100644 index 0000000000..264d263dfd --- /dev/null +++ b/research/p112-common24-caller/PROOF.md @@ -0,0 +1,201 @@ +# A common24 rank-seven bound and two literal C5 callers + +Fix the 120 doubled E8 root lines R, oriented by first nonzero coordinate, +the eight frame lines F = {2e_0 +/- 2e_1,...,2e_6 +/- 2e_7}, and P=R\F. +The original caller table orders P lexicographically. Its labels are +ell(r)=(1,c(r) mod2) in F2^9, where c(r) are the integral simple coordinates +in the pinned simple system. Binary weight means the rank of the actual +support labels, not the number of support sites. + +For a characteristic-zero field K put C={c_h : h in K^8}, where +c_h(r)=r dot h for r in P. Let Off(h) be its nonzero support. + +**Theorem.** For every ONE fixed S subset P of size at most 24, the nonzero +directions h with + + rank_F2 ell(Off(h)\S) <= 7 + +occupy at most TWO projective lines over K. Their K-linear span has +dimension at most two. A literal independent pair at a cut of size 24 +attains two. Sharpness of the cut allowance 24 is not claimed. + +**Caller corollary.** Eleven collectively independent pieces with binary +weight bounds either + + 2,2,2,2,3,5,7,7,7,7,7 + 2,2,2,2,4,4,7,7,7,7,7 + +cannot have dim(span(pieces) intersect C)>=5. These are two actual historical +TWOSIDE (b,t)=(5,6) profiles, each with strict excess deficit one. This is a +scoped exclusion, not the full cell, C5, a decoder floor, supplier admission +or a new kappa. + +## 1. Complete finite spaces and the root-normal reduction + +The primary reconstructs the 112 original table rows and adds exactly F. +It checks the elementary 56 two-coordinate and 64 all-odd E8 line patterns, +the nonsingular simple system, every exact coordinate reconstruction, uniform +simple-coordinate signs and the original 112 label bindings. The live Gram +matrix is 112 I_8. Evaluation is therefore injective over every characteristic- +zero K. The binary labels all have leading bit one. + +Every seven-space is the kernel of a unique two-dimensional annihilator +in reduced row-echelon form. The reversed-column enumeration chooses its +highest pivots and all free nonpivot entries below each pivot. Uniqueness of +RREF proves coverage and nonduplication. All 43,435 spaces are enumerated; +their full-root trace maximum is 36. Smaller residual spans extend to a +seven-space. Consequently a qualifying direction has + + |Off(h)| <= |S|+36 <= 60 < 70. + +Here is the needed chamber statement, including the field step. The checked +eight simple reflections permute all 240 signed roots (1,920 images). Since +these roots span, their generated group acts faithfully on a finite set and +is finite. The checked rational rho satisfies rho dot alpha_i=1. For a real +normal v maximize rho dot g(v) over this finite group. If g(v) dot alpha_i<0, +reflecting in alpha_i strictly increases that functional, a contradiction. +Thus g(v) is in the closed chamber. Uniform signs of the simple coordinates +imply that a root is perpendicular exactly when its simple support lies in +the zero simple pairings. The perpendicular roots are therefore a checked +simple face. This argument classifies full-root zero systems; no move is +assumed to preserve the removed frame or live support labels. + +The largest face on at most six simple nodes has 36 full root lines. The +seven-node face counts are 42,28,22,14,16,23,37,63. The last face has a single +normal root line. If the rational span Z of the live roots perpendicular to +a qualifying K-normal had rank at most six, choose a generic real normal +to Z avoiding all other root hyperplanes. Such a choice exists because a +finite union of proper hyperplanes cannot cover a real vector space. Its +perpendicular roots span Z, so its chamber face has rank at most six. +But it has at least 112-60=52 perpendicular live roots, contradicting 36. + +Thus Z has rational rank seven. Rational minors and Gaussian elimination +preserve this rank over any characteristic-zero K; its one-dimensional +rational kernel extends to the kernel over K and contains h. A rational +generator is real and has at least 52 perpendicular roots. Of the listed +seven-node faces only the 63-line face can occur. Its normal is a root, +and inverse reflection transport preserves the signed root set. Therefore +h is a K-scalar multiple of one of the 120 rational root normals. No embedding +of K into R or C is assumed. Direct evaluation gives support 53 for each +of the 112 live normals and 56 for each of the eight frame normals. + +## 2. Exact completion cuts, including frame normals + +For each root normal a and every binary seven-space V define + + C(a,V) = Off(a)\Lambda(V), + +where Lambda(V) is the live root trace of V. A normal qualifies under S +exactly when C(a,V) subset S for some V. This includes arbitrary partial +supports: extend their residual binary span to a seven-space. The primary +tests all 120*43,435=5,212,200 normal/space pairs. The root-word trace maximum +is 32. The complete records with |C(a,V)|<=24 are: + +| Normal type | Cut size | Records | +|---|---:|---:| +| Live | 21 | 336 | +| Live | 23 | 5,376 | +| Frame | 24 | 504 | + +There are 6,216 records and 6,188 distinct cuts. There are no other cut +sizes at most 24. Each of the 336 size-21 cuts has exactly one record, +hence one normal owner. Retaining frame normals is necessary at size 24. +Complete sorted record and flat-multiplicity digests, not just maxima, are +reconstructed and compared in RESULT.json. + +## 3. Why the finite common-cut test covers every S + +Make a graph on the 336 size-21 cuts, joining two distinct cuts when their +union has size at most 24. Exact comparison of every pair gives 168 edges, +each vertex of degree one: the graph is a perfect matching. Therefore no +set S of size at most 24 can contain three distinct size-21 cuts. Since +these cuts have single owners, they admit at most two normal directions. + +To cover any remaining possibility, enumerate all size-23 and size-24 cuts, +and all unions of one size-23 cut with any completion cut whenever the union +has size at most 24. These give exactly 8,540 candidate sets: + +| Size | Admitted normal directions | Candidate sets | +|---:|---:|---:| +| 23 | 1 | 5,376 | +| 24 | 1 | 448 | +| 24 | 2 | 2,716 | + +Suppose S admitted at least three distinct normals. Select one contained +completion cut for each. They cannot all have size 21 by the matching. +If a selected cut has size 24, it equals S and is a candidate. Otherwise +a selected cut B has size 23. If all selected cuts lie in B, B already +admits the normals and is a candidate. If some selected cut T does not +lie in B, then B union T has size 24, equals S, and is an enumerated +candidate. All cases contradict the table's maximum two. Arbitrary unused +sites in S do not invalidate this argument. It does not replace one common +cut by separately chosen cuts for different directions. + +The theorem follows over every characteristic-zero K because section 1 +reduces all directions to rational root lines. The pair witness lists the +actual live labels, root normals, seven-space trace masks and a positive +Gram determinant. Direct residual-label ranks verify its attainment. + +## 4. Two different literal caller bindings + +Let T be the span of either eleven-piece list in the corollary, with +D=T intersect C and dim D>=5. The quotient T/D has dimension at most six. +The first six pieces have support-cap sums + + 4*2+4+12=24, 4*2+8+8=24. + +Ranks two, three and four permit at most 2,4,8 leading-one points. The +rank-five capacity 12 is Nick Petalas's prior bound and is independently +rechecked on all 3,309,747 binary five-spaces here. Since 24<53, every +nonzero combination of these six independent pieces has support below +the code distance and cannot be a codeword. Their quotient images are +independent, so the quotient dimension is exactly six and dim D is exactly +five. Let S be their ONE actual support union, of size at most 24. + +For each of the five remaining weight-seven pieces q_y there is a unique +a_y in the six-piece span with c_y=q_y-a_y in C. These five codewords are +independent: their coefficients on the five distinct nonbasis pieces are +the identity matrix in the original independent piece basis. Injective +evaluation gives five independent h_y. Outside S their supports are subsets +of support(q_y), of binary rank at most seven. The theorem allows at most +two projective directions, contradicting five independent directions. +Coefficients, overlaps and cancellations are unrestricted over K. + +The pinned PR3154 filter is retained in canonical main by PR3282. Both +literal lists satisfy its necessary conditions and have +sum(w-2)=29<30. No failed sufficient filter is interpreted as a construction. +This proof does not assert that the two lists were the only publicly open +profiles or that (5,6) is closed. + +## 5. Independent implementation, predecessor credit and limits + +The primary uses the table model adapted from this donor's PR3951 and a +reversed-column annihilator enumeration. The separate checker imports no +primary or predecessor executable. It constructs the E8 shell, uses Cramer's +rule with integer Bareiss determinants for the labels, and enumerates all +10,795 binary six-spaces in F2^8 and their four affine cosets. These 43,180 +affine sections, plus 255 leading-zero seven-spaces, reproduce the entire +flat-multiplicity inventory and every critical record. + +Its common-cut composition uses different joins: size-23 cuts sharing a +22-subset, and size-23/21 pairs sharing a 20-subset. Admission is checked by +looking up the candidate's 21-,23- and24-subsets. Complete candidate/admission +digests agree with the primary union and per-normal containment loops. +This is computational corroboration in the same author/assistant context, +not independent human or formal-kernel acceptance. + +Credit Nick Petalas for the retained global capacities, root geometry, +root-shortening and shared-cut predecessors, including PR3163/3282/3289; +DreamingOfClouds/PR3154 for TWOSIDE and C5, David Arias for the quadratic model, +joaqcoo and the retained E8/P112 lineage. PR3931 already supplies a common23 +bound of three and a different caller; its adjacent 2^3,3,5,7^5 application +requires only cut22 and is not a new geometric theorem here. PR3951 supplies +the previous dependency audit and chamber/field argument. The new result is +the common24 bound and these two caller applications. The donor's adapted +model is credited, not presented as newly independent relative to PR3951. + +No full C5, complete decoder reduction, physical/supplier or multiplication +theorem, selected cold replay, new kappa, independent human review or formal +proof-kernel verification follows. Frozen predecessors and the selected +record remain unchanged. New work: Chris R / Clear1nsight, with substantial +OpenAI Codex assistance, Apache-2.0. diff --git a/research/p112-common24-caller/README.md b/research/p112-common24-caller/README.md new file mode 100644 index 0000000000..238d596f0a --- /dev/null +++ b/research/p112-common24-caller/README.md @@ -0,0 +1,101 @@ +# A common24 bound excludes two different literal C5 callers + +For ONE common set of at most **24 live P112 coordinates**, at most **two +projective characteristic-zero directions** have residual binary support rank +at most seven. Their linear span therefore has dimension at most two. A literal +independent pair at cut24 attains two. Sharpness of the cut allowance is unclaimed. + +This excludes the actual historical TWOSIDE `(b,t)=(5,6)` independent-piece +profiles **`2^4,3,5,7^5`** and **`2^4,4^2,7^5`** at code-intersection dimension +at least five. Their six small pieces have support-cap sums `8+4+12=24` and +`8+8+8=24`, both below code distance53. They form a quotient basis of dimension +six; the five remaining rank-seven pieces force five independent code directions, +contradicting the new limit two. All462 six-piece subsets are checked for each +profile; the minimum *capacity sum* is24, not a lower bound on actual unions. + +[PROOF.md](PROOF.md) states the quantifiers, finite coverage, chamber/field proof +and exact caller transfer. This is a scoped code theorem and two caller exclusions, +not full C5, the entire cell, a decoder floor, supplier or a new kappa. + +## Complete finite evidence + +The primary checks all **43,435 binary seven-spaces** and all **5,212,200** +root-normal/space pairs, including the eight frame normals. Exactly **6,216** +completion records have cuts through24:336 live cuts of size21,5,376 live cuts +of size23 and504 frame cuts of size24. They have6,188 distinct cut masks. + +The336 small cuts form a perfect matching with168 compatibility edges. A written +coverage argument then reduces every remaining common set through24 to **8,540** +explicit candidates. Each admits at most two root normals. Complete flat, +completion-record and admission digests are compared, not just maxima. + +A separate checker imports no primary or predecessor executable. It uses integer +Cramer's-rule/Bareiss labels, all43,180 affine six-sections plus255 leading-zero +spaces, subset joins and subset-based admission. It matches every finite-core +receipt. The primary model is explicitly adapted from this donor's PR3951; +the two implementations share the same author/assistant context. + +The root-normal reduction is proved from finite reflection closure, a chamber +maximum and rational kernels. It does not assume a general characteristic-zero +field embeds into the reals or that Weyl transformations preserve the removed +frame. Global rank-five capacity12 is prior work, credited and rechecked here +on all3,309,747 five-spaces. + +## Reproduce + +Python3.12, standard library only, from repository root: + +```sh +python3.12 -I -Werror -B scripts/research_package.py --package research/p112-common24-caller +``` + +VERIFY.json runs the primary, separate checker and behavioral controls under +`-I -O -Werror -B`, sequentially with180-second bounds. All direct commands work +from a source-only committed export containing the four declared inputs. Default +replay is read-only and compares RESULT.json. Controls use owned temporary copies. +SOURCES.json pins every input's SHA256/Git blob to canonical main20ecf289. +CHECKS.json records actual executions and limits. + +Controls include all67 binary subspaces of a four-space by exhaustive generating +subsets; all12,166 original `(5,6)` filter multisets, yielding77 historical +survivors; an actual independent attaining pair; five independent directions +with separate21-cuts whose minimum common union is44 across all243 choices; +characteristic-two loss; swapped-label/duplicate-key rejection; and three actual +optimized CLI corruptions, including a Boolean substituted for an integer-one +receipt field. + +## Selection, overlap and credit + +Explicit user follow-up to PR3951. Its exact9aacf01 CI passed and had no comments, +submitted reviews or inline review threads at entry. The nearby ten-piece +`2^3,3,5,7^5` already follows from PR3931's common23 theorem after binding its +five-piece quotient basis of support22; that is credited reuse. The new two +callers require the next capacity sum24. No novelty or universal frontier count +is inferred from historical filters or an incomplete contract inventory. + +Entry overlap checked657 open PR bodies including drafts,2,492 local records, +and rendered C5/handoff/start-here text. Discussion-wide refresh and arbitrary +closed/private/diff coverage remain partial. Canonical main and revision6 are +refreshed unchanged at research/publication checkpoints. Final overlap covered662 open PR bodies at06:58:54UTC; TASK.json records exact coverage. +Frozen predecessors and the selected frontier are unchanged. + +Credit Nick Petalas (global capacities, geometry, root-shortening/shared-cut +predecessors, PR3163/3282/3289), DreamingOfClouds/PR3154 (TWOSIDE/C5), David Arias +(quadratic model), joaqcoo and E8/P112 lineage; this donor's PR3931 and PR3951 +supply the previous theorem/audit context and adapted model. PREDECESSORS.json +retains exact heads and roles. New work by Chris R / Clear1nsight with substantial +OpenAI Codex assistance; Apache-2.0. No independent human or proof-kernel +acceptance is claimed. + +## Open next questions + +Review PROOF.md's generic-normal rank argument, the size21 matching reduction +and the complete common-cut candidate split. The executable checks are separate +from acceptance of those written implications. + +For another caller, first reconcile current public exclusions. The different +historical profile `2^5,6,7^5` has a preferred six-piece quotient support-cap sum +30 and needs five independent residual-rank-seven directions. The present24 +contract does not cover it; no current-public-frontier or nonexistence claim +is made about that profile. It requires a new, literal hypothesis check before +another census. This session stops after the two named exclusions. diff --git a/research/p112-common24-caller/RESULT.json b/research/p112-common24-caller/RESULT.json new file mode 100644 index 0000000000..864b5be89b --- /dev/null +++ b/research/p112-common24-caller/RESULT.json @@ -0,0 +1,230 @@ +{ + "analysis": { + "attaining_pair": { + "Gram_determinant": 64, + "completion_masks": [ + 250208855666007290719278910056951744, + 997164386914800566739725793531789312 + ], + "cut_labels": [ + 65, + 97, + 109, + 17, + 49, + 113, + 125, + 61, + 111, + 199, + 455, + 355, + 47, + 135, + 391, + 291, + 127, + 215, + 471, + 371, + 63, + 151, + 407, + 307 + ], + "normal_indices": [ + 12, + 30 + ], + "normals": [ + [ + 0, + 0, + 0, + 2, + -2, + 0, + 0, + 0 + ], + [ + 0, + 2, + -2, + 0, + 0, + 0, + 0, + 0 + ] + ] + }, + "candidate_admission_digest": "95bc481971a7c00e0fa2ac373fd933f5b6ddec3b7ada3c97c817032abfc890b1", + "candidate_direction_histogram": { + "23:1": 5376, + "24:1": 448, + "24:2": 2716 + }, + "candidate_sizes": { + "23": 5376, + "24": 3164 + }, + "maximum_directions": 2 + }, + "callers": [ + { + "basis_indices": [ + 0, + 1, + 2, + 3, + 4, + 5 + ], + "basis_support_cap": 24, + "cell": [ + 5, + 6 + ], + "independent_directions_required": 5, + "minimum_six_piece_capacity_sum": 24, + "proved_direction_limit": 2, + "quotient_dimension": 6, + "required_code_dimension": 5, + "six_piece_subsets_checked": 462, + "strict_excess_deficit": 1, + "weights": [ + 2, + 2, + 2, + 2, + 3, + 5, + 7, + 7, + 7, + 7, + 7 + ] + }, + { + "basis_indices": [ + 0, + 1, + 2, + 3, + 4, + 5 + ], + "basis_support_cap": 24, + "cell": [ + 5, + 6 + ], + "independent_directions_required": 5, + "minimum_six_piece_capacity_sum": 24, + "proved_direction_limit": 2, + "quotient_dimension": 6, + "required_code_dimension": 5, + "six_piece_subsets_checked": 462, + "strict_excess_deficit": 1, + "weights": [ + 2, + 2, + 2, + 2, + 4, + 4, + 7, + 7, + 7, + 7, + 7 + ] + } + ], + "chamber": { + "E7_normal": [ + 0, + 0, + 0, + 0, + 0, + 0, + 2, + 2 + ], + "rank6_face_maximum": 36, + "rho": [ + "0", + "1/2", + "1", + "3/2", + "2", + "5/2", + "3", + "23/2" + ], + "seven_node_counts": [ + 42, + 28, + 22, + 14, + 16, + 23, + 37, + 63 + ], + "signed_reflections": 1920 + }, + "critical_record_digest": "9a2dd7d5d850c3f4194f5c10bbb19a94fea41d1dc192e99a4e7096425f028ae7", + "critical_records": 6216, + "flat_inventory_digest": "5009cb750c3a5c0a1f71b0331892b3b34a4fb8f1c025a69c109516428d22efb9", + "full_trace5_histogram": { + "0": 99450, + "10": 548352, + "12": 107100, + "4": 321300, + "6": 913920, + "8": 1319625 + }, + "full_trace7_histogram": { + "0": 255, + "24": 5355, + "28": 16320, + "32": 16065, + "36": 5440 + }, + "root_trace_histogram": { + "0": 46856, + "1": 14224, + "10": 387072, + "11": 774144, + "12": 1067808, + "13": 230496, + "14": 556416, + "15": 830592, + "16": 812112, + "17": 145936, + "18": 48384, + "19": 59136, + "20": 41552, + "21": 5376, + "22": 5376, + "24": 3640, + "26": 10752, + "28": 4160, + "30": 5376, + "32": 840, + "4": 336, + "5": 112, + "6": 8064, + "7": 45696, + "8": 86912, + "9": 20832 + }, + "schema": "p112-common24-caller/v1", + "small_cut_matching_edges": 168, + "spaces7": 43435, + "unique_cuts": 6188 +} diff --git a/research/p112-common24-caller/SOURCES.json b/research/p112-common24-caller/SOURCES.json new file mode 100644 index 0000000000..e1c527c9c1 --- /dev/null +++ b/research/p112-common24-caller/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "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-b6-t4-reconciliation/vendor/PR3154-TWOSIDE.md", + "usage": "input", + "git_blob": "e3fd3f2b1dfd77b597f000b38ec2dbec3dbca931", + "sha256": "226cd59ccc6bc065319e5e4c4768c889206169ff58f74ef4053eeadc5b2e03c8" + }, + { + "path": "research/p112-b6-t4-reconciliation/vendor/bk2b.py", + "usage": "input", + "git_blob": "3394029014bb13f16225587a153fa7b70016de6d", + "sha256": "dff16eff255c883db372a587cf3f34e6f35c08f75c60af9d11952be5a5838807" + }, + { + "path": "research/p112-root-simplex-exclusion/geometry.py", + "usage": "input", + "git_blob": "222ea556faf2b275f73815c4e7d0d5f1e3294f2f", + "sha256": "b8ac379e41f5ad83bdb6c7f7c55129fc3d9c07801ea61591478f25d72ff0b021" + } + ] +} diff --git a/research/p112-common24-caller/TASK.json b/research/p112-common24-caller/TASK.json new file mode 100644 index 0000000000..2a13fa71bd --- /dev/null +++ b/research/p112-common24-caller/TASK.json @@ -0,0 +1,88 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "Common24 rank-seven direction bound of two over every characteristic-zero field; exact quotient and exclusion of literal historical (5,6) callers 2^4,3,5,7^5 and2^4,4^2,7^5.", + "scope_change_reason": "Explicit user follow-up to PR3951; no task reroll. Live overlap and current source contracts are reconciled before investigating the next literal caller.", + "bottleneck_link": "The eleven-piece (5,6) caller needs five independent residual-rank-seven directions after one common24-site cut. A span bound below five would exclude it without a general two-flat rank-seven census.", + "budget_minutes": 60, + "stop_rule": "Finish one bounded common24 root-direction certificate or literal obstruction; stop geometric expansion once this caller is decided. Keep final quarter for independent checks, exact sources and handoff.", + "outcome": "completed", + "evidence": "All43435 binary7spaces,5212200 normal/space traces,6216 records,6188 cuts,8540 complete common-cut candidates; separate affine/Cramer/subset implementation agrees. Two literal callers force5 independent directions in quotient dimension6; common support cap24.", + "author": "Chris R / Clear1nsight with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance; same donor/assistant as PR3931/3951, no independent human or formal-kernel review.", + "open_questions": [ + { + "question": "Can an independent reviewer validate the root-normal rank argument and common-cut candidate split?", + "why_it_matters": "The complete finite tables still require their written coverage and scalar-extension implications.", + "first_step": "Challenge PROOF.md sections1 and3 against both executable enumeration methods.", + "blocked_by": "No independent human or formal-kernel acceptance is claimed." + }, + { + "question": "Does a different actual caller such as 2^5,6,7^5 admit another valid reduction?", + "why_it_matters": "Its preferred six-piece quotient cap30 exceeds the new24 bound.", + "first_step": "Refresh public overlap and establish its exact quotient/support constraints before another census.", + "blocked_by": "Its actual coefficient/common-support obligation is outside this session." + } + ], + "freshness": { + "canonical_main": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "priority_revision": 6, + "entry_open_PR_bodies": 657, + "final_open_PR_bodies": 662, + "final_PR_snapshot_completed_UTC": "2026-10-19 06:58:54 UTC", + "local_records": 2492, + "Discussion_coverage": "partial: rendered C5, latest loaded handoff and start-here; no all-Discussion refresh", + "selected_frontier_unchanged": true + } +} diff --git a/research/p112-common24-caller/VERIFY.json b/research/p112-common24-caller/VERIFY.json new file mode 100644 index 0000000000..d2ba9b2e10 --- /dev/null +++ b/research/p112-common24-caller/VERIFY.json @@ -0,0 +1,50 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/one-sided-six-multisets/data/data.txt", + "research/p112-b6-t4-reconciliation/vendor/PR3154-TWOSIDE.md", + "research/p112-b6-t4-reconciliation/vendor/bk2b.py", + "research/p112-root-simplex-exclusion/geometry.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "All43435 binary7spaces, all5212200 root-word traces, complete6216 records and8540 common-cut candidates; global5capacity, chamber/field facts and two exact caller bindings." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 180, + "checks": "No primary/predecessor import: Cramer/Bareiss labels,43180 affine generator sections, subset joins and complete record/admission digest agreement." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/test_controls.py" + ], + "timeout_seconds": 180, + "checks": "Complete67-small-space oracle; original filter; actual independent pair; separate/common cut control; char2 and label/JSON failures; three actual optimized CLI corruptions." + } + ] +} diff --git a/research/p112-common24-caller/independent.py b/research/p112-common24-caller/independent.py new file mode 100644 index 0000000000..8910cae770 --- /dev/null +++ b/research/p112-common24-caller/independent.py @@ -0,0 +1,215 @@ +#!/usr/bin/env python3 +"""Separate finite-core check: Cramer's rule, affine generator spaces, subset joins. + +No primary or predecessor executable is imported. Same author/assistant context; +this is computational corroboration, not independent human or kernel acceptance. +Chris R / Clear1nsight with substantial OpenAI Codex assistance; Apache-2.0. +""" +import ast +from collections import Counter, defaultdict +import hashlib +from itertools import combinations, product +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +MANIFEST_SHA = '4d49389e8131d6ec139722f60e12d697e4d0d31eba205b5e6d11543d22b4afd3' + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def unique(pairs): + result = {} + for key,value in pairs: + need(key not in result, 'duplicate JSON key') + result[key] = value + return result + + +def digest(value): + return hashlib.sha256(json.dumps(value,sort_keys=True,separators=(',',':')).encode()).hexdigest() + + +def sources(): + raw = (HERE/'SOURCES.json').read_bytes() + need(hashlib.sha256(raw).hexdigest() == MANIFEST_SHA, 'source manifest identity') + result = {} + for row in json.loads(raw,object_pairs_hook=unique)['files']: + if row['usage'] != 'input': + continue + p = ROOT/row['path'] + need(not any(x.is_symlink() for x in [p,*p.parents]), 'input symlink') + data = p.read_bytes() + need(len(data)<=2_000_000 and hashlib.sha256(data).hexdigest()==row['sha256'], 'source SHA256') + need(hashlib.sha1(b'blob '+str(len(data)).encode()+b'\0'+data).hexdigest()==row['git_blob'], 'Git blob') + result[row['path']] = data + return result + + +def determinant(matrix): + a = [list(row) for row in matrix] + previous,sign = 1,1 + for k in range(len(a)-1): + pivot = next((i for i in range(k,len(a)) if a[i][k]),None) + if pivot is None: + return 0 + if pivot != k: + a[k],a[pivot] = a[pivot],a[k] + sign = -sign + p = a[k][k] + for i in range(k+1,len(a)): + for j in range(k+1,len(a)): + value = p*a[i][j]-a[i][k]*a[k][j] + need(value%previous == 0, 'Bareiss exact division') + a[i][j] = value//previous + a[i][k] = 0 + previous = p + return sign*a[-1][-1] + + +def reconstruct(payloads): + text = payloads['research/one-sided-six-multisets/data/data.txt'].decode().splitlines() + live_rows = [tuple(map(int,line.split())) for line in text[2:114]] + geometry = ast.parse(payloads['research/p112-root-simplex-exclusion/geometry.py']) + simple = next(ast.literal_eval(n.value) for n in geometry.body if isinstance(n,ast.Assign) + and any(isinstance(t,ast.Name) and t.id=='SIMPLE' for t in n.targets)) + frame = {tuple((2 if k==i else 2*s if k==i+1 else 0) for k in range(8)) + for i in range(0,8,2) for s in [-1,1]} + all_rows = set() + for i,j in combinations(range(8),2): + for sign in [-1,1]: + all_rows.add(tuple(2 if k==i else 2*sign if k==j else 0 for k in range(8))) + for tail in product([-1,1],repeat=7): + if sum(x<0 for x in tail)%2 == 0: + all_rows.add((1,*tail)) + roots = sorted(all_rows) + need(len(roots)==120 and sorted(all_rows-frame)==live_rows, 'literal E8 shell/frame') + matrix = [list(row) for row in zip(*simple)] + det = determinant(matrix) + need(det != 0, 'simple system invertible') + labels = [] + for r in roots: + coords = [] + for j in range(8): + modified = [row[:] for row in matrix] + for i in range(8): + modified[i][j] = r[i] + numerator = determinant(modified) + need(numerator%det==0, 'integral Cramer coordinates') + coords.append(numerator//det) + need(all(sum(coords[j]*simple[j][i] for j in range(8))==r[i] for i in range(8)), 'Cramer reconstruction') + labels.append(1+sum((x%2)<<(j+1) for j,x in enumerate(coords))) + live = sum(1<>i&1] == list(map(int,text[0].split())), 'original label binding') + return roots,labels,live + + +def affine_inventory(labels): + point = {x>>1:1<p] + for word in range(1<>bit&1: + rows[i] |= 1<>i&1)<>i&1 and sum(x*y for x,y in zip(r,normal))) + for mask,multiplicity in inventory.items(): + traces[(word&mask).bit_count()] += multiplicity + cut = word&~mask + if cut.bit_count()<=24: + records.extend([(a,mask,cut)]*multiplicity) + records.sort() + owners = defaultdict(set) + for a,_,cut in records: + owners[cut].add(a) + small = [c for c in owners if c.bit_count()==21] + medium = [c for c in owners if c.bit_count()==23] + candidates = {c for c in owners if c.bit_count()>=23} + joins20,joins22 = defaultdict(list),defaultdict(list) + for s in small: + for bit in range(120): + if s>>bit&1: + joins20[s^(1<>i&1] + for bit in positions: + joins22[s^bit].append(s) + for x,y,z in combinations(positions,3): + for t in joins20.get(s^x^y^z,()): + candidates.add(s|t) + for group in joins22.values(): + for s,t in combinations(group,2): + candidates.add(s|t) + edges = [(s,t) for s,t in combinations(small,2) if (s|t).bit_count()<=24] + degrees = Counter(c for pair in edges for c in pair) + need(len(small)==336 and len(edges)==168 and set(degrees.values())=={1}, 'small-cut matching') + admitted,counts = [],Counter() + for p in sorted(candidates): + normals = set(owners.get(p,())) + positions = [1<>i&1] + if len(positions)==24: + for bit in positions: + normals.update(owners.get(p^bit,())) + for deleted in combinations(positions,len(positions)-21): + q = p + for bit in deleted: + q ^= bit + normals.update(owners.get(q,())) + need(len(normals)<=2, 'independent common24 upper bound') + ns = sorted(normals) + counts[(p.bit_count(),len(ns))] += 1 + admitted.append((p,ns)) + return {'spaces7':sum(inventory.values()), + 'full_trace7_histogram':{str(k):v for k,v in sorted(Counter({s:sum(n for m,n in inventory.items() if m.bit_count()==s) for s in set(m.bit_count() for m in inventory)}).items())}, + 'flat_inventory_digest':digest(sorted(inventory.items())), + 'root_trace_histogram':{str(k):v for k,v in sorted(traces.items())}, + 'critical_records':len(records), 'critical_record_digest':digest(records), + 'unique_cuts':len(owners), 'small_cut_matching_edges':len(edges), + 'analysis':{'candidate_sizes':{str(s):sum(p.bit_count()==s for p in candidates) for s in [23,24]}, + 'candidate_direction_histogram':{f'{s}:{n}':v for (s,n),v in sorted(counts.items())}, + 'candidate_admission_digest':digest(admitted),'maximum_directions':2}} + + +def compute(): + roots,labels,live = reconstruct(sources()) + return core(roots,labels,live,affine_inventory(labels)) + + +def main(): + need(not sys.argv[1:], 'no arguments accepted') + observed = compute() + expected = json.loads((HERE/'RESULT.json').read_bytes(),object_pairs_hook=unique) + for key,value in observed.items(): + target = {k:expected[key][k] for k in value} if key=='analysis' else expected[key] + need(json.dumps(value,sort_keys=True)==json.dumps(target,sort_keys=True), 'independent receipt mismatch: '+key) + print('PASS_COMMON24_INDEPENDENT affine_spaces=43180 leading_zero=255 Cramer_roots=120 subset_join_candidates=8540') + + +if __name__ == '__main__': + main() diff --git a/research/p112-common24-caller/model.py b/research/p112-common24-caller/model.py new file mode 100644 index 0000000000..951f5344c5 --- /dev/null +++ b/research/p112-common24-caller/model.py @@ -0,0 +1,124 @@ +"""Table model adapted from PR3951 (Chris R / Clear1nsight). +No predecessor executable is imported. New rank-seven computation is in verify.py. + +Chris R / Clear1nsight with substantial OpenAI Codex assistance. Apache-2.0. +Definitions retain Nick Petalas, David Arias and the E8/P112 lineage. +""" + +import ast +from fractions import Fraction +from itertools import combinations, product + +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(ok, message): + if not ok: + raise ValueError(message) + + +def dot(a, b): + return sum(x * y for x, y in zip(a, b, strict=True)) + + +def canonical(row): + return row if next(x for x in row if x) > 0 else tuple(-x for x in row) + + +def basis(values, width=9): + rows = [0] * width + for value in values: + for j in range(width - 1, -1, -1): + if value >> j & 1: + if rows[j]: + value ^= rows[j] + else: + rows[j] = value + break + return [row for row in rows if row] + + +def span(rows): + values = [0] + for row in rows: + values += [x ^ row for x in values] + return values + + +def solve(matrix, columns): + """Exact dense simultaneous solve, independent of triangular source formulas.""" + n = len(matrix) + a = [[Fraction(x) for x in row] + [Fraction(c[i]) for c in columns] + for i, row in enumerate(matrix)] + for j in range(n): + p = next(i for i in range(j, n) if a[i][j]) + a[j], a[p] = a[p], a[j] + scale = a[j][j] + a[j] = [x / scale for x in a[j]] + for i in range(n): + if i != j: + scale = a[i][j] + a[i] = [x - scale * y for x, y in zip(a[i], a[j], strict=True)] + return [tuple(row[j] for row in a) for j in range(n, len(a[0]))] + + +def reconstruct(table, geometry): + assignments = ast.parse(geometry).body + literal = next(ast.literal_eval(n.value) for n in assignments + if isinstance(n, ast.Assign) + and any(isinstance(t, ast.Name) and t.id == 'SIMPLE' for t in n.targets)) + require(literal == SIMPLE, 'simple-system definition binding') + lines = table.decode().splitlines() + live = [tuple(map(int, line.split())) for line in lines[2:114]] + original_labels = list(map(int, lines[0].split())) + frame = [tuple(2 * (i == a) + s * 2 * (i == a + 1) for i in range(8)) + for a in (0, 2, 4, 6) for s in (-1, 1)] + roots = sorted(live + frame) + shell = {tuple(2 * (k == i) + s * (k == j) for k in range(8)) + for i, j in combinations(range(8), 2) for s in (-2, 2)} + shell.update((1, *t) for t in product((-1, 1), repeat=7) if sum(t) % 4 == 3) + require(roots == sorted(shell) and len(roots) == 120, 'full E8 root patterns') + coordinates = solve(list(zip(*SIMPLE, strict=True)), roots) + require(all(x.denominator == 1 for c in coordinates for x in c), 'integral coordinates') + coordinates = [tuple(map(int, c)) for c in coordinates] + require(all(tuple(sum(c[i] * SIMPLE[i][j] for i in range(8)) for j in range(8)) == r + for r, c in zip(roots, coordinates, strict=True)), 'exact coordinate equations') + require(all(min(c) >= 0 or max(c) <= 0 for c in coordinates), 'simple-coordinate signs') + labels = [1 + sum((x % 2) << (i + 1) for i, x in enumerate(c)) for c in coordinates] + require(len(set(labels)) == 120 and all(x & 1 for x in labels), 'full affine labels') + require([x for r, x in zip(roots, labels) if r not in frame] == original_labels, + 'original caller label convention') + live_mask = sum(1 << i for i, r in enumerate(roots) if r in live) + require(live_mask.bit_count() == 112 and live == sorted(live), 'literal P112 frame') + require(all(sum(r[i] * r[j] for r in live) == 112 * (i == j) + for i in range(8) for j in range(8)), 'evaluation Gram') + return roots, labels, coordinates, live_mask + + +def annihilators(n, dimension): + """Unique reduced row-echelon annihilators, highest pivot convention.""" + for pivots in combinations(range(n), n - dimension): + choices = [] + for pivot in pivots: + free = [j for j in range(pivot) if j not in pivots] + choices.append([(1 << pivot) | sum(((c >> k) & 1) << j + for k, j in enumerate(free)) for c in range(1 << len(free))]) + yield from product(*choices) + + +def kernels(labels, ambient): + locations = {x: i for i, x in enumerate(span(ambient))} + inside = [(i, locations[x]) for i, x in enumerate(labels) if x in locations] + return [sum(1 << i for i, x in inside if (h & x).bit_count() % 2 == 0) + for h in range(1 << len(ambient))] + + +def masks(ker, rows): + for annihilator in rows: + mask = ker[0] + for h in annihilator: + mask &= ker[h] + yield mask diff --git a/research/p112-common24-caller/test_controls.py b/research/p112-common24-caller/test_controls.py new file mode 100644 index 0000000000..6cbb91e21b --- /dev/null +++ b/research/p112-common24-caller/test_controls.py @@ -0,0 +1,133 @@ +#!/usr/bin/env python3 +"""Behavioral, mathematical and actual optimized CLI controls; owned copies only. + +Chris R / Clear1nsight, substantial OpenAI Codex assistance; Apache-2.0. +""" +import ast +from itertools import combinations_with_replacement, product +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +sys.path.insert(0,str(HERE)) +import verify as v +import independent as other + + +def rejection(call, message): + try: + call() + except (ValueError,KeyError): + return + raise ValueError('failed rejection: '+message) + + +def run(): + payloads = v.authenticate() + roots,labels,coords,live = v.m.reconstruct(payloads[v.TABLE],payloads[v.GEOMETRY]) + # Complete generating-subset oracle, independent of any RREF convention. + oracle = set() + for word in range(1<<16): + values = {0} + for x in range(16): + if word>>x&1: + values |= {a^x for a in tuple(values)} + oracle.add(sum(1<','exec'),namespace) + examined,survivors = 0,0 + for n in range(5,12): + for weights in combinations_with_replacement(range(2,8),n): + retained = (sum(w-2 for w in weights)<30 and namespace['feasible'](weights,5) + and not namespace['killed'](weights,5)) + v.m.require(retained==v.historical(weights,5), 'original filter disagreement') + examined += 1 + survivors += retained + v.m.require(survivors==77, 'historical (5,6) count') + # Independent false-bound-one control from literal receipt. + receipt = v.load((HERE/'RESULT.json').read_bytes()) + witness = receipt['analysis']['attaining_pair'] + cut = set(witness['cut_labels']) + normals = [tuple(r) for r in witness['normals']] + v.m.require(len(cut)==24 and other.determinant([[v.m.dot(a,b) for a in normals] for b in normals])>0, + 'literal independent pair') + for a in normals: + remaining = [labels[i] for i,r in enumerate(roots) if live>>i&1 + and v.m.dot(a,r) and labels[i] not in cut] + v.m.require(len(v.m.basis(remaining))==7, 'literal residual rank seven') + # Five independent directions pass separate21 cuts. Exhaust all3^5 common unions. + flats = list(v.m.masks(v.m.kernels(labels,[1<>i&1: + continue + trial = selected+[r] + gram = [[v.m.dot(a,b) for a in trial] for b in trial] + if other.determinant(gram)==0: + continue + selected.append(r) + choices = sorted({c for a,_,c in records if a==i and c.bit_count()==21}) + v.m.require(len(choices)==3, 'separate-cut completion options') + options.append(choices) + if len(selected)==5: + break + minimum = 113 + for chosen in product(*options): + union = 0 + for c in chosen: + union |= c + minimum = min(minimum,union.bit_count()) + v.m.require(len(selected)==5 and minimum>24, 'separate/common quantifier control') + # Wrong label association is rejected after direct parsing, independent of hashes. + lines = payloads[v.TABLE].decode().splitlines() + original = lines[0].split() + original[0],original[1] = original[1],original[0] + lines[0] = ' '.join(original) + rejection(lambda:v.m.reconstruct(('\n'.join(lines)+'\n').encode(),payloads[v.GEOMETRY]),'label association') + rejection(lambda:v.load('{"x":1,"x":2}'),'duplicate JSON keys') + # Characteristic zero is a real hypothesis: this nonzero rational word vanishes mod2. + values = [r[0]+r[1] for i,r in enumerate(roots) if live>>i&1] + v.m.require(any(values) and all(x%2==0 for x in values), 'characteristic-two boundary') + # Three actual isolated optimized CLI corruptions, with source-only owned exports. + for kind in ['source','manifest','Boolean receipt']: + with tempfile.TemporaryDirectory(prefix='p112-common24-control-') as temporary: + root = Path(temporary) + package = root/'research'/HERE.name + shutil.copytree(HERE,package,ignore=shutil.ignore_patterns('__pycache__')) + for row in v.load((HERE/'SOURCES.json').read_bytes())['files']: + if row['usage']=='input': + target = root/row['path'];target.parent.mkdir(parents=True,exist_ok=True) + target.write_bytes(payloads[row['path']]) + if kind=='source': + path = root/v.TABLE;path.write_bytes(path.read_bytes()+b'changed\n') + expected = 'source SHA256' + elif kind=='manifest': + path = package/'SOURCES.json';path.write_bytes(path.read_bytes()+b'\n') + expected = 'source manifest identity' + else: + path = package/'RESULT.json' + data = json.loads(path.read_bytes());data['callers'][0]['strict_excess_deficit']=True + path.write_text(json.dumps(data)) + expected = 'result receipt mismatch' + completed = subprocess.run([sys.executable,'-I','-O','-Werror','-B',str(package/'verify.py')], + cwd=root,capture_output=True,text=True,timeout=180) + v.m.require(completed.returncode!=0 and expected in completed.stderr, + 'optimized CLI did not reject '+kind) + print(f'PASS_COMMON24_CONTROLS spaces4=67 original_multisets={examined} survivors=77 ' + f'separate21_minimum_common={minimum} semantic_rejections=2 CLI_rejections=3') + + +if __name__=='__main__': + v.m.require(not sys.argv[1:], 'no arguments accepted') + run() diff --git a/research/p112-common24-caller/verify.py b/research/p112-common24-caller/verify.py new file mode 100644 index 0000000000..00f3be6958 --- /dev/null +++ b/research/p112-common24-caller/verify.py @@ -0,0 +1,230 @@ +#!/usr/bin/env python3 +"""Common24 rank-seven theorem and two literal C5 callers. + +Chris R / Clear1nsight with substantial OpenAI Codex assistance; Apache-2.0. +Credit Nick Petalas, DreamingOfClouds/3154, David Arias and E8/P112 lineage. +""" +from collections import Counter +import hashlib +from itertools import combinations +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(HERE)) +import model as m + +MANIFEST_SHA = '4d49389e8131d6ec139722f60e12d697e4d0d31eba205b5e6d11543d22b4afd3' +TABLE = 'research/one-sided-six-multisets/data/data.txt' +GEOMETRY = 'research/p112-root-simplex-exclusion/geometry.py' +FILTER = 'research/p112-b6-t4-reconciliation/vendor/bk2b.py' + + +def unique(pairs): + m.require(len(pairs) == len({k for k, _ in pairs}), 'duplicate JSON key') + return dict(pairs) + + +def load(raw): + return json.loads(raw, object_pairs_hook=unique) + + +def digest(value): + return hashlib.sha256(json.dumps(value, sort_keys=True, separators=(',', ':')).encode()).hexdigest() + + +def histogram(values): + return {str(k): n for k, n in sorted(Counter(values).items())} + + +def authenticate(root=ROOT, package=HERE): + raw = (package / 'SOURCES.json').read_bytes() + m.require(hashlib.sha256(raw).hexdigest() == MANIFEST_SHA, 'source manifest identity') + result = {} + for row in load(raw)['files']: + if row['usage'] != 'input': + continue + path = root / row['path'] + m.require(path.resolve().is_relative_to(root.resolve()), 'input escaped root') + m.require(not any(p.is_symlink() for p in [path, *path.parents]), 'input symlink') + data = path.read_bytes() + m.require(len(data) <= 2_000_000, 'source size limit') + m.require(hashlib.sha256(data).hexdigest() == row['sha256'], 'source SHA256') + m.require(hashlib.sha1(b'blob '+str(len(data)).encode()+b'\0'+data).hexdigest() + == row['git_blob'], 'source Git blob') + result[row['path']] = data + return result + + +def chamber(roots, coordinates): + signed = set(roots) | {tuple(-x for x in r) for r in roots} + for alpha in m.SIMPLE: + for r in signed: + p = m.dot(alpha, r) + m.require(p % 4 == 0, 'reflection integrality') + m.require(tuple(x-p//4*y for x, y in zip(r, alpha)) in signed, + 'signed reflection closure') + rho = m.solve(m.SIMPLE, [[1]*8])[0] + m.require(all(m.dot(rho, a) == 1 for a in m.SIMPLE), 'strict chamber functional') + faces = [[r for r, c in zip(roots, coordinates) if all(c[j] == 0 for j in range(8) + if not mask >> j & 1)] for mask in range(256)] + cap6 = max(len(faces[x]) for x in range(256) if x.bit_count() <= 6) + seven = [len(faces[255 ^ (1 << j)]) for j in range(8)] + m.require(cap6 == 36 and seven == [42,28,22,14,16,23,37,63], 'face bounds') + normal = [r for r in roots if all(m.dot(r, z) == 0 for z in faces[127])] + m.require(len(normal) == 1, 'E7 root normal') + return {'signed_reflections': 1920, 'rho': [str(x) for x in rho], + 'rank6_face_maximum': cap6, 'seven_node_counts': seven, + 'E7_normal': normal[0]} + + +def cut_records(roots, live, flats): + off = [sum(1 << i for i, r in enumerate(roots) if live >> i & 1 and m.dot(r, a)) + for a in roots] + m.require(histogram(x.bit_count() for x in off) == {'53':112,'56':8}, 'root distances') + records, trace_hist = [], Counter() + for a, word in enumerate(off): + for flat in flats: + trace = (flat & word).bit_count() + trace_hist[trace] += 1 + cut = word & ~flat + if cut.bit_count() <= 24: + records.append((a, flat, cut)) + m.require(max(trace_hist) == 32, 'root-word rank-seven trace cap') + records.sort() + counts = Counter(('live' if live >> a & 1 else 'frame', cut.bit_count()) + for a, _, cut in records) + m.require(counts == {('live',21):336,('live',23):5376,('frame',24):504}, + 'critical cut classes') + return records, off, {str(k):v for k,v in sorted(trace_hist.items())} + + +def candidate_cuts(records): + cuts = sorted({c for _, _, c in records}) + small = [c for c in cuts if c.bit_count() == 21] + edges = [(i,j) for i,j in combinations(range(len(small)),2) + if (small[i] | small[j]).bit_count() <= 24] + degrees = Counter(i for pair in edges for i in pair) + m.require(len(small) == 336 and len(edges) == 168 and set(degrees.values()) == {1}, + '21-cut compatibility is a matching') + candidates = {c for c in cuts if c.bit_count() >= 23} + for s in cuts: + if s.bit_count() != 23: + continue + for t in cuts: + union = s | t + if union.bit_count() <= 24: + candidates.add(union) + return sorted(candidates), len(edges) + + +def analyze(roots, labels, live, records, candidates): + by_normal = [[] for _ in roots] + for a, _, cut in records: + by_normal[a].append(cut) + counts, witness = Counter(), None + admitted_rows = [] + for p in candidates: + normals = [a for a, cuts in enumerate(by_normal) if any(c & ~p == 0 for c in cuts)] + m.require(len(normals) <= 2, 'common24 direction limit exceeded') + counts[(p.bit_count(),len(normals))] += 1 + admitted_rows.append((p, normals)) + if len(normals) == 2 and p.bit_count() == 24 and witness is None: + a,b = normals + determinant = m.dot(roots[a], roots[a])*m.dot(roots[b], roots[b])-m.dot(roots[a],roots[b])**2 + m.require(determinant > 0, 'independent attaining pair') + completions = [next((flat,cut) for n,flat,cut in records + if n == normal and cut & ~p == 0) for normal in normals] + for normal,(flat,_) in zip(normals,completions): + residual = [label for i,label in enumerate(labels) + if live>>i&1 and m.dot(roots[normal],roots[i]) and not p>>i&1] + m.require(all(flat>>i&1 for i in range(120) if live>>i&1 + and m.dot(roots[normal],roots[i]) and not p>>i&1), + 'witness completion containment') + m.require(len(m.basis(residual)) <= 7, 'witness residual rank') + witness = {'cut_labels':[x for i,x in enumerate(labels) if p>>i&1], + 'normal_indices':normals, 'normals':[roots[a],roots[b]], + 'completion_masks':[flat for flat,_ in completions], + 'Gram_determinant':determinant} + m.require(witness is not None, 'two-direction attainment missing') + m.require(sum(counts.values()) == 8540, 'candidate domain size') + return {'candidate_sizes':histogram(p.bit_count() for p in candidates), + 'candidate_direction_histogram':{f'{s}:{n}':v for (s,n),v in sorted(counts.items())}, + 'candidate_admission_digest':digest(admitted_rows), 'maximum_directions':2, + 'attaining_pair':witness} + + +def historical(weights, b): + caps = {2:2,3:4,4:8,5:12,6:20,7:36} + distance = [0,53,78,92,100,106,109,111,112] + if sum(w-2 for w in weights) >= 6*b: + return False + for level in range(1,b+1): + kept = weights[:len(weights)-b+level] + total = sum(caps[w] for w in kept) + target = sum(32 if w == 7 else caps[w] for w in kept) + if level == 1 and target < 53 and total < 73: + return False + if level == 2 and target < 78 and total < 82: + return False + if level >= 3 and total < distance[level]: + return False + base = weights[:len(weights)-b] + return not (sum(caps[w] for w in base) < 53 and + (sum(base) <= 7 or any(sum(x)<=6 and sum(base)-sum(x)<=6 + for n in range(len(base)+1) for x in combinations(base,n)))) + + +def callers(): + result = [] + for weights in [(2,2,2,2,3,5,7,7,7,7,7),(2,2,2,2,4,4,7,7,7,7,7)]: + m.require(historical(weights,5), 'literal historical caller not a survivor') + base = weights[:6] + cap = sum({2:2,3:4,4:8,5:12}[w] for w in base) + m.require(cap == 24 and cap < 53, 'quotient independence cap') + all_caps = [sum({2:2,3:4,4:8,5:12,7:36}[weights[i]] for i in indices) + for indices in combinations(range(11),6)] + m.require(len(all_caps)==462 and min(all_caps)==24, 'all quotient-basis cap tests') + m.require(len(weights)-6 == 5 and all(w == 7 for w in weights[6:]), 'five endpoints') + result.append({'weights':weights, 'cell':[5,6], 'required_code_dimension':5, + 'quotient_dimension':6, 'basis_indices':list(range(6)), + 'basis_support_cap':cap, 'minimum_six_piece_capacity_sum':min(all_caps), + 'six_piece_subsets_checked':len(all_caps), 'independent_directions_required':5, + 'proved_direction_limit':2, 'strict_excess_deficit':30-sum(w-2 for w in weights)}) + return result + + +def compute(payloads): + roots, labels, coordinates, live = m.reconstruct(payloads[TABLE],payloads[GEOMETRY]) + ker = m.kernels(labels,[1 << j for j in range(9)]) + flats = list(m.masks(ker,m.annihilators(9,7))) + m.require(len(flats) == 43435 and max(x.bit_count() for x in flats) == 36, + 'complete rank-seven capacity') + full5 = Counter(x.bit_count() for x in m.masks(ker,m.annihilators(9,5))) + m.require(sum(full5.values()) == 3309747 and max(full5) == 12, 'caller rank-five capacity') + records, _, traces = cut_records(roots,live,flats) + candidates, edges = candidate_cuts(records) + analysis = analyze(roots,labels,live,records,candidates) + return {'schema':'p112-common24-caller/v1', 'spaces7':len(flats), + 'full_trace7_histogram':histogram(x.bit_count() for x in flats), + 'full_trace5_histogram':{str(k):v for k,v in sorted(full5.items())}, + 'flat_inventory_digest':digest(sorted(Counter(flats).items())), + 'root_trace_histogram':traces, 'critical_records':len(records), + 'critical_record_digest':digest(records), 'unique_cuts':len({c for _,_,c in records}), + 'small_cut_matching_edges':edges, 'chamber':chamber(roots,coordinates), + 'analysis':analysis, 'callers':callers()} + + +def main(): + m.require(not sys.argv[1:], 'no arguments accepted') + observed = compute(authenticate()) + expected = load((HERE/'RESULT.json').read_bytes()) + m.require(json.dumps(observed,sort_keys=True) == json.dumps(expected,sort_keys=True), + 'result receipt mismatch') + print('PASS_COMMON24_CALLER spaces7=43435 cuts=6188 candidates=8540 directions<=2 callers=2') + + +if __name__ == '__main__': + main() From 7e8d98e351ac153d81943218bf168dc8548b1cea Mon Sep 17 00:00:00 2001 From: Chris R Date: Mon, 19 Oct 2026 18:04:42 +1100 Subject: [PATCH 2/2] Make private corruption controls writable after read-only export Restore owner-write permission only on owned test copies. Preserve scientific code, proof, numerical receipt and frozen inputs. --- research/p112-common24-caller/CHECKS.json | 3 ++- research/p112-common24-caller/test_controls.py | 3 +++ 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/research/p112-common24-caller/CHECKS.json b/research/p112-common24-caller/CHECKS.json index 9b5d0b7baf..defe04c46d 100644 --- a/research/p112-common24-caller/CHECKS.json +++ b/research/p112-common24-caller/CHECKS.json @@ -22,7 +22,8 @@ "timing_limit": "Single-run timings, not benchmarks.", "development_corrections": [ "Before final validation: fixed a proof-note line-join typo; changed literal witness verification to check all live residual sites before asserting completion containment.", - "Added all462 six-piece capacity-sum checks per caller; regenerated the receipt. No numerical bound changed." + "Added all462 six-piece capacity-sum checks per caller; regenerated the receipt. No numerical bound changed.", + "Committed read-only export exposed copytree preserving read-only modes in private corruption copies. Controls now restore owner-write permission only on their owned copied package files before mutating them. Primary, independent checker, proof, source pins and numerical receipt are unchanged." ], "verification_status": "PASS final complete registered replay: primary, separate finite-core checker and all behavioral/actual optimized CLI controls. PASS syntax, JSON, whitespace and metadata/source pins. Committed-byte/history, official committed export and hosted CI are post-commit obligations and will be reported with the exact publication head.", "limits": [ diff --git a/research/p112-common24-caller/test_controls.py b/research/p112-common24-caller/test_controls.py index 6cbb91e21b..381821d63c 100644 --- a/research/p112-common24-caller/test_controls.py +++ b/research/p112-common24-caller/test_controls.py @@ -105,6 +105,9 @@ def run(): root = Path(temporary) package = root/'research'/HERE.name shutil.copytree(HERE,package,ignore=shutil.ignore_patterns('__pycache__')) + for owned in package.rglob('*'): + if owned.is_file(): + owned.chmod(owned.stat().st_mode | 0o200) for row in v.load((HERE/'SOURCES.json').read_bytes())['files']: if row['usage']=='input': target = root/row['path'];target.parent.mkdir(parents=True,exist_ok=True)