From 2f586ad5253a0a8065bf444f33f728b93129b0ed Mon Sep 17 00:00:00 2001 From: apoursh <8867770+apoursh@users.noreply.github.com> Date: Sat, 24 Oct 2026 23:41:49 -0400 Subject: [PATCH] research: prove twenty-field helper block has a 38-H1 floor --- .../helper300-twenty-field-floor/PROOF.md | 265 ++++++++++++ .../helper300-twenty-field-floor/README.md | 145 +++++++ .../helper300-twenty-field-floor/RESULT.json | 1 + .../helper300-twenty-field-floor/SOURCES.json | 42 ++ .../helper300-twenty-field-floor/TASK.json | 99 +++++ .../helper300-twenty-field-floor/VERIFY.json | 77 ++++ .../check_certificate.py | 193 +++++++++ .../check_window.py | 381 ++++++++++++++++++ .../helper300-twenty-field-floor/verify.py | 336 +++++++++++++++ 9 files changed, 1539 insertions(+) create mode 100644 research/helper300-twenty-field-floor/PROOF.md create mode 100644 research/helper300-twenty-field-floor/README.md create mode 100644 research/helper300-twenty-field-floor/RESULT.json create mode 100644 research/helper300-twenty-field-floor/SOURCES.json create mode 100644 research/helper300-twenty-field-floor/TASK.json create mode 100644 research/helper300-twenty-field-floor/VERIFY.json create mode 100644 research/helper300-twenty-field-floor/check_certificate.py create mode 100644 research/helper300-twenty-field-floor/check_window.py create mode 100644 research/helper300-twenty-field-floor/verify.py diff --git a/research/helper300-twenty-field-floor/PROOF.md b/research/helper300-twenty-field-floor/PROOF.md new file mode 100644 index 0000000000..de6d3b44cb --- /dev/null +++ b/research/helper300-twenty-field-floor/PROOF.md @@ -0,0 +1,265 @@ +# Exact 38-H1 floor for the twenty-field backward boundary + +## Result and scope + +For the selected backward provider's event interval **[9044,9137)**, let the +field set be the dependency closure of roles {19,300,301}. Every exact +replacement in the following model has the source's original per-field +strict frame chains, hence exactly **38 rank-one paid climbs**. The original +block attains the bound. In particular, its paid moment cannot be reduced +for any exponent 0 < t < 1. + +The model permits any finite rational ADD/nonzero-SCALE factorization, +arbitrary coefficients, arbitrary chronology, and temporary changes of +basis. It fixes the twenty fields, their capacities, their arbitrary +entering values, and their individual entry and exit frames. ADD operands +must occupy the same actual frame. Paid operations are strict nested frame +ascents of rank dim(new)-dim(old). All intermediate binary subspaces are +allowed; the search is not restricted to the source frame catalogue. + +The model excludes auxiliary fields, access to fields outside this closed +block, new warps, descents, chart-changing exchanges, cross-column +conversions, approximate encoding, and changed input/output contracts. +The result is a local finite-frame theorem conditional on the inherited +native chart interpretation. It is not a new kappa, a whole-provider +impossibility theorem, or an unconditional multiplication theorem. + +## Source binding and independent exact extraction + +Canonical checkpoint: `32890bc5de034ab8fc93ac88ead7279a6a416d04`. + +The actual backward tape is: + +`research/coupled-helper-neutral-completion/capsule/workspace/swarm-provider-audit-sol-high-20261024/repository/research/native-rank8-helper-provider/WORD.json.gz` + +Its compressed SHA256 is +`7dc356001ed597ad6fc9fd3e0bc6ff7e3ec3a580a579a956827aa17fccfdd2dc`; +its decompressed SHA256 is +`05490717144b3e6c69c0cc9e5c5df5c69d841ca13bf29aabd1b0db180628f038`. +Its source-payload link binds +`research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz`, whose compressed +and decompressed hashes are respectively +`7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05` and +`cfcd36b40326d7a5815e1db5313444379b3fb756b27d5201c561574c085cc0dd`. + +Indices are zero-based and the interval is half-open. Its exact field closure +is `[18,19,39,40,288,289,290,291,292,293,294,295,296,297,298,299,300,301,302,303]`. +The 85 relevant source events are 38 H1 climbs, 43 ADDs and four SCALEs. +Every interval event touching this set touches only this set. There is no +warp, cache copy, clear or zero retag inside it. Intervening instructions on +other fields commute with a replacement of the isolated block. + +The matrix is computed over Q by starting with twenty independent unit rows +and applying every relevant scalar event. Its rank is twenty. The prefix +through event 9043 has only invertible persistent ADD/SCALE, warp and climb +operations, invertible chart adapters and phase annotations. The native +interpretation of those frame changes is inherited. Within that model it +imposes no relation on the twenty values; no zero-input specialization is +used. + +| Role | Entry frame | Exit frame | Retained strict chain | +|---|---:|---:|---| +|18|20|437|20,425,437| +|19|21|436|21,423,436| +|39|41|436|41,426,436| +|40|42|422|42,422| +|288|103|432|103,422,432| +|289|103|434|103,423,434| +|290|56|432|56,425,432| +|291|56|433|56,426,433| +|292|104|434|104,427,434| +|293|104|431|104,428,431| +|294|57|433|57,429,433| +|295|57|431|57,430,431| +|296|20|435|20,427,435| +|297|20|420|20,420| +|298|42|435|42,429,435| +|299|42|419|42,419| +|300|0|437|0,21,430,437| +|301|0|419|0,21,419| +|302|0|428|0,41,428| +|303|0|420|0,41,420| + +Here zero, line, plane and cube mean dimensions 0,1,2,3 in F_2^9. The +boundary has thirteen line-to-cube fields, three line-to-plane fields, +one zero-to-cube field and three zero-to-plane fields. Its invariant total +paid rank mass is 13*2+3+3+3*2 = 38. The optimistic direct-endpoint profile +would be {H1:3,H2:16,H3:1}, but it is not realizable under this contract. + +This enlarged boundary differs from the previous eight-field +one. It has four zero-start fields, and several old plane exits have become +cubes. In particular the old two-input/one-carrier lemma cannot simply be +transferred. The proof below uses the freshly extracted twenty-field matrix +and complete new frame intervals. + +## Why rational row equality is the right local condition + +Under the inherited native chart contract, a climb preserves its formal +row while changing the invertible chart map; a coframed ADD/SCALE applies its +rational elementary matrix to the formal rows. Therefore a legal warp-free +window with transfer matrix T has physical map + + G_exit (T tensor I) G_entry^{-1}. + +With fixed boundary charts, equality of T is necessary and sufficient for +exact local equality at every positive width in that native model. Exterior +scalar coefficients are not raised to the width. This assertion does not +admit new unproved physical primitives or replace absolute-phase validation +where it is required. It states the source semantics used for this local +obstruction. A modified window containing warps would need labelled +operator rows or additional protected boundaries. + +Restoring all twenty rows and charts at event 9137 preserves the unchanged +continuation by composition. The first cached-centre copy is later, at +11207; all eight cached copies and all eight zero retags lie after this +boundary. No fresh full caller or physical phase replay is claimed here. + +## Frame-path coverage + +A field's strict frame path is the chain remaining after suppressing time +spent doing scalar operations at one frame. Every possible path lies in the +finite subspace interval [entry,exit]. The complete path counts are: + +- line to plane: one; +- line to cube: four, consisting of a direct jump or one of the three + intermediate planes containing the entry line; +- zero to plane: four, a direct jump or one of the three lines; +- zero to cube: 36, consisting of one direct jump, seven line-only paths, + seven plane-only paths and 21 complete flags. + +Consequently the full domain has + + 4^13 * 36 * 4^3 = 154,618,822,656 + +path assignments. This is a finite coverage count, not a claim that that +many programs were executed. Scalar programs are not enumerated: the +necessary conditions below apply to every factorization on a given path +assignment. + +## Soundness of the optimistic station model + +Make a vertex for each actual binary subspace visited by a path. For each +field ascent E -> F, add one directed edge E -> F of unit field capacity. +Parallel edges from different fields retain their multiplicity. All vertices +with the same subspace are merged. Grant unrestricted linear mixing and +storage at each resulting vertex, ignoring chronological overlap and +invertibility constraints. + +This graph is an optimistic relaxation. A legal ADD/SCALE can only change +coefficients among values at the same vertex; every change of frame occurs +along an actual field edge. Merging visits that do not occur simultaneously +can add possible communication but cannot remove one. Each strictly ascending +edge is traversed once by its field and carries one whole-field value. No +field returns to that earlier frame. Repeated reads, in-place updates and +fanout at a station do not transmit a second independent value through an +edge already traversed. + +Two necessary conditions follow. + +**Reachability.** If T[o,i] is nonzero, there must be a directed path from +input i's entry station to output o's exit station. A linear coefficient +cannot appear at a station unreachable from its source. + +**Cut rank.** Choose input columns I and output rows O. If deleting a set +of ascent edges disconnects every selected input station from every selected +output station, then + + rank_Q T[O,I] <= sum of the deleted edge capacities. + +To see this, set all other entering values to zero. The chosen outputs can +depend on the selected inputs only through the values on the removed edges. +Their joint information dimension is at most one field capacity per edge. +Equivalently in formal rows their span has dimension at most the number of +edges, with multiplicity. The graph is acyclic because every edge strictly +increases dimension. Arbitrary mixing, feedback within a station, temporary +bases and repeated reads cannot increase that cut dimension. At physical +field capacity N the two sides simply acquire a common factor N. + +These conditions are only necessary. A path assignment that passes them is +not automatically implementable. The final survivor below is known to be +implementable because it is the original checked scalar word. + +## Domain pruning and the remaining exact certificates + +Initially give each field every strict path in its complete interval. To +test one candidate path p for one field, fix that field to p and take the +union of the edges from every currently allowed path for each other field. +This union can contain mutually incompatible choices, and is therefore an +even more permissive reachability relaxation. If a required nonzero matrix +entry has no path in this union, p occurs in no feasible completion. + +Deleting such a path is sound. Inductively, earlier deletions have already +preserved every feasible complete assignment. A later union of the surviving +domains still contains every actual field edge of every remaining feasible +assignment. Thus domain pruning does not assume a fixed scalar circuit or +discard a solution because of an unfavorable choice of other paths. + +There are 68 certified deletions. They leave only four non-singleton domains: +roles 293 and 295 have four paths each, role 300 has seven, and role 302 has +four. The exact remaining Cartesian product has 4*4*7*4 = **448** members. + +All 448 members are then handled separately: + +- 315 have a required nonzero entry with no directed path even for that + assignment's optimistic merged stations; +- 132 have an explicit cut whose capacity is below the exact rational rank + of the required matrix minor; +- one survives, with exactly the retained frame chain on every field. + +The independent audit does not trust a max-flow solver to establish the +cut claims. It recomputes every minor rank, verifies every listed cut edge +and its complete parallel-edge capacity, deletes those edges, and checks +disconnection between every selected source and sink. It also checks that +the 447 rejected assignments are distinct, belong to the reconstructed +remaining Cartesian product, and leave exactly the original assignment. + +The source assignment uses 38 H1 climbs. Thus every exact factorization in +the stated model must use those same strict per-field frame chains and has +the same paid profile. The floor is attained, and the normalized moment is +38 for every 0 < t < 1. This conclusion concerns arbitrary legal scalar +factorizations, not merely the scalar programs attempted during discovery. + +## Reproduction and independent evidence + +The primary verifier emits the source-bound certificate `RESULT.json`. +The independently authored `check_certificate.py` validates this sibling +certificate by default, with the repository root resolved from the package +location. Optional `--repo` and `--certificate` flags support separate +read-only audit locations. + +`check_certificate.py` imports no search code. It +independently extracts the source matrix, frames and invoice; enumerates +subspaces by spans of every subset of each terminal space; and validates +all coverage and rejection certificates directly. Its observed normal run +took less than one second under CPython 3.13. Three semantic controls run the +actual checker on altered certificates: deleting a rejection exposes a +coverage gap, changing a cut capacity fails the source edge count, and +changing a target rank fails exact minor reconstruction. Normal output is a +concise PASS receipt; `--json` provides the source hashes and detailed +checks. The result is +`PASS_INDEPENDENT_TWENTY_FIELD_PATH_CERTIFICATE`. No whole-provider, selected +cold, compiler, outer, Lean or Docker replay was run for this audit. + +This is an exact finite certificate combined with the written station/cut +lemmas. It is not a proof-assistant certificate or independent human review. + +## What a further change would have to alter + +Reassociation, changes of basis, different intermediate binary subspaces, +and different scalar chronology within this boundary cannot improve the +paid profile. Another attempt must change at least one actual hypothesis: +for example an entry/exit chart or target interface, a transport or warp, +or the field/capacity contract with a fully paid producer and consumer. +Adding one H1 to save one H1+H1 -> H2 merge is already unprofitable, since +the saving 2-2^t is less than one for 01};counts=Counter() + for rejection in d['rank_screen']['rejections']: + indices=rejection['path_indices'];require(set(indices)==variable,'exact variable path selectors') + require(all(type(i)is int and 0<=i 0, f'{index}: nonpositive climb') + current[field] = after + elif kind == 'warp': + _, owner, signed_id, before, after = event + require(owner[0] == 'L' and current[owner[1]] == before, + f'{index}: warp input frame mismatch') + require(abs(signed_id) in warps, f'{index}: unknown warp') + columns = warps[abs(signed_id)]['G_columns'] + lookup = {} + for x in range(1 << len(columns)): + y = 0 + for bit, column in enumerate(columns): + if x & (1 << bit): + y ^= column + lookup[x] = y + require(len(set(lookup.values())) == len(lookup), f'{index}: singular warp') + if signed_id < 0: + lookup = {y:x for x,y in lookup.items()} + require({lookup[x] for x in span(frames[before])} == span(frames[after]), + f'{index}: warp frame map mismatch') + current[owner[1]] = after + elif kind == 'adapter': + require(event[1] == 'old_to_new', f'{index}: unexpected adapter direction') + require(current[event[2]] == event[3], f'{index}: adapter chart mismatch') + else: + require(kind == 'phase', f'{index}: unexpected event {kind}') + + +def execute_local(window, fields, entry, frames, warps): + require(closure(window) == fields, 'closure changed') + positions = {field:i for i,field in enumerate(fields)} + current = dict(zip(fields, entry)) + matrix = identity(len(fields)) + selected = [] + omitted = [] + for offset,e in enumerate(window): + touched = refs(e) + if not any(kind == 'L' and r in positions for kind,r in touched): + omitted.append(LO+offset) + continue + require(all(kind == 'L' and r in positions for kind,r in touched), + f'{LO+offset}: boundary or owned contact') + require(e[0] in ('scalar','climb'), f'{LO+offset}: local non-add-scale-climb event') + advance_frames(e,current,frames,warps,LO+offset) + if e[0] == 'scalar': + op = e[1] + row = positions[op[1][1]] + q = Q(op[-2],op[-1]) + if op[0] == 'add': + add_row(matrix,row,positions[op[2][1]],q) + else: + matrix[row] = [q*x for x in matrix[row]] + selected.append(LO+offset) + return matrix,[current[r] for r in fields],selected,omitted + + +def macro_formula(fields): + """Independent mathematical circuit, with four swaps and ten butterflies.""" + rows = dict(zip(fields,identity(len(fields)))) + for dest,source in [(19,300),(19,301),(39,302),(39,303)]: + rows[dest] = [x-y for x,y in zip(rows[dest],rows[source])] + for a,b in [(297,18),(299,40),(301,19),(303,39)]: + rows[a],rows[b] = rows[b],rows[a] + for a,b in [(40,288),(19,289),(18,290),(39,291),(296,292), + (302,293),(298,294),(300,295),(303,297),(301,299)]: + x,y = rows[a],rows[b] + rows[a] = [u-v for u,v in zip(x,y)] + rows[b] = [(u+v)/2 for u,v in zip(x,y)] + for dest,source in [(293,295),(288,290),(291,294),(289,292), + (298,296),(39,19),(18,300)]: + rows[dest] = [x-y for x,y in zip(rows[dest],rows[source])] + return [rows[field] for field in fields] + + +def direct_vector(window, fields, vector): + values = dict(zip(fields,vector)) + for e in window: + if e[0] != 'scalar': + continue + op = e[1] + if op[1][0] != 'L' or op[1][1] not in values: + continue + d = op[1][1] + if op[0] == 'add': + values[d] += Q(op[3],op[4])*values[op[2][1]] + elif op[0] == 'scale': + values[d] *= Q(op[2],op[3]) + else: + raise ValueError('protected scalar in vector execution') + return [values[r] for r in fields] + + +def strings(matrix): + return [[str(x) for x in row] for row in matrix] + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--repo',type=Path,default=Path(__file__).resolve().parents[2], + help='Repository root; defaults to this package two directories above') + parser.add_argument('--json',action='store_true',help='Print full exact source-audit evidence') + args = parser.parse_args() + inputs = {} + objects = {} + for rel,pins in PINS.items(): + compressed = (args.repo/rel).read_bytes() + raw = gzip.decompress(compressed) + require((digest(compressed),digest(raw)) == pins, f'input hash mismatch: {rel}') + inputs[rel] = {'compressed_sha256':digest(compressed), 'content_sha256':digest(raw), + 'compressed_bytes':len(compressed),'content_bytes':len(raw)} + objects[rel] = json.loads(raw) + provider = objects[WORD_REL] + source = objects[SOURCE_REL] + require(provider['direction'] == 'backward','wrong provider direction') + require(provider['source_sha256'] == PINS[SOURCE_REL][1],'provider source binding mismatch') + word = provider['word'] + canonical = source['canonical'] + frames = canonical['frames'] + require(all(len(binary_basis(b)) == len(b) for b in frames),'dependent source frame basis') + require(all(all(0 <= v < 2**canonical['h'] for v in b) for b in frames), + 'frame basis outside binary ambient dimension') + warps = {w['op']:w for w in canonical['warps']} + require(len(warps) == len(canonical['warps']),'duplicate warp IDs') + prefix_frames = dict(enumerate(canonical['start'])) + for index,event in enumerate(word[:LO]): + advance_frames(event,prefix_frames,frames,warps,index) + window = word[LO:HI] + require(all(kind=='L' for e in window for kind,_ in refs(e)), + 'owned/cache/scratch contact inside complete interval') + fields = closure(window) + require(fields == EXPECTED_FIELDS,'wrong twenty-field closure') + entry = [prefix_frames[f] for f in fields] + matrix,exit_frames,selected,omitted = execute_local(window,fields,entry,frames,warps) + require(matrix == macro_formula(fields),'independent macro transfer mismatch') + for column,vector in enumerate(identity(len(fields))): + require(direct_vector(window,fields,vector) == [r[column] for r in matrix], + f'basis-vector execution mismatch {column}') + probe = [Q((-1)**i*(i+1),i+2) for i in range(len(fields))] + require(direct_vector(window,fields,probe) == [sum(x*y for x,y in zip(r,probe)) for r in matrix], + 'signed rational dirty-vector mismatch') + determinant,inverse = exact_inverse(matrix) + require(determinant == 1,'unexpected determinant') + require(product(matrix,inverse) == identity(len(fields)), 'right inverse failed') + require(product(inverse,matrix) == identity(len(fields)), 'left inverse failed') + selected_events = [word[i] for i in selected] + event_counts = Counter(e[0] for e in selected_events) + scalar_counts = Counter(e[1][0] for e in selected_events if e[0]=='scalar') + paid = Counter(e[5] for e in selected_events if e[0]=='climb') + require(dict(event_counts) == {'climb':38,'scalar':47},'event count mismatch') + require(dict(scalar_counts) == {'add':43,'scale':4},'scalar count mismatch') + require(dict(paid) == {1:38},'paid histogram mismatch') + require(sum(len(frames[f]) for f in exit_frames)-sum(len(frames[f]) for f in entry) == 38, + 'endpoint total rank mismatch') + # Mutation acceptance is compared to semantic boundary obligations, not source hashes. + def validate(candidate, candidate_entry=entry): + a,b,c,d = execute_local(candidate,fields,candidate_entry,frames,warps) + require(a == matrix,'mutated transfer') + require(b == exit_frames,'mutated output frames') + require(len(candidate)==HI-LO,'mutated interval length') + require([candidate[i-LO] for i in omitted] == [window[i-LO] for i in omitted], + 'changed disjoint interval event') + require(Counter(e[5] for e in candidate if e[0]=='climb' and e[2] in fields)==paid, + 'mutated paid histogram') + controls = [] + def reject(name,candidate,candidate_entry=entry): + try: + validate(candidate,candidate_entry) + except (ValueError,KeyError,IndexError,ZeroDivisionError) as exc: + controls.append({'name':name,'rejected':True,'reason':str(exc)}) + return + raise ValueError('semantic control unexpectedly accepted: '+name) + c=deepcopy(window); c[9045-LO][1][3]=1; reject('initial dirty-input sign',c) + c=deepcopy(window); c[9047-LO][1][3]=0; reject('drop second dirty-input contribution',c) + c=deepcopy(window); c[9075-LO][1][4]=1; reject('replace butterfly half by one',c) + c=deepcopy(window); c[9052-LO],c[9053-LO]=c[9053-LO],c[9052-LO]; reject('swap serialized swap ADD order',c) + c=deepcopy(window); c[9118-LO][2]=432; reject('wrong scalar contact frame',c) + c=deepcopy(window); c[9116-LO][5]=0; reject('undercharge a paid climb',c) + c=deepcopy(window); c[9045-LO][1][2]=['C',1]; reject('introduce owned-cache source',c) + c=deepcopy(window); c[9136-LO][1][3]=0; reject('drop final post-mix',c) + c=deepcopy(window); c[9070-LO][1][3]=1; reject('modify disjoint interval event',c) + reject('truncate last boundary event',deepcopy(window[:-1])) + bad_entry=entry.copy(); bad_entry[fields.index(300)]=21 + reject('zero-frame dirty carrier assigned wrong entry frame',deepcopy(window),bad_entry) + all_copies = [{'index':i,'operation':e[1],'frame':e[2]} for i,e in enumerate(word) + if i>=HI and e[0]=='scalar' and e[1][0]=='copy'] + cache_taps = [e for e in all_copies if e['operation'][1][0]=='C' + and e['operation'][2][0]=='L'] + direct_taps = [e for e in cache_taps if e['operation'][2][1] in fields] + require(direct_taps[0]['index']==11322,'unexpected first later direct cache tap') + serialized = strings(matrix) + result = { + 'status':'PASS','python':platform.python_version(),'optimized':not __debug__, + 'input_pins':inputs,'provider_source_binding':provider['source_sha256'], + 'direction':provider['direction'],'total_provider_events':len(word), + 'interval':[LO,HI],'seeds':sorted(SEEDS),'fields':fields, + 'entry_frames':entry,'exit_frames':exit_frames, + 'entry_bases':[frames[f] for f in entry], 'exit_bases':[frames[f] for f in exit_frames], + 'all_contact_frame_bases':{str(f):frames[f] for f in sorted({x for e in selected_events for x in + ([e[3],e[4]] if e[0]=='climb' else [e[2]])})}, + 'selected_indices':selected,'omitted_indices':omitted, + 'omitted_events':[{'index':i,'event':word[i]} for i in omitted], + 'selected_event_counts':dict(event_counts),'selected_scalar_counts':dict(scalar_counts), + 'paid_histogram':dict(paid),'entry_rank_sum':sum(len(frames[f]) for f in entry), + 'exit_rank_sum':sum(len(frames[f]) for f in exit_frames), + 'endpoint_rank_difference_histogram':dict(Counter(len(frames[b])-len(frames[a]) + for a,b in zip(entry,exit_frames))), + 'matrix':serialized,'matrix_sha256':digest(json.dumps(serialized,separators=(',',':')).encode()), + 'determinant':str(determinant),'inverse':strings(inverse), + 'prefix_event_counts':dict(Counter(e[0] for e in word[:LO])), + 'prefix_scalar_counts':dict(Counter(e[1][0] for e in word[:LO] if e[0]=='scalar')), + 'prefix_warp_ids':sorted({abs(e[2]) for e in word[:LO] if e[0]=='warp'}), + 'prefix_invertibility':{ + 'persistent_registers':len(canonical['start']), + 'nonzero_scale_checks':334,'distinct_owner_add_checks':8107, + 'warp_binary_permutations_checked':96, + 'claim':'Constructive grammar proof in inherited normalized/native chart semantics: ' + 'all persistent ADDs have distinct owners, all SCALEs are nonzero, every warp ' + 'has a bijective ambient binary map and correct source/target frame span. ' + 'Climbs and adapters retain the inherited invertible chart interpretation. ' + 'Consequently arbitrary twenty cut-coordinate inputs are legitimate; ' + 'zero entry frames do not mean zero register values.', + }, + 'protected_contacts':{ + 'inside_window':[], 'later_persistent_cache_taps':cache_taps, + 'later_cache_to_scratch_copies':[e for e in all_copies if e['operation'][2][0]=='C'], + 'first_direct_tap_from_closure':direct_taps[0], + 'preservation':'Exact equality of all twenty endpoint values and charts, with the ' + 'eight disjoint interval events unchanged, preserves every later ' + 'owned/cache/scratch relation by composition. No fresh complete ' + 'physical-provider replay is claimed.', + }, + 'semantic_controls':controls, + 'checks':['source hashes and source binding','binary frame basis independence', + 'prefix chart/invertibility grammar','fixed-point closure','monotone paid climbs', + 'same-frame scalar contacts','exact twenty-row transfer','independent macro formula', + 'twenty basis-vector runs','signed rational dirty-vector run', + 'exact determinant and two-sided inverse','eleven rejected semantic mutations'], + 'scope':'Finite exact source-bound normalized-transfer audit; no new kappa, no whole-provider ' + 'impossibility, no replacement feasibility proof, and no new native/phase theorem.' + } + if args.json: + print(json.dumps(result,indent=2,sort_keys=True)) + else: + print('PASS_INDEPENDENT_SOURCE fields=20 paid_climbs=38 determinant=1 controls=' + +str(len(controls))) + + +if __name__=='__main__': + main() diff --git a/research/helper300-twenty-field-floor/verify.py b/research/helper300-twenty-field-floor/verify.py new file mode 100644 index 0000000000..80af58febe --- /dev/null +++ b/research/helper300-twenty-field-floor/verify.py @@ -0,0 +1,336 @@ +#!/usr/bin/env python3 +"""Exact twenty-field monotone scalar-ADD floor; standard library only. + +Station mixing relaxes chronology, invertibility and field storage. Reachability +and rank conditions are necessary; passing is never a construction test. +OpenAI Codex assisted this source-bound research audit. +""" +import argparse +from collections import Counter, defaultdict, deque +from fractions import Fraction as Q +import gzip +from hashlib import sha256 +import itertools +import json +import math +from pathlib import Path + +CANONICAL = 'research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz' +PROVIDER = ('research/coupled-helper-neutral-completion/capsule/workspace/' + 'swarm-provider-audit-sol-high-20261024/repository/research/' + 'native-rank8-helper-provider/WORD.json.gz') +PINS = {CANONICAL: '7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05', + PROVIDER: '7dc356001ed597ad6fc9fd3e0bc6ff7e3ec3a580a579a956827aa17fccfdd2dc'} +SEMANTIC_PINS = { + 'research/kappa-rebuild/complex/native_extensions.py': '50ad007d9c386393657e86c99a96ae0a63a8fbc52872579b185002cc626e88e3', + 'research/kappa-causal-continuation/buffer-borrowing/verify_buffers.py': '106b4d5e052427230df452f0c901d5390a0583782960b80a8af94d9a984022c7', +} +START, STOP = 9044, 9137 +FIELDS = [18,19,39,40,*range(288,304)] + +def need(ok, why): + if not ok: raise ValueError(why) + +def span(vectors): + s = {0} + for v in vectors: s |= {x ^ v for x in s} + return frozenset(s) + +def dim(s): return len(s).bit_length() - 1 + +def touched(e): + if e[0] == 'scalar': return {tuple(x) for x in e[1][1:] if isinstance(x,list)} + if e[0] == 'climb': return {('L',e[2])} + if e[0] == 'warp': return {tuple(e[1])} + if e[0] == 'center': return {('C',e[1])} + return set() + +def load(root): + docs = {} + for name,pin in PINS.items(): + raw = (root/name).read_bytes() + need(sha256(raw).hexdigest() == pin, 'source container pin '+name) + docs[name] = json.loads(gzip.decompress(raw)) + need(docs[PROVIDER]['direction'] == 'backward', 'provider direction') + need(docs[PROVIDER]['source_sha256'] == sha256(gzip.decompress((root/CANONICAL).read_bytes())).hexdigest(), 'provider canonical payload link') + need(docs[PROVIDER]['word'][START:STOP] == docs[CANONICAL]['programs']['backward'][START:STOP], 'provider local tape equals inherited backward tape') + for name,pin in SEMANTIC_PINS.items(): + need(sha256((root/name).read_bytes()).hexdigest() == pin, 'semantic source pin '+name) + return docs[CANONICAL]['canonical'], docs[PROVIDER]['word'] + +def invertible_prefix(w): + """Native climb/warp invertibility is inherited, not re-proved here.""" + for e in w[:START]: + need(e[0] in ('scalar','warp','climb','phase','adapter','residual_adapter'), 'invertible persistent prefix grammar') + if e[0]=='scalar': + op=e[1] + need(op[0] in ('add','scale') and op[1][0]=='L','no destructive prefix scalar') + if op[0]=='add':need(op[2][0]=='L' and op[1]!=op[2] and op[4]!=0,'invertible prefix ADD') + else:need(op[2]!=0 and op[3]!=0,'nonzero prefix SCALE') + elif e[0]=='warp':need(e[1][0]=='L','persistent prefix warp') + +def extract(c,w): + chosen = {('L',i) for i in (19,300,301)} + while True: + nxt = chosen | set().union(*(touched(e) for e in w[START:STOP] if chosen & touched(e))) + if nxt == chosen: break + chosen = nxt + need(sorted(chosen) == [('L',i) for i in FIELDS], 'twenty-field dependency closure') + frames = {('L',i):f for i,f in enumerate(c['start'])} + frames['C',0] = None + for e in w[:START]: + if e[0] == 'climb': + _,_,i,a,b,r=e; need(frames['L',i]==a,'prefix climb'); frames['L',i]=b + elif e[0] == 'warp': + _,f,_,a,b=e; need(frames[tuple(f)]==a,'prefix warp'); frames[tuple(f)]=b + elif e[0] == 'center': + _,i,a,b,_=e; need(frames['C',i]==a,'prefix center'); frames['C',i]=b + elif e[0] == 'scalar' and e[1][0]=='clear': frames[tuple(e[1][1])]=e[2] + spaces=[span(v) for v in c['frames']] + entry={i:frames['L',i] for i in FIELDS} + rows={i:[Q(i==j) for j in FIELDS] for i in FIELDS} + paths={i:[spaces[entry[i]]] for i in FIELDS} + paid=Counter(); events=[] + for k in range(START,STOP): + e=w[k] + if not touched(e)&chosen: continue + need(touched(e)<=chosen,'closed local event'); events.append([k,e]) + if e[0]=='climb': + _,_,i,a,b,r=e + need(frames['L',i]==a and spaces[a]0:prior[b]=a;todo.append(b) + if sink not in prior:break + edges=[];b=sink + while b!=source:a=prior[b];edges.append((a,b));b=a + amount=min(residual[e] for e in edges) + for a,b in edges:residual[a,b]-=amount;residual[b,a]+=amount + flow+=amount + cut=[(a,b,n) for (a,b),n in cap.items() if a in prior and b not in prior] + need(sum(n for a,b,n in cut)==flow,'exact maxflow cut certificate') + encode=lambda x:x if isinstance(x,str) else sorted(x) + return {'capacity':flow,'cut_edges':[[encode(a),encode(b),n] for a,b,n in cut], + 'source_side':[encode(x) for x in sorted(prior,key=key)]} + +def enumerate_remaining(domains,block): + indices={f:i for i,f in enumerate(FIELDS)} + allspaces=set(s for pp in domains.values() for p in pp for s in p) + groups=defaultdict(list) + for i in FIELDS:groups[domains[i][0][0]].append(i) + zero=[300,301,302,303] + inputsets=[zero]+[v for v in groups.values() if v!=zero] + inputsets += [sorted(set(zero+v)) for v in groups.values() if v!=zero] + tests=[];seen=set() + for ins in inputsets: + for space in sorted(allspaces,key=lambda s:(len(s),tuple(sorted(s)))): + outs=[i for i in FIELDS if not space<=domains[i][0][-1]] + key=(tuple(ins),tuple(outs)) + if key in seen or not outs:continue + seen.add(key) + required=rank([[block['matrix'][indices[o]][indices[i]] for i in ins] for o in outs]) + if required:tests.append((ins,outs,required,space)) + rejects=[];passing=[];summary=Counter();classified=Counter() + for assignment,selected in enumerate(itertools.product(*(domains[i] for i in FIELDS))): + paths=dict(zip(FIELDS,selected));p=tuple(sum(profile(q)[i] for q in selected) for i in range(3)) + need(sum((i+1)*v for i,v in enumerate(p))==38,'boundary rank mass for every path assignment') + path_indices={i:domains[i].index(paths[i]) for i in FIELDS if len(domains[i])>1} + common={'assignment':assignment,'path_indices':path_indices,'profile':p} + category='neutral' if p==(38,0,0) else 'saving' + reach=check_reachability({i:[q] for i,q in paths.items()},block) + if reach: + rejects.append({**common,'kind':'reachability','witness':reach});summary['reachability']+=1;classified['reachability_'+category]+=1;continue + for ins,outs,required,space in tests: + cut=rank_cut(paths,ins,outs) + if cut['capacity']=STOP for k,e in copies),'eight later protected centre copies') + need(len(retags)==8 and all(k>=STOP for k,e in retags),'eight later zero-retags') + endpoint=Counter(dim(b['spaces'][b['exit'][i]])-dim(b['spaces'][b['entry'][i]]) for i in FIELDS) + capped={k:sum(n*min(r,k) for r,n in endpoint.items())-38 for k in (1,2,3)} + need(endpoint=={1:3,2:16,3:1} and capped=={1:-18,2:-1,3:0},'optimistic infeasible endpoint invoice') + return {'status':'PASS_TWENTY_FIELD_MONOTONE_ADD_FLOOR_NO_NEW_KAPPA','schema_version':1, + 'scope':'Fixed twenty arbitrary persistent fields, exact normalized transfer and boundary frames; rational scalar ADD/SCALE and strict monotone subspace climbs; no auxiliary fields, new warps, chart-changing exchanges, erasure or zero-retags. Native chart semantics remain inherited conditional.', + 'block':[START,STOP],'indexing':'zero-based half-open','fields':FIELDS, + 'entry':b['entry'],'exit':b['exit'],'matrix':[[str(x) for x in r] for r in b['matrix']], + 'source_inputs':[{'path':p,'sha256':h} for p,h in {**PINS,**SEMANTIC_PINS}.items()], + 'source_events':b['events'],'original_paid':{1:38},'path_counts':{i:len(p) for i,p in options.items()}, + 'histograms':[{'profile':p,'count':n} for p,n in sorted(hist.items())], + 'complete_assignments':sum(hist.values()),'saving_assignments_rejected':sum(hist.values())-hist[38,0,0], + 'remaining_histograms':[{'profile':p,'count':n} for p,n in sorted(reduced_hist.items())], + 'reachability_remaining_counts':{i:len(p) for i,p in domains.items()}, + 'reachability_remaining_paths':{i:[[sorted(x) for x in p] for p in pp] for i,pp in domains.items()}, + 'reachability_rejections':failures,'rank_screen':screen, + 'prefix_events_checked_for_invertible_grammar':START, + 'protected_cache_copies':copies,'later_zero_retags':retags, + 'infeasible_endpoint_relaxation':{'paid_profile':dict(endpoint),'signed_capped_rank_moments_versus_38H1':capped}, + 'minimum_paid_profile':{1:38},'moment_exponent_interval':'0