diff --git a/research/p112-six-dimensional-incidence/CHECKS.json b/research/p112-six-dimensional-incidence/CHECKS.json new file mode 100644 index 0000000000..935061d128 --- /dev/null +++ b/research/p112-six-dimensional-incidence/CHECKS.json @@ -0,0 +1,15 @@ +{ + "environment": "3.12.3", + "primary": "Exact rational rank2/3 closure census passed; independent modular101 full closure census also matched during exploration, not part of the registered final verification contract.", + "independent": "23 positive definite Gram3 patterns/2875 integral targets;393 Gram4 patterns/245625 integral targets, max12 lines and complete case digest independently agree.", + "controls": "Meaningful boundary, actual-code, characteristic and optimized receipt-mutation checks.", + "unrun": [ + "Selected cold replay", + "Lean or proof-kernel formalization", + "Docker", + "Full historical predecessor censuses", + "Human mathematical review" + ], + "scope": "Fresh local checks; committed-source/history/export verification and hosted CI are reported separately in PR/handoff.", + "peer_review": "Separate agent checked arbitrary characteristic-zero scalar transfer, singleton active-set counting, exact quotient, pair-incidence algebra and Gram3/4 certificates. No human/formal review." +} diff --git a/research/p112-six-dimensional-incidence/PREDECESSORS.json b/research/p112-six-dimensional-incidence/PREDECESSORS.json new file mode 100644 index 0000000000..d96ca95387 --- /dev/null +++ b/research/p112-six-dimensional-incidence/PREDECESSORS.json @@ -0,0 +1,29 @@ +{ + "canonical_main": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "credits": [ + { + "contributor": "Nick Petalas", + "pr": 3269, + "commit": "ebe02d33157dc6c6d3b35df204e4a39242b7429e", + "role": "Inherited binary support capacities12/20; analytic proof retained as canonical input." + }, + { + "contributor": "Nick Petalas", + "pr": 3300, + "scientific_commit": "4c811083d1a4a7cb084b9d972ac8e8f1c843cba9", + "public_head": "cd2cab515db136d7eb49242fc1111299f28a53a8", + "role": "Inherited binary rank7 support capacity36; analytic proof retained as canonical input." + }, + { + "contributor": "DreamingOfClouds", + "pr": 3154, + "commit": "708f0ad8928c383de8294aea3c126e9461d2066d", + "role": "Historical TWOSIDE callers and generalized-weight context; original filter retained on main." + }, + { + "contributor": "Nick Petalas; David Arias; joaqcoo and retained E8/P112 lineage", + "role": "Root-simplex coordinates, quadratic-model interpretation and decoder context; predecessor notices preserved." + } + ], + "new_contribution": "Root-matroid fiber incidence floor with common-zero charging; two literal maximal profile applications, not a first-exclusion or current-residue-count claim." +} diff --git a/research/p112-six-dimensional-incidence/PROOF.md b/research/p112-six-dimensional-incidence/PROOF.md new file mode 100644 index 0000000000..6c988538e5 --- /dev/null +++ b/research/p112-six-dimensional-incidence/PROOF.md @@ -0,0 +1,232 @@ +# Six code dimensions force a support-incidence bill + +Let K be any characteristic-zero field. Let P be the fixed 112 doubled E8 +root lines in the declared P112 convention, and let + + C = {(r dot h)_(r in P) : h in K^8}. + +For arbitrary vectors p_1,...,p_n in K^112 suppose their span contains a +six-dimensional subspace D of C. Independence of the pieces is unnecessary. +Write M=sum_i |supp(p_i)|, and let z coordinates vanish on every word of D. +We prove both + + M >= 224 - 6n + (n-2)z, (1) + + M >= ceil(((2n-3)(112-z) - binomial(n,2)(12-z))/(n-2)). (2) + +In particular eleven pieces require at least 164+4z, hence164, total support incidences. +Consequently the literal historical TWOSIDE (b,t)=(6,5) profiles 5^10,7 and +5^9,6^2 are impossible. Their inherited capacity sums are156 and148, giving +strict contradiction margins 8 and 16. The profiles 5^11 and5^10,6 follow by +componentwise domination. This is not an assertion that these four profiles +were the only public residues, or a full reconciliation of the174 historical +survivors in that cell. + +## The pairing of mathematical viewpoints + +Generalized Hamming weights constrain how many coordinates can vanish on a +code subspace. The additional datum here is the size of each projective fiber +of the evaluation map, which is controlled by a contraction of the rational +root matroid. Singleton support incidence then combines the common zero set +with all fibers at once. Charging their shared zero roots is what sharpens +the naive bound using d_6>=109 from 152 to 158 at n=11. Pair incidence +then improves the uniform bill further to 164, a gain of twelve over that +naive relaxation. No common-cut extension, +new high-dimensional binary-flat census or Weyl-chamber assumption is needed +for the new incidence theorem. + +## Root-matroid capacity in rational rank three + +Every subset of full E8 root lines whose rational span has dimension at most +three contains at most six lines. The primary certificate enumerates every +pair and triple of the 120 root lines using exact primitive integer RREF. +There are 7,140 independent pairs and 279,720 independent triples. Grouping +bases by their rational span yields: + +| Rank | Distinct root-spanned flats | Closure-size histogram | Maximum | +|---|---:|---|---:| +| 2 | 4,900 | 2:3,780; 3:1,120 | 3 | +| 3 | 85,680 | 3:37,800; 4:40,320; 6:7,560 | 6 | + +Each closure is the union of the roots occurring in its bases. This is complete: +any root belonging to a root-spanned flat extends to a basis of that flat. +The root shell has rank eight, so smaller root-spanned spaces can also be +extended to a three-root span. Arbitrary ambient subspaces contain no more +roots than the root-spanned subspace generated by their contained roots. +The receipt binds all closure masks by canonical SHA256 and retains extremizers. + +There is also a much smaller independent integer certificate. Normalize root +norms to two. Three independent roots have Gram matrix + + G = [[2,a,b],[a,2,c],[b,c,2]], a,b,c in {-1,0,1}. + +Positive definiteness gives det(G)=8+2abc-2(a^2+b^2+c^2)>0. Exactly 23 of the 27 +patterns qualify. For a root r in their span, its integral inner-product +vector k lies in {-2,-1,0,1,2}^3 and satisfies + + k^T adj(G) k = 2 det(G). + +The root is uniquely determined by k because the Gram matrix is invertible. +Enumerating 23*125=2,875 possibilities gives signed-vector counts 6,8,12 with +pattern multiplicities 1,6,16. Thus at most 12 signed roots, or six lines, occur. +This argument is an upper bound: no claim that every enumerated k represents +an actual E8 root is necessary. The separate checker imports neither the +primary exact-elimination code nor the source geometry module. A separate +review agent derived this Gram certificate while auditing the argument; this +is computational and conceptual corroboration by the same assisted team, +not independent human review or a formal proof-kernel check. + +## Root-matroid capacity in rational rank four + +The analogous uniform bound in dimension four is twelve root lines. Choose +four independent roots and form their norm-two Gram matrix, with six free +entries in {-1,0,1}. All 729 matrices are tested; Sylvester's criterion +requires every leading principal minor to be positive, not just the determinant. +Exactly 393 patterns survive. For each, enumerate all 625 integral vectors +k in {-2,-1,0,1,2}^4 and retain k^T adj(G) k=2 det(G). The complete signed +count histogram is10:12,12:12,14:64,20:200,24:105. Thus at most24 signed +roots, or twelve root lines, fit into the span. Smaller root-spanned spaces +extend to a four-root span, as the full shell has rank eight. + +The primary computes determinants by fraction-free Bareiss elimination; the +separate checker uses the permutation formula, with a separately constructed +Gram matrix. Both cover all 393*625=245,625 integral targets and agree on the +canonical case digest. The characteristic-zero inference uses rational rank +preservation, just as for the three-dimensional bound. The primary separately +authenticates all distinct full-root inner products as -4,0,4 in doubled +coordinates, so the normalized integral-pairing alphabet is source-bound. +The actual twelve-root D4 coordinate section is an attaining control and +also shows why the rank-three bound cannot be reused in dimension four. + +## Scalar extension and the common zero set + +Evaluation on P is injective: the live doubled-root Gram sum is 112 I_8. +Choose independent normals h_1,...,h_6 whose codewords form a basis of D, +and define E:K^8 -> K^6 by E(r)=(r dot h_j)_j. Its rank is six and its +kernel has dimension two. Let Z={r in P:E(r)=0} and z=|Z|. + +A rational root matrix has the same rank over Q and over K. A rational minor +nonzero over Q remains nonzero over characteristic zero; vanishing minors +remain zero. Therefore the roots in Z have rational rank at most two and +z<=3 by the rank-two certificate. This uses no embedding of K into R and +makes no rationality assumption about h_j or their coefficients. + +Express each of the six chosen codewords as a linear combination of the n +pieces. For piece i let v_i in K^6 be its six coefficients. At a coordinate +r where exactly piece i is nonzero, E(r)=p_i(r)v_i. Count such a coordinate +as an active singleton only if E(r) is nonzero. Let s_i be the number of +active singletons of piece i. + +If v_i=0, then s_i=0. Otherwise every singleton root of piece i, together +with every root in Z, lies in E^{-1}(K v_i). This preimage has dimension +2+1=3. By rational rank preservation its rational roots have rank at most +three, hence + + s_i + z <= 6. + +The same inequality holds when v_i=0 because s_i=0 and z<=3. Crucially, Z +is the same set for every piece. Projective fiber bounds for separately +chosen code subspaces would not establish this simultaneous inequality. + +## Incidence count + +There are 112-z active coordinates. An active singleton consumes one piece +incidence; every other active coordinate consumes at least two. Arbitrary +cancellations are permitted. Therefore + + 2(112-z) <= M + sum_i s_i <= M+n(6-z). + +Incidences outside the active set only increase M and have not been silently +removed. Rearranging proves(1). Because n>=6 and z>=0 it implies M>=224-6n. + +The weak route using only generalized support weight d_6>=109 and the +unadjusted fiber bound six gives M>=218-6n, or152 at n=11. That relaxation +does not exclude capacity156. Counting common zero roots in every fiber +raises the necessary bill to 158, a measurable improvement of six incidences before the pair strengthening. +Neither incidence formula is asserted to be attained by actual pieces. + +## Pair incidence raises the eleven-piece floor to 164 + +For each unordered pair of piece indices i,j, every active coordinate whose +nonzero pieces are contained in that pair has evaluation in span_K(v_i,v_j). +Together with Z, these roots lie in its inverse image under E, of dimension +at most2+2=4. This remains valid for zero or proportional coefficient columns. +The rank-four bound therefore gives at most 12-z such active coordinates per +pair. + +Let u,v,w count active coordinates of piece multiplicity exactly one, +exactly two, and at least three. Then N=112-z=u+v+w. Summing the pair bound +counts each singleton n-1 times and each doubleton once, yielding + + (n-1)u+v <= binomial(n,2)(12-z). + +Substitute v=N-u-w. The exact rearrangement is + + (n-2)u-w <= binomial(n,2)(12-z)-N. + +Since n>=6 and w>=0, it implies the weaker but useful bound + + (n-2)(u-w) <= binomial(n,2)(12-z)-N. + +Meanwhile M>=u+2v+3w=2N-u+w. Substitution proves(2); M is an integer so the +ceiling is legitimate. With eleven pieces this reads + + M >= ceil((1468+36z)/9)=164+4z. + +No integrality or sign condition is imposed on piece coefficients. Multiple +nonzero pieces can cancel at a coordinate, and all such costs are retained +or omitted only in the direction that weakens the lower bound. Pair incidence +is an additional constraint on this same actual caller, rather than an +extension to a different cut budget or a larger historical multiset census. +The parent coordination agent proposed this strengthening and the separate +conceptual-review agent independently checked the inequality and all 393 Gram +patterns. The registered primary and separate checker reproduce the result. + +## Literal caller and quotient binding + +Use the inherited binary support capacities g(5)=12,g(6)=20,g(7)=36 for the +leading-one labels of the pinned geometry. Their analytic source proofs are +explicit inputs; their large historical censuses are not replayed here. +The original independent pieces span T, with dim(T intersect C)>=6. +There are eleven pieces, so the quotient Q=T/(T intersect C) has dimension +at most five. To bind the exact quotient, choose six rank-five pieces. Their +union has size at most 72=78; the new incidence contradiction +only needs the original at-least-six intersection hypothesis and does not +depend on that extra quotient calculation. The five smallest individual +capacity sums equal 60, above distance 53, so a strict-below-distance quotient +basis certificate is unavailable from those sums alone. No lower bound on +actual support union is inferred. + +For 5^10,7, the strict excess is10*3+5=35<36, and M<=10*12+36=156<164. +For 5^9,6^2, the excess is9*3+2*4=35<36, and M<=9*12+2*20=148<164. +Both pass the original PR3154 necessary filters; the primary reimplementation +and separate execution of its unchanged feasible/killed functions agree. +We bind these two literal rows only, not a new exhaustive current frontier. + +## Dependencies, credit and remaining obligations + +The new support-incidence theorem is supplied by the written linear algebra +and the two bounded exact root-capacity certificates. Its literal weight +applications inherit Nick Petalas's global quadratic support capacities12/20, +the retained rank-seven capacity36 proof and the declared label convention. +The quotient annotation and historical survivor status retain +DreamingOfClouds/PR3154's generalized-weight and TWOSIDE context. Credit also +stays with the root-simplex geometry lineage, David Arias's quadratic-model +work, joaqcoo and all named predecessors in their retained sources. +SOURCES.json pins every input to canonical main20ecf2891d80b5acf18d980b2164fb44ea7faa90. +Predecessor packages are unchanged. Substantial OpenAI Codex assistance was +used; new work is Apache-2.0. + +This is a local C5 caller exclusion and a reusable incidence inequality. Full +C5, a global decoder lower bound, physical realization, supplier admission, +complete multiplication theorem and a kappa increase do not follow. Excluding +an optimistic low-cost decoder shape does not construct a cheaper decoder. +The selected conditional kappa remains 0.001672660197076918. Human or formal +acceptance, complete historical/current caller reconciliation and constructive +cost improvements remain separate obligations. diff --git a/research/p112-six-dimensional-incidence/README.md b/research/p112-six-dimensional-incidence/README.md new file mode 100644 index 0000000000..794966e501 --- /dev/null +++ b/research/p112-six-dimensional-incidence/README.md @@ -0,0 +1,71 @@ +# Six code dimensions force 164 support incidences at eleven pieces + +For arbitrary pieces spanning a six-dimensional subspace of the characteristic-zero +P112 root-evaluation code, the total support-incidence bill satisfies + + sum_i |supp(p_i)| >= 224 - 6n + (n-2)z, + +where z is the number of coordinates vanishing on that same code subspace. +A pair-incidence strengthening gives + + sum_i |supp(p_i)| >= ceil(((2n-3)(112-z)-binomial(n,2)(12-z))/(n-2)). + +In particular eleven pieces require at least 164+4z, hence164, incidences. This excludes the +literal historical (6,5) profiles 5^10,7 and5^9,6^2, whose inherited support +caps total156 and148. Their exact quotient is five-dimensional and their +code intersection is six-dimensional under the stated inherited second-weight +bound. The contradiction itself only requires six code dimensions. + +[PROOF.md](PROOF.md) pairs generalized Hamming weights with rational root-matroid +contraction fibers and singleton incidence. Charging common zero roots raises +the naive152-incidence floor to 158, and pair incidence strengthens this +to 164. The first named caller is excluded with margin eight. The dominated profiles 5^11 and5^10,6 also follow. No complete +current residue count or first-exclusion claim is made. + +The primary checks all 4,900 rank-two and 85,680 rank-three root-spanned flats +using rational elimination. The separate checker proves the needed cap of six +root lines through 23 integral rank-three Gram patterns and 2,875 target vectors. +All 393 positive definite rank-four Gram patterns, covering 245,625 integral +targets, independently certify the pair-fiber cap of twelve root lines. +It imports no primary geometry or elimination code. Both literal profiles +pass the unchanged original PR3154 necessary filter. A separate team agent +critiqued the scalar-extension/common-zero argument and supplied the Gram +certificate; this is assisted-team corroboration, not independent human or +proof-kernel acceptance. + +## Reproduce + +From the repository root, with Python3.12 and its standard library: + +```sh +python3.12 -I -Werror -B scripts/research_package.py --package research/p112-six-dimensional-incidence +``` + +The registered commands are also directly runnable in the official Git-free +export. Normal replay is read-only; only `verify.py --write-expected` regenerates +the receipt. `SOURCES.json` authenticates every canonical-main input; the +historical filter is reused for binding and the capacities remain inherited +proof dependencies. The bounded root-capacity theorem itself needs neither a +Weyl-chamber theorem nor an embedding of the coefficient field into the reals. + +## Open next questions + +First independently audit the common-zero charging and the characteristic-zero +rank transfer. A further application should name an actual caller whose total +support cap reaches164 and identify additional multi-piece incidence structure. +The uniform bound's attainability and such a caller are not established here; +a larger census is not automatically warranted. + +This local C5 progress does not construct a cheaper decoder or improve kappa. +Full C5, physical supplier admission, the full multiplication theorem and +human/formal acceptance remain open. The selected conditional kappa remains +0.001672660197076918. + +## Credit + +Nick Petalas/PR3269 and3300 supply the inherited12/20/36 capacities; +DreamingOfClouds/PR3154 supplies the historical reduction. Retain the +root-simplex lineage, David Arias's quadratic-model work and joaqcoo's decoder +context. Exact source pins and scope distinctions are in `PREDECESSORS.json` +and `SOURCES.json`. Chris R / Clear1nsight with substantial OpenAI Codex +assistance. Apache-2.0. Predecessor packages and selected artifacts are unchanged. diff --git a/research/p112-six-dimensional-incidence/RESULT.json b/research/p112-six-dimensional-incidence/RESULT.json new file mode 100644 index 0000000000..4fd2b90a22 --- /dev/null +++ b/research/p112-six-dimensional-incidence/RESULT.json @@ -0,0 +1,115 @@ +{ + "callers": [ + { + "b": 6, + "code_intersection_dimension": 6, + "contradiction_margin": 8, + "inherited_second_weight": 78, + "n": 11, + "new_support_floor": 164, + "preferred_five_piece_capacity": 60, + "quotient_dimension": 5, + "singleton_support_floor": 158, + "six_rank5_capacity": 72, + "strict_excess": 35, + "t": 5, + "total_support_capacity": 156, + "weights": [ + 5, + 5, + 5, + 5, + 5, + 5, + 5, + 5, + 5, + 5, + 7 + ] + }, + { + "b": 6, + "code_intersection_dimension": 6, + "contradiction_margin": 16, + "inherited_second_weight": 78, + "n": 11, + "new_support_floor": 164, + "preferred_five_piece_capacity": 60, + "quotient_dimension": 5, + "singleton_support_floor": 158, + "six_rank5_capacity": 72, + "strict_excess": 35, + "t": 5, + "total_support_capacity": 148, + "weights": [ + 5, + 5, + 5, + 5, + 5, + 5, + 5, + 5, + 5, + 6, + 6 + ] + } + ], + "model": "full120 E8 root lines; fixed112 puncture", + "no_new_kappa": true, + "rank4_gram": { + "candidate_vectors": 245625, + "case_digest": "34f01cd205fbaf4c1f19ec2e308c6c4b6617ea6ad74e96a268e495e0a22bf002", + "maximum_lines": 12, + "patterns": 393, + "signed_target_histogram": { + "10": 12, + "12": 12, + "14": 64, + "20": 200, + "24": 105 + } + }, + "rational_flats": [ + { + "closure_digest": "f2d3dcc95790f37884e28bc2078c9c3ddc7e24dd16773e9f62135f62fadbfa70", + "flats": 4900, + "histogram": { + "2": 3780, + "3": 1120 + }, + "independent_bases": 7140, + "maximizer": [ + 0, + 2, + 3 + ], + "maximum": 3, + "rank": 2 + }, + { + "closure_digest": "0954f5ade536fa6e74ab7c037c72dcb101cb757716ab6faee35c298dff23f796", + "flats": 85680, + "histogram": { + "3": 37800, + "4": 40320, + "6": 7560 + }, + "independent_bases": 279720, + "maximizer": [ + 0, + 1, + 2, + 3, + 4, + 5 + ], + "maximum": 6, + "rank": 3 + } + ], + "schema_version": 1, + "theorem": "M >= ceil(((2*n-3)*(112-z)-choose(n,2)*(12-z))/(n-2)); at n=11, M>=164+4*z" +} diff --git a/research/p112-six-dimensional-incidence/SOURCES.json b/research/p112-six-dimensional-incidence/SOURCES.json new file mode 100644 index 0000000000..453966a7d7 --- /dev/null +++ b/research/p112-six-dimensional-incidence/SOURCES.json @@ -0,0 +1,48 @@ +{ + "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/e8-quadratic-support-capacity/PROOF.md", + "usage": "input", + "git_blob": "4da8e98edcfbbb9d5cd17b7ee921aa323d2fc724", + "sha256": "0a68df931e4da65a9568a5ad3731c2a6c6f6b6fca57839d7d4c12a6fba0b333e" + }, + { + "path": "research/e8-rank7-capacity/PROOF.md", + "usage": "input", + "git_blob": "a85d734bf81511139b7651b5d54b0e3fa8284df4", + "sha256": "96769d503752d6c1fb16ab3fb4fc456c62f623537385594dd88c1f87c3e3e2cf" + }, + { + "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-six-dimensional-incidence/TASK.json b/research/p112-six-dimensional-incidence/TASK.json new file mode 100644 index 0000000000..72a6977af4 --- /dev/null +++ b/research/p112-six-dimensional-incidence/TASK.json @@ -0,0 +1,86 @@ +{ + "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": "Six-dimensional P112 singleton and pair incidence bounds; eleven-piece support floor164 and exact historical (6,5) caller exclusions5^10,7 and5^9,6^2.", + "scope_change_reason": "Explicit multi-agent follow-up requests contrasting mathematical specializations; combine generalized support weights with root-matroid contraction fibers and singleton incidence.", + "bottleneck_link": "A complete decoder lower bound needs actual caller exclusions. These two profiles have no below-distance five-piece basis certified by capacity sums; a joint common-zero incidence bound excludes their total bills directly.", + "budget_minutes": 60, + "stop_rule": "Stop after one new source-bound incidence implication and named literal applications; reserve final quarter for independent critique, exact source checks and committed read-only export.", + "outcome": "completed", + "evidence": "Exact rational4900 rank2 and85680 rank3 flats; independent23-Gram3 and393-Gram4 certificates, root caps6/12; support floor152 to164, two maximal caller margins8,16.", + "author": "Chris R / Clear1nsight with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance. Parent coordination agent proposed pair-incidence strengthening; separate conceptual-review agent checked it and supplied small Gram certificates. Same assisted contributor, no human or formal-kernel approval.", + "open_questions": [ + { + "question": "Does a current actual caller with support bill at least164 violate a stronger fiber-incidence constraint?", + "why_it_matters": "The pair-incidence relaxation stops at164 and does not determine full C5.", + "first_step": "Bind the caller and its actual code-subspace/quotient constraints; test multi-piece incidence or equality before any larger census.", + "blocked_by": "No new caller or stronger inequality is established here." + }, + { + "question": "Can the characteristic-zero fiber proof and its bounded certificates be independently accepted?", + "why_it_matters": "Publication and CI do not constitute mathematical acceptance.", + "first_step": "Audit E inverse projective-line dimension and common zero charging, then replay both exact root-capacity methods.", + "blocked_by": "Independent human or proof-kernel review remains open." + } + ], + "freshness": { + "canonical_main": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "priority_revision": 6, + "open_PR_bodies": 679, + "PR_snapshot_UTC": "2026-10-19 07:50 UTC", + "Discussion_coverage": "Parent rendered active, handoff and C5 current portions; broader Discussion, closed and private coverage partial", + "own_semantic_check": "No matching named profile or support158/224-6n lemma in679 bodies or local research proofs; not a novelty guarantee" + } +} diff --git a/research/p112-six-dimensional-incidence/VERIFY.json b/research/p112-six-dimensional-incidence/VERIFY.json new file mode 100644 index 0000000000..c2074248cc --- /dev/null +++ b/research/p112-six-dimensional-incidence/VERIFY.json @@ -0,0 +1,51 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/e8-quadratic-support-capacity/PROOF.md", + "research/e8-rank7-capacity/PROOF.md", + "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": "All rank2/3 rational root flats,393 Gram4 patterns via Bareiss determinants, live Gram identity and exact two caller bindings." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 180, + "checks": "Independent23 Gram3 and393 Gram4 patterns via permutation determinants; original caller filter and pair-incidence integer ceiling." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/test_controls.py" + ], + "timeout_seconds": 180, + "checks": "Rank3 attainment, rank4 boundary, actual code fiber fixture, characteristic2 exclusion and optimized CLI receipt corruption." + } + ] +} diff --git a/research/p112-six-dimensional-incidence/independent.py b/research/p112-six-dimensional-incidence/independent.py new file mode 100644 index 0000000000..ce3cc82651 --- /dev/null +++ b/research/p112-six-dimensional-incidence/independent.py @@ -0,0 +1,79 @@ +#!/usr/bin/env python3 +"""Independent Gram-matrix upper bound, with no primary or geometry imports. +Chris R / Clear1nsight with OpenAI Codex assistance. Apache-2.0. +The 23-pattern certificate was supplied by a separate conceptual-review agent. +""" +from collections import Counter +from hashlib import sha256 +from itertools import product, permutations +import json +from pathlib import Path +HERE=Path(__file__).resolve().parent +ROOT=HERE.parents[1] + +def check(ok,message): + if not ok:raise ValueError(message) + +def gram_bound(): + cases=[] + for a,b,c in product((-1,0,1),repeat=3): + det=8+2*a*b*c-2*(a*a+b*b+c*c) + if det<=0:continue + adj=((4-c*c,b*c-2*a,a*c-2*b), + (b*c-2*a,4-b*b,a*b-2*c), + (a*c-2*b,a*b-2*c,4-a*a)) + targets=[] + for k in product(range(-2,3),repeat=3): + quadratic=sum(k[i]*adj[i][j]*k[j] for i in range(3) for j in range(3)) + if quadratic==2*det:targets.append(k) + check(all(tuple(-x for x in k) in targets for k in targets),'opposite root absent') + cases.append({'off_diagonal':[a,b,c],'determinant':det,'signed_targets':len(targets)}) + check(len(cases)==23,'positive definite Gram pattern count') + check(Counter(x['signed_targets'] for x in cases)=={6:1,8:6,12:16},'Gram target histogram') + return cases + +def determinant(matrix): + n=len(matrix);answer=0 + for order in permutations(range(n)): + value=(-1)**sum(order[i]>order[j] for i in range(n) for j in range(i+1,n)) + for i in range(n):value*=matrix[i][order[i]] + answer+=value + return answer + +def gram4_bound(): + cases=[] + for a,b,c,d,e,f in product((-1,0,1),repeat=6): + g=((2,a,b,c),(a,2,d,e),(b,d,2,f),(c,e,f,2)) + if any(determinant([r[:k] for r in g[:k]])<=0 for k in range(1,5)):continue + det=determinant(g) + adj=[[(-1)**(i+j)*determinant([[g[a][b] for b in range(4) if b!=i] for a in range(4) if a!=j]) for j in range(4)] for i in range(4)] + count=0 + for k in product(range(-2,3),repeat=4): + if sum(k[i]*adj[i][j]*k[j] for i in range(4) for j in range(4))==2*det:count+=1 + cases.append([[a,b,c,d,e,f],det,count]) + hist=Counter(c[2] for c in cases) + check(hist=={10:12,12:12,14:64,20:200,24:105},'rank4 Gram histogram') + return {'patterns':len(cases),'candidate_vectors':len(cases)*625,'signed_target_histogram':{str(k):hist[k] for k in sorted(hist)},'maximum_lines':12,'case_digest':sha256(json.dumps(cases,separators=(',',':')).encode()).hexdigest()} + +def original_functions(): + path=ROOT/'research/p112-b6-t4-reconciliation/vendor/bk2b.py' + namespace={};exec(compile(path.read_text().split('import sys')[0],str(path),'exec'),namespace) + return namespace + +def main(): + for item in json.loads((HERE/'SOURCES.json').read_text())['files']: + if item['usage']=='input':check(sha256((ROOT/item['path']).read_bytes()).hexdigest()==item['sha256'],'source changed') + receipt=json.loads((HERE/'RESULT.json').read_text()) + cases=gram_bound() + check(max(x['signed_targets'] for x in cases)//2==receipt['rational_flats'][1]['maximum']==6,'rank-three bound') + check(gram4_bound()==receipt['rank4_gram'],'independent rank4 Gram certificate') + old=original_functions() + for c in receipt['callers']: + w=c['weights'];check(old['feasible'](w,6) and not old['killed'](w,6),'original filter rejects caller') + check(sum(x-2 for x in w)<36 and len(w)==11,'historical cell') + cap=sum({2:2,3:4,4:8,5:12,6:20,7:36}[x] for x in w) + bounds=[(19*(112-z)-55*(12-z)+8)//9 for z in range(4)] + check(bounds==[164,168,172,176] and cap=224-6*len(pieces)+(len(pieces)-2)*len(zero),'actual support floor') + multiplicities=[sum(p[t]!=0 for p in pieces) for t in range(112) if t not in zero] + n=len(pieces);u=multiplicities.count(1);vv=multiplicities.count(2);ww=sum(m>=3 for m in multiplicities) + check((n-1)*u+vv<=n*(n-1)//2*(12-len(zero)),'actual pair count') + check(total>=2*(112-len(zero))-u+ww,'actual multiplicity lower bound') + # Characteristic two destroys doubled-root norm and injective evaluation. + check(all(sum(x*x for x in row)%2==0 for row in roots),'characteristic two excluded') + # Corrupt an on-disk result and run the separate optimized checker; it must fail. + with tempfile.TemporaryDirectory(prefix='p112-incidence-control-') as temp: + root=Path(temp);dest=root/'research'/HERE.name + shutil.copytree(HERE,dest) + for entry in json.loads((HERE/'SOURCES.json').read_text())['files']: + if entry['usage']=='input': + out=root/entry['path'];out.parent.mkdir(parents=True,exist_ok=True);shutil.copyfile(HERE.parents[1]/entry['path'],out) + target=dest/'RESULT.json';target.chmod(target.stat().st_mode|0o200) + mutant=json.loads(target.read_text());mutant['callers'][0]['contradiction_margin']=9;target.write_text(json.dumps(mutant)) + proc=subprocess.run([sys.executable,'-I','-O','-B',str(dest/'independent.py')],capture_output=True,text=True) + check(proc.returncode!=0 and 'caller margin' in proc.stderr,'optimized mutated receipt accepted') + print('PASS_P112_INCIDENCE_CONTROLS rank3_attainment rank4_boundary common_zero actual_code char2 optimized_receipt_mutant') +if __name__=='__main__':main() diff --git a/research/p112-six-dimensional-incidence/verify.py b/research/p112-six-dimensional-incidence/verify.py new file mode 100644 index 0000000000..1b9b79b130 --- /dev/null +++ b/research/p112-six-dimensional-incidence/verify.py @@ -0,0 +1,153 @@ +#!/usr/bin/env python3 +"""Exact rational low-rank root flats and one literal C5 incidence application. +Chris R / Clear1nsight with OpenAI Codex assistance. Apache-2.0. +""" +import argparse +from collections import Counter +from hashlib import sha256 +import importlib.util +from itertools import combinations, product +import json +from math import gcd +from pathlib import Path + +HERE=Path(__file__).resolve().parent +ROOT=HERE.parents[1] +CAP={2:2,3:4,4:8,5:12,6:20,7:36} + +def require(ok, message): + if not ok: raise ValueError(message) + +def authenticate(): + source=json.loads((HERE/'SOURCES.json').read_text()) + for item in source['files']: + if item['usage']=='input': + require(sha256((ROOT/item['path']).read_bytes()).hexdigest()==item['sha256'],'source digest: '+item['path']) + +def primitive(row): + g=gcd(*row) + if not g:return tuple(row) + if next(x for x in row if x)<0:g=-g + return tuple(x//g for x in row) + +def basis(rows): + """Canonical primitive integer version of rational RREF; no floating point.""" + out=[] + for original in rows: + row=tuple(original) + for old in out: + pivot=next(i for i,x in enumerate(old) if x) + if row[pivot]:row=primitive(tuple(old[pivot]*x-row[pivot]*y for x,y in zip(row,old))) + if not any(row):continue + row=primitive(row);pivot=next(i for i,x in enumerate(row) if x) + out=[primitive(tuple(row[pivot]*x-old[pivot]*y for x,y in zip(old,row))) if old[pivot] else old for old in out] + out.append(row);out.sort(key=lambda r:next(i for i,x in enumerate(r) if x)) + return tuple(out) + +def load_roots(): + spec=importlib.util.spec_from_file_location('pinned_geometry',ROOT/'research/p112-root-simplex-exclusion/geometry.py') + module=importlib.util.module_from_spec(spec);spec.loader.exec_module(module) + roots=module.root_lines() + require(len(roots)==120 and all(sum(x*x for x in r)==8 for r in roots),'root shell') + frame=set() + for i in range(0,8,2): + for sign in (-2,2): + row=[0]*8;row[i]=2;row[i+1]=sign;frame.add(tuple(row)) + live=[r for r in roots if r not in frame] + require(len(live)==112,'live puncture') + require(all(sum(x*y for x,y in zip(a,b)) in (-4,0,4) for a,b in combinations(roots,2)),'distinct root Cartan inner products') + require(all(sum(r[i]*r[j] for r in live)==(112 if i==j else 0) for i in range(8) for j in range(8)),'live evaluation Gram identity') + return roots + +def flats(roots, rank): + groups={} + independent=0 + for indices in combinations(range(len(roots)),rank): + key=basis(roots[i] for i in indices) + if len(key)!=rank:continue + independent+=1 + mask=sum(1<>i&1] for m in masks if m.bit_count()==max(histogram))} + +def old_filter(weights,b): + if sum(w-2 for w in weights)>=6*b:return False + d=[0,53,78,92,100,106,109,111,112] + for level in range(1,b+1): + small=weights[:len(weights)-b+level] + total=sum(CAP[w] for w in small) + tight=sum(32 if w==7 else CAP[w] for w in small) + if level==1 and tight<53 and total<73:return False + if level==2 and tight<78 and total<82:return False + if level>=3 and total=53:return True + if sum(small)<=7:return False + for mask in range(1<>i&1)<=6 and sum(w for i,w in enumerate(small) if not(mask>>i&1))<=6:return False + return True + +def determinant(rows): + a=[list(row) for row in rows];n=len(a);previous=1;sign=1 + for k in range(n-1): + pivot=next((j for j in range(k,n) if a[j][k]),None) + if pivot is None:return 0 + if pivot!=k:a[k],a[pivot]=a[pivot],a[k];sign=-sign + for i in range(k+1,n): + for j in range(k+1,n): + numerator=a[k][k]*a[i][j]-a[i][k]*a[k][j] + require(numerator%previous==0,'Bareiss divisibility') + a[i][j]=numerator//previous + previous=a[k][k] + for i in range(k+1,n):a[i][k]=0 + return sign*a[-1][-1] + +def rank4_gram(): + cases=[] + for off in product((-1,0,1),repeat=6): + g=[[2 if i==j else 0 for j in range(4)] for i in range(4)] + for (i,j),x in zip(combinations(range(4),2),off):g[i][j]=g[j][i]=x + if any(determinant([r[:k] for r in g[:k]])<=0 for k in range(1,5)):continue + det=determinant(g) + adj=[[(-1)**(i+j)*determinant([[g[a][b] for b in range(4) if b!=i] for a in range(4) if a!=j]) for j in range(4)] for i in range(4)] + count=sum(sum(k[i]*adj[i][j]*k[j] for i in range(4) for j in range(4))==2*det for k in product(range(-2,3),repeat=4)) + cases.append([list(off),det,count]) + histogram=Counter(c[2] for c in cases) + require(len(cases)==393 and max(histogram)==24,'rank4 Gram target cap') + return {'patterns':len(cases),'candidate_vectors':len(cases)*625,'signed_target_histogram':{str(k):histogram[k] for k in sorted(histogram)},'maximum_lines':max(histogram)//2,'case_digest':sha256(json.dumps(cases,separators=(',',':')).encode()).hexdigest()} + +def caller(weights): + require(old_filter(weights,6),'not an original historical survivor') + total=sum(CAP[w] for w in weights);n=len(weights) + require(total<164,'no strict incidence contradiction') + return {'weights':weights,'b':6,'t':5,'n':n,'strict_excess':sum(w-2 for w in weights), + 'quotient_dimension':5,'code_intersection_dimension':6, + 'total_support_capacity':total,'singleton_support_floor':224-6*n,'new_support_floor':164, + 'contradiction_margin':164-total, + 'six_rank5_capacity':72,'inherited_second_weight':78, + 'preferred_five_piece_capacity':60} + +def compute(): + authenticate();roots=load_roots() + pair=flats(roots,2);triple=flats(roots,3) + require(pair['maximum']==3 and triple['maximum']==6,'low rank root capacities') + return {'schema_version':1,'model':'full120 E8 root lines; fixed112 puncture', + 'rational_flats':[pair,triple],'rank4_gram':rank4_gram(), + 'theorem':'M >= ceil(((2*n-3)*(112-z)-choose(n,2)*(12-z))/(n-2)); at n=11, M>=164+4*z', + 'callers':[caller([5]*10+[7]),caller([5]*9+[6,6])], + 'no_new_kappa':True} + +def main(): + ap=argparse.ArgumentParser();ap.add_argument('--write-expected',action='store_true');args=ap.parse_args() + result=compute() + encoded=json.dumps(result,indent=2,sort_keys=True)+'\n' + if args.write_expected:(HERE/'RESULT.json').write_text(encoded) + else:require(result==json.loads((HERE/'RESULT.json').read_text()),'receipt mismatch') + print('PASS_P112_SIX_DIMENSIONAL_INCIDENCE root_rank3_cap=6 root_rank4_cap=12 support_floor164 caller_margins8,16 no_new_kappa') +if __name__=='__main__':main()