diff --git a/research/gaussian-nonlinear-copy-floor/CERTIFICATE.json b/research/gaussian-nonlinear-copy-floor/CERTIFICATE.json new file mode 100644 index 0000000000..d1cc4d6f1d --- /dev/null +++ b/research/gaussian-nonlinear-copy-floor/CERTIFICATE.json @@ -0,0 +1,459 @@ +{ + "assignment_seed": 44, + "base_commit": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "concentrated_twelve_port_floor": 12, + "demand_coefficient": "2/3", + "finite_nonlinear_controls": { + "conditional_transcript_projections": { + "active_intersection_census": { + "0": 4, + "1": 52, + "2": 268, + "3": 316 + }, + "assignment_checks": 2621440, + "conditional_classes": 559104, + "injective": true, + "input_assignments_per_clique": 4096, + "maximum_cliques": 640 + }, + "frame_search": { + "orthogonal_frames": 105, + "selection": "seed44 shuffle of sorted four-line frames; first three disjoint" + }, + "geometry_source": { + "commit": "9671c5d72f3119ba26f3774f40aa7130c67bcf77", + "sha256": "4a3e2cee2e35ccebde346e63fd9869ed48b2d59de120f570650ecb9c8875f5e4" + }, + "negative_controls": { + "dropped_output_bits": [ + { + "detected": true, + "dropped_output_bit": 0, + "projection_rejection": "conditional transcript collision: {\"first_inside_word\": 0, \"local_mask\": 546, \"message_word\": 0, \"outside_word\": 0, \"second_inside_word\": 2}", + "receiver_failure_count": 12288, + "witness": { + "decoded": 0, + "expected": 1, + "input_word": 1, + "message_word": 0, + "receiver_local_index": 0 + } + }, + { + "detected": true, + "dropped_output_bit": 1, + "projection_rejection": "conditional transcript collision: {\"first_inside_word\": 0, \"local_mask\": 546, \"message_word\": 0, \"outside_word\": 0, \"second_inside_word\": 32}", + "receiver_failure_count": 12288, + "witness": { + "decoded": 0, + "expected": 1, + "input_word": 16, + "message_word": 0, + "receiver_local_index": 4 + } + }, + { + "detected": true, + "dropped_output_bit": 2, + "projection_rejection": "conditional transcript collision: {\"first_inside_word\": 0, \"local_mask\": 546, \"message_word\": 0, \"outside_word\": 0, \"second_inside_word\": 512}", + "receiver_failure_count": 8192, + "witness": { + "decoded": 1, + "expected": 0, + "input_word": 17, + "message_word": 3, + "receiver_local_index": 8 + } + } + ], + "illegal_nonorthogonal_side_information": { + "active_demands": 12, + "averaged_floor_if_orthogonality_held": 8, + "clique_floor_if_orthogonality_held": 12, + "clique_ports": [ + 0, + 1, + 3, + 7, + 9, + 11, + 13, + 14, + 15, + 21, + 23, + 24 + ], + "conditional_projection_rejection": "conditional transcript collision: {\"first_inside_word\": 1, \"local_mask\": 4095, \"message_word\": 1, \"outside_word\": 0, \"second_inside_word\": 2}", + "cost": 4, + "detected": true, + "first_violation": [ + 0, + 1 + ], + "input_assignments": 4096, + "ordered_side_information_violations": 132, + "output_bits": 1, + "pairing_rank_charge": 4, + "receiver_decodes": 49152 + }, + "omitted_nonlinear_inversion": { + "detected": true, + "receiver_failure_count": 4096, + "witness": { + "decoded": 1, + "expected": 0, + "input_word": 17, + "message_word": 7, + "receiver_local_index": 8 + } + }, + "per_bit_charging": { + "certified_active_floor": 8, + "correct_three_bit_charge": 12, + "detected": true, + "incorrect_one_message_charge": 4, + "rejection": "charged copied-information cost is below the certified floor" + } + }, + "nonlinear_example": { + "active_demands": 12, + "averaged_demand_floor": 8, + "cost": 12, + "distinct_message_words": 8, + "encoder": "three frame parities z0,z1,z2, then z2 ^= z0 & z1", + "frames": [ + [ + 10, + 14, + 37, + 48 + ], + [ + 4, + 15, + 40, + 49 + ], + [ + 16, + 21, + 35, + 42 + ] + ], + "input_assignments": 4096, + "maximum_clique_demand_floor": 3, + "nonlinear_second_difference": { + "checks": 4096, + "nonzero_output_word": 4, + "source_local_indices": [ + 0, + 4 + ] + }, + "output_bits": 3, + "pairing_rank_charge": 4, + "reader_ports": [ + 10, + 14, + 37, + 48, + 4, + 15, + 40, + 49, + 16, + 21, + 35, + 42 + ], + "reader_rank": 4, + "receiver_decodes": 49152, + "side_information": [ + [ + 14, + 37, + 48 + ], + [ + 10, + 37, + 48 + ], + [ + 10, + 14, + 48 + ], + [ + 10, + 14, + 37 + ], + [ + 15, + 40, + 49 + ], + [ + 4, + 40, + 49 + ], + [ + 4, + 15, + 49 + ], + [ + 4, + 15, + 40 + ], + [ + 21, + 35, + 42 + ], + [ + 16, + 35, + 42 + ], + [ + 16, + 21, + 42 + ], + [ + 16, + 21, + 35 + ] + ], + "side_information_checks": 36, + "source_dependence_counts": [ + 4096, + 4096, + 4096, + 4096, + 4096, + 4096, + 4096, + 4096, + 4096, + 4096, + 4096, + 4096 + ], + "source_ports": [ + 10, + 14, + 37, + 48, + 4, + 15, + 40, + 49, + 16, + 21, + 35, + 42 + ], + "source_rank": 4 + }, + "seed": 44 + }, + "geometric_premise": { + "abstract_row_upper_bound": 60, + "deficit_upper_bound": { + "intercept": -120, + "slope": 40 + }, + "exact_pairing_rank_pairs": 749390, + "flat_census": { + "0": [ + { + "cliques_hit": 0, + "count": 1, + "lines": 0 + } + ], + "1": [ + { + "cliques_hit": 128, + "count": 60, + "lines": 1 + } + ], + "2": [ + { + "cliques_hit": 256, + "count": 360, + "lines": 2 + }, + { + "cliques_hit": 308, + "count": 320, + "lines": 3 + }, + { + "cliques_hit": 320, + "count": 30, + "lines": 6 + } + ], + "3": [ + { + "cliques_hit": 436, + "count": 960, + "lines": 4 + }, + { + "cliques_hit": 492, + "count": 480, + "lines": 6 + }, + { + "cliques_hit": 512, + "count": 60, + "lines": 15 + } + ], + "4": [ + { + "cliques_hit": 640, + "count": 1, + "lines": 60 + } + ] + }, + "gaussian_copy_floor": 40, + "lines": 60, + "maximal_clique_sizes": { + "10": 2304, + "11": 1920, + "12": 640, + "7": 1920, + "8": 1920 + }, + "maximum_clique_size": 12, + "maximum_cliques": 640, + "negative_controls": 6, + "nonempty_flats": 2271, + "rank_bound_pairs": 1827741, + "rational_copy_floor": 80, + "roots": 240, + "sharp_witness": { + "F": [ + 0, + 1, + 2, + 11, + 12, + 45 + ], + "G": [ + 0, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 54, + 55, + 56, + 57, + 58, + 59 + ], + "joint_hits": 192, + "pairing_rank": 1, + "ranks": [ + 2, + 3 + ] + }, + "uniform_coefficient": 192, + "unordered_nonempty_flat_pairs": 2579856, + "zero_joint_hit_pairs": 2725 + }, + "optimistic_deficit_per_bit": { + "1": -80, + "2": -40, + "3": 0, + "5": 80, + "7": 160 + }, + "port_clique_incidences": [ + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128, + 128 + ], + "schema": 1, + "status": "scoped negative result; no new kappa", + "uniform_gaussian_floor_per_bit": 40, + "uniform_rational_floor_per_bit": 80 +} diff --git a/research/gaussian-nonlinear-copy-floor/CLAIM.json b/research/gaussian-nonlinear-copy-floor/CLAIM.json new file mode 100644 index 0000000000..b865b86f9c --- /dev/null +++ b/research/gaussian-nonlinear-copy-floor/CLAIM.json @@ -0,0 +1,28 @@ +{ + "track": "structural decoder research", + "os_random_seed": 44, + "base_commit": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "started_utc": "2026-10-13T09:59:00Z", + "claimed_utc": "2026-10-13T10:01:50.923535+00:00", + "finish_utc": "2026-10-13T10:39:00Z", + "verification_start_utc": "2026-10-13T10:29:00Z", + "object": "Fixed-support deterministic zero-error nonlinear block messages on PR738 Gaussian E8 60-line geometry", + "method": "Conditional transcript injectivity on all 640 maximum nonorthogonal cliques; inherited exact flat-pair charge inequality; unequal independent bit demands", + "deliverable": "Scoped nonlinear copy floor C >= (2/3) sum b_t (40b uniform), finite nonlinear controls, source-pinned complete geometry replay, proof and handoff", + "candidates": [ + "Gaussian nonlinear block-message extension of scalar floor40", + "Exact asymmetric-sink feasibility of P112 float screen", + "Higher-target signed-star puncture mechanisms" + ], + "selection": "Seed44 is even: choose Gaussian rather than Eisenstein/Hurwitz. Existing #785 and #814 cover those two geometries; #738 covers only scalar binary totals. No compute-only reopening of the existing decoder optimization search.", + "coordination": "Repository open-issue inventory contains only #650, no sprint coordination issue. Claim recorded locally. Live PR searches inspected decoder, puncture, star and nonlinear work through #884.", + "selected_kappa": "1661634653669567/1000000000000000000", + "workers": "One read-only predecessor/model reviewer; later bounded verification only.", + "result_update": { + "status": "completed mathematical/model result, verified locally; packaging and submission in progress", + "result": "C >= max(ceil(2 sum b_t/3), max_Q sum_Q b_t); uniform40b Gaussian/80b rational; inherited Dfc gives D/T <= 40b(s-3)", + "evidence": "Complete2,579,856 flat-pair replay;49,152 nonlinear receiver decodes;2,621,440 conditional projection assignments; explicit pricing, side-information and decoding controls", + "link": "README.md", + "verification": "All three focused package tests and selected-record integrity pass; separate AI-assisted proof/code review finds no actionable issue." + } +} diff --git a/research/gaussian-nonlinear-copy-floor/NOTICE.md b/research/gaussian-nonlinear-copy-floor/NOTICE.md new file mode 100644 index 0000000000..226ae8aa51 --- /dev/null +++ b/research/gaussian-nonlinear-copy-floor/NOTICE.md @@ -0,0 +1,33 @@ +# Attribution and assistance + +Prepared for **@ToikY** with substantial **OpenAI Codex assistance** in task +selection, proof composition, implementation, finite verification and writing. +Separate AI workers supplied model/proof review and an independently written +nonlinear truth-table checker. This is not independent human peer review. + +- **Sagar Thakrar / @thakrarsagar, PR738**: Gaussian E8 geometry, full flat-pair + weighted-clique certificate, floor40 and conditional three-stage budget. + Six files under vendor/pr738 are retained verbatim at + `9671c5d72f3119ba26f3774f40aa7130c67bcf77`, with their original metadata. +- **Alexander Templeton / @azide0x37, PR785**: conditional transcript injection + and explicit per-bit nonlinear pricing model, originally for Hurwitz E8. +- **Michael Fischler / @shiftybitshiftr, PR814**: the composition of that + argument with a general nonorthogonal clique certificate, unequal demands, + concentration inequality and nonlinear controls for Eisenstein E8. + The analogous composition here is credited and no method-priority claim is made. +- **Joel Pulikkan / @GamingPuzzled, PR620**: Gaussian geometry and asymmetric + decoder question; **Douglas R. Colkitt / @Mister-Meeseeks, PR703**: + predecessor averaged-clique method; **DreamingOfClouds, PR446/PR595**: + pairing-rank and conditional deficit accounting. Their retained source credit + remains in PR738's original files. +- **@chinmayarvind23, PR770** and **William Lawyer / @WilliamLawyer, PR868**: + distinct Gaussian clique-certificate ceilings. Their pending implementations + and ceilings are not dependencies or composed savings here. +- The accepted construction remains **Jeremy Kothe's PR799**, **Chafik + Boukhalfa's PR741**, **DreamingOfClouds' PR589**, **eumemic's PR555** and their + retained source-gauge/compiler/analytic lineage. + +The original predecessor proof documents are retained under sources/ with +exact source heads and hashes in SOURCES.json. New material and the retained +PR files follow the repository's **Apache-2.0** license. No upstream/ file is +changed. No literature-wide priority or official OpenAI endorsement is claimed. diff --git a/research/gaussian-nonlinear-copy-floor/OVERLAP.json b/research/gaussian-nonlinear-copy-floor/OVERLAP.json new file mode 100644 index 0000000000..3ef6d4940b --- /dev/null +++ b/research/gaussian-nonlinear-copy-floor/OVERLAP.json @@ -0,0 +1,166 @@ +{ + "checked_utc": "2026-10-13 10:16:34 UTC", + "repository": "CrocSwap/integer-mult-bounds", + "base_commit": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "pins": [ + { + "pr": 738, + "title": "Scoped negative result: Gaussian E8 copy floor 40 excludes three stages", + "head": "9671c5d72f3119ba26f3774f40aa7130c67bcf77", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/738", + "role": "dependency" + }, + { + "pr": 785, + "title": "Scoped negative result: Hurwitz copy floor for fixed-support nonlinear messages", + "head": "83e78085ae9c110a34bff87e71387292d85e47c0", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/785", + "role": "dependency" + }, + { + "pr": 814, + "title": "Research: Eisenstein nonlinear message copy floor 22b under explicit width pricing", + "head": "d91c5152b314391406b0ec792b6765a5cf0af2f1", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/814", + "role": "dependency" + }, + { + "pr": 770, + "title": "Research: Gaussian E8 weighted maximal-clique ceiling 40 and independent replay", + "head": "48d027a664288ea1d4e987de63cb79588b8b936b", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/770", + "role": "related, no code or numerical premise imported" + }, + { + "pr": 868, + "title": "Research: Gaussian E8 all-clique certificate ceiling is 40 (no new kappa)", + "head": "54cbbea75b587bdf43a1c123e52220f936641d6f", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/868", + "role": "related, no code or numerical premise imported" + } + ], + "focused_query": "Gaussian nonlinear", + "focused_results": [ + { + "pr": 785, + "title": "Scoped negative result: Hurwitz copy floor for fixed-support nonlinear messages" + }, + { + "pr": 679, + "title": "Scoped negative result: volume-aware selector batching of complex children" + }, + { + "pr": 508, + "title": "Conditional kappa 0.001372554837726243: coordinated gauge collapse with retimed asynchronous whole owners" + } + ], + "recent_open_prs": [ + { + "pr": 887, + "title": "[Lean] Prove reserved-scratch echo bounds and equality family (no new kappa)" + }, + { + "pr": 886, + "title": "Scoped negative result: PR589's bit word is exactly frame-optimal (no new kappa)" + }, + { + "pr": 885, + "title": "[Lean] Prove the selected PR799 native Real moment bound" + }, + { + "pr": 884, + "title": "Research construction: R439 frame-521 block, 47 to 31 ADDs (no new kappa)" + }, + { + "pr": 882, + "title": "Research construction: seven grid-preserving JP8 circuits save 104 primitives per orientation (no new kappa)" + }, + { + "pr": 883, + "title": "Research construction: four-primitive X4 preconditions save 784 per orientation (no new kappa)" + }, + { + "pr": 669, + "title": "Research: prove higher-target star-code hierarchies and decoder geometry" + }, + { + "pr": 881, + "title": "Independent verification: PR869's U8 word and \u03ba with a code-disjoint checker (no new kappa)" + }, + { + "pr": 880, + "title": "Research/r439 block1 schedule seed8" + }, + { + "pr": 879, + "title": "Independent verification: exact synthetic-transform physical layouts (no new kappa)" + }, + { + "pr": 717, + "title": "Format limits part 2 (no \u03ba claim): erratum to #595, exact invoice prices, frontier-word censuses, decoder floors, spec requirements, centre and fragmentation walls" + }, + { + "pr": 878, + "title": "[Lean] Verify selected PR589 B boundaries and XOR interfaces" + }, + { + "pr": 877, + "title": "Research audit: quartic precision for balanced dirty cyclic inverses (no new kappa)" + }, + { + "pr": 876, + "title": "Scoped negative result: simultaneous full pair/triple exchanges do not beat SW4 (seed 29)" + }, + { + "pr": 860, + "title": "Research construction: signed CK reuse saves 926 primitives" + }, + { + "pr": 875, + "title": "Scoped negative result: classify the E8 rank-five boundary at 36 punctures" + }, + { + "pr": 874, + "title": "Research audit: X4 profile changes add, ideal exponent gains do not (no new kappa)" + }, + { + "pr": 873, + "title": "Research construction: shorten R439 phase-B block 508 from 37 to 30 ADDs (no new kappa)" + }, + { + "pr": 872, + "title": "[Lean] Packed Clifford representation bridge and a source-bound CK child" + }, + { + "pr": 871, + "title": "Tooling: exact modular rank fast path for historical joint-frame verification" + }, + { + "pr": 870, + "title": "Conditional \u03ba = 0.001661956299899884: PR858's sixteen-replica owner controller on the U8 word" + }, + { + "pr": 869, + "title": "Conditional \u03ba = 0.001661948695165034: eight triangle-hybrid B deliveries in block 0 on PR799's word" + }, + { + "pr": 868, + "title": "Research: Gaussian E8 all-clique certificate ceiling is 40 (no new kappa)" + }, + { + "pr": 867, + "title": "Research consolidation: selected-source provenance gap map + 298-row vendored-source re-verification (no new kappa)" + }, + { + "pr": 866, + "title": "Research audit: CK Horner reversal raises scalar-grid guard from 3 to 5 bits (no new kappa)" + } + ], + "open_issues": [ + { + "issue": 650, + "title": "Can we turn on Discussions?" + } + ], + "conclusion": "No overlapping Gaussian nonlinear block-message contribution found in the focused results or most recent 25 open PRs through #887. PR738 is scalar; PR785 and PR814 address distinct Hurwitz and Eisenstein geometries. PR770/#868 optimize the clique-certificate method on scalar Gaussian geometry, not nonlinear block-message scope. This is a bounded metadata overlap check, not an exhaustive semantic audit of every open PR." +} diff --git a/research/gaussian-nonlinear-copy-floor/PROOF.md b/research/gaussian-nonlinear-copy-floor/PROOF.md new file mode 100644 index 0000000000..576d109491 --- /dev/null +++ b/research/gaussian-nonlinear-copy-floor/PROOF.md @@ -0,0 +1,171 @@ +# Gaussian E8 nonlinear block-message copy floor + +This composes Sagar Thakrar's Gaussian geometric certificate in [PR738](https://github.com/CrocSwap/integer-mult-bounds/pull/738) +with Alexander Templeton's conditional transcript argument in [PR785](https://github.com/CrocSwap/integer-mult-bounds/pull/785), +as also applied by Michael Fischler to Eisenstein geometry in [PR814](https://github.com/CrocSwap/integer-mult-bounds/pull/814). +The methods are inherited. The new coverage is Gaussian nonlinear block messages, +unequal demands, and explicit controls of the pricing and side-information assumptions. + +## Model and result + +There are 60 Gaussian E8 lines, with the exact ordering and complex structure +of the pinned PR738 geometry. Port t holds an independent arbitrary b_t-bit +string X_t; each b_t is a fixed nonnegative integer. There are finitely many +messages with fixed source sets A_j, reader sets R_j and integer widths q_j >= 0: + + Y_j = f_j((X_a) for a in A_j) in {0,1}^{q_j}. + +All members of R_j receive the entire same message. Receiver t must recover +X_t on every input tuple using its received messages and all inputs X_u on +lines orthogonal to t. It has no free self-input. The functions, supports and +widths are fixed before inputs are chosen; encoders and joint decoders may +be arbitrary nonlinear functions. Unused declared sources can remain declared. + +For S a line set, let V_S be any rational row basis of the span of the +representatives of S and their J-images. Set + + c(R,A) = rank_Q(V_R V_A^T)/2, + C = sum_j q_j c(R_j,A_j). + +**Additive per-bit pairing-rank pricing is an explicit premise.** A scalar +copy-tree argument does not by itself establish this pricing for arbitrary +physical nonlinear circuits. This result applies to the specified message +model, not every conceivable way to share work across coordinates. + +For every such zero-error code, + + C >= max(ceil((2/3) sum_t b_t), max_Q sum_(t in Q) b_t), (1) + +where Q ranges over nonempty pairwise nonorthogonal cliques. In particular, +for uniform b_t=b, C >= **40b Gaussian / 80b rational units**. Direct per-port +messages give the abstract upper bound 60b. No cost-40b decoder or exact +nonlinear optimum is asserted. The nonlinear floor remains an interval [40b,60b]. +For demands supported on a nonorthogonal clique, (1) is sharp: direct messages +cost sum b_t, which equals its concentration term. + +Correlated inputs, errors, variable-length/average-cost messages, adaptive or +interactive encoding, sub-line supports, extra nonorthogonal side information, +and cheaper physical sharing between bits are outside this model. + +## Exact inherited Gaussian premise + +The doubled E8 roots have two nonzero coordinates +/-2, or eight coordinates ++/-1 with an even number of minus signs. The block complex structure sends +(x_0,x_1,...,x_6,x_7) to (-x_1,x_0,...,-x_7,x_6). It is orthogonal, squares to +-I and permutes the 240 roots. Its four-root orbits define 60 Gaussian lines. +Their spans have Gaussian dimension at most four. + +A line-generated space is J-invariant. Its pairing kernel with another such +space is also J-invariant: J is orthogonal and preserves both spaces. The +rational dimensions of domain and kernel are even, so c(R,A) is an integer. +Changing row bases does not change the product rank. The self-pairing of a +nonzero line is nonzero; orthogonality excludes the port itself. + +PR738 assigns weight 1/192 to all 640 maximum nonorthogonal cliques, each of +size 12. For any R,A, its certified geometric inequality is + + H(R,A) := number of those cliques meeting both R and A + H(R,A) <= 192 c(R,A). (2) + +The new driver replays PR738's unchanged exact geometry and calculation; +it does not claim an independent implementation of (2). All 2,272 flats, +including the empty flat, are generated by adjoining a line and taking exact +closure. Every flat has a line basis, so induction on its basis size proves +completeness. Closing a support preserves its span and pairing rank and only +increases clique-hit indicators. Symmetry therefore reduces (2) for all +2^60 by 2^60 supports to 2,579,856 unordered nonempty flat pairs. Empty supports +have zero hits and charge. The retained checker partitions them into 2,725 +zero-hit pairs, 1,827,741 rank-bound pairs, and 749,390 exact-rank pairs. +The committed sharp rank-two/rank-three witness still has pairing rank one +and 192 joint hits. Six inherited rejection controls are rerun. + +Each of the 60 ports belongs to exactly 128 of the 640 cliques; the new driver +checks every incidence literally. Its total weight is 128/192 = 2/3. +The retained historical source-check entry point is not invoked: its old +selected-record pin differs from today's base. Instead the new source checker +binds every retained byte and current-base dependency in SOURCES.json before +calling the unchanged calculate() function. Original source metadata and +notices are preserved; no selected record is rewritten. + +## Conditional transcript injection + +Fix any nonorthogonal clique Q and any assignment of all inputs outside Q. +Let J_Q contain exactly the messages whose source and reader sets both meet Q. +The map from X_Q to the displayed transcript (Y_j) for j in J_Q is injective. + +Suppose two different X_Q assignments gave the same transcript. Every message +received by a receiver in Q but absent from J_Q has sources disjoint from Q, +so its value is fixed and identical. Every receiver's orthogonal side +information is outside Q, so it too is identical. Each receiver in Q thus +has identical complete decoder input and returns the same X_t. This contradicts +the difference in X_Q. No assumption about linearity or separate decoding of +message coordinates is used. + +Counting all possible inputs and fixed-width transcripts gives + + sum_(t in Q) b_t <= sum_j q_j [Q meets R_j and A_j]. (3) + +This is an all-width written proof. Finite truth tables below are controls, +not a substitute for injectivity at arbitrary widths. + +Multiply (3) by 1/192 and sum over the 640 maximum cliques. The literal +128-incidence property and (2) give + + (2/3) sum_t b_t + <= sum_j q_j H(R_j,A_j)/192 + <= sum_j q_j c(R_j,A_j) = C. + +Integrality of c and q supplies the ceiling in (1). For any clique, if both +supports meet it, choose one line from each intersection. They are the same +nonzero line or two nonorthogonal lines, so the Gram product has a nonzero +block and c >= 1. Equation (3) therefore also gives C >= sum_(t in Q) b_t. +For nonnegative demands the maximum occurs on an inclusion-maximal clique; +all 8,704 such cliques are enumerated, including those smaller than size 12. + +## Nonlinear and boundary controls + +The separate implementation independent_controls.py chooses three disjoint +orthogonal four-line frames using seed44. For their three parities z_0,z_1,z_2, +it broadcasts (z_0,z_1,z_2 XOR (z_0 AND z_1)) to those twelve active ports. +After inverting the Boolean shear, each receiver recovers its own bit using +the other three frame inputs, which are legal orthogonal side information. +The common source/reader span has Gaussian rank four and width three, so +charge is 12, while (1)'s averaged active-demand floor is eight. +All 4,096 input tuples and every receiver are checked. A mixed Boolean +derivative certifies genuine nonlinearity. All conditional projections of +the 640 weighted cliques are checked, including every outside assignment. + +Charging that entire three-bit message only once would give four rather +than twelve, violating the certified active floor eight. This correct +code is a boundary example for the *pricing premise*, not a counterexample +to (1). Similarly, twelve mutually nonorthogonal ports can decode one parity +if granted all other eleven inputs as side information. The pairing charge +is four versus clique demand twelve; the code is correct but its side +information is inadmissible. Dropped message bits and failure to invert the +nonlinear shear are decoding failure controls. The exact finite coverage +and rejection counts are recorded in CERTIFICATE.json. + +## Optimistic complete budget + +Only if the implementation obeys both the declared message charge and the +separate inherited Dfc stage identity may one set v=60, rational port rank +k=2b and cst=2C. Then + + D/T = (s-1) 120b - s 2C <= 40b(s-3). + +At three stages this is nonpositive. Helper preparation, source access, +encoding/decoding, frame changes, extra copies, restoration, and recursive +children have all been granted zero additional expense. Adding any +nonnegative expense cannot repair this screen. Thus this three-stage mechanism +cannot yield a positive supplier saving under those premises, regardless +of which other supplier would bind the assembly. Five or more stages and +changed accounting remain open; no physical invoice is built. + +The original all-size/compiler, realization, whole-call hosting, +precision/tape/exact recovery and analytic obligations remain inherited. +No selected construction or kappa changes. Written mathematical argument +and finite replay are not a proof-assistant verification of integer multiplication. + +Prepared for @ToikY with substantial OpenAI Codex assistance, including +proof development, implementation and a separate AI-assisted model review. +No independent human review or literature priority is claimed. Apache-2.0. diff --git a/research/gaussian-nonlinear-copy-floor/README.md b/research/gaussian-nonlinear-copy-floor/README.md new file mode 100644 index 0000000000..3f3e40bf9e --- /dev/null +++ b/research/gaussian-nonlinear-copy-floor/README.md @@ -0,0 +1,86 @@ +# Gaussian nonlinear message copy floor + +**Scoped negative result; no new kappa or physical supplier.** On the 60 +Gaussian E8 lines, fixed-support, deterministic, zero-error nonlinear block +messages obey + + C >= max(ceil((2/3) sum b_t), max_Q sum_(t in Q) b_t). + +Here a q-bit message pays q times its Gaussian reader/source pairing rank, +additively across messages. This pricing is an explicit premise, not a proved +physical cost law for arbitrary nonlinear circuits. Receivers may use all +orthogonal input ports as free side information. For uniform b-bit demand, +the lower bound is **40b Gaussian / 80b rational units**. Direct messages cost +60b; the optimum remains unresolved. Demand confined to any nonorthogonal +clique has sharp cost sum b_t. + +The [proof](PROOF.md) composes PR738's exact Gaussian certificate with the +conditional transcript argument of PR785/PR814. PR738 covers scalar binary +totals; PR785 and PR814 cover Hurwitz and Eisenstein geometries. This adds the +Gaussian block/nonlinear case. The methods and predecessor work are credited +in [NOTICE.md](NOTICE.md); no priority for the methods is claimed. + +Only with the additional inherited Dfc accounting does the optimistic screen +become D/T <= 40b(s-3). Three stages cannot give positive deficit, even granting +zero helper, source-access, encoding, decoding, frame, restoration and extra +recursive costs. Five or more stages and different accounting remain open. +No supplier implementation, physical invoice or improved exponent is claimed. + +## Reproduce + +From the repository root, with **Python 3.10+ and the standard library**: + +```sh +python3 -I -B research/gaussian-nonlinear-copy-floor/verify.py +python3 -I -B research/gaussian-nonlinear-copy-floor/test_package.py +``` + +Expected primary marker: + +```text +PASS_GAUSSIAN_NONLINEAR_COPY_FLOOR lines=60 cliques=640 flat_pairs=2579856 floor=40b no_new_kappa +``` + +The verifier is offline and read-only by default. `--output NEW.json` writes a +verified receipt only to a new file. `--check-sources` checks immutable inputs +only and does **not** replay the theorem. Optimized Python (`-O`) is deliberately +rejected because the retained PR738 geometry uses assertions. + +The driver hashes every retained input before import, calls PR738's unchanged +exact calculation and compares its complete certificate, checks every port's +128 clique incidences, and runs a separately implemented nonlinear truth-table +checker. Its own manifest binds today's selected source context; it does not +call the retained verifier's historical selected-record entry point. +All 2,579,856 nonempty flat pairs are covered. Closure and symmetry explain +why this covers every ordered support pair. The finite nonlinear checks cover +a three-parity Boolean shear on twelve active ports, all 4,096 inputs, every +receiver and every conditional clique transcript. Pricing and illegal side +information have correct-code boundary examples; omitted decoding work has +failure controls. Exact counts are in [CERTIFICATE.json](CERTIFICATE.json). + +Package tests check zero, uniform and concentrated unequal demands on all five +maximal-clique sizes, invalid demands, receipt corruption, source tampering, +missing input, minimal relocated input closure and deliberate `-O` rejection. +[VALIDATION.md](VALIDATION.md) records actual execution and its limits. + +## Pins and scope + +- Base: `f567884aeb8851b6e794af1184119a3bfbe1e631`. +- OS assignment seed44, structural decoder track; local [claim](CLAIM.json). +- Gaussian certificate PR738: `9671c5d72f3119ba26f3774f40aa7130c67bcf77`. +- Hurwitz method PR785: `83e78085ae9c110a34bff87e71387292d85e47c0`. +- Eisenstein composition PR814: `d91c5152b314391406b0ec792b6765a5cf0af2f1`. +- Exact immutable input SHA256/Git-blob pins: [SOURCES.json](SOURCES.json). + +Fixed supports and widths, independent demands, deterministic zero-error +recovery, whole Gaussian-line pairing and additive per-bit pricing are essential. +Interactive/adaptive encoding, correlated demands, error, variable/average length, +sub-line supports, extra nonorthogonal side information and cheaper physical +coordinate sharing are excluded. No previously closed decoder search is reopened; +there is no candidate search or claim of decoder optimality. + +The selected conditional kappa remains **1661634653669567/10^18**. Its +all-size/compiler, realization, hosting, precision/tape/exact-recovery and +analytic assumptions remain. Finite replay and the written argument are not +formal verification of the integer multiplication theorem. Only this research +package is added; existing files, the selected frontier and upstream/ stay intact. diff --git a/research/gaussian-nonlinear-copy-floor/SOURCES.json b/research/gaussian-nonlinear-copy-floor/SOURCES.json new file mode 100644 index 0000000000..7f06a66a98 --- /dev/null +++ b/research/gaussian-nonlinear-copy-floor/SOURCES.json @@ -0,0 +1,96 @@ +{ + "base_commit": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "selected_kappa": "1661634653669567/1000000000000000000", + "vendor": { + "vendor/pr738/geometry.py": { + "source_path": "research/gaussian-clique-copy-bound/geometry.py", + "commit": "9671c5d72f3119ba26f3774f40aa7130c67bcf77", + "sha256": "4a3e2cee2e35ccebde346e63fd9869ed48b2d59de120f570650ecb9c8875f5e4", + "git_blob": "150762c7643a0ab5463a2b447d0541a32d7701fe" + }, + "vendor/pr738/verify.py": { + "source_path": "research/gaussian-clique-copy-bound/verify.py", + "commit": "9671c5d72f3119ba26f3774f40aa7130c67bcf77", + "sha256": "966c5181f6a2d0865ae9a4be90ecb2a04cad8ca3b8acfc328fbe24ceaf9a7c6c", + "git_blob": "71f0c21ecc2e9b0da7d0b0d937ab6ac0fe952db6" + }, + "vendor/pr738/certificate.json": { + "source_path": "research/gaussian-clique-copy-bound/certificate.json", + "commit": "9671c5d72f3119ba26f3774f40aa7130c67bcf77", + "sha256": "c50858aaab863b34c7533211ca07ae038ee000328bd5134b73219992ae078875", + "git_blob": "cacb07d8e71177175c0702e5f455cc986dce5d42" + }, + "vendor/pr738/PROOF.md": { + "source_path": "research/gaussian-clique-copy-bound/PROOF.md", + "commit": "9671c5d72f3119ba26f3774f40aa7130c67bcf77", + "sha256": "e33a3950f172bc93400fffd85df55236059f5391d4ed8a82e0f12bcd7f196812", + "git_blob": "748e6324394d53cf910836eb55e28578d8bc684a" + }, + "vendor/pr738/README.md": { + "source_path": "research/gaussian-clique-copy-bound/README.md", + "commit": "9671c5d72f3119ba26f3774f40aa7130c67bcf77", + "sha256": "3853e8bb59bf96c708dc08d89457a9ce807a7b46ed4fb84747340738960f1253", + "git_blob": "71fab92b57ea47b5eec325a175322b07a84992b9" + }, + "vendor/pr738/SOURCES.json": { + "source_path": "research/gaussian-clique-copy-bound/SOURCES.json", + "commit": "9671c5d72f3119ba26f3774f40aa7130c67bcf77", + "sha256": "4ac0c419be13c5caf306aaa827b90fed469f63950128d08027c1db640c3f8ef7", + "git_blob": "ca6f490c997b0f57c26657ac305e20074d8d181d" + } + }, + "base_sources": { + "certificates/selected-result.json": { + "sha256": "9873519224e2db72d6a8c926f51e3e75129671e467948c6f6b03744f8bcfc699", + "git_blob": "1f107b55a2f045fa66d9c35d658b3b79549f5ba6" + }, + "docs/research/current-status.md": { + "sha256": "415f85180f698329bea968798f2bc2519f56374cccc3e07c8e9051bd65192730", + "git_blob": "018b9b5aef5debdf7e951f247e7e22686a7c9753" + }, + "docs/research/pr-ledger.md": { + "sha256": "d8169a360cd6e5842b47008362c7cce0ffcdd62733a8e8210ef6a8ff32bb65c9", + "git_blob": "bcdfa8c49100755cc05594295aa9acd3a18d0d78" + }, + "docs/research/community-frontier799-review.md": { + "sha256": "bd91c10c67f2a873fd456b95cbb43f715a43dac0e0a66938737d591c6b754052", + "git_blob": "7a2cd0a64199e0aaf93451377acbed3e8c7ae6b7" + }, + "research/gauge44-frames-x/PROOF-NOTE-FRAMES-X4.md": { + "sha256": "39c50420ebb6e8813706a49b2cf759f277c4afac9f6780fc0a7ac6a5fb86e036", + "git_blob": "a456a8127badf654c6b2ac64e54818bfa6ec0837" + }, + "research/e8-decoder-floors-and-cold14-notes/s1-extension-rings/REPORT.md": { + "sha256": "e8de809976a1253087e9058d346dfcc7b098f6481c64f1569aa3072d27345e02", + "git_blob": "1a766e365587b0c1bce414b50ffb7b916ba28da9" + }, + "research/e8-decoder-floors-and-cold14-notes/s1-extension-rings/gauss_geom.py": { + "sha256": "4750d252d87e4022e17fbfe0ac697d5d4c077a85541e217c4f206d39d5cfa2ae", + "git_blob": "7caaaeddc5a3b785fd4abb5afccaaff1e1bda61d" + }, + "research/e8-decoder-floors-and-cold14-notes/s1-extension-rings/algebra_lines.py": { + "sha256": "bc4037049debf9b7affeb7e6b30da0193dea8c3850a7317afd045ac7ac481108", + "git_blob": "6ecaf65779aa2eaa42124e8ed8f3f755d70efbc1" + }, + "research/format-limits/README.md": { + "sha256": "0fa0d6b2df96ddc06b876c41c5fa8d2335b97f36bc8f17d1371296d23199c263", + "git_blob": "2f7aaf5b8225717394fe6adda6b313026eaf8090" + } + }, + "predecessors": { + "785": { + "commit": "83e78085ae9c110a34bff87e71387292d85e47c0", + "source_path": "research/hurwitz-nonlinear-copy-floor/PROOF.md", + "local_path": "sources/pr785-PROOF.md", + "sha256": "62206654c5e6928324563bd5883db7186917a4546126ae64b72eee8914d9f573", + "git_blob": "9811bf631707a087086f2efb1c2eb6db24eab20c" + }, + "814": { + "commit": "d91c5152b314391406b0ec792b6765a5cf0af2f1", + "source_path": "research/eisenstein-message-copy-bound/PROOF.md", + "local_path": "sources/pr814-PROOF.md", + "sha256": "dd8c7890d661ae87167d038d12356845470a2822733c45bd9ab4c9208e381311", + "git_blob": "86d6e25ed60488646c0316a2c930e1f9e3ade99a" + } + } +} diff --git a/research/gaussian-nonlinear-copy-floor/VALIDATION.md b/research/gaussian-nonlinear-copy-floor/VALIDATION.md new file mode 100644 index 0000000000..291828783d --- /dev/null +++ b/research/gaussian-nonlinear-copy-floor/VALIDATION.md @@ -0,0 +1,60 @@ +# Validation record + +Validated on macOS with CPython **3.12.14**, standard library only, on +2026-10-13. Base: `f567884aeb8851b6e794af1184119a3bfbe1e631`. +The local runtime was +`/Users/evaayala/.cache/codex-runtimes/codex-primary-runtime/dependencies/python/bin/python3`. +The reproduction commands below use `python3` with Python 3.10 or later. + +## Completed checks + +```sh +python3 -I -B research/gaussian-nonlinear-copy-floor/verify.py --output /path/to/NEW.json +python3 -I -B research/gaussian-nonlinear-copy-floor/test_package.py +make selected-record-check +``` + +- Complete primary replay passed with the marker in + [evidence/full-replay.txt](evidence/full-replay.txt). The newly written + receipt was byte-identical to CERTIFICATE.json. It covers all **2,579,856 + unordered nonempty flat pairs**, all **640 maximum cliques**, and all + **60 port-incidence counts**. The unchanged PR738 calculation and its six + rejection controls are retained; this is not a new independent geometry proof. +- The separately written nonlinear checker passes **49,152 receiver decodes** + on all **4,096 input tuples**, **4,096 mixed-derivative checks**, and + **2,621,440 conditional projection assignments** over **559,104 outside + assignment classes**. Omitted inversion fails on 4,096 receiver cases; + dropped bits fail on 12,288 / 12,288 / 8,192 receiver cases. Width underpricing + and illegal side information are explicit correct-code boundary examples. +- All **three focused package tests** passed in 0.468 seconds; output is in + [evidence/package-tests.txt](evidence/package-tests.txt). They cover zero, + uniform and concentrated demands on all five maximal-clique sizes; invalid + demands; five changed receipt fields; source tampering and omission; selected + source tampering; isolated relocated source checks; deliberate optimized-mode + rejection; and preservation of an existing output file. +- A minimal copy containing only this package and the nine pinned base inputs + passed the **complete** isolated replay from an unrelated working directory + outside the checkout. Its fresh receipt was byte-identical; see + [evidence/relocated-replay.txt](evidence/relocated-replay.txt). This goes beyond + the source-only relocation check in the focused tests. +- `make selected-record-check` passed. The selected conditional kappa remains + `1661634653669567/1000000000000000000`. +- A separate AI worker reviewed the written proof, accounting scope, controls + and code, and individually checked nonorthogonality and inclusion-maximality + of all **8,704 maximal cliques**. No actionable issue remained; the bounded + record and reviewed code hashes are in [evidence/review.json](evidence/review.json). + This is not independent human peer review. + +## Interpretation and limits + +The all-width injection argument is in PROOF.md. Truth tables establish the +stated finite controls, not arbitrary-width correctness by enumeration. +The driver deliberately rejects optimized Python (`-O`) because its retained +geometry uses assertions. No successful optimized replay is claimed. + +Only this new research package is submitted. No generator, existing certificate, +selected construction or upstream/ file changes. Full `make verify`, selected +supplier cold replay, hosted CI and proof-assistant verification were not run or +claimed for this isolated note. The physical per-bit pricing and inherited stage +accounting remain explicit premises; the full multiplication theorem and the +nonlinear decoder optimum remain unresolved. diff --git a/research/gaussian-nonlinear-copy-floor/evidence/full-replay.txt b/research/gaussian-nonlinear-copy-floor/evidence/full-replay.txt new file mode 100644 index 0000000000..c827aa4f11 --- /dev/null +++ b/research/gaussian-nonlinear-copy-floor/evidence/full-replay.txt @@ -0,0 +1 @@ +PASS_GAUSSIAN_NONLINEAR_COPY_FLOOR lines=60 cliques=640 flat_pairs=2579856 floor=40b no_new_kappa diff --git a/research/gaussian-nonlinear-copy-floor/evidence/package-tests.txt b/research/gaussian-nonlinear-copy-floor/evidence/package-tests.txt new file mode 100644 index 0000000000..4ee88f247d --- /dev/null +++ b/research/gaussian-nonlinear-copy-floor/evidence/package-tests.txt @@ -0,0 +1,8 @@ +test_certificate_mutations (__main__.PackageChecks.test_certificate_mutations) ... ok +test_demands_and_concentration (__main__.PackageChecks.test_demands_and_concentration) ... ok +test_relocated_source_corruption_and_optimization (__main__.PackageChecks.test_relocated_source_corruption_and_optimization) ... ok + +---------------------------------------------------------------------- +Ran 3 tests in 0.468s + +OK diff --git a/research/gaussian-nonlinear-copy-floor/evidence/relocated-replay.txt b/research/gaussian-nonlinear-copy-floor/evidence/relocated-replay.txt new file mode 100644 index 0000000000..c827aa4f11 --- /dev/null +++ b/research/gaussian-nonlinear-copy-floor/evidence/relocated-replay.txt @@ -0,0 +1 @@ +PASS_GAUSSIAN_NONLINEAR_COPY_FLOOR lines=60 cliques=640 flat_pairs=2579856 floor=40b no_new_kappa diff --git a/research/gaussian-nonlinear-copy-floor/evidence/review.json b/research/gaussian-nonlinear-copy-floor/evidence/review.json new file mode 100644 index 0000000000..caed842206 --- /dev/null +++ b/research/gaussian-nonlinear-copy-floor/evidence/review.json @@ -0,0 +1,24 @@ +{ + "reviewer": "separate OpenAI Codex AI worker; not independent human peer review", + "status": "no actionable correctness or scope issues found", + "checked": [ + "conditional transcript proof and inherited pricing scope", + "ceil(2 total demand /3)", + "all8704 maximal cliques individually nonorthogonal and inclusion-maximal", + "2,621,440 conditional assignment checks and559,104 outside classes", + "actual dropped-bit and omitted-inversion decoding failures", + "pricing and inadmissible side-information correct-code boundary examples" + ], + "clique_census": { + "7": 1920, + "8": 1920, + "10": 2304, + "11": 1920, + "12": 640 + }, + "code_sha256": { + "verify.py": "f4c1f58b3eb5b070df69aad111d6ca287ffcb0b32dbd403d43533f482a90314b", + "independent_controls.py": "6a7847cdebd35da3c72e89c8744971df985157b5a2cefa685a825ffdf41c648e" + }, + "limitations": "Shared retained PR738 geometry; not independent reconstruction of all flat-pair ranks or proof-assistant theorem verification." +} diff --git a/research/gaussian-nonlinear-copy-floor/independent_controls.py b/research/gaussian-nonlinear-copy-floor/independent_controls.py new file mode 100644 index 0000000000..08214f5db6 --- /dev/null +++ b/research/gaussian-nonlinear-copy-floor/independent_controls.py @@ -0,0 +1,339 @@ +"""Finite nonlinear-message controls; no code imported from PR785 or PR814. + +Only the pinned PR738 Gaussian E8 geometry is reused. These finite controls +test decoder and accounting hypotheses, not the universal entropy theorem. +All new obligations use explicit exceptions, including the negative controls. +""" + +from collections import Counter +from fractions import Fraction +import hashlib +import importlib.util +from itertools import combinations +import json +from pathlib import Path +import random + + +GEOMETRY_SHA256 = "4a3e2cee2e35ccebde346e63fd9869ed48b2d59de120f570650ecb9c8875f5e4" +GEOMETRY_COMMIT = "9671c5d72f3119ba26f3774f40aa7130c67bcf77" +SEED = 44 +INPUT_BITS = 12 +INPUT_COUNT = 1 << INPUT_BITS +INPUT_MASK = INPUT_COUNT - 1 + + +def _load_geometry(): + path = Path(__file__).resolve().parent / "vendor" / "pr738" / "geometry.py" + if hashlib.sha256(path.read_bytes()).hexdigest() != GEOMETRY_SHA256: + raise ValueError("retained PR738 geometry source hash mismatch") + specification = importlib.util.spec_from_file_location("pr738_controls_geometry", path) + if specification is None or specification.loader is None: + raise ValueError("cannot load retained PR738 geometry") + module = importlib.util.module_from_spec(specification) + specification.loader.exec_module(module) + return module + + +def _rank(rows): + """Independent rational Gaussian elimination, avoiding retained rank code.""" + rows = [list(map(Fraction, row)) for row in rows] + if not rows: + return 0 + rank = 0 + for column in range(len(rows[0])): + pivot = next((i for i in range(rank, len(rows)) if rows[i][column]), None) + if pivot is None: + continue + rows[rank], rows[pivot] = rows[pivot], rows[rank] + scale = rows[rank][column] + rows[rank] = [entry / scale for entry in rows[rank]] + for i in range(rank + 1, len(rows)): + scale = rows[i][column] + rows[i] = [entry - scale * pivot_entry + for entry, pivot_entry in zip(rows[i], rows[rank])] + rank += 1 + if rank == len(rows): + break + return rank + + +def _rows(geometry, lines, ports): + return tuple(row for port in ports for row in (lines[port], geometry.J(lines[port]))) + + +def _pair_charge(geometry, lines, source_ports, reader_ports): + source_rows = _rows(geometry, lines, source_ports) + reader_rows = _rows(geometry, lines, reader_ports) + source_rank, reader_rank = _rank(source_rows), _rank(reader_rows) + pairing_rank = _rank(tuple(tuple(geometry.dot(a, b) for b in reader_rows) + for a in source_rows)) + if any(rank % 2 for rank in (source_rank, reader_rank, pairing_rank)): + raise ValueError("Gaussian dimensions must have even real rank") + return source_rank // 2, reader_rank // 2, pairing_rank // 2 + + +def _select_frames(graph): + frames = [] + for frame in combinations(range(len(graph)), 4): + mask = sum(1 << port for port in frame) + if all(not (graph[port] & mask) for port in frame): + frames.append(frame) + if len(frames) != 105: + raise ValueError("expected exactly 105 orthogonal four-line frames") + random.Random(SEED).shuffle(frames) + selected, used = [], set() + for frame in frames: + if used.isdisjoint(frame): + selected.append(frame) + used.update(frame) + if len(selected) == 3: + return tuple(selected), len(frames) + raise ValueError("cannot select three disjoint orthogonal frames") + + +def _encode(word): + z0 = (word & 15).bit_count() % 2 + z1 = ((word >> 4) & 15).bit_count() % 2 + z2 = ((word >> 8) & 15).bit_count() % 2 + return z0 | (z1 << 1) | ((z2 ^ (z0 & z1)) << 2) + + +def _undo_toffoli(message): + z0, z1 = message & 1, (message >> 1) & 1 + return message ^ ((z0 & z1) << 2) + + +def _receiver_failures(transcript, invert=True): + count, witness = 0, None + for word, message in enumerate(transcript): + parities = _undo_toffoli(message) if invert else message + for receiver in range(INPUT_BITS): + frame = receiver // 4 + mates = (15 << (4 * frame)) ^ (1 << receiver) + decoded = ((parities >> frame) & 1) ^ ((word & mates).bit_count() % 2) + expected = (word >> receiver) & 1 + if decoded != expected: + count += 1 + if witness is None: + witness = {"input_word": word, "receiver_local_index": receiver, + "message_word": message, "decoded": decoded, + "expected": expected} + return count, witness + + +def _conditional_projection(transcript, local_mask): + """Condition outside a clique; require injectivity of its requested bits.""" + outside_mask = INPUT_MASK ^ local_mask + seen, fiber_sizes = {}, Counter() + for word, message in enumerate(transcript): + outside = word & outside_mask + key = outside, message + inside = word & local_mask + if key in seen and seen[key] != inside: + raise ValueError("conditional transcript collision: " + json.dumps({ + "local_mask": local_mask, "outside_word": outside, + "message_word": message, "first_inside_word": seen[key], + "second_inside_word": inside}, sort_keys=True)) + if key not in seen: + seen[key] = inside + fiber_sizes[outside] += 1 + expected_fibers = 1 << (INPUT_BITS - local_mask.bit_count()) + expected_transcripts = 1 << local_mask.bit_count() + if len(fiber_sizes) != expected_fibers: + raise ValueError("conditional projection omitted an outside assignment") + if any(size != expected_transcripts for size in fiber_sizes.values()): + raise ValueError("conditional transcript has the wrong fiber size") + return expected_fibers, expected_transcripts + + +def _side_info_violations(graph, ports, side_information): + violations = [] + for receiver, known in zip(ports, side_information): + for source in known: + if receiver == source or graph[receiver] & (1 << source): + violations.append((receiver, source)) + return violations + + +def _require_accounting(charge, floor): + if charge < floor: + raise ValueError("charged copied-information cost is below the certified floor") + + +def calculate(lines=None, graph=None, cliques=None): + """Return deterministic JSON-compatible evidence for the finite controls. + + Inputs may be supplied by the complete geometry replay. ``cliques`` may + contain all maximal cliques or just the 640 maximum cliques. + """ + if not __debug__: + raise ValueError("optimized Python is unsupported because retained geometry uses assertions") + geometry = _load_geometry() + expected_lines = geometry.gaussian_lines() + lines = expected_lines if lines is None else tuple(lines) + if lines != expected_lines: + raise ValueError("controls require the pinned 60-line Gaussian E8 geometry") + expected_graph = geometry.nonorthogonality(lines) + graph = expected_graph if graph is None else tuple(graph) + if graph != expected_graph: + raise ValueError("nonorthogonality graph does not match retained geometry") + all_cliques = geometry.maximal_cliques(graph) if cliques is None else tuple(cliques) + maximum_cliques = tuple(sorted(c for c in all_cliques if c.bit_count() == 12)) + if len(maximum_cliques) != 640 or len(set(maximum_cliques)) != 640: + raise ValueError("controls require all 640 distinct maximum cliques") + for clique in maximum_cliques: + members = tuple(port for port in range(60) if clique & (1 << port)) + if len(members) != 12 or any((clique ^ (1 << port)) & ~graph[port] + for port in members): + raise ValueError("invalid maximum nonorthogonality clique") + + frames, frame_count = _select_frames(graph) + ports = tuple(port for frame in frames for port in frame) + source_rank, reader_rank, pair_charge = _pair_charge(geometry, lines, ports, ports) + if (source_rank, reader_rank, pair_charge) != (4, 4, 4): + raise ValueError("nonlinear example does not span a full rank-four source and reader") + side_information = tuple(tuple(port for port in frames[receiver // 4] + if port != ports[receiver]) + for receiver in range(INPUT_BITS)) + if _side_info_violations(graph, ports, side_information): + raise ValueError("nonlinear example uses nonorthogonal side information") + transcript = tuple(_encode(word) for word in range(INPUT_COUNT)) + failures, witness = _receiver_failures(transcript) + if failures: + raise ValueError("nonlinear receiver failed: " + json.dumps(witness, sort_keys=True)) + if len(set(transcript)) != 8: + raise ValueError("the three-bit message must attain all eight output words") + + dependence_counts = [] + for variable in range(INPUT_BITS): + count = sum(transcript[word] != transcript[word ^ (1 << variable)] + for word in range(INPUT_COUNT)) + if count != INPUT_COUNT: + raise ValueError("message omitted an advertised source variable") + dependence_counts.append(count) + derivative_counts = Counter(transcript[word] ^ transcript[word ^ 1] + ^ transcript[word ^ 16] ^ transcript[word ^ 17] + for word in range(INPUT_COUNT)) + if derivative_counts != Counter({4: INPUT_COUNT}): + raise ValueError("nonlinear second-difference witness is missing") + + intersection_counts, conditional_classes = Counter(), 0 + local_masks = [] + for clique in maximum_cliques: + local_mask = sum(1 << i for i, port in enumerate(ports) if clique & (1 << port)) + local_masks.append(local_mask) + intersection_counts[local_mask.bit_count()] += 1 + classes, _ = _conditional_projection(transcript, local_mask) + conditional_classes += classes + if max(intersection_counts) != 3: + raise ValueError("expected a three-demand maximum-clique concentration") + active_floor = (2 * len(ports) + 2) // 3 + correct_charge = 3 * pair_charge + _require_accounting(correct_charge, active_floor) + + omitted_failures, omitted_witness = _receiver_failures(transcript, invert=False) + if not omitted_failures: + raise ValueError("negative control failed to detect omitted nonlinear inversion") + three_demand_mask = next(mask for mask in local_masks if mask.bit_count() == 3) + dropped_controls = [] + for bit in range(3): + dropped = tuple(message & ~(1 << bit) for message in transcript) + count, witness = _receiver_failures(dropped) + if not count: + raise ValueError("negative control failed to detect a dropped output bit") + try: + _conditional_projection(dropped, three_demand_mask) + except ValueError as error: + projection_error = str(error) + else: + raise ValueError("dropped-bit conditional collision was not detected") + dropped_controls.append({"dropped_output_bit": bit, "detected": True, + "receiver_failure_count": count, "witness": witness, + "projection_rejection": projection_error}) + try: + _require_accounting(pair_charge, active_floor) + except ValueError as error: + undercharge_error = str(error) + else: + raise ValueError("negative control failed to reject one charge for three output bits") + + illegal_clique = maximum_cliques[0] + illegal_ports = tuple(port for port in range(60) if illegal_clique & (1 << port)) + illegal_side_info = tuple(tuple(port for port in illegal_ports if port != receiver) + for receiver in illegal_ports) + illegal_violations = _side_info_violations(graph, illegal_ports, illegal_side_info) + if len(illegal_violations) != 132: + raise ValueError("illegal maximum-clique side-information control is incomplete") + illegal_ranks = _pair_charge(geometry, lines, illegal_ports, illegal_ports) + if illegal_ranks != (4, 4, 4): + raise ValueError("illegal maximum-clique example has unexpected geometry") + illegal_transcript = tuple(word.bit_count() % 2 for word in range(INPUT_COUNT)) + illegal_decodes = 0 + for word, parity in enumerate(illegal_transcript): + for receiver in range(INPUT_BITS): + mates = INPUT_MASK ^ (1 << receiver) + decoded = parity ^ ((word & mates).bit_count() % 2) + if decoded != (word >> receiver) & 1: + raise ValueError("illegal-side-information parity decoder failed") + illegal_decodes += 1 + try: + _conditional_projection(illegal_transcript, INPUT_MASK) + except ValueError as error: + illegal_projection_error = str(error) + else: + raise ValueError("illegal-side-information transcript collision was not detected") + + return { + "geometry_source": {"commit": GEOMETRY_COMMIT, "sha256": GEOMETRY_SHA256}, + "seed": SEED, + "frame_search": {"orthogonal_frames": frame_count, + "selection": "seed44 shuffle of sorted four-line frames; first three disjoint"}, + "nonlinear_example": { + "frames": [list(frame) for frame in frames], "source_ports": list(ports), + "reader_ports": list(ports), "side_information": [list(known) for known in side_information], + "side_information_checks": 36, "source_rank": source_rank, "reader_rank": reader_rank, + "pairing_rank_charge": pair_charge, "output_bits": 3, + "encoder": "three frame parities z0,z1,z2, then z2 ^= z0 & z1", + "input_assignments": INPUT_COUNT, "receiver_decodes": INPUT_COUNT * INPUT_BITS, + "distinct_message_words": len(set(transcript)), "cost": correct_charge, + "active_demands": INPUT_BITS, "averaged_demand_floor": active_floor, + "maximum_clique_demand_floor": max(intersection_counts), + "source_dependence_counts": dependence_counts, + "nonlinear_second_difference": {"source_local_indices": [0, 4], + "nonzero_output_word": 4, "checks": INPUT_COUNT}, + }, + "conditional_transcript_projections": { + "maximum_cliques": len(maximum_cliques), + "input_assignments_per_clique": INPUT_COUNT, + "assignment_checks": len(maximum_cliques) * INPUT_COUNT, + "conditional_classes": conditional_classes, + "active_intersection_census": {str(k): intersection_counts[k] + for k in sorted(intersection_counts)}, + "injective": True, + }, + "negative_controls": { + "per_bit_charging": {"detected": True, "incorrect_one_message_charge": pair_charge, + "correct_three_bit_charge": correct_charge, + "certified_active_floor": active_floor, "rejection": undercharge_error}, + "omitted_nonlinear_inversion": {"detected": True, + "receiver_failure_count": omitted_failures, + "witness": omitted_witness}, + "dropped_output_bits": dropped_controls, + "illegal_nonorthogonal_side_information": { + "detected": True, "clique_ports": list(illegal_ports), + "ordered_side_information_violations": len(illegal_violations), + "first_violation": list(illegal_violations[0]), + "output_bits": 1, "pairing_rank_charge": illegal_ranks[2], + "cost": illegal_ranks[2], "active_demands": INPUT_BITS, + "averaged_floor_if_orthogonality_held": active_floor, + "clique_floor_if_orthogonality_held": INPUT_BITS, + "input_assignments": INPUT_COUNT, "receiver_decodes": illegal_decodes, + "conditional_projection_rejection": illegal_projection_error, + }, + }, + } + + +if __name__ == "__main__": + print(json.dumps(calculate(), indent=2, sort_keys=True)) diff --git a/research/gaussian-nonlinear-copy-floor/sources/pr785-PROOF.md b/research/gaussian-nonlinear-copy-floor/sources/pr785-PROOF.md new file mode 100644 index 0000000000..9811bf6317 --- /dev/null +++ b/research/gaussian-nonlinear-copy-floor/sources/pr785-PROOF.md @@ -0,0 +1,153 @@ +# A counting extension of the Hurwitz copy floor + +**Scoped result.** For the ten Hurwitz E8 lines, fixed-support, deterministic, +zero-error messages of arbitrary binary widths have minimum charge +`C = sum_t b_t`, when port t demands b_t independent bits and a q-bit message +with reader/source sets R,A is charged `q c(R,A)`. In particular, equal +block width b costs at least 10b quaternionic units, or 40b rational units. +Encoders and decoders may be nonlinear. No bound on the number of messages +is imposed, other than finiteness. + +This extends the scalar-total argument of Douglas R. Colkitt's +[#703](https://github.com/CrocSwap/integer-mult-bounds/pull/703), at commit +`358383e2f1b0f292d4d6eb897c06fd8558a4f5e6`. The perfect-matching geometry, +pairing charge, transversal weights and scalar optimum are predecessor work. +The addition here is conditional transcript injectivity in place of binary +rank, together with nonlinear attaining examples and assumption controls. + +## 1. Geometry and the pricing premise + +Use the E8 roots in doubled coordinates: vectors in Q^8 with either two +entries in {2,-2} and the rest zero, or eight entries in {1,-1} and an even +number of minus signs. Regard Q^8 as H_Q^2 and take the spans of the four +left multiples 1,i,j,k of each root. These are ten four-dimensional rational +subspaces. Their orthogonality graph is five disjoint pairs; write mate(t) +for the unique orthogonal line. Any two distinct lines span Q^8. + +For concatenated row bases V_R and V_A, set + + c(R,A) = rank_Q(V_R V_A^T) / 4. + +The exact charge table is: + +- 0 if a set is empty, or R and A are singletons at orthogonal mates; +- 1 otherwise if a nonempty set is a singleton; +- 2 if both sets have at least two elements. + +Two spanning sets have rank-eight pairing. A singleton against a spanning +set has rank four. Nonorthogonal singletons have rank-four pairing; mates +have zero pairing. The verifier reconstructs all roots and line bases, +checks every singleton pairing and every two-line span over the integers, +then checks every support pair against the transversal inequality below. + +**Explicit pricing premise:** a message of fixed width q_j, sent from source +set A_j to reader set R_j, is charged `q_j c(R_j,A_j)` quaternionic units. +Charges add over messages. Every transmitted bit is priced, even if the +encoder combines coordinates nonlinearly. This is the chosen block-message +model. It is **not** a derivation of nonlinear physical copy costs from +#446's scalar pairing-rank theorem. A supplier that shares physical work +between message coordinates more cheaply is outside this result. + +## 2. Information model + +There are independent inputs X_t ranging freely over {0,1}^{b_t}; b_t are +nonnegative integers. Message j has a fixed nonnegative integer width q_j +and is a deterministic function + + Y_j = f_j((X_a)_{a in A_j}) in {0,1}^{q_j}. + +The supports, widths and functions do not depend on the input. Every reader +t in R_j receives the same full Y_j; it may process those bits arbitrarily. +Receiver t must reconstruct X_t for **every** input tuple, using its received +messages and free side information X_mate(t). The decoder may jointly use +all those messages and need not be linear. Granting the entire mate input +is an optimistic relaxation of orthogonal residual correction. + +Source access, encoding, decoding and side-information preparation are free +in this model. There is no interactive relay, adaptive support, input +correlation, decoding error or additional nonorthogonal side information. +The theorem also covers a scalar fitting decoder from #703: each rank-one +total is one width-one message, and its mate contamination can be removed +using the granted side information. Fixed-support block-linear codes are +included as well, without requiring coordinatewise encoding. + +## 3. Transcript injectivity + +A transversal T chooses exactly one endpoint of each of the five mate +pairs. For this T define + + J_T = { j : R_j intersects T and A_j intersects T }. + +Fix **any** assignment of all inputs outside T. The map + + X_T -> (Y_j)_{j in J_T} + +is injective. To see this, suppose two different X_T assignments have the +same displayed transcript. Every message received by a receiver in T is +either in J_T or has A_j disjoint from T. Messages in the latter class are +identical because their source inputs were fixed. Every receiver's mate is +outside T, so all its side information is also identical. Its deterministic +decoder would therefore return the same X_t in both assignments, for all +t in T, contradicting the distinct X_T assignments. + +Consequently, counting possible transcripts gives + + 2^(sum_{t in T} b_t) <= 2^(sum_{j in J_T} q_j), + sum_{t in T} b_t <= sum_j q_j a_T(R_j,A_j), (1) + +where a_T is 1 exactly when both supports meet T. No probabilistic, +asymptotic or linearity assumption is used. The proof is for every finite +block width and every finite number of messages, not an extrapolation from +the truth tables used as controls. + +## 4. Average over the 32 transversals + +Each line lies in 16 transversals. For every R,A the predecessor inequality +is + + sum_T a_T(R,A) <= 16 c(R,A). (2) + +If c=0 no transversal hits both supports. If c=1 a singleton support occurs +in only 16 transversals. If c=2 the total number of transversals is 32. +Thus (2) follows in all cases. Summing (1) and dividing by 16 gives + + sum_t b_t <= sum_j q_j (sum_T a_T(R_j,A_j))/16 + <= sum_j q_j c(R_j,A_j) = C. + +The bound is sharp in the abstract model for arbitrary b_t: send X_t +directly from {t} to {t} with width b_t. This costs sum_t b_t. For equal +width b, another attaining code broadcasts the five mate-pair XORs in a +single 5b-bit message with all ports as sources and readers. Its charge is +`2 * 5b = 10b`. Apply any bijection of its 5b bits before transmission; +receivers invert it and recover their pair XOR using their mate input. +For example, the reversible update `z_2 ^= z_0 & z_1` makes the encoder +nonlinear and preserves both correctness and charge. The replay verifies +this example on all 1,024 inputs for ten one-bit ports, and a vector example +on all 256 inputs for four two-bit ports in the matching geometry. + +## 5. Optimistic complete-budget screen + +If, in addition, these b-fold ports satisfy the inherited Dfc stage +accounting with v=10, k=4b and cst=4C, then + + D/T = (s-1) * 40b - s * 4C <= -40b + +for every positive integer s and b. Helpers, source access, frame changes, +copies beyond this lower bound, restoration and recursive children were +all granted zero additional expense in this screen. Any nonnegative charge +for them cannot repair its negative deficit. There is no positive supplier +saving to feed into an assembly, regardless of the other supplier. +Accordingly no circuit implementation or kappa optimization is attempted. +The algebraic inequality supplies the all-s conclusion; the receipt's +finite arithmetic examples are only error controls. + +The use of Dfc and the conversion from message width to physical rank are +explicit additional assumptions. This note does not establish them for +nonlinear circuits. It does not bound interactive/adaptive codes, variable +length or average-cost communication, fractional physical sub-line copying, +correlated demands, other geometries or different stage accounting. + +Prepared by Alexander Templeton (@azide0x37) with substantial OpenAI Codex +assistance in the proof extension, implementation, checks and writing. +This is a written mathematical argument with finite exact checks, not a +proof-assistant formalization or a verification of integer multiplication. diff --git a/research/gaussian-nonlinear-copy-floor/sources/pr814-PROOF.md b/research/gaussian-nonlinear-copy-floor/sources/pr814-PROOF.md new file mode 100644 index 0000000000..86d6e25ed6 --- /dev/null +++ b/research/gaussian-nonlinear-copy-floor/sources/pr814-PROOF.md @@ -0,0 +1,220 @@ +# Fixed-support nonlinear messages on the Eisenstein E8 lines + +This note extends Jonathan Lam's [PR798](https://github.com/CrocSwap/integer-mult-bounds/pull/798) +scalar Eisenstein certificate to finite messages that may mix payload bits +nonlinearly. It uses Alexander Templeton's conditional-transcript argument +from [PR785](https://github.com/CrocSwap/integer-mult-bounds/pull/785), which +treats a different, Hurwitz geometry. Neither method is claimed as new here. +The new result is their composition on the Eisenstein geometry, including +unequal demands, a concentration bound, and explicit nonlinear controls. + +## Statement and model + +Let the 40 ports be the Eisenstein E8 lines specified below. Port t holds an +independent input X_t ranging freely over all b_t-bit strings, where b_t is a +nonnegative integer. There are finitely many messages. Message j has fixed +source and reader sets A_j,R_j, fixed integer width q_j >= 0, and value + + Y_j = f_j((X_a)_(a in A_j)) in {0,1}^{q_j}. + +Every reader in R_j receives the same complete Y_j. Receiver t must recover +X_t on **every** input tuple, using all its received messages and the full +inputs of ports orthogonal to t. Functions and joint decoders may be +nonlinear. Supports, widths and functions are fixed before the input is +chosen. Granting full orthogonal inputs as free side information is an +optimistic model of residual correction. + +For line sets R,A, let V_R,V_A be rational row bases of their spans and set + + c(R,A) = rank_Q(V_R V_A^T)/2, + C = sum_j q_j c(R_j,A_j). + +**The charge is a premise of this message model:** every transmitted bit +pays its support pairing rank, and charges add over messages. PR446's +scalar copy-tree interpretation does not establish this pricing for +arbitrary nonlinear physical circuits. Sharing physical work between bits +more cheaply would be outside the result. + +Write Q for any clique of pairwise nonorthogonal lines, including singletons. +The following bound holds for all finite widths and message counts: + + C >= max( ceil(11 sum_t b_t / 20), max_Q sum_(t in Q) b_t ). (1) + +In particular, if every port demands b bits, **C >= 22b Eisenstein rank +units**, or **44b rational rank units**. This is a lower bound, not the +optimum decoder cost. Direct messages give the abstract upper bound 40b. + +This model excludes adaptive/interactive supports, correlated inputs, +errors, variable-length or average-cost messages, rational sub-line +supports, and additional nonorthogonal side information. It includes +fixed-support block-linear codes, coordinate mixing, arbitrary nonlinear +encoding and joint decoding. It does not assert that every physical +vector-valued circuit has the declared additive charge. + +## Exact geometric premise (predecessor work, replayed independently) + +Use the 240 doubled E8 roots: two nonzero coordinates in {2,-2}, or eight +coordinates in {1,-1} with an even number of minus signs. Each has norm +squared eight. The root order and four mutually orthogonal A2 pairs in the +certificate match the `standard_e8`/`a2_rotation` object in Joel Pulikkan / +GamingPuzzled's archived PR620. For a root a, its reflection is + + s_a(x) = x - (x dot a) a / 4. + +Let J be the product of s_a s_b over the four pairs. The checker reconstructs +J and verifies J^2+J+I=0, J^T J=I, and preservation of every root. The six-root +orbits under ±J are exactly the roots in their rational two-dimensional +spans. They define 40 K-lines for K=Q(omega), in K-dimension four. The +certificate uses `rotation4 = 4J` to keep integer coordinates. + +Every line-generated space is J-invariant. So is the kernel of its pairing +with another such space: orthogonality of J gives invariance of X_A^perp. +Domain and kernel therefore have even rational dimension. Thus c is an +integer, independent of the chosen row bases. Pairing rank need not equal +either support's dimension. + +The scalar certificate in PR798 assigns weight 1/40 to each of the 40 +singletons, and 1/960 to each of the 2,880 seven-line nonorthogonal cliques. +Call these weights lambda_Q. Its geometric inequality is + + sum_Q lambda_Q [Q meets R and A] <= c(R,A). (2) + +Our implementation imports no predecessor executable code. It reconstructs +the geometry and checks the following integer form of (2) on every pair +of flats F,G: + + 24 |F intersect G| + H_7(F,G) <= 960 c(F,G). (3) + +Here H_7 counts seven-line cliques meeting both flats. The exact census is +772 flats and 298,378 unordered pairs including empty supports. Symmetry +covers both orders. All 30,880 one-line extensions remain in the flat list. +Flats are generated from the empty span by adjoining a line and taking +closure. Every flat has a line basis, so induction on basis size proves +completeness. Closing arbitrary supports preserves their spans and pairing +rank and can only increase clique-hit indicators. Hence (3) proves (2) for +all support pairs, not just the enumerated flat masks. + +Every port lies in exactly 504 seven-line cliques, as checked literally for +each of the 40 ports. Its total weight is therefore + + sum_(Q contains t) lambda_Q = 1/40 + 504/960 = 11/20. (4) + +The flat census by (K-rank, cardinality) is + + (0,0):1; (1,1):40; (2,2):240; (2,4):90; + (3,5):360; (3,12):40; (4,40):1. + +The geometric inequality and its scalar application belong to PR798. +This note does not claim a new optimality theorem for clique weights; that +PR also gives a separate dual certificate, which is not needed here. + +## Conditional transcript proof for arbitrary widths + +Fix a nonorthogonal clique Q and **any** assignment of all inputs outside +Q. Let J_Q be the messages whose source and reader sets both meet Q. Then + + X_Q -> (Y_j)_(j in J_Q) + +is injective. If two assignments of X_Q had the same displayed transcript, +each receiver in Q would have the same received messages: omitted messages +have all sources outside Q, so their values were fixed. Each receiver's +orthogonal side information is also outside Q, since distinct vertices of +Q are nonorthogonal. Every deterministic receiver would return the same +X_t in both assignments, contradicting their difference. + +Counting input tuples and possible fixed-width transcripts now gives + + sum_(t in Q) b_t <= sum_j q_j [Q meets R_j and A_j]. (5) + +This is the argument from PR785, applied to general nonorthogonal cliques. +It uses no linearity and holds for every finite width by proof, rather than +by extrapolating the truth-table controls. + +Multiply (5) by lambda_Q, sum over Q, and apply (2) and (4): + + (11/20) sum_t b_t + <= sum_j q_j sum_Q lambda_Q [Q meets R_j and A_j] + <= sum_j q_j c(R_j,A_j) = C. + +Integrality of q_j and c gives the ceiling in (1). + +For the other part of (1), if a clique meets both supports, choose a line +from each intersection. They are either the same nonzero line or two +nonorthogonal lines. The corresponding Gram block is nonzero. Evenness of +pairing rank gives c(R,A) >= 1. Thus (5) directly yields +C >= sum_(t in Q) b_t for every Q. Since b_t >= 0, the largest such demand +sum occurs on an inclusion-maximal clique. The checker enumerates all +2,970 maximal cliques, including the 90 of size four that are not contained +in seven-line cliques. + +The concentration term matters: demands supported on a seven-line clique +give C >= sum_t b_t, whereas (11/20) times their total alone is weaker. +No claim is made that (1) is the strongest inequality for every demand vector. + +## Nonlinear examples and assumption controls + +The seed-41 control chooses an exact partition into ten orthogonal +four-frames. For the first three frames, let z_0,z_1,z_2 be their input +parities. Broadcast to those 12 ports the three-bit message + + (z_0, z_1, z_2 XOR (z_0 AND z_1)). + +Receivers invert the last Boolean update. A receiver knows its other three +frame inputs as orthogonal side information, so its frame parity recovers +its own bit. The source and reader spans are full K-rank four, giving +charge 3*4=12. Its mixed Boolean derivative is nonzero, so this encoding is +nonlinear. The verifier exhausts all 4,096 inputs, all 12 receivers and +303,104 conditional transcripts from 74 distinct projections of the +weighted cliques. Adding 28 direct one-bit messages gives a cost-40 code +on all 40 ports. This product extension is justified algebraically; the +checker does not claim to enumerate 2^40 inputs. Independent repetitions +give cost 40b for arbitrary equal b, without claiming optimality. + +A second control uses demands 0,1,2,3 on one orthogonal four-frame, sending +each active bit-plane parity only to the ports with that bit. It checks all +64 inputs and 192 transcripts, with charge six and bound four. Inactive +and unequal-width ports are thus exercised explicitly. + +Two boundary examples show why the premises cannot be dropped: + +- Charging the three-bit nonlinear message just once would cost four, + below the certified integer bound seven for its 12 active inputs. It is + the per-bit charge, not a scalar copy theorem, that prevents this. +- Seven pairwise nonorthogonal ports could all recover from one parity + if each were given the other six inputs for free. Their joint span has + K-rank four, giving charge four versus the clique demand seven. This + code is correct on all 128 inputs, but violates the side-information + premise. The verifier accepts its decoding and rejects its admission. + +Twelve rejection controls cover understated widths, undeclared sources, +dropped message bits, constant messages, a missing nonlinear inverse, +illegal side information, underpriced width, a non-clique, the rational +rank conversion, excessive geometric weights, omitted singleton weights +and negative demands. These test mathematical failure modes. + +## Optimistic cost screen and remaining obligations + +Only if the physical implementation obeys the message pricing and the +inherited Dfc accounting may one substitute v=40, rational port rank 2b, +and cst=2C. Then + + D/T = (s-1)*80b - s*2C <= b*(36s-80). + +At three stages the upper deficit is **28b**, which is positive. This +result does **not** exclude a three-stage supplier. The nonlinear cost-40b +example has deficit -80b for every stage count and supplies no saving. +Helpers, source access, encoding, decoding, frame changes, further copies, +restoration and recursive children have all been granted zero additional +expense in this optimistic screen. Any achieved supplier must price them; +none is constructed here. The other supplier and outer assembly are not +replaced or repriced, and no new kappa follows. + +This contribution changes no selected record or supplier. All-size realization, +compiler, hosting, precision, tape and analytic obligations are inherited +and unresolved by this finite result. The transcript argument is a written +proof; the geometry has exhaustive finite premises. Neither is a +proof-assistant formalization of integer multiplication. + +Prepared by Michael Fischler (@shiftybitshiftr) with substantial OpenAI Codex +assistance in proof development, implementation, verification and writing. +Apache-2.0. See SOURCES.json and NOTICE.md for predecessor pins and credit. diff --git a/research/gaussian-nonlinear-copy-floor/test_package.py b/research/gaussian-nonlinear-copy-floor/test_package.py new file mode 100644 index 0000000000..7a29fd55ef --- /dev/null +++ b/research/gaussian-nonlinear-copy-floor/test_package.py @@ -0,0 +1,95 @@ +#!/usr/bin/env python3 +"""Focused admission/provenance controls; Python 3.10+, standard library.""" +import copy +import importlib.util +import json +import shutil +import subprocess +import sys +import tempfile +import unittest +from pathlib import Path + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location('nonlinear_floor_driver', HERE / 'verify.py') +verify = importlib.util.module_from_spec(spec) +spec.loader.exec_module(verify) + + +class PackageChecks(unittest.TestCase): + def test_demands_and_concentration(self): + verify.check_sources() + geometry, _ = verify.load_vendor() + cliques = geometry.maximal_cliques(geometry.nonorthogonality(geometry.gaussian_lines())) + for size in (7, 8, 10, 11, 12): + q = next(c for c in cliques if c.bit_count() == size) + demand = [3 * ((q >> i) & 1) for i in range(60)] + self.assertEqual(verify.demand_floor(demand, cliques), 3 * size) + self.assertEqual(verify.demand_floor([0] * 60, cliques), 0) + self.assertEqual(verify.demand_floor([2] * 60, cliques), 80) + for demand in ([1] * 59, [-1] + [0] * 59, [True] + [0] * 59, [0.5] + [0] * 59): + with self.assertRaises(ValueError): + verify.demand_floor(demand, cliques) + + def test_certificate_mutations(self): + actual = json.loads((HERE / 'CERTIFICATE.json').read_text()) + verify.compare_receipt(actual, copy.deepcopy(actual)) + for field in ('uniform_gaussian_floor_per_bit', 'demand_coefficient', 'concentrated_twelve_port_floor', 'assignment_seed'): + bad = copy.deepcopy(actual) + bad[field] = 'wrong' + with self.assertRaises(ValueError): + verify.compare_receipt(actual, bad) + bad = copy.deepcopy(actual) + bad['geometric_premise']['unordered_nonempty_flat_pairs'] -= 1 + with self.assertRaises(ValueError): + verify.compare_receipt(actual, bad) + + def test_relocated_source_corruption_and_optimization(self): + manifest = json.loads((HERE / 'SOURCES.json').read_text()) + with tempfile.TemporaryDirectory(prefix='gaussian nonlinear ') as tmp: + root = Path(tmp) + package = root / 'research' / HERE.name + shutil.copytree(HERE, package, ignore=shutil.ignore_patterns('__pycache__')) + for local in manifest['base_sources']: + target = root / local + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(verify.ROOT / local, target) + command = [sys.executable, '-I', '-B', str(package / 'verify.py'), '--check-sources'] + def run(): + return subprocess.run(command, cwd=tmp, text=True, capture_output=True) + result = run() + self.assertEqual(result.returncode, 0, result.stderr) + vendor = package / 'vendor/pr738/geometry.py' + saved = vendor.read_bytes() + vendor.write_bytes(saved + b'\n# mutation\n') + self.assertNotEqual(run().returncode, 0) + vendor.write_bytes(saved) + manifest_path = package / 'SOURCES.json' + saved_manifest = manifest_path.read_bytes() + bad_manifest = json.loads(saved_manifest) + del bad_manifest['vendor']['vendor/pr738/verify.py'] + manifest_path.write_text(json.dumps(bad_manifest)) + self.assertNotEqual(run().returncode, 0) + manifest_path.write_bytes(saved_manifest) + vendor.unlink() + self.assertNotEqual(run().returncode, 0) + vendor.write_bytes(saved) + selected = root / 'certificates/selected-result.json' + saved_selected = selected.read_bytes() + selected.write_bytes(saved_selected + b'\n') + self.assertNotEqual(run().returncode, 0) + selected.write_bytes(saved_selected) + result = subprocess.run([sys.executable, '-I', '-O', '-B', str(package / 'verify.py')], cwd=tmp, text=True, capture_output=True) + self.assertNotEqual(result.returncode, 0) + self.assertIn('optimized Python is unsupported', result.stderr) + sentinel = package / 'kept-output.json' + sentinel.write_text('existing receipt\n') + result = subprocess.run([sys.executable, '-I', '-B', str(package / 'verify.py'), + '--output', str(sentinel)], cwd=tmp, text=True, capture_output=True) + self.assertNotEqual(result.returncode, 0) + self.assertIn('output path already exists', result.stderr) + self.assertEqual(sentinel.read_text(), 'existing receipt\n') + + +if __name__ == '__main__': + unittest.main(verbosity=2) diff --git a/research/gaussian-nonlinear-copy-floor/vendor/pr738/PROOF.md b/research/gaussian-nonlinear-copy-floor/vendor/pr738/PROOF.md new file mode 100644 index 0000000000..748e632439 --- /dev/null +++ b/research/gaussian-nonlinear-copy-floor/vendor/pr738/PROOF.md @@ -0,0 +1,170 @@ +# Weighted clique certificate for scalar Gaussian decoders + +The exact certificate gives a copy-charge lower bound of **40 Gaussian rank +units**, or **80 rational rank units**, for every decoder in the class below. +It does not assert a new multiplication bound. + +Let V index the 60 Gaussian lines obtained from the E8 roots in Q^8 by the +complex structure J with J e_(2a) = e_(2a+1) and +J e_(2a+1) = -e_(2a), for a=0,...,3. For a line set S, let X_S be the +rational span of its representatives and their J-images. Write + + c(R,A) = rank_Q(V_R V_A^T) / 2, + +where V_S has rows spanning X_S. This is the Gaussian pairing rank, in +Gaussian rather than rational rank units. It is not the dimension of the +source span, and it is not the binary rank of a decoder submatrix. + +Consider any finite scalar-total binary factorization + + B = sum_j 1_(R_j) 1_(A_j)^T over F2, + +with B_tt=1 and B_ts=0 when distinct Gaussian lines t,s are nonorthogonal. +Reader/source supports may differ; orthogonal off-diagonal entries are free. +The abstract copy charge is C=sum_j c(R_j,A_j). + +## Certificate theorem + +Let K be any finite collection of pairwise nonorthogonal cliques. Assign +nonnegative rational weights lambda_Q to its cliques. Suppose that, for +every ordered pair of flats F,G of the Gaussian line matroid, + + sum_(Q in K) lambda_Q [Q meets F and Q meets G] <= c(F,G). (1) + +Then every fitting scalar-total factorization satisfies + + C >= sum_(Q in K) lambda_Q |Q|. (2) + +Proof: the fitting constraints force B[Q,Q]=I_|Q|. A rectangle restricted +to Q has binary rank one exactly when both supports meet Q, and has rank +zero otherwise. Binary rank subadditivity therefore gives + + |Q| <= sum_j [Q meets R_j and Q meets A_j]. + +Multiply by lambda_Q, sum over Q, and apply (1) to each term. The reduction +from arbitrary supports to flats in that last step is justified below. +There is no assumption on the binary rank of B, the number of totals, or +symmetry of the factorization. Zero-charge terms are allowed. + +## Why all flat pairs suffice + +Define cl(S)={t in V: X_{t} is contained in X_S}. This closure contains S +and spans exactly X_S. Consequently + + c(cl(R),cl(A)) = c(R,A). + +Each clique-hit indicator is nondecreasing when either support grows, so +its value on (R,A) is at most its value on (cl(R),cl(A)). Thus (1), checked +on all flat pairs, covers every one of the 2^60 by 2^60 support pairs. +This is a completeness argument, not an inference from sampled supports. + +All flats can be generated starting with the empty flat and adjoining one +line outside a previously generated flat, followed by exact closure. +Completeness follows by induction on rank: choose a line basis of any +nonempty flat, remove its last line, and use the lower-rank closure as its +parent. The rank is at most four, so this process terminates after rank +four. The verifier checks exact closure, Gaussian invariance, and that the +basis equals the canonical span of the stated lines. An independent Fraction +elimination checks fixed rank cases and the sharp witness's Gram matrix. + +For zero pairing rank the left side of (1) is automatically zero. If a +clique met both supports, a chosen reader/source pair would either be the +same nonzero line or two distinct nonorthogonal lines. Either choice has a +nonzero Gram block, contradicting zero pairing rank. + +## Uniform weights and their exact limitation + +For equal-size cliques of size q, let n=|K| and + + h(F,G) = number of cliques meeting both F and G; + rho = max_(c(F,G)>0) h(F,G)/c(F,G). + +The largest valid uniform weight is exactly 1/rho, and the resulting floor +is n*q/rho. An exhaustive exact maximum over flat pairs therefore certifies +both the bound and optimality within this uniform-weight method. A pair +attaining rho is a useful witness against every larger uniform weight. + +Here n=640, q=12, and rho=192. The committed certificate records all 2,272 +flats, including the empty flat, and all 2,579,856 unordered pairs of nonempty +flats. Symmetry of both the Gram rank and joint-hit count covers both orders. +Empty supports have zero charge and zero hits. + +For a pair with h>0 and flat ranks r,s, the proof above gives c>=1. +Sylvester's rank inequality on the real Gram product gives c>=r+s-4. +The verifier therefore accepts h<=192 max(1,r+s-4) directly. It computes +the exact rational Gram rank for every remaining pair. This partitions the +entire domain into 2,725 zero-hit pairs, 1,827,741 rank-bound pairs and +749,390 exact-rank pairs. No candidate is skipped on a numerical tolerance. + +With the lexicographic line numbering in `geometry.py`, the pair + + F = {0,1,2,11,12,45} + G = {0,3,4,5,6,7,8,9,10,54,55,56,57,58,59} + +has ranks 2 and 3, pairing rank 1, and joint-hit count 192. Thus 1/192 is +valid and is the largest uniform weight on these 640 cliques. Applying the +certificate theorem gives C>=640*12/192=40. The witness is also a concrete +reason that replacing pairing rank by a support's dimension would be invalid. +This sharpness concerns the certificate method; it does not exhibit a +cost-40 decoder. + +There is also a limitation independent of the computed maximum. Take both +supports to be the full ground set. Its cost is four and it meets every +nonempty clique, so every feasible system of nonnegative clique weights +must satisfy sum_Q lambda_Q <= 4. If the maximum nonorthogonal clique size +is 12, no such weighted-clique certificate can prove a floor larger than +48, even with nonuniform weights or with smaller cliques included. This is +a limitation of this certificate method, not an upper bound on the true +minimum copy charge. + +For comparison, every fitting B has an abstract decomposition of cost 60: +take one rectangle per row, with R={t} and A equal to that row's nonzero +support. Its Gram pairing has rank one because B_tt=1, while every other +possible nonzero entry in that row lies on a line orthogonal to t. This +upper bound does not establish a physical supplier or attainability without +additional expenses. + +## Conditional three-stage consequence + +Under the separate Dfc accounting of #595 and the Gaussian scaling argued +in #620, v=60 and each line has rational rank k=2. For T replicas and s +stages, the optimistic deficit therefore satisfies + + D/T = (s-1) v k - s cst <= 120(s-1) - 80s = 40s-120. + +At s=3 this is nonpositive. Under the same pressure identity with +nonnegative paid children and fallback cost, a positive supplier saving +requires positive deficit. Thus this three-stage Gaussian format cannot +give a positive saving, even before charging helper preparation, source +access, frame changes, restoration, or recursive children. Those required +costs cannot repair a nonpositive optimistic deficit. + +The bound allows positive deficit at s>=5. It does not decide the best +decoder cost, construct a complete supplier, or price the other supplier +and outer assembly. No kappa improvement follows. Changing stage accounting +or allowing sub-line/vector-valued operations is outside this consequence. + +## Provenance and scope + +The Gaussian object above is exactly the object in Joel Pulikkan / +GamingPuzzled's #620 `gauss_geom.py`: its J is also exactly the block-diagonal +`Li` in `algebra_lines.py: left_quat()`. Each rational Gaussian root line +contains its four roots r,Jr,-r,-Jr; changing representatives only permutes +the line indices and multiplies rows by invertible Gaussian scalars. + +The weighted-clique argument extends the method of Douglas R. Colkitt / +Mister-Meeseeks' concurrent PR #703, at commit +358383e2f1b0f292d4d6eb897c06fd8558a4f5e6. That work proves a sharp bound for +the ten Hurwitz lines using 32 orthogonal-pair transversals. Its numerical +Hurwitz bound is not imported here. + +The result concerns whole Gaussian-line supports, scalar binary totals and +the declared pairing-rank charge. It does not cover arbitrary rational +sub-line supports, vector-linear totals, modified fitting patterns, or +other geometries. Translating it into a supplier obstruction requires the +repository's separate frame and accounting assumptions. Finite exact replay +is not a proof-assistant formalization of the multiplication theorem. + +Prepared by Sagar Thakrar (@thakrarsagar) with substantial OpenAI Codex +assistance in the proof, implementation, review and documentation. +Apache-2.0, as specified by the repository license. diff --git a/research/gaussian-nonlinear-copy-floor/vendor/pr738/README.md b/research/gaussian-nonlinear-copy-floor/vendor/pr738/README.md new file mode 100644 index 0000000000..71fab92b57 --- /dev/null +++ b/research/gaussian-nonlinear-copy-floor/vendor/pr738/README.md @@ -0,0 +1,111 @@ +# Gaussian E8 copy floor from clique ranks + +**Research note and scoped negative result. No new kappa.** Every asymmetric +scalar binary decoder of the 60-line Gaussian E8 fitting pattern has abstract +copy charge at least **40 Gaussian rank units, or 80 rational rank units**. +This holds for arbitrarily many totals, with the pairing-rank cost of #446. +It does not assume symmetric decoding or full-rank totals. + +The [proof](PROOF.md) extends the averaged clique argument of concurrent +[#703](https://github.com/CrocSwap/integer-mult-bounds/pull/703) to the Gaussian +geometry posed in [#620](https://github.com/CrocSwap/integer-mult-bounds/pull/620). +All 640 maximum nonorthogonal cliques have size 12. Each receives weight +1/192. Exact flat-pair checks prove this weighting is valid, and a rank-one +pairing between a rank-two and a rank-three flat proves it is sharp for this +uniform weighting. The actual minimum decoder cost remains between 40 and 60. + +Under #595's separate deficit identity and #620's Gaussian rank scaling, + + D/T <= 120(s-1) - 80s = 40s-120. + +Thus the three-stage Gaussian format has no positive deficit even before +helper, access, frame, restoration and recursive expenses. This excludes that +specific route to a positive supplier saving. Five or more stages remain +unresolved. The previous notes report a symmetric CP-SAT lower bound of 9 and +a separately solver-reported fitting-matrix minrank of 15. Neither solver +claim is needed for this proof or replay. + +## Reproduce + +From the repository root, with Python 3.10 or later and no third-party packages: + +```sh +python3 -B research/gaussian-clique-copy-bound/verify.py +``` + +Expected output: + +```text +PASS_GAUSSIAN_CLIQUE_COPY_BOUND: cost >= 40 Gaussian / 80 rational; 2579856 flat pairs; 6 negative controls; kappa unchanged +``` + +The verifier reads the committed [certificate](certificate.json), verifies +the [source hashes](SOURCES.json), and recomputes the result without writing +files. Python optimization is explicitly rejected because the geometry code +uses assertions. A missing or modified source or certificate fails the run. + +The complete domain consists of 240 roots, 60 Gaussian lines and 2,272 flats. +Closure of supports preserves their pairing rank and can only increase +clique hits. This reduces every possible support pair to the finite flat +domain. Symmetry reduces it to 2,579,856 nonempty unordered pairs. The empty +flat is handled by the proof. Of these pairs, 2,725 have no joint hits; +1,827,741 satisfy the inequality by the exact dimension bound; and 749,390 +receive explicit rational Gram-rank calculations. This is a completed census, +with no randomized search or timeout stopping rule. + +Six rejection controls cover a too-large uniform weight, confusion between +Gaussian and rational units, a false clique, a duplicate clique, a missing +decoder diagonal, and a forbidden decoder entry. Positive controls accept +the identity decoder and an asymmetric edit at an orthogonal free entry, +including its cost-60 row decomposition. A separate Fraction elimination +checks arithmetic cases and the sharp witness's expanded Gram matrix. + +## Validation record + +On 2026-10-13, the command above passed on macOS 26.5.2 arm64 with Python +3.14.8 and 3.11.15. The second run used a temporary directory containing +only this package and the six pinned source files, with `/` as the working +directory. A changed source byte failed hash validation; `python3.11 -O` +failed explicitly. Changing the receipt's floor from 40 to 41 in memory +failed after a fresh complete replay. All six built-in negative controls +passed in the successful runs. + +`python3 -B scripts/verify_selected_result.py` also passed. A separate code +review checked the flat-pair argument, pruning inequality and source geometry. +As a development check, independent Fraction elimination agreed on 1,000 +integer matrices drawn with seed 46, with row-order and dependent-row checks. +That development sampling is separate from the exhaustive flat-pair census. + +The unchanged repository-wide `make verify` and selected construction's +expensive cold replay were not rerun. No Linux CI pass is claimed. This +package does not change their code, generators, certificates or inputs. + +## Scope and provenance + +Base commit: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. The selected accepted +certificate at that base has +`kappa=51110230636731/31250000000000000=0.001635527380375392`. +The [local sprint claim](CLAIM.md) records OS assignment seed 46, candidate +selection and coordination. The even seed chose Gaussian over Eisenstein +geometry. No pinned coordination issue existed. + +Joel Pulikkan / GamingPuzzled's #620 supplies the extension-ring question, +geometry and previous search results. Its retained head and exact source +hashes are recorded in `SOURCES.json`. DreamingOfClouds' #446/#595 supply the +pairing-rank accounting and conditional deficit framework. Douglas R. +Colkitt / Mister-Meeseeks' #703, pinned at +`358383e2f1b0f292d4d6eb897c06fd8558a4f5e6`, supplies the precursor weighted +clique argument for the different ten-line Hurwitz geometry. This package +imports no predecessor executable code and uses no SAT solver. + +The bound covers whole Gaussian-line supports, scalar binary totals and the +specified fitting pattern. It does not cover sub-line supports, vector-valued +totals, other geometries, or alternative stage accounting. It is not a formal +verification of the integer multiplication theorem. The selected construction +and its compiler, realization, hosting, precision, tape and analytic assumptions +are unchanged. This package changes only its own research directory. + +Prepared by **Sagar Thakrar (@thakrarsagar)** with substantial **OpenAI Codex +assistance** in proof development, implementation, verification and writing. +No independent human review is claimed. New material is licensed under the +repository's [Apache-2.0 license](../../LICENSE). diff --git a/research/gaussian-nonlinear-copy-floor/vendor/pr738/SOURCES.json b/research/gaussian-nonlinear-copy-floor/vendor/pr738/SOURCES.json new file mode 100644 index 0000000000..ca6f490c99 --- /dev/null +++ b/research/gaussian-nonlinear-copy-floor/vendor/pr738/SOURCES.json @@ -0,0 +1,30 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "selected_kappa": "51110230636731/31250000000000000", + "assignment_seed": 46, + "predecessors": { + "620": { + "author": "Joel Pulikkan / GamingPuzzled", + "retained_head": "419c7374c3bf5f2eee28f08b1e50c1d57934081c", + "open_head_at_start": "e9cf03bbdf7094b5a83f6dbd1d74bfd77a05fb87", + "role": "Gaussian E8 geometry, asymmetric fitting-decoder question, extension-ring accounting" + }, + "703": { + "author": "Douglas R. Colkitt / Mister-Meeseeks", + "head": "358383e2f1b0f292d4d6eb897c06fd8558a4f5e6", + "role": "Averaged clique-rank proof for the distinct Hurwitz E8 geometry; no code imported" + }, + "446/595": { + "author": "DreamingOfClouds", + "role": "Pairing-rank copy charge and conditional format accounting, retained at the pinned base" + } + }, + "sha256": { + "certificates/selected-result.json": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53", + "research/e8-decoder-floors-and-cold14-notes/s1-extension-rings/REPORT.md": "e8de809976a1253087e9058d346dfcc7b098f6481c64f1569aa3072d27345e02", + "research/e8-decoder-floors-and-cold14-notes/s1-extension-rings/algebra_lines.py": "bc4037049debf9b7affeb7e6b30da0193dea8c3850a7317afd045ac7ac481108", + "research/e8-decoder-floors-and-cold14-notes/s1-extension-rings/gauss_geom.py": "4750d252d87e4022e17fbfe0ac697d5d4c077a85541e217c4f206d39d5cfa2ae", + "research/format-limits/scripts/e8units.py": "3134443d8327d0bf2a8a66c26327cf5268cec6b7ffd85dde750b7e197ce63ef1", + "research/format-limits/README.md": "0fa0d6b2df96ddc06b876c41c5fa8d2335b97f36bc8f17d1371296d23199c263" + } +} diff --git a/research/gaussian-nonlinear-copy-floor/vendor/pr738/certificate.json b/research/gaussian-nonlinear-copy-floor/vendor/pr738/certificate.json new file mode 100644 index 0000000000..cacb07d8e7 --- /dev/null +++ b/research/gaussian-nonlinear-copy-floor/vendor/pr738/certificate.json @@ -0,0 +1,40 @@ +{ + "roots": 240, + "lines": 60, + "maximal_clique_sizes": {"7": 1920, "8": 1920, "10": 2304, "11": 1920, "12": 640}, + "maximum_clique_size": 12, + "maximum_cliques": 640, + "flat_census": { + "0": [{"lines": 0, "cliques_hit": 0, "count": 1}], + "1": [{"lines": 1, "cliques_hit": 128, "count": 60}], + "2": [ + {"lines": 2, "cliques_hit": 256, "count": 360}, + {"lines": 3, "cliques_hit": 308, "count": 320}, + {"lines": 6, "cliques_hit": 320, "count": 30} + ], + "3": [ + {"lines": 4, "cliques_hit": 436, "count": 960}, + {"lines": 6, "cliques_hit": 492, "count": 480}, + {"lines": 15, "cliques_hit": 512, "count": 60} + ], + "4": [{"lines": 60, "cliques_hit": 640, "count": 1}] + }, + "nonempty_flats": 2271, + "unordered_nonempty_flat_pairs": 2579856, + "zero_joint_hit_pairs": 2725, + "rank_bound_pairs": 1827741, + "exact_pairing_rank_pairs": 749390, + "uniform_coefficient": 192, + "gaussian_copy_floor": 40, + "rational_copy_floor": 80, + "abstract_row_upper_bound": 60, + "deficit_upper_bound": {"slope": 40, "intercept": -120}, + "sharp_witness": { + "F": [0, 1, 2, 11, 12, 45], + "G": [0, 3, 4, 5, 6, 7, 8, 9, 10, 54, 55, 56, 57, 58, 59], + "ranks": [2, 3], + "pairing_rank": 1, + "joint_hits": 192 + }, + "negative_controls": 6 +} diff --git a/research/gaussian-nonlinear-copy-floor/vendor/pr738/geometry.py b/research/gaussian-nonlinear-copy-floor/vendor/pr738/geometry.py new file mode 100644 index 0000000000..150762c764 --- /dev/null +++ b/research/gaussian-nonlinear-copy-floor/vendor/pr738/geometry.py @@ -0,0 +1,215 @@ +"""Exact Gaussian E8 geometry, using only Python's standard library. + +Coordinates are doubled E8 roots. A Gaussian line is the rational real plane +spanned by r and J(r); a Gaussian flat's real dimension is twice its rank. +""" + +from collections import Counter +from fractions import Fraction +from functools import reduce +from itertools import combinations, product +from math import gcd + + +def doubled_roots(): + roots = set() + for i, j in combinations(range(8), 2): + for a, b in product((-2, 2), repeat=2): + root = [0] * 8 + root[i], root[j] = a, b + roots.add(tuple(root)) + roots.update(signs for signs in product((-1, 1), repeat=8) + if sum(x < 0 for x in signs) % 2 == 0) + return tuple(sorted(roots)) + + +def J(row): + return tuple(x for i in range(0, 8, 2) for x in (-row[i + 1], row[i])) + + +def dot(left, right): + return sum(a * b for a, b in zip(left, right)) + + +def gaussian_lines(): + roots = doubled_roots() + root_set = set(roots) + assert len(roots) == 240 + assert all(dot(r, r) == 8 and J(r) in root_set for r in roots) + assert all(J(J(r)) == tuple(-x for x in r) for r in roots) + orbits = {min(r, J(r), tuple(-x for x in r), + tuple(-x for x in J(r))) for r in roots} + assert len(orbits) == 60 + return tuple(sorted(orbits)) + + +def bits(mask): + while mask: + bit = mask & -mask + yield bit.bit_length() - 1 + mask ^= bit + + +def nonorthogonality(lines): + return tuple(sum(1 << j for j, right in enumerate(lines) + if i != j and (dot(left, right) or dot(left, J(right)))) + for i, left in enumerate(lines)) + + +def maximal_cliques(adjacency): + """Exhaustive pivoted Bron--Kerbosch, returning vertex bitmasks.""" + found = [] + + def visit(clique, possible, excluded): + if not (possible | excluded): + found.append(clique) + return + pivot = max(bits(possible | excluded), + key=lambda i: (possible & adjacency[i]).bit_count()) + candidates = possible & ~adjacency[pivot] + for vertex in bits(candidates): + bit = 1 << vertex + visit(clique | bit, possible & adjacency[vertex], + excluded & adjacency[vertex]) + possible &= ~bit + excluded |= bit + + visit(0, (1 << len(adjacency)) - 1, 0) + return tuple(sorted(found)) + + +def primitive(row): + divisor = reduce(gcd, row, 0) + if not divisor: + return tuple(row) + if next(x for x in row if x) < 0: + divisor = -divisor + return tuple(x // divisor for x in row) + + +def remainder(row, basis): + row = tuple(row) + for old in basis: + pivot = next(i for i, x in enumerate(old) if x) + if row[pivot]: + row = primitive(tuple(old[pivot] * x - row[pivot] * y + for x, y in zip(row, old))) + return row + + +def canonical_basis(rows): + """Canonical rational row space via primitive integer elimination.""" + basis = [] + for row in rows: + row = primitive(remainder(row, basis)) + if not any(row): + continue + pivot = next(i for i, x in enumerate(row) if x) + basis = [primitive(tuple(row[pivot] * x - old[pivot] * y + for x, y in zip(old, row))) + if old[pivot] else old for old in basis] + basis.append(row) + basis.sort(key=lambda old: next(i for i, x in enumerate(old) if x)) + return tuple(basis) + + +def gaussian_flats(lines): + """All root-generated Gaussian flats, grouped by rank. + + Each item is (line_mask, canonical_real_basis). Extending every rank-r + flat by every line outside it exhausts the rank-(r+1) flats. + """ + levels = {0: ((0, ()),)} + for rank in range(1, 4): + spaces = set() + for mask, basis in levels[rank - 1]: + for i, line in enumerate(lines): + if not (mask >> i) & 1: + spaces.add(canonical_basis((*basis, line, J(line)))) + flats = [] + for basis in spaces: + assert len(basis) == 2 * rank + mask = sum(1 << i for i, line in enumerate(lines) + if not any(remainder(line, basis))) + flats.append((mask, basis)) + assert len({mask for mask, _ in flats}) == len(flats) + levels[rank] = tuple(sorted(flats)) + full_basis = canonical_basis(lines) + assert len(full_basis) == 8 + levels[4] = (((1 << len(lines)) - 1, full_basis),) + return levels + + +def clique_hits(flat_mask, cliques): + return sum(1 << i for i, clique in enumerate(cliques) if flat_mask & clique) + + +def pairing_rank(left_basis, right_basis): + """Gaussian rank of the Hermitian pairing between two Gaussian flats.""" + real_rank = len(canonical_basis(tuple(dot(left, right) for right in right_basis) + for left in left_basis)) + assert real_rank % 2 == 0 + return real_rank // 2 + + +def self_check(): + """Cross-check integer elimination and the sharp witness independently.""" + def fraction_rank(rows): + rows = [list(map(Fraction, row)) for row in rows] + rank = 0 + for column in range(len(rows[0]) if rows else 0): + pivot = next((i for i in range(rank, len(rows)) + if rows[i][column]), None) + if pivot is None: + continue + rows[rank], rows[pivot] = rows[pivot], rows[rank] + divisor = rows[rank][column] + rows[rank] = [value / divisor for value in rows[rank]] + for i in range(rank + 1, len(rows)): + scale = rows[i][column] + rows[i] = [x - scale * y for x, y in zip(rows[i], rows[rank])] + rank += 1 + return rank + + cases = ( + ((), 0), + (((0, 0, 0),), 0), + (((2, 4, 6), (3, 6, 9)), 1), + (((1, 1), (1, -1)), 2), + (((1, 0, 1), (0, 1, 1), (1, 1, 0)), 3), + ) + for rows, expected in cases: + basis = canonical_basis(rows) + assert len(basis) == fraction_rank(rows) == expected + assert canonical_basis(reversed(rows)) == basis + assert canonical_basis((*rows, *rows)) == basis + + lines = gaussian_lines() + left = (0, 1, 2, 11, 12, 45) + right = (0, 3, 4, 5, 6, 7, 8, 9, 10, 54, 55, 56, 57, 58, 59) + left_rows = tuple(row for i in left for row in (lines[i], J(lines[i]))) + right_rows = tuple(row for i in right for row in (lines[i], J(lines[i]))) + gram = tuple(tuple(dot(a, b) for b in right_rows) for a in left_rows) + assert fraction_rank(left_rows) == 4 + assert fraction_rank(right_rows) == 6 + assert fraction_rank(gram) == 2 + assert pairing_rank(canonical_basis(left_rows), canonical_basis(right_rows)) == 1 + + +if __name__ == "__main__": + self_check() + lines = gaussian_lines() + graph = nonorthogonality(lines) + cliques = maximal_cliques(graph) + maximum = max(clique.bit_count() for clique in cliques) + maximum_cliques = tuple(c for c in cliques if c.bit_count() == maximum) + assert len(cliques) == len(set(cliques)) + assert all(all((clique ^ (1 << i)) & ~graph[i] == 0 for i in bits(clique)) + for clique in cliques) + print("roots", len(doubled_roots()), "lines", len(lines)) + print("nonorthogonal degrees", dict(Counter(mask.bit_count() for mask in graph))) + print("maximal clique size census", dict(sorted(Counter(c.bit_count() for c in cliques).items()))) + for rank, flats in gaussian_flats(lines).items(): + census = Counter((mask.bit_count(), clique_hits(mask, maximum_cliques).bit_count()) + for mask, _ in flats) + print("rank", rank, "flats", len(flats), "(size, max-cliques-hit): multiplicity", dict(sorted(census.items()))) diff --git a/research/gaussian-nonlinear-copy-floor/vendor/pr738/verify.py b/research/gaussian-nonlinear-copy-floor/vendor/pr738/verify.py new file mode 100644 index 0000000000..71f0c21ecc --- /dev/null +++ b/research/gaussian-nonlinear-copy-floor/vendor/pr738/verify.py @@ -0,0 +1,180 @@ +#!/usr/bin/env python3 +"""Replay the Gaussian clique copy bound. Python 3.10+, standard library.""" + +import hashlib +import json +from collections import Counter +from pathlib import Path + +from geometry import (J, bits, canonical_basis, clique_hits, doubled_roots, + gaussian_flats, gaussian_lines, maximal_cliques, + nonorthogonality, pairing_rank, remainder, self_check) + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def check_sources(): + sources = json.loads((HERE / "SOURCES.json").read_text()) + for path, expected in sources["sha256"].items(): + actual = hashlib.sha256((ROOT / path).read_bytes()).hexdigest() + require(actual == expected, f"source hash mismatch: {path}") + selected = json.loads((ROOT / "certificates/selected-result.json").read_text()) + require(selected["kappa"] == sources["selected_kappa"], "selected kappa changed") + + +def check_cliques(cliques, graph): + require(len(cliques) == len(set(cliques)), "duplicate clique") + for clique in cliques: + require(clique > 0 and clique >> len(graph) == 0, "invalid clique vertices") + for vertex in bits(clique): + require((clique ^ (1 << vertex)) & ~graph[vertex] == 0, + "clique contains orthogonal lines") + + +def check_charge(hits, rank, coefficient=192): + require(hits <= coefficient * rank, "clique charge exceeds pairing rank") + + +def check_fitting(rows, graph): + require(len(rows) == len(graph), "wrong decoder dimension") + for i, row in enumerate(rows): + require(row >> len(rows) == 0 and row >= 0, "invalid decoder bits") + require((row >> i) & 1, "decoder diagonal is zero") + require(row & graph[i] == 0, "decoder violates nonorthogonal zero") + + +def rejected(function, *args): + try: + function(*args) + except ValueError: + return + raise ValueError(f"negative control was accepted: {function.__name__}") + + +def calculate(): + self_check() + lines = gaussian_lines() + graph = nonorthogonality(lines) + require(all(mask.bit_count() == 44 for mask in graph), "wrong Gaussian graph") + all_cliques = maximal_cliques(graph) + check_cliques(all_cliques, graph) + maximum = max(c.bit_count() for c in all_cliques) + cliques = tuple(c for c in all_cliques if c.bit_count() == maximum) + require(maximum == 12 and len(cliques) == 640, "wrong maximum-clique census") + flats = gaussian_flats(lines) + rows = [] + flat_census = {} + for rank, level in flats.items(): + census = Counter() + for mask, basis in level: + require(len(basis) == 2 * rank, "wrong flat rank") + generated = canonical_basis(v for i in bits(mask) + for v in (lines[i], J(lines[i]))) + require(generated == basis, "flat basis does not match its lines") + require(all(not any(remainder(J(v), basis)) for v in basis), + "flat is not Gaussian") + closure = sum(1 << i for i, line in enumerate(lines) + if not any(remainder(line, basis))) + require(closure == mask, "flat is not closed") + hits = clique_hits(mask, cliques) + census[(mask.bit_count(), hits.bit_count())] += 1 + if rank: + rows.append((rank, mask, basis, hits)) + flat_census[str(rank)] = [ + {"lines": size, "cliques_hit": hits, "count": count} + for (size, hits), count in sorted(census.items())] + + exact = pruned = zero = pairs = 0 + for i, (rank_f, _, basis_f, hits_f) in enumerate(rows): + for rank_g, _, basis_g, hits_g in rows[i:]: + pairs += 1 + hits = (hits_f & hits_g).bit_count() + if not hits: + zero += 1 + continue + # A joint-hit clique gives a nonzero pairing; Sylvester gives r+s-4. + lower_rank = max(1, rank_f + rank_g - 4) + if hits <= 192 * lower_rank: + pruned += 1 + continue + rank = pairing_rank(basis_f, basis_g) + exact += 1 + check_charge(hits, rank) + + witness_f = [0, 1, 2, 11, 12, 45] + witness_g = [0, 3, 4, 5, 6, 7, 8, 9, 10, 54, 55, 56, 57, 58, 59] + masks = [sum(1 << i for i in indices) for indices in (witness_f, witness_g)] + by_mask = {mask: (rank, basis, hits) for rank, mask, basis, hits in rows} + rf, bf, hf = by_mask[masks[0]] + rg, bg, hg = by_mask[masks[1]] + beta, hits = pairing_rank(bf, bg), (hf & hg).bit_count() + require((rf, rg, beta, hits) == (2, 3, 1, 192), "sharp witness changed") + require(pairing_rank(bg, bf) == beta, "pairing symmetry failed") + require(pairs == len(rows) * (len(rows) + 1) // 2, "incomplete pair coverage") + require(pairs == exact + pruned + zero, "pair accounting mismatch") + weighted_clique_size = len(cliques) * maximum + require(weighted_clique_size % 192 == 0, "nonintegral bound") + gaussian_floor = weighted_clique_size // 192 + rational_floor = 2 * gaussian_floor + deficit_slope = 2 * len(lines) - rational_floor + require(3 * deficit_slope - 2 * len(lines) == 0, "three-stage budget changed") + + # Positive controls: row totals realize I and an asymmetric free-entry edit. + identity = [1 << i for i in range(60)] + check_fitting(identity, graph) + free = next(j for j in range(1, 60) if not (graph[0] >> j) & 1) + asymmetric = identity.copy() + asymmetric[0] |= 1 << free + check_fitting(asymmetric, graph) + row_cost = sum(pairing_rank(canonical_basis((lines[i], J(lines[i]))), + canonical_basis(v for j in bits(row) + for v in (lines[j], J(lines[j])))) + for i, row in enumerate(asymmetric)) + require(row_cost == 60, "row-decomposition upper bound failed") + + # Each control changes a proof-relevant condition. + rejected(check_charge, hits, beta, 191) + rejected(check_charge, hits, beta, 96) # confusing rational and Gaussian units + rejected(check_cliques, (1 | (1 << free),), graph) + rejected(check_cliques, (cliques[0], cliques[0]), graph) + rejected(check_fitting, [0] * 60, graph) + corrupted = identity.copy() + corrupted[0] |= 1 << next(bits(graph[0])) + rejected(check_fitting, corrupted, graph) + + return { + "roots": len(doubled_roots()), "lines": len(lines), + "maximal_clique_sizes": {str(k): v for k, v in + sorted(Counter(c.bit_count() for c in all_cliques).items())}, + "maximum_clique_size": maximum, "maximum_cliques": len(cliques), + "flat_census": flat_census, + "nonempty_flats": len(rows), "unordered_nonempty_flat_pairs": pairs, + "zero_joint_hit_pairs": zero, "rank_bound_pairs": pruned, + "exact_pairing_rank_pairs": exact, + "uniform_coefficient": 192, "gaussian_copy_floor": gaussian_floor, + "rational_copy_floor": rational_floor, "abstract_row_upper_bound": row_cost, + "deficit_upper_bound": {"slope": deficit_slope, "intercept": -2 * len(lines)}, + "sharp_witness": {"F": witness_f, "G": witness_g, + "ranks": [rf, rg], "pairing_rank": beta, "joint_hits": hits}, + "negative_controls": 6, + } + + +def main(): + require(__debug__, "optimized Python disables geometry assertions; run without -O") + check_sources() + result = calculate() + expected = json.loads((HERE / "certificate.json").read_text()) + require(result == expected, "certificate mismatch") + print("PASS_GAUSSIAN_CLIQUE_COPY_BOUND: cost >= 40 Gaussian / 80 rational; " + "2579856 flat pairs; 6 negative controls; kappa unchanged") + + +if __name__ == "__main__": + main() diff --git a/research/gaussian-nonlinear-copy-floor/verify.py b/research/gaussian-nonlinear-copy-floor/verify.py new file mode 100644 index 0000000000..2f74cd0558 --- /dev/null +++ b/research/gaussian-nonlinear-copy-floor/verify.py @@ -0,0 +1,136 @@ +#!/usr/bin/env python3 +"""Source-pinned Gaussian nonlinear message floor. Python 3.10+, stdlib.""" +import argparse +import hashlib +import importlib.util +import json +import sys +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def digest(data): + return hashlib.sha256(data).hexdigest() + + +def check_sources(): + sources = json.loads((HERE / 'SOURCES.json').read_text()) + require(sources['base_commit'] == 'f567884aeb8851b6e794af1184119a3bfbe1e631', 'base pin changed') + require(set(sources['vendor']) == {'vendor/pr738/' + name for name in + ('geometry.py', 'verify.py', 'certificate.json', 'PROOF.md', 'README.md', 'SOURCES.json')}, + 'vendor pin inventory changed') + require(set(sources['predecessors']) == {'785', '814'}, 'method pin inventory changed') + require(set(sources['base_sources']) == { + 'certificates/selected-result.json', 'docs/research/current-status.md', + 'docs/research/pr-ledger.md', 'docs/research/community-frontier799-review.md', + 'research/gauge44-frames-x/PROOF-NOTE-FRAMES-X4.md', + 'research/e8-decoder-floors-and-cold14-notes/s1-extension-rings/REPORT.md', + 'research/e8-decoder-floors-and-cold14-notes/s1-extension-rings/gauss_geom.py', + 'research/e8-decoder-floors-and-cold14-notes/s1-extension-rings/algebra_lines.py', + 'research/format-limits/README.md'}, 'base pin inventory changed') + for local, pin in sources['vendor'].items(): + require(digest((HERE / local).read_bytes()) == pin['sha256'], 'vendor source mismatch: ' + local) + for pin in sources['predecessors'].values(): + require(digest((HERE / pin['local_path']).read_bytes()) == pin['sha256'], 'predecessor source mismatch') + for local, pin in sources['base_sources'].items(): + require(digest((ROOT / local).read_bytes()) == pin['sha256'], 'base source mismatch: ' + local) + selected = json.loads((ROOT / 'certificates/selected-result.json').read_text()) + require(selected['kappa'] == sources['selected_kappa'], 'selected kappa changed') + return sources + + +def load_vendor(): + require(__debug__, 'retained PR738 geometry uses assertions; optimized Python is unsupported') + def load(name, path): + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + require(Path(module.__file__).resolve() == path.resolve(), 'unexpected module origin') + return module + geometry = load('geometry', HERE / 'vendor/pr738/geometry.py') + replay = load('gaussian_pr738_replay', HERE / 'vendor/pr738/verify.py') + return geometry, replay + + +def demand_floor(demands, cliques): + require(len(demands) == 60 and all(type(x) is int and x >= 0 for x in demands), 'invalid demand vector') + averaged = (2 * sum(demands) + 2) // 3 + concentrated = max(sum(demands[i] for i in range(60) if (q >> i) & 1) for q in cliques) + return max(averaged, concentrated) + + +def compare_receipt(actual, expected): + require(actual == expected, 'certificate mismatch') + + +def calculate(): + check_sources() + geometry, replay = load_vendor() + # Retained verifier's calculate() is called without its historical source/selected + # check. Our check_sources() binds the same geometry and the current base instead. + inherited = replay.calculate() + compare_receipt(inherited, json.loads((HERE / 'vendor/pr738/certificate.json').read_text())) + lines = geometry.gaussian_lines() + graph = geometry.nonorthogonality(lines) + all_cliques = geometry.maximal_cliques(graph) + cliques = tuple(q for q in all_cliques if q.bit_count() == 12) + incidences = [sum((q >> i) & 1 for q in cliques) for i in range(60)] + require(incidences == [128] * 60, 'unequal or incorrect clique incidence') + require(demand_floor([1] * 60, all_cliques) == 40, 'uniform floor changed') + concentrated = [(cliques[44] >> i) & 1 for i in range(60)] + require(demand_floor(concentrated, all_cliques) == 12, 'concentration floor changed') + rounded = [0] * 60 + rounded[44] = 1 + require(demand_floor(rounded, all_cliques) == 1, 'integer demand floor changed') + spec = importlib.util.spec_from_file_location('gaussian_nonlinear_controls', HERE / 'independent_controls.py') + controls = importlib.util.module_from_spec(spec) + spec.loader.exec_module(controls) + finite = controls.calculate(lines, graph, cliques) + deficits = {str(s): 40 * (s - 3) for s in (1, 2, 3, 5, 7)} + require(deficits['3'] == 0 and deficits['5'] > 0, 'optimistic stage screen changed') + return { + 'schema': 1, + 'base_commit': 'f567884aeb8851b6e794af1184119a3bfbe1e631', + 'assignment_seed': 44, + 'status': 'scoped negative result; no new kappa', + 'geometric_premise': inherited, + 'port_clique_incidences': incidences, + 'demand_coefficient': '2/3', + 'uniform_gaussian_floor_per_bit': 40, + 'uniform_rational_floor_per_bit': 80, + 'concentrated_twelve_port_floor': 12, + 'optimistic_deficit_per_bit': deficits, + 'finite_nonlinear_controls': finite, + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--check-sources', action='store_true', help='check only immutable inputs, not the theorem') + parser.add_argument('--output', type=Path, help='write a verified receipt to a NEW file') + args = parser.parse_args() + require(__debug__, 'retained PR738 geometry uses assertions; optimized Python is unsupported') + if args.output: + require(not args.output.exists(), 'output path already exists') + if args.check_sources: + check_sources() + print('PASS_GAUSSIAN_NONLINEAR_SOURCES_ONLY') + return + actual = calculate() + compare_receipt(actual, json.loads((HERE / 'CERTIFICATE.json').read_text())) + if args.output: + with args.output.open('x') as out: + out.write(json.dumps(actual, indent=2, sort_keys=True) + '\n') + print('PASS_GAUSSIAN_NONLINEAR_COPY_FLOOR lines=60 cliques=640 flat_pairs=2579856 floor=40b no_new_kappa') + + +if __name__ == '__main__': + main()