From b084bc5bc7aaa4ee51aba7e3d668ea3da9af4934 Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Tue, 13 Oct 2026 13:29:18 -0500 Subject: [PATCH] Prove local block splitting and exclude two regular blocks --- research/kappa-nine/MIXED-GEOMETRY.md | 313 + research/kappa-nine/build_mixed_geometry.py | 79 + .../mixed-geometry-base-selection.json | 177 + .../mixed-geometry-certificate.json | 7206 +++++++++++++++++ research/kappa-nine/mixed-geometry-claim.json | 20 + research/kappa-nine/verify_mixed_geometry.py | 306 + 6 files changed, 8101 insertions(+) create mode 100644 research/kappa-nine/MIXED-GEOMETRY.md create mode 100644 research/kappa-nine/build_mixed_geometry.py create mode 100644 research/kappa-nine/mixed-geometry-base-selection.json create mode 100644 research/kappa-nine/mixed-geometry-certificate.json create mode 100644 research/kappa-nine/mixed-geometry-claim.json create mode 100644 research/kappa-nine/verify_mixed_geometry.py diff --git a/research/kappa-nine/MIXED-GEOMETRY.md b/research/kappa-nine/MIXED-GEOMETRY.md new file mode 100644 index 0000000000..35a41879a2 --- /dev/null +++ b/research/kappa-nine/MIXED-GEOMETRY.md @@ -0,0 +1,313 @@ +# A local block decomposition and the two-regular-block obstruction + +Ali Romman, with substantial OpenAI Codex assistance. October 13, 2026. +Apache-2.0. This work builds on Douglas Colkitt's `kappa-nine` investigation. + +**Scoped negative result:** in uniform mode 3, at most one anchor block can +be regular. This excludes all 28 four-exception and all 21 five-exception +sets that survived `MIXED-RANK-TEST.md`. The seven six-exception sets and the +all-exception set remain open. These 49 patterns are regularity patterns inside uniform mode 3. They are +not the complete remainder-mode branches. Uniform mode 3 still has eight +open exception patterns, so it remains open, as do the other 102 complete +branch representatives. There is no new kappa. + +The proof also gives a necessary local form for every anchor block. Its +restrictions split into two complementary idempotent parts. This form is +forced by the graph; it does not impose permutation covariance, a common +bilinear form, positivity, or a choice of scalar coordinates. + +## Scope and notation + +Use the pinned nine-point problem over Q. There are seven anchor planes +E_0,...,E_6 and one remainder coordinate. For every triple T, let + + P_T = A_T B_T, B_T A_T = I_2. + +For adjacent labels T,U, both B_T A_U and B_U A_T are zero. Adjacency means +that the triples intersect in one point. In uniform mode 3, the 42 Y labels +have no remainder coordinate in either factor. The other 35 variable labels +are X labels; this proof does not construct or constrain their extension. + +Write the fixed Fano lines as + + 012, 034, 056, 135, 146, 236, 245. + +For a point p in {0,...,6}, let star(p) be the three anchor lines through p. +For z in {7,8}, the three labels + + C(p,z) = {(L minus {p}) union {z} : L in star(p)} + +form a clique. Their common allowed support is the six-dimensional sum of +the planes in star(p). The six image columns and six dual rows are bases of +that support. Their projectors therefore sum to its identity. + +Fix an anchor line K and its plane E. For p in K, define the singleton label + + S(p,z) = (K minus {p}) union {z}. + +The other two members of C(p,z) are denoted N(p,z). Put a_T=A_T restricted +to the rows of E and b_T=B_T restricted to the columns of E. These are +2-by-2 matrices. Set + + D(p,z) = a_S(p,z) b_S(p,z), + R(p,z) = sum over T in N(p,z) of a_T b_T. + +The saturated clique identity gives D(p,z)+R(p,z)=I_E. + +## The local decomposition theorem + +**Theorem.** There are complementary idempotents C_7,C_8 on E such that, +for every p in K, + + D(p,z) = C_z, + C_7 + C_8 = I_E, + C_7 C_8 = C_8 C_7 = 0. + +For singleton restrictions, the image of a_S(p,z) is im(C_z), and the +row space of b_S(p,z) is the row space of C_z. Both restriction ranks equal +rank(C_z). Each nonsingleton restriction in N(p,z) lies in the complementary +part: a_T=C_(15-z) a_T and b_T=b_T C_(15-z). In particular, + + rank(a_S(p,7)) + rank(a_S(p,8)) = 2, + rank(b_S(p,7)) + rank(b_S(p,8)) = 2. + +**Proof.** If p and q are distinct points of K, the allowed supports of +C(p,z) and C(q,w) meet only in E. The following pairs are adjacent: + +1. S(p,z) and each member of N(q,z). +2. S(p,z) and S(q,15-z). +3. Every member of N(p,z) and every member of N(q,15-z). + +Thus each global zero product for these pairs is a zero product on E. +The certificate checks all these pairs on all seven blocks. For the first +family, multiplication by the outer a and b factors gives + + D(p,z) R(q,z) = R(q,z) D(p,z) = 0. + +Substitute R(q,z)=I-D(q,z). It follows that + + D(p,z) D(q,z) = D(p,z) = D(q,z) D(p,z). + +Interchange p and q. The same products equal D(q,z), so D(p,z)=D(q,z). +Call the common value C_z. The displayed identity now gives C_z^2=C_z. +The second edge family gives C_z C_(15-z)=0 in both orders. The third gives + + (I-C_z)(I-C_(15-z))=0. + +Expand this product and use C_z C_(15-z)=0. Then C_z+C_(15-z)=I. + +The first edge family also gives R(q,z) a_S(p,z)=0 and +b_S(p,z) R(q,z)=0. Hence C_z a_S(p,z)=a_S(p,z) and +b_S(p,z) C_z=b_S(p,z). Since a_S(p,z)b_S(p,z)=C_z, these inclusions are +equalities of image and row spaces. The restriction ranks equal rank(C_z). +For T in N(p,z), use S(q,z), with q distinct from p. The first edge family +gives C_z a_T=0 and b_T C_z=0, which proves the complementary support +statements. The two rank sums follow from the direct sum of the images of +the complementary idempotents. This proves the theorem. + +The argument works over any field. The package states the application over +Q and uses rational controls. A finite-field experiment is not used to +infer the result. + +## Why two regular blocks are impossible + +A block is regular when all its 18 allowed Y restrictions have rank one +for both A and B. The source line-alignment argument applies to each such +block. The graph of sole-common-block edges is connected and bipartite; +its two image lines are distinct, and the two dual lines select the same +coordinates. In each C(p,z), exactly one label uses one line on the block; +the other two use the other line. The singleton is S(p,z). + +Take any two regular blocks E_r,E_s. Their anchor lines meet at a point p. +Let E_k be the third block in star(p). For each z in {7,8}, apply the +complementary-block lemma from `MIXED-RANK-TEST.md` to C(p,z), with the +label T_z=S_k(p,z) singled out on E_k. The lemma only needs the other two +blocks to be regular. It does not require a rank assumption on E_k. +It gives + + rank(A_Tz restricted to E_k) = rank(B_Tz restricted to E_k) = 2. + +For completeness, concatenate the three A factors on their common support +into a 6-by-6 matrix A, and stack the B factors into B. Then B=A^{-1}. +Order E_k and T_z first. The two regular blocks have distinct singleton +labels among the other two labels. Their singleton rows and their rows on +the other regular block are independent. The corresponding B columns are +independent as well. This follows from the saturated clique identity: a +singleton diagonal entry is 1 and its off-diagonal entries are zero. +Thus the lower-right 4-by-4 blocks of both A and B are invertible after +permuting rows or columns. The block inverse formula forces both upper-left +2-by-2 blocks to be invertible. This is the source lemma; no stronger form +of it is assumed here. + +Apply the local decomposition theorem to E_k. The two displayed A ranks +must sum to 2, but the complementary-block lemma makes their sum 4. This +is a contradiction. The B ranks give the same contradiction. + +There are 21 unordered pairs of anchor blocks. The certificate gives the +common point, third block, two forcing labels and two clique witnesses for +each pair. It also checks the required singleton colors. Therefore no two +regular blocks can coexist. + +For example, choose regular blocks 5=236 and 6=245. Their common point is +2, and the third block is 0=012. The labels 017 and 018 would both have +invertible restrictions on block 0. The local rank sum forbids this. +An equivalent zero-propagation proof uses the clique {027,357,467}: +018 forces the 027 restriction to vanish on block 0, and 017 forces the +357 and 467 restrictions to vanish there. Their clique identity cannot +then equal I on that block. + +## Complete coverage of exception sets + +The new argument excludes every exception set with at most five elements. +Here an exception means a block that is not regular, including a zero +restriction. This does not mean that every restriction on that block has +rank zero or two. + +| Exception-set size | Source survivors | Survivors after this proof | +|---|---:|---:| +| 0-3 | 0 | 0 | +| 4 | 28 | 0 | +| 5 | 21 | 0 | +| 6 | 7 | 7 | +| 7 | 1 | 1 | + +The survivor counts describe necessary patterns, not matrix constructions. +The rank sum and local decomposition remain necessary in the last eight +patterns. This proof does not classify all their nonsingleton restrictions. +In particular, a rank-one local summand can contain a zero restriction; +rank-one complementary idempotents do not make a block regular. + +## Cost at the frozen experimental base + +The base is `abdc6a7002abdbcd9e21bfc5e1a795784deacfdf`. At this base, the +selected PR942 record has kappa=1661960547713947/10^18. Its complex coarse +endpoint is b=0.001664727258740678855772 and its bit endpoint is +c=0.001733427039589844234749. The exact base selection is saved unchanged in +`mixed-geometry-base-selection.json`. Its digest is checked without reading +the mutable live selection. The historical PR82 comparator in +`ASSESSMENT.md` is not the selected result at this base. + +The changed block geometry can change the gross rank deficit. It is outside +the fixed E8 profile and owner restrictions. That is why this necessary +nine-point problem remains relevant. Its relevance does not supply a +complete improved construction. + +The replay also checks the inherited optimistic dimension-15, rank-two, +16-point ledger with five roles per label on each axis. Its normalized +volume is W=12, parent dimension is 225, and its charged child counts are + + {4: 1, 26: 4, 30: 10+26/525, 169: 2, 195: 10}. + +These charges include the proposed endpoint, both data calls, four growth +calls, central rank mass and both role boundaries. They grant ideal full +batching. They do not implement source access, copies, restoration, frame +changes, ordered recursive children, or the physical producer. + +Exact integer-power enclosures give moment <1 at a=1/511, approximately +0.999957094. Since b1, approximately 1.003682180. Thus this specific +profile cannot reach kappa>0.01 under the inherited balance condition, +even before the unbuilt interfaces are supplied. + +A bit-only improvement cannot move the frozen outer grid point if the +complex supplier stays fixed. Its necessary ceiling is b/(1+b), which is +strictly between the selected kappa and the next 10^-18 grid point. A useful +complete improvement needs a compatible complex supplier as well. A new +nine-point rational geometry must also extend to 16 points, have a compact +charged producer, and satisfy the copied/ordered transfer interfaces. +Changed maximum children require a new row-stock and finite-bridge check. + +## Separate live-main refresh + +During the sprint, main moved to +`ba82555c64e1879e4b7decce28186f208fcb8262` and selected Jeremy Kothe's +PR1042. The immutable selected record has +kappa=1672188119205421/10^18. Its assembly records +b=0.001674989015937672328468 and the unchanged +c=0.001733427039589844234749. These values were read from that exact Git +commit, after the experiment. They do not replace the experiment's base pins. + +The same comparisons hold: b= 2 + for k in exception) + if hits and not conflict: + old_survivors.append(exception_tuple) + new_counts = {size: sum(len(c) == size for c in old_survivors) for size in (4, 5)} + require(new_counts == {4: 28, 5: 21} and len(old_survivors) == 57 and + [c for c in old_survivors if len(c) >= 6] == expected, 'source survivor census') + budget = verify_budget(data['budget_context']) + return {'normal_form_blocks': 7, 'local_zero_edges': 378, + 'regular_pairs_excluded': 21, 'new_four_exception_exclusions': new_counts[4], + 'new_five_exception_exclusions': new_counts[5], 'remaining_exception_sets': 8, + 'coordinate_Y_control': '42 exact rank-two coordinate projectors; no X extension', + 'budget_context': budget} + + +def verify_budget(data): + """Check the inherited relaxed profile and exact root intervals.""" + d, ell, n, r, roles = 15, 2, 560, 16, Q(5) + m, volume = d * d, 2 + 2 * roles + expected = {(d - ell) ** 2: Q(2), ell ** 2: Q(1), + ell * (d - ell): Q(4), + d * ell: 2 * roles + Q(2 * r * ell * (d - ell), n * d * ell), + m - d * ell: 2 * roles} + require(data['dimension'] == m and Q(data['volume_per_label']) == volume and + Q(data['roles_per_label_per_axis']) == roles, 'relaxed profile parameters') + moments = {} + for check in data['moment_checks']: + degree = check['degree'] + require(degree in (511, 99) and degree not in moments, 'moment degree') + rows = check['roots'] + require(len(rows) == len(expected) and + {row['child']: Q(row['count']) for row in rows} == expected, + 'relaxed profile charges') + lower = upper = Q(0) + for row in rows: + child = row['child'] + lo, hi = map(Q, row['interval']) + require(0 < lo <= hi and lo ** degree <= Q(m, child) <= hi ** degree, + 'root enclosure') + weight = expected[child] * child / (volume * m) + lower += weight * lo + upper += weight * hi + moments[degree] = (lower, upper) + require(set(moments) == {511, 99}, 'moment coverage') + require(moments[511][1] < 1 and moments[99][0] > 1, 'relaxed moment conclusions') + b, c = Q(data['complex_coarse']), Q(data['bit_coarse']) + require(b == Q('0.001664727258740678855772') and + c == Q('0.001733427039589844234749'), 'selected coarse endpoints') + require(0 < b < c < Q(1, 511), 'current coarse comparison') + selected = json.loads((HERE / 'mixed-geometry-base-selection.json').read_text()) + kappa = Q(selected['kappa']) + cap = b / (1 + b) + require(kappa <= cap < kappa + Q(1, 10 ** 18), 'unchanged-complex ceiling') + return {'scope': 'Inherited optimistic profile, not an emitted construction', + 'moment_intervals': {str(Q(1, d)): list(map(str, v)) + for d, v in sorted(moments.items())}, + 'bit_only_next_kappa_grid_point_excluded': True} + + +def local_controls(data): + """Test all three local ranks in a rational basis that is not orthogonal.""" + identity = [[Q(1), Q(0)], [Q(0), Q(1)]] + zero = [[Q(0), Q(0)], [Q(0), Q(0)]] + change = [[Q(1), Q(1)], [Q(0), Q(1)]] + inverse = [[Q(1), Q(-1)], [Q(0), Q(1)]] + block = data['normal_form_blocks'][0] + for rank in (0, 1, 2): + c = multiply(multiply(change, [[Q(rank > 0), 0], [0, Q(rank > 1)]]), inverse) + d = [[identity[i][j] - c[i][j] for j in range(2)] for i in range(2)] + parts = {7: c, 8: d} + factors = {} + for partition in block['partitions']: + z = partition['outside'] + factors[tuple(partition['singleton'])] = (parts[z], parts[z]) + for label in partition['others']: + x = parts[15 - z] + factors[tuple(label)] = (x, [[v / 2 for v in row] for row in x]) + for left, right in block['edges']: + for t, u in ((tuple(left), tuple(right)), (tuple(right), tuple(left))): + require(multiply(factors[t][1], factors[u][0]) == zero, + 'local zero-product control') + for partition in block['partitions']: + total = zero + for label in [partition['singleton']] + partition['others']: + total = add(total, multiply(*factors[tuple(label)])) + require(total == identity, 'local saturation control') + require(multiply(*factors[tuple(partition['singleton'])]) == parts[partition['outside']], + 'local decomposition control') + return 3 + + +def negative_controls(data): + cases = [] + bad = deepcopy(data) + bad['regular_pair_witnesses'].pop() + cases.append(('regular pair coverage', bad)) + bad = deepcopy(data) + bad['regular_pair_witnesses'][0]['forced_labels'][1] = bad['regular_pair_witnesses'][0]['forced_labels'][0] + cases.append(('paired forced labels', bad)) + bad = deepcopy(data) + bad['normal_form_blocks'][0]['edges'].pop() + cases.append(('local edge coverage', bad)) + bad = deepcopy(data) + part = bad['normal_form_blocks'][0]['partitions'][0] + part['singleton'], part['others'][0] = part['others'][0], part['singleton'] + cases.append(('singleton label', bad)) + bad = deepcopy(data) + bad['remaining_exception_sets'].append([0, 1, 2, 3, 4]) + cases.append(('remaining pattern census', bad)) + bad = deepcopy(data) + bad['budget_context']['moment_checks'][0]['roots'][0]['interval'] = ['1', '1'] + cases.append(('root enclosure', bad)) + bad = deepcopy(data) + bad['budget_context']['moment_checks'][0]['roots'][0]['count'] = '0' + cases.append(('relaxed profile charges', bad)) + for reason, bad in cases: + try: + verify(bad) + except ValueError as error: + require(str(error) == reason, 'wrong rejection: ' + str(error)) + else: + raise ValueError('accepted negative control: ' + reason) + return len(cases) + + +if __name__ == '__main__': + parser = argparse.ArgumentParser() + parser.add_argument('certificate', type=Path, nargs='?', default=HERE / 'mixed-geometry-certificate.json') + args = parser.parse_args() + data = json.loads(args.certificate.read_text()) + result = verify(data) + result['local_rational_controls'] = local_controls(data) + result['negative_controls_rejected'] = negative_controls(data) + print(json.dumps(result, indent=2))