diff --git a/research/p112-linear-endpoint-lifts/CERTIFICATE.json b/research/p112-linear-endpoint-lifts/CERTIFICATE.json new file mode 100644 index 0000000000..5eb9e84231 --- /dev/null +++ b/research/p112-linear-endpoint-lifts/CERTIFICATE.json @@ -0,0 +1,511 @@ +{ + "basis_edges": [ + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 0, + 3 + ], + [ + 0, + 4 + ], + [ + 0, + 5 + ], + [ + 0, + 6 + ], + [ + 0, + 12 + ], + [ + 0, + 25 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 1, + 3 + ], + [ + 1, + 4 + ], + [ + 1, + 5 + ], + [ + 1, + 7 + ], + [ + 1, + 16 + ], + [ + 1, + 26 + ], + [ + 2, + 0 + ], + [ + 2, + 1 + ], + [ + 2, + 3 + ], + [ + 2, + 4 + ], + [ + 2, + 5 + ], + [ + 2, + 8 + ], + [ + 2, + 12 + ], + [ + 2, + 27 + ], + [ + 3, + 0 + ], + [ + 3, + 1 + ], + [ + 3, + 2 + ], + [ + 3, + 4 + ], + [ + 3, + 5 + ], + [ + 3, + 9 + ], + [ + 3, + 13 + ], + [ + 3, + 28 + ], + [ + 4, + 0 + ], + [ + 4, + 1 + ], + [ + 4, + 2 + ], + [ + 4, + 3 + ], + [ + 4, + 5 + ], + [ + 4, + 10 + ], + [ + 4, + 14 + ], + [ + 4, + 29 + ], + [ + 5, + 0 + ], + [ + 5, + 1 + ], + [ + 5, + 2 + ], + [ + 5, + 3 + ], + [ + 5, + 4 + ], + [ + 5, + 11 + ], + [ + 5, + 15 + ], + [ + 5, + 30 + ], + [ + 6, + 0 + ], + [ + 6, + 7 + ], + [ + 6, + 8 + ], + [ + 6, + 9 + ], + [ + 6, + 10 + ], + [ + 6, + 11 + ], + [ + 6, + 12 + ], + [ + 6, + 25 + ], + [ + 7, + 1 + ], + [ + 7, + 8 + ], + [ + 8, + 2 + ], + [ + 9, + 3 + ], + [ + 10, + 4 + ], + [ + 11, + 5 + ], + [ + 12, + 0 + ], + [ + 12, + 2 + ], + [ + 12, + 6 + ], + [ + 12, + 13 + ], + [ + 12, + 14 + ], + [ + 12, + 15 + ], + [ + 12, + 16 + ], + [ + 12, + 26 + ], + [ + 13, + 3 + ], + [ + 25, + 0 + ], + [ + 25, + 6 + ], + [ + 25, + 16 + ], + [ + 25, + 17 + ], + [ + 25, + 18 + ], + [ + 25, + 19 + ], + [ + 25, + 20 + ], + [ + 25, + 26 + ], + [ + 26, + 1 + ] + ], + "anchors": [ + 0, + 1, + 2, + 54, + 55, + 76, + 82, + 89 + ], + "edge_vertices": [ + { + "pair": [ + 0, + 1 + ], + "vertex": 107 + }, + { + "pair": [ + 0, + 2 + ], + "vertex": 104 + }, + { + "pair": [ + 0, + 3 + ], + "vertex": 65 + }, + { + "pair": [ + 0, + 4 + ], + "vertex": 64 + }, + { + "pair": [ + 0, + 6 + ], + "vertex": 35 + }, + { + "pair": [ + 0, + 7 + ], + "vertex": 16 + }, + { + "pair": [ + 1, + 2 + ], + "vertex": 100 + }, + { + "pair": [ + 1, + 3 + ], + "vertex": 71 + }, + { + "pair": [ + 1, + 4 + ], + "vertex": 70 + }, + { + "pair": [ + 1, + 5 + ], + "vertex": 48 + }, + { + "pair": [ + 1, + 7 + ], + "vertex": 12 + }, + { + "pair": [ + 2, + 3 + ], + "vertex": 74 + }, + { + "pair": [ + 2, + 4 + ], + "vertex": 73 + }, + { + "pair": [ + 2, + 5 + ], + "vertex": 51 + }, + { + "pair": [ + 2, + 6 + ], + "vertex": 31 + }, + { + "pair": [ + 3, + 5 + ], + "vertex": 4 + }, + { + "pair": [ + 3, + 6 + ], + "vertex": 91 + }, + { + "pair": [ + 3, + 7 + ], + "vertex": 84 + }, + { + "pair": [ + 4, + 5 + ], + "vertex": 5 + }, + { + "pair": [ + 4, + 6 + ], + "vertex": 90 + }, + { + "pair": [ + 4, + 7 + ], + "vertex": 83 + }, + { + "pair": [ + 5, + 6 + ], + "vertex": 85 + }, + { + "pair": [ + 5, + 7 + ], + "vertex": 78 + }, + { + "pair": [ + 6, + 7 + ], + "vertex": 56 + } + ], + "archive_members": { + "candidate/strict/global/base/providers/gauge44/CANONICAL-WORD.json.gz": "16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219", + "candidate/strict/global/base/providers/gauge44/LOCAL-PROGRAMS.json.gz": "241fde27d4e43f5a9cb6b128f9f76c5131a53d09f0371676163f914d0b0fef3a", + "candidate/strict/global/base/work/complex-nine-native/DATA-PHASES.json": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "candidate/strict/global/hosted/GLOBAL-TEMPLATE.json.gz": "2acf02b418078e37090495c601fe550448751d4f35912757b13a1f778efc7760", + "candidate/strict/global/hosted/IDLE-REMAINDER-FRAMES.json.gz": "650c14a1de75015fdae5c02ea18f1d0fd2de35d249b5ff2cd77f3b1afe604985" + } +} diff --git a/research/p112-linear-endpoint-lifts/PROOF.md b/research/p112-linear-endpoint-lifts/PROOF.md new file mode 100644 index 0000000000..6b8e74c3eb --- /dev/null +++ b/research/p112-linear-endpoint-lifts/PROOF.md @@ -0,0 +1,302 @@ +# Endpoint dimension and the cost of linear lifts + +All vector spaces in Sections 1--3 are over the field with two elements. +The ambient form is symmetric and nondegenerate. An endpoint subspace is +nondegenerate for the restricted form. Alternating endpoint planes are allowed. +No positivity assumption is used. + +## 1. The graph and two exact certificates + +Use the 112 binary ports in the selected canonical word. Join distinct +ports a,b when their binary dot product is zero. This is the P112 +source/target interaction graph used by the retained scalar identity. +It has 5,824 ordered edges. Each vertex has a label t_a in dimension 9, +with nondegenerate symmetric form S=I9, such that + + t_a^T S t_a = 1; t_a^T S t_b = 0 on every graph edge. + +The verifier reads the selected source bytes, checks all 12,544 binary +pairings, and checks the following two certificates. No graph isomorphism +to a different port model is assumed. + +**Certificate A.** The edge tensors `t_a tensor t_b` have rank 80 in the +81-dimensional matrix space. The 80 listed edges form a basis. S is a +nonzero null vector, so every bilinear form K that vanishes on graph edges +is `K = c S`. + +**Certificate B.** There is an eight-vertex clique with vertices a_0,...,a_7. +There are 24 further vertices b_ij, one for each edge ij of a graph J on +eight points. J is K8 with one perfect matching removed. Vertex b_ij is +adjacent to every a_k except a_i,a_j. Two b vertices are adjacent exactly +when their J edges have a common endpoint. In particular J is 6-regular. +The certificate lists the 32 distinct vertices. The verifier checks every +required and absent edge, rather than accepting a claimed graph name. + +The certificates are finite premises of the following all-size arguments. +The verifier is not a proof-assistant formalization of those arguments. + +## 2. Sharp dimension bound for arbitrary two-plane labels + +Suppose each graph vertex is assigned a nondegenerate two-dimensional +subspace U_a in an h-dimensional space, and graph edges give orthogonal +subspaces. The assignment need not depend linearly on the old labels. +Then **h >= 18**. The binary tensor construction `U_a = t_a tensor F2^2` +in the form `S tensor I2` attains 18. + +The eight anchor planes in Certificate B are mutually orthogonal. Their +orthogonal direct sum E has dimension 16. Thus h >= 16. Put +`H = E_0 perpendicular ... perpendicular E_7 perpendicular Z`. +For h <= 17, the dimension z of Z is zero or one. The plane U_ij lies in +`E_i + E_j + Z` because it is orthogonal to the other six anchor planes. + +Choose any basis for each U_ij. Its nondegenerate 2-by-2 Gram matrix is D_ij. +Let K_ij,i be the Gram matrix of its projection to E_i, and let R_ij be +the Gram matrix of its projection to Z. Thus + + D_ij = K_ij,i + K_ij,j + R_ij. (1) + +For a fixed i, collect the six incident planes in one matrix. Their E_i +projection has a Gram matrix K_i of rank at most two. Their Z projection +has a Gram matrix R_i of rank at most z. Distinct incident planes are +orthogonal, and their other anchor blocks differ. Therefore the off-diagonal +blocks of K_i and R_i agree. Hence + + H_i = K_i + R_i + +is block diagonal, with blocks `H_ij,i = K_ij,i + R_ij`, and + + sum_(j:ij in J) rank(H_ij,i) = rank(H_i) <= 2 + z. (2) + +If z=0, (1) gives `2 <= rank(H_ij,i) + rank(H_ij,j)`. +Summing over 24 edges contradicts (2): `48 <= 16`. + +If z=1, choose the unit basis of Z. Write its coordinate row on U_ij as +u_ij, so `R_ij = u_ij^T u_ij`. Characteristic two gives + + D_ij = H_ij,i + H_ij,j + u_ij^T u_ij. + +Thus `rank(H_ij,i) + rank(H_ij,j) >= 1`. Summing over J and using (2) +gives equality throughout: the total is 24, every vertex contributes 3, +and every edge contributes 1. Also every u_ij is nonzero; otherwise its +edge would need a contribution at least 2. + +At each vertex i there are therefore three rank-one diagonal blocks in +H_i and three zero blocks. Let u_i be the concatenation of its six rows +u_ij. It has a nonzero component at every zero block. Consequently +`u_i^T` is not in the image of H_i. A rank-one update by this vector +cannot reduce rank: if `(H_i + u_i^T u_i)x=0`, then +`H_i x = u_i^T (u_i x)`. Since `u_i^T` is not in the image of H_i, +we have `u_i x=0` and `H_i x=0`. The new kernel is contained in the old +kernel. Hence + + rank(K_i) = rank(H_i + u_i^T u_i) >= rank(H_i) = 3, + +contrary to `rank(K_i) <= 2`. This excludes h=17 and proves the bound. + +This theorem fixes the least ambient dimension. It does not classify all +dimension-18 assignments or bound the cost of every new word on them. + +## 3. Rigidity of all coupled linear lifts + +Let V have dimension r >= 1. Let `A: F2^9 tensor V -> H` be linear and +write `A(t)v = A(t tensor v)`. Assume all spaces `A(t_a)V` have dimension +r and a nondegenerate restricted form. Require them to be orthogonal on +every graph edge. There is no block-diagonal or independent-copy assumption. + +For v,w in V, the function + + K_(v,w)(x,y) = + +is a bilinear form on the old nine-dimensional space and vanishes on all +graph edges. Certificate A gives a scalar D(v,w) such that + + K_(v,w)(x,y) = (x^T S y) D(v,w). (3) + +Linearity shows that D is bilinear. Symmetry of the ambient form shows +that D is symmetric. At any vertex t_a, (3) restricts to D because +`t_a^T S t_a=1`. Nondegeneracy of the endpoint makes D nondegenerate. +Thus the pullback Gram matrix of A is `S tensor D`, of rank 9r. +The map A is injective, its image is nondegenerate, and h >= 9r. + +For every old subspace U, its image is `A(U tensor V)` and has dimension +`r dim(U)`. Intersections, sums and orthogonal complements inside this +image are the old ones tensored with V. This proves rigidity for every +fibre size, every ambient dimension, and all linear couplings. + +## 4. The complete accounting class + +The cost conclusion concerns an endpoint lift of a fixed complete supplier +and controller diagram. This condition matters. It does not cover a new +scalar program or a new controller that reuses stages in a different way. + +The reference diagram includes every source-access edge, helper edge, +copied-centre edge, restoration edge and idle child. It has ambient width m, +W live role streams of equal volume, and paid edge ranks t_e. Each scalar +gate uses a common exact frame on all its incident streams. In the selected +instance, `m=73`, `W=14336`, and the complete histogram is + + {1:349604, 2:60192, 3:62585, 4:20448, + 5:11808, 7:7, 8:1152, 48:4866}. + +The linear lift replaces the old core by its r-fold tensor image. In the +retained nine-stage orthogonal-slot controller, this has width 73r. At each +retained boundary, the lifted subspace has intersection with this core equal +to the image of the old boundary subspace. Additional ambient coordinates +are permitted, with arbitrary slanted subspaces, nonmonotone transitions, +and extra gates. Their entrance quotient dimension is zero and their final +quotient dimension is their full width on every live role. The complete +auxiliary/centre ledger must also be retained. An auxiliary input does not +become a known-zero input. All W physical live streams persist through the +serialized schedule. A local role can use a different owner in a later call; +this does not move a physical stream path to a private centre. Each scalar +operation has the same frame before and after on each incident live path. +Private centre paths can start and end at different padding dimensions. +Their costs are nonnegative. They are not used in the signed sum below. + +Each individual retained role-stream edge may use any exact native +factorization, with any number of rank-zero adapters. Joint children that +encode several arrays or combine different frozen edges are outside this class. No assumption that its old child is run r times is +made. Each native child acts on the original role-stream volume; creating +extra role streams does not create extra normalization weight. A factorization +that crosses a retained scalar-gate boundary changes the reference diagram +and is outside this class. + +### Source-bound minimum-rank bridge + +The selected archive is `research/community-frontier1094-audit/selected-replay.tar.gz` +at the base commit in SOURCES.json. The verifier reads five exact members from +this Git object. It does not use historical files with similar names. Each +member has a SHA256 pin in CERTIFICATE.json. + +The source frame lemma in `notes/general-clifford-frames.tex` gives + + rank B(T_V T_U^(-1)) = dim U + dim V - 2 dim(U intersect V). + +This is an exact Fourier-rank identity. It applies to degenerate U and V, +and does not require the operators T_U and T_V to commute. The verifier +checks that this note has the same bytes as the copy in the selected source +manifest. Reverse/complement words preserve the same transition distance. + +For each of the two emitted local programs, the verifier reads every `climb` +and `center` edge and computes this distance from its actual binary frame +bases. It checks equality with the paid rank, not only a lower bound. There +are 3,494 edges per orientation. All eight private-centre edges go between +the specified rank-eight centre frame and the zero frame. Each has minimum +rank eight. Copying the centre value at its high frame does not erase that +transition. The total local rank mass is 5,586. + +The selected global controller contains 144 complete calls. Its 704 local +roles per call have distinct owners in the live range [0,14336); the private +centre range is separate. The verifier checks this assignment, the complete +per-replica event order, and the final live-family range. Thus changing a +helper's owner between calls changes the local role name, not the identity +of a physical stream. The selected owner audit supplies the inherited exact +chart and busy-window validity. This package does not repeat that audit. + +For each of the 7,526 idle children, the verifier reads the actual remainder +axes, checks the matching controller row, and checks that they are the exact +suffix of the inherited pending axes. It checks that their Gram matrix is +identity. This is a coordinate Fourier child on that subspace, so its minimum +rank is the number of these axes. Its entrance and exit frames have this +exact distance. The idle histogram is `{1:2276, 3:377, 7:7, 48:4866}`. +Adding the 144 literal local histograms gives the full histogram above and +rank mass 1,041,408. All 510,662 reference native children are included. +There is no unexamined histogram entry that could conceal an overcharged +reference transition. + +Exact scalar identities, phases, source wrappers, and the controller's charts +remain inherited from the selected review. The fresh check covers ranks and +stream accounting; it is not a cold replay of the supplier or compiler. + +## 5. No native factorization or ambient padding improves the moment + +Write `p=1-b`, with `0= r t_e`. Since `sum_j k_j^p >= (sum_j k_j)^p`, its +moment charge is at least `(r t_e/(rm))^p = (t_e/m)^p`. +One rank-r t_e child attains this lower bound whenever it is available; +granting it for free as an interface is an optimistic relaxation otherwise. + +Now add z>0 ambient coordinates. Put `M'=rm+z` and `lambda=rm/M'`. +At a boundary B let q_B be its dimension outside the tensor core. +For an old edge U->V, let `d_e=|q_V-q_U|`. The subspace distance satisfies + + distance(U',V') >= r distance(U,V) + d_e. (4) + +To see this, the core part of `U' intersect V'` has dimension +`r dim(U intersect V)`, and its quotient part has dimension at most +`min(q_U,q_V)`. Substitute in `dim U' + dim V' - 2 dim(U' intersect V')`. +This proof allows slanted frames and does not assume an orthogonal splitting +at each gate. The same native-factorization argument bounds an edge's charge +below by `((r t_e+d_e)/M')^p`. + +Sum signed q changes separately along each physical live stream. Scalar +operations do not change q on that path. This includes a copy from a live +stream to a private centre: it creates a private value but preserves the +live path and its frame. Rank-zero adapters preserve the preimage frame. +The native transitions on each live path therefore have net change z. +Their absolute changes sum to at least z. Summing the W live paths gives +`sum_e d_e >= Wz`, before any private-path cost is added. Private descents +cannot cancel this lower bound. New edges have old rank zero. Also +`0<=d_e/z<=1`. Concavity gives, edge by edge, + + ((r t_e+d_e)/M')^p + >= lambda (t_e/m)^p + (1-lambda) (d_e/z)^p. + +Summing, and using `x^p>=x` on [0,1], gives + + M_lift(p) >= lambda M(p) + (1-lambda). (5) + +If the reference moment is at least one, the lifted moment is at least one. +This includes arbitrary padding size, all extra transitions and every native +factorization at the retained boundaries. The unpadded tensor lift attains the +same moment in the ideal native-child model. Thus the optimal complex moment +exponent cannot increase in this class. A second unpaid direction is offset by +the forced growth of every geometric rank and of the ambient denominator. + +## 6. Consequence for the selected kappa grid + +The exact accounting check reconstructs the selected full histogram and +checks + + M(1-b_low) < 1 < M(1-b_high), + b_low = 0.001675462676808103522925, + b_high = b_low + 10^-24. + +It also checks the exact rational inequality + + b_high/(1+b_high) < 0.001672660197076919. + +The retained balanced outer reduction requires `kappa < b/(1+b)`. +Equation (5) therefore excludes the next 10^-18 kappa grid point and every +larger one for this lift class, even before new scalar, chart, source-access, +movement, restoration, or finite-invoice costs are imposed. Those costs are +nonnegative. The original bit supplier is retained; its restriction can only +decrease the feasible outer saving. Its raw exponent is not substituted for +an outer kappa. This result neither changes nor reproves the selected supplier. + +The all-size compiler, exact common-frame realization, whole-call hosting, +precision/tape, analytic transfer and bit H1--H5 conditions remain inherited. +Arbitrary dimension-18 plane assignments, other interaction graphs, new scalar +programs, and new outer reductions remain outside the no-improvement theorem. + +## 7. Relation to general endpoint labels + +The arbitrary-plane theorem in Section 2 is stronger than the linear-lift +hypothesis as a statement about dimension. It does not imply Section 5 for +all plane assignments. In dimension 18, a nonlinear assignment might have +other intersections at internal frames and might admit a new scalar word. +No classification or cost bound for those words is proved here. + +PR791, at `f80382efd4cd3e37c67b2a966398b55bb56af53c`, proves a separate +rational-idempotent path formula. Its rank-two examples show that a generic +endpoint penalty need not double. This proof does not assume that rule. +Section 3 first forces a tensor pullback form in the linear class. The +actual preimage-frame distances then scale by r. Without that rigidity or +without the retained boundaries, this rank-scaling conclusion is not used. diff --git a/research/p112-linear-endpoint-lifts/README.md b/research/p112-linear-endpoint-lifts/README.md new file mode 100644 index 0000000000..21061653b4 --- /dev/null +++ b/research/p112-linear-endpoint-lifts/README.md @@ -0,0 +1,162 @@ +# P112 endpoint dimension and linear-lift obstruction + +**Scoped negative result. No new kappa.** Any nondegenerate two-plane +representation of the selected P112 interaction graph needs ambient dimension +at least 18. This bound is sharp. For arbitrary coupled linear endpoint lifts, +the graph forces a tensor form in every fibre dimension. In the retained +supplier and controller, these lifts cannot improve the complex moment exponent. + +The proof permits arbitrary native factorizations of each individual retained +role-stream edge, rank-zero adapters, and any number of extra coordinates. +Extra frames can be slanted and nonmonotone. The scalar-gate boundaries and +physical live stream paths remain fixed. Joint children that encode several +arrays or combine different frozen edges are outside the theorem. + +This closes a concrete coverage-law proposal: replacing each old unpaid line +by a plane does not give two free coordinates at the old geometric cost. +Even arbitrary nonlinear plane labels need twice the old local dimension. +For linear lifts, the complete rank cost grows with the unpaid dimension. +The broader question of a new word on nonlinear dimension-18 labels stays open. + +## Results and full cost + +[PROOF.md](PROOF.md) gives three arguments. + +1. A 32-vertex subgraph forces ambient dimension at least 18 for arbitrary + nondegenerate two-plane labels. The form can be any nondegenerate symmetric + binary form. Alternating planes are allowed. The tensor construction attains 18. +2. The 5,824 ordered graph-edge tensors span dimension 80 of the 81-dimensional + bilinear-form space. Thus a linear lift with fibre dimension r has pullback + form `I9 tensor D`, where D is nondegenerate. It needs dimension at least 9r. +3. Let M(p) be the complete reference moment. With z extra coordinates and + `lambda=73r/(73r+z)`, every lift in the declared class satisfies + `M_lift(p) >= lambda M(p) + 1-lambda` for every `0 0, 'positive paid rank') + paid[charge] += 1 + require(sorted(centres) == list(range(8)), 'all private centre transitions') + require(dict(paid) == LOCAL, 'literal paid local histogram') + report[orientation] = {'native_edges': sum(paid.values()), 'centre_edges': 8, + 'rank_mass': sum(k * v for k, v in paid.items())} + require(set(report) == {'forward', 'backward'}, 'both orientations') + return report + + +def check_global(word, programs, template, idle_frames, phases): + require((template['m'], template['live'], template['physical']) == (73, 14336, 14826), + 'selected global dimensions') + require(template['private_namespace'] == { + 'centers': [14336, 14344], 'reserved_tableau': [14344, 14824], + 'coefficient': [14824, 14826]}, 'private/live namespace separation') + require(set(template['local_providers']) == {'gauge44'}, 'selected provider') + provider = template['local_providers']['gauge44'] + require(provider['local_programs'] == programs, 'hosted programs equal selected programs') + require(provider['ports'] == word['ports'], 'hosted port binding') + calls = template['calls'] + require(len(calls) == 144, 'call count') + require({(c['stage'], c['replica']) for c in calls} + == {(s, r) for s in range(9) for r in range(16)}, 'all controller calls') + for index, call in enumerate(calls): + owners = [x[0] for x in call['owners']] + require(len(owners) == len(set(owners)) == 704, 'injective whole-call owners') + require(all(0 <= x < 14336 for x in owners), 'all helper roles on live paths') + require(call['time'] == index, 'serialized call order') + require(call['orientation'] in programs, 'call orientation') + schedule = template['execution_schedule'] + per_replica = {r: [] for r in range(16)} + local_order, block = [], -1 + for event in schedule[:-2]: + require('replica' in event, 'per-replica event') + replica = event['replica'] + per_replica[replica].append(event['source_event']) + if event['kind'] == 'local_cover_sweep': + block += 1 + local_order.append((event['stage'], replica)) + require(event['time'] == block, 'complete call before owner reassignment') + require(local_order == [(c['stage'], c['replica']) for c in calls], 'local schedule order') + require(all(order == list(range(30)) for order in per_replica.values()), 'complete replica paths') + require(schedule[-1]['families'] == [0, 14336] + and schedule[-1]['charged_calls_per_cover'] == 14336, 'all final live paths') + require(schedule[-2]['families'] == [14336, 14336], 'no bank replaces a live path') + require(len(idle_frames) == len(template['idle_children']) == 7526, 'idle child count') + paid = Counter() + for frame, child in zip(idle_frames, template['idle_children']): + require({k: v for k, v in frame.items() if k != 'orthogonal_axes'} == child, + 'idle frame/controller binding') + axes = frame['orthogonal_axes'] + inherited = phases['recipes'][frame['port']]['idle_children'][frame['child']]['orthogonal_axes'] + require(axes == inherited[frame['pending_offset']:], 'literal pending frame tail') + require(len(axes) == frame['rank'] and rank(axes) == len(axes), 'idle minimum rank') + require(all(0 < x < (1 << 73) for x in axes), 'idle axis width') + require(all((x & y).bit_count() % 2 == int(i == j) + for i, x in enumerate(axes) for j, y in enumerate(axes)), 'orthogonal idle axes') + paid[frame['rank']] += frame['replicas'] + idle_histogram = dict(sorted(paid.items())) + for call in calls: + paid.update(LOCAL) + require(dict(paid) == GLOBAL, 'complete global histogram') + return {'live_paths': 14336, 'complete_calls': 144, 'whole_call_owner_roles': 144 * 704, + 'idle_children': len(idle_frames), 'idle_histogram': idle_histogram, + 'paid_histogram': dict(sorted(paid.items())), + 'rank_mass': sum(k * v for k, v in paid.items()), + 'scope': 'Frame ranks, selected program binding, and persistent ownership; no scalar-map or cold compiler replay.'} diff --git a/research/p112-linear-endpoint-lifts/arithmetic.py b/research/p112-linear-endpoint-lifts/arithmetic.py new file mode 100644 index 0000000000..66a2bf1bde --- /dev/null +++ b/research/p112-linear-endpoint-lifts/arithmetic.py @@ -0,0 +1,57 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Enclose the complete selected moment with rational series bounds.""" +from fractions import Fraction as Q +from functools import lru_cache + +EPS = Q(1, 1 << 192) + + +def atanh_log(value): + t = (value - 1) / (value + 1) + if not 0 <= t <= Q(1, 3): + raise ValueError('log series domain') + total, power, k = Q(0), t, 0 + while True: + total += power / (2 * k + 1) + power *= t * t + k += 1 + tail = 2 * power / ((2 * k + 1) * (1 - t * t)) + if tail < EPS: + return 2 * total, 2 * total + tail + + +@lru_cache(None) +def log_ratio(m, r): + value, k = Q(m, r), 0 + while value >= 2: + value /= 2 + k += 1 + lo, hi = atanh_log(value) + l2, u2 = atanh_log(Q(2)) + return lo + k * l2, hi + k * u2 + + +def exponential(value): + if not 0 <= value <= Q(1, 2): + raise ValueError('exp series domain') + total, term, k = Q(1), Q(1), 0 + while True: + k += 1 + term *= value / k + total += term + next_term = term * value / (k + 1) + tail = next_term / (1 - value / (k + 2)) + if tail < EPS: + return total, total + tail + + +def moment(histogram, m, live, saving): + low, high = Q(0), Q(0) + for rank, count in histogram.items(): + lo, hi = log_ratio(m, rank) + a = exponential(saving * lo)[0] + b = exponential(saving * hi)[1] + scale = Q(count * rank, m * live) + low += scale * a + high += scale * b + return low, high diff --git a/research/p112-linear-endpoint-lifts/controls.py b/research/p112-linear-endpoint-lifts/controls.py new file mode 100644 index 0000000000..6e075c3966 --- /dev/null +++ b/research/p112-linear-endpoint-lifts/controls.py @@ -0,0 +1,99 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Check rejected premises and small exact controls for the proof lemmas.""" +from copy import deepcopy +from itertools import combinations_with_replacement +from accounting import check_local, distance +from geometry import model, rank, require, verify_graph_certificate + + +def reject(name, operation, expected): + try: + operation() + except ValueError as error: + require(str(error) == expected, 'unexpected rejection: ' + name) + else: + raise ValueError('control accepted: ' + name) + return name + + +def run(certificate, word, programs): + labels, form, edges = model(word['ports']) + rejected = [] + bad = deepcopy(certificate) + bad['basis_edges'][0] = [0, 0] + rejected.append(reject('nonedge in tensor basis', + lambda: verify_graph_certificate(bad, labels, form, edges), 'basis edge membership')) + bad = deepcopy(certificate) + bad['basis_edges'].pop() + rejected.append(reject('missing tensor basis edge', + lambda: verify_graph_certificate(bad, labels, form, edges), 'basis has 80 distinct edges')) + bad = deepcopy(certificate) + bad['edge_vertices'][0]['vertex'] = bad['anchors'][0] + rejected.append(reject('aliased anchor witness', + lambda: verify_graph_certificate(bad, labels, form, edges), 'distinct witness vertices')) + bad = deepcopy(programs) + next(e for e in bad['forward'] if e[0] == 'center')[-1] = 7 + rejected.append(reject('rank-seven charge for rank-eight centre', + lambda: check_local(word, bad), 'minimum Fourier rank')) + bad = deepcopy(programs) + next(e for e in bad['forward'] if e[0] == 'climb')[-1] += 1 + rejected.append(reject('overcharged reference edge', + lambda: check_local(word, bad), 'minimum Fourier rank')) + + # If nondegeneracy is removed, every endpoint can be one isotropic plane. + isotropic = [0b0011, 0b1100] + require(rank(isotropic) == 2 and all((x & y).bit_count() % 2 == 0 + for x in isotropic for y in isotropic), 'degenerate endpoint counterexample') + + # This control includes an alternating fibre and a coupled non-diagonal fibre. + forms = [[[1, 0], [0, 1]], [[0, 1], [1, 0]], [[1, 1], [1, 0]]] + for fibre in forms: + gram = [[form[i // 2][j // 2] * fibre[i % 2][j % 2] + for j in range(18)] for i in range(18)] + require(rank([sum(x << j for j, x in enumerate(row)) for row in gram]) == 18, + 'sharp dimension tensor witness') + require(rank([sum(x << j for j, x in enumerate(row)) for row in fibre]) == 2, + 'nondegenerate fibre') + + updates = 0 + positions = list(combinations_with_replacement(range(4), 2)) + for code in range(1 << len(positions)): + matrix = [0] * 4 + for bit, (i, j) in enumerate(positions): + if code >> bit & 1: + matrix[i] |= 1 << j + matrix[j] |= 1 << i + old_rank = rank(matrix) + for u in range(1, 16): + if rank(matrix + [u]) == old_rank: + continue + updated = [row ^ (u if u >> i & 1 else 0) for i, row in enumerate(matrix)] + require(rank(updated) >= old_rank, 'rank-one update outside the image') + updates += 1 + + # Enumerate all subspaces in four dimensions, including slanted subspaces. + spaces = {frozenset({0})} + pending = list(spaces) + while pending: + space = pending.pop() + for v in range(1, 16): + other = space | frozenset(x ^ v for x in space) + if other not in spaces: + spaces.add(other) + pending.append(other) + require(len(spaces) == 67, 'four-dimensional subspace census') + pairs = 0 + for first in spaces: + for second in spaces: + core_first = [x for x in first if x < 4] + core_second = [x for x in second if x < 4] + q_first = rank(first) - rank(core_first) + q_second = rank(second) - rank(core_second) + require(distance(list(first), list(second)) >= + distance(core_first, core_second) + abs(q_first - q_second), + 'padding quotient distance') + pairs += 1 + return {'rejected_mutations': rejected, 'degenerate_dimension_four_counterexample': True, + 'dimension_eighteen_fibre_forms': forms, 'rank_one_update_cases': updates, + 'padding_subspace_pairs': pairs, + 'scope': 'Finite controls for the stated premises; the all-size proofs are in PROOF.md.'} diff --git a/research/p112-linear-endpoint-lifts/geometry.py b/research/p112-linear-endpoint-lifts/geometry.py new file mode 100644 index 0000000000..d86355c23c --- /dev/null +++ b/research/p112-linear-endpoint-lifts/geometry.py @@ -0,0 +1,86 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Construct the exact P112 graph and its binary label model.""" +from itertools import combinations + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def rank(rows): + pivots = {} + for row in rows: + while row: + pivot = row.bit_length() - 1 + if pivot in pivots: + row ^= pivots[pivot] + else: + pivots[pivot] = row + break + return len(pivots) + + +def model(ports): + require(len(ports) == len(set(ports)) == 112, 'selected port count') + require(all(0 < x < 512 and x.bit_count() % 2 == 1 for x in ports), + 'norm-one binary ports') + require(rank(ports) == 9, 'port span') + labels = [[(x >> j) & 1 for j in range(9)] for x in ports] + form = [[int(i == j) for j in range(9)] for i in range(9)] + edges = [[a, b] for a in range(112) for b in range(112) + if a != b and (ports[a] & ports[b]).bit_count() % 2 == 0] + require(len(edges) == 5824, 'ordered edge count') + return labels, form, edges + + +def tensor_row(labels, edge): + a, b = edge + return sum((labels[a][i] * labels[b][j]) << (9 * i + j) + for i in range(9) for j in range(9)) + + +def basis_edges(labels, edges): + pivots, chosen = {}, [] + for edge in edges: + row = tensor_row(labels, edge) + while row: + pivot = row.bit_length() - 1 + if pivot in pivots: + row ^= pivots[pivot] + else: + pivots[pivot] = row + chosen.append(edge) + break + return chosen + + +def verify_graph_certificate(certificate, labels, form, edges): + edge_set = {tuple(edge) for edge in edges} + chosen = certificate['basis_edges'] + require(len(chosen) == 80 and len({tuple(x) for x in chosen}) == 80, + 'basis has 80 distinct edges') + require(all(tuple(edge) in edge_set for edge in chosen), 'basis edge membership') + require(rank([tensor_row(labels, edge) for edge in chosen]) == 80, 'edge tensor rank') + null = sum(form[i][j] << (9 * i + j) for i in range(9) for j in range(9)) + require(all((tensor_row(labels, e) & null).bit_count() % 2 == 0 for e in edges), + 'bilinear null form') + anchors = certificate['anchors'] + pairs = certificate['edge_vertices'] + require(len(anchors) == 8 and len(pairs) == 24, 'anchor certificate size') + require(len(set(anchors + [x['vertex'] for x in pairs])) == 32, 'distinct witness vertices') + require(all((a, b) in edge_set for a, b in combinations(anchors, 2)), 'anchor clique') + support = {tuple(x['pair']): x['vertex'] for x in pairs} + require(len(support) == 24 and all(0 <= i < j < 8 for i, j in support), + 'edge-vertex indexing') + missing = [p for p in combinations(range(8), 2) if p not in support] + require(len(missing) == 4 and sorted(i for p in missing for i in p) == list(range(8)), + 'missing perfect matching') + for pair, vertex in support.items(): + require(all(((vertex, a) in edge_set) == (k not in pair) + for k, a in enumerate(anchors)), 'anchor incidence') + for (pair, a), (other, b) in combinations(support.items(), 2): + require(((a, b) in edge_set) == bool(set(pair) & set(other)), 'edge incidence') + return {'ordered_edges': len(edges), 'tensor_rank': 80, 'nullity': 1, + 'anchor_vertices': 8, 'edge_vertices': 24, + 'edge_vertex_undirected_edges': 120, 'minimum_two_plane_dimension': 18} diff --git a/research/p112-linear-endpoint-lifts/verify.py b/research/p112-linear-endpoint-lifts/verify.py new file mode 100644 index 0000000000..2a1b1394e2 --- /dev/null +++ b/research/p112-linear-endpoint-lifts/verify.py @@ -0,0 +1,123 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Verify source-bound premises and exact accounting for the endpoint theorems.""" +import argparse +import gzip +import hashlib +import io +import json +from pathlib import Path +import subprocess +import tarfile +from fractions import Fraction as Q + +from accounting import GLOBAL, check_global, check_local +from arithmetic import moment +from controls import run as controls +from geometry import model, require, verify_graph_certificate + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +ARCHIVE = 'research/community-frontier1094-audit/selected-replay.tar.gz' +PREFIX = 'candidate/strict/global/' +MEMBERS = { + 'word': PREFIX + 'base/providers/gauge44/CANONICAL-WORD.json.gz', + 'programs': PREFIX + 'base/providers/gauge44/LOCAL-PROGRAMS.json.gz', + 'phases': PREFIX + 'base/work/complex-nine-native/DATA-PHASES.json', + 'template': PREFIX + 'hosted/GLOBAL-TEMPLATE.json.gz', + 'idle_frames': PREFIX + 'hosted/IDLE-REMAINDER-FRAMES.json.gz', +} + + +def source_bytes(name, sources): + row = next(x for x in sources['files'] if x['path'] == name) + data = subprocess.check_output(['git', 'show', sources['base_commit'] + ':' + name], cwd=ROOT) + require(hashlib.sha256(data).hexdigest() == row['sha256'], 'source SHA256: ' + name) + return data + + +def load_inputs(sources, certificate): + raw = source_bytes(ARCHIVE, sources) + inputs = {} + with tarfile.open(fileobj=io.BytesIO(raw), mode='r:gz') as archive: + for key, name in MEMBERS.items(): + data = archive.extractfile(name).read() + require(hashlib.sha256(data).hexdigest() == certificate['archive_members'][name], + 'archive member SHA256: ' + name) + inputs[key] = json.loads(gzip.decompress(data) if name.endswith('.gz') else data) + return inputs + + +def enclosure(low, high): + scale = 10 ** 55 + return [str(Q((low * scale).numerator // (low * scale).denominator, scale)), + str(Q(-((-high * scale).numerator // (-high * scale).denominator), scale))] + + +def verify(): + sources = json.loads((PACKAGE / 'SOURCES.json').read_text()) + certificate = json.loads((PACKAGE / 'CERTIFICATE.json').read_text()) + inputs = load_inputs(sources, certificate) + word, programs = inputs['word'], inputs['programs'] + labels, form, edges = model(word['ports']) + graph = verify_graph_certificate(certificate, labels, form, edges) + local = check_local(word, programs) + global_bill = check_global(**inputs) + selected = json.loads(source_bytes('research/community-frontier1094-audit/ASSEMBLY.json', sources)) + require({int(k): v for k, v in selected['complex_profile'].items()} == GLOBAL, + 'selected assembly profile') + selected_manifest = json.loads(source_bytes( + 'research/community-frontier1094-audit/SELECTED-SOURCE.json', sources)) + bindings = {} + for name in ('research/gauge44-slots-t16/code/audit_allcold.py', + 'research/gauge44-slots/code/invoice_allcold.py', + 'research/gauge44-slots/independent/audit_local.py'): + digest = hashlib.sha256(source_bytes(name, sources)).hexdigest() + require(selected_manifest['files'][name] == digest, 'selected code binding') + bindings[name] = digest + frame_note = hashlib.sha256(source_bytes('notes/general-clifford-frames.tex', sources)).hexdigest() + require(frame_note == selected_manifest['files'][ + 'research/complex-sw4-frame8/vendor/main/research/complex-k492-owner-repair/' + 'vendor/multicold/vendor/pr559/notes/general-clifford-frames.tex'], 'selected frame lemma binding') + b_low = Q(selected['complex_lower']) + b_high = b_low + Q(1, 10 ** 24) + at_low, at_high = moment(GLOBAL, 73, 14336, b_low), moment(GLOBAL, 73, 14336, b_high) + require(at_low[1] < 1 < at_high[0], 'exact complex root bracket') + next_kappa = Q(selected['kappa']) + Q(1, 10 ** 18) + ideal_cap = b_high / (1 + b_high) + require(ideal_cap < next_kappa, 'next outer kappa grid point excluded') + report = { + 'status': 'PASS_P112_ENDPOINT_DIMENSION_AND_LINEAR_LIFT_OBSTRUCTION', + 'base_commit': sources['base_commit'], 'graph': graph, + 'local_minimum_ranks': local, 'global_accounting': global_bill, + 'selected_source_code_sha256': bindings, 'frame_distance_lemma_sha256': frame_note, + 'moment': {'b_low': str(b_low), 'b_high': str(b_high), + 'at_low_minus_one': enclosure(at_low[0] - 1, at_low[1] - 1), + 'at_high_minus_one': enclosure(at_high[0] - 1, at_high[1] - 1)}, + 'outer': {'selected_kappa': selected['kappa'], 'excluded_next_grid': str(next_kappa), + 'optimistic_complex_cap': str(ideal_cap), + 'retained_raw_bit_lower': selected['bit_lower'], + 'scope': 'The complex necessary condition alone excludes the next selected grid point. The bit and finite-invoice conditions can only restrict it further.'}, + 'controls': controls(certificate, word, programs), + 'proof_scope': 'All-size handwritten proofs use the checked finite graph premises and frame-distance lemma. No proof-assistant formalization or fresh cold replay is claimed.', + } + return report + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--output', type=Path, help='Write the checked report to this path.') + args = parser.parse_args() + report = verify() + if args.output: + args.output.write_text(json.dumps(report, indent=2, sort_keys=True) + '\n') + else: + expected = json.loads((PACKAGE / 'RESULT.json').read_text()) + require(json.loads(json.dumps(report)) == expected, 'stored report mismatch') + print(report['status']) + print('tensor_rank=80; arbitrary_two_plane_dimension=18; local_edges=3494 per orientation; idle_edges=7526') + print('exact_complex_bracket=PASS; next_kappa_grid=EXCLUDED; controls=PASS') + + +if __name__ == '__main__': + main()