From c63fbb875847399aca6af03992c2305f01852f79 Mon Sep 17 00:00:00 2001 From: ywz65 <154373401+ywz65@users.noreply.github.com> Date: Thu, 15 Oct 2026 09:39:13 -0700 Subject: [PATCH 1/2] Bound the expected Gaussian cost of adaptive public routing --- .../gaussian-adaptive-header-tax/PROOF.md | 102 +++++++ .../gaussian-adaptive-header-tax/README.md | 120 ++++++++ .../gaussian-adaptive-header-tax/RESULT.json | 184 +++++++++++ .../gaussian-adaptive-header-tax/SOURCES.json | 54 ++++ .../gaussian-adaptive-header-tax/TASK.json | 86 ++++++ .../VALIDATION.md | 44 +++ .../gaussian-adaptive-header-tax/VERIFY.json | 25 ++ .../geometry_check.py | 24 ++ .../gaussian-adaptive-header-tax/verify.py | 287 ++++++++++++++++++ 9 files changed, 926 insertions(+) create mode 100644 research/gaussian-adaptive-header-tax/PROOF.md create mode 100644 research/gaussian-adaptive-header-tax/README.md create mode 100644 research/gaussian-adaptive-header-tax/RESULT.json create mode 100644 research/gaussian-adaptive-header-tax/SOURCES.json create mode 100644 research/gaussian-adaptive-header-tax/TASK.json create mode 100644 research/gaussian-adaptive-header-tax/VALIDATION.md create mode 100644 research/gaussian-adaptive-header-tax/VERIFY.json create mode 100644 research/gaussian-adaptive-header-tax/geometry_check.py create mode 100644 research/gaussian-adaptive-header-tax/verify.py diff --git a/research/gaussian-adaptive-header-tax/PROOF.md b/research/gaussian-adaptive-header-tax/PROOF.md new file mode 100644 index 0000000000..317d8324c2 --- /dev/null +++ b/research/gaussian-adaptive-header-tax/PROOF.md @@ -0,0 +1,102 @@ +# Conditional transcripts with paid prefix codes + +Let the 60 ports be the Gaussian E8 lines of PR738. Each port t supplies an +independent uniform b_t-bit string X_t, with b_t a fixed nonnegative integer. +The receiver for t initially knows all X_u on lines orthogonal to t and does +not know X_t. Source and receiver roles are distinct. + +A central encoder, optimistically given all inputs, chooses M=h(X). Distinct +header values have distinct words in a finite prefix-free binary code. +Every receiver and every payload encoder receives M. Header bits are charged +the pairing rank of the **declared full source and full reader spans**, namely 4. +This full public-observation contract is a premise, not an inference that all +possible implementations of a header must cost 4 per bit. + +For each M=m there is a fixed finite ordered list of payloads. Payload j has +fixed supports A_j(m),R_j(m), codebook K_j(m), and value + + Y_j = f_j(m, X_(A_j(m))) in K_j(m). + +Every K_j(m) is a finite prefix-free set of binary strings, including the empty +word only for a singleton codebook. Each reader receives the entire codeword. +All choices of list, order, supports, functions and codebooks are determined +by m and carry no further input-dependent metadata. Payloads do not relay +previous payloads. Arbitrary nonlinear joint decoding is allowed and must +recover every demand on every input. Declare + + c(R,A) = rank_Q(V_R V_A^transpose)/2, + C(X) = 4 length(M) + sum_j c(R_j(M),A_j(M)) length(Y_j). + +The bases V span representatives and their J-images. Additive per-bit pricing +and this geometry are explicit assumptions; encoding and decoding are free. + +PR738 supplies 640 nonorthogonal cliques Q of size 12, each weight 1/192. Each +port lies in 128 cliques. For every support pair, + + sum_Q [Q meets R and A]/192 <= c(R,A). (G) + +The full geometry replay covers all 2,579,856 nonempty flat pairs. Closing a +support preserves its pairing rank and only increases clique intersections, +so (G) covers arbitrary supports. For any individual nonorthogonal clique, +meeting both supports implies c(R,A)>=1: choose one line in each intersection; +their pairing is nonzero. These are retained geometric facts, not new results. + +Fix any such Q and fix X outside Q. Given m, retain only payloads with both +supports meeting Q, in their m-determined order; call their tuple Z_Q. Then +(M,Z_Q) determines X_Q. Any omitted payload received by Q has sources disjoint +from Q and can be recomputed from m and the fixed outside inputs. All free +orthogonal side information is outside Q. Equal retained transcripts would +therefore give equal complete decoder inputs at every receiver in Q, forcing +equal X_Q. This does not assume linearity or conditional independence after M. + +For every fixed m and outside assignment, each retained payload distribution +is supported on a subset of its declared prefix-free codebook. Thus + + H(Y_j | M=m, X_outside=u) <= E[length(Y_j) | m,u]. + +Indeed, Kraft K=sum_y 2^-length(y)<=1 and q_y=2^-length(y)/K give, by +nonnegativity of relative entropy, H(Y)<=E[length(Y)]+log2 K<=E[length(Y)]. +Zero-probability codewords do not matter. This also proves H(M)<=E[length(M)]. +Apply entropy subadditivity within each fixed branch, then average: + + B_Q = sum_(t in Q) b_t + <= H(M | X_outside) + + E[sum_j length(Y_j) [Q meets R_j(M) and A_j(M)]]. (1) + +All variables have finite alphabets. Expectations use the original uniform +independent inputs. The payload count can vary between branches because the +branch is conditioned on before the sum. + +Put B=sum_t b_t, L=E[length(M)], H=H(M), and P=C-4 length(M). +Multiply (1) by 1/192 and sum the 640 cliques. Use 128 incidences per port, +H(M|X_outside)<=H, and (G) on each realized branch with nonnegative lengths: + + (2/3)B <= (10/3)H + E[P]. + +Consequently + + E[C] >= (2/3)B + 4L -(10/3)H + >= (2/3)(B+L). (2) + +For any one nonorthogonal clique, rank>=1 instead gives B_Q<=H+E[P], hence + + E[C] >= B_Q+4L-H >= B_Q+3L. (3) + +Both (2) and (3) hold, so their maximum may be used. No integrality ceiling +follows merely because realized charges are integral. A constant header with +positive length has H=0, so the sharper entropy forms charge its full 4L; +an empty constant header gives L=H=0. A nonconstant prefix-free code has L>0 +and incurs the strictly positive 2L/3 penalty. The theorem bounds the average, +and therefore the maximum cost; it does not bound each individual execution. + +For uniform b-bit demands B=60b, charge is at least 40b+2L/3. Only with the +separate Dfc stage equation and a worst-case rational copy allowance at least +2 max_X C(X) does this give + + D/T <= (s-1)120b -2s(40b+2L/3) + = 40b(s-3) -(4s/3)L. + +No physical realization or all-size implication follows from this entropy +argument. The geometry and conditional-transcript/paid-header methods retain +their credit. New coverage is the Gaussian header gap and conditional +prefix-free payloads. diff --git a/research/gaussian-adaptive-header-tax/README.md b/research/gaussian-adaptive-header-tax/README.md new file mode 100644 index 0000000000..4236d999ff --- /dev/null +++ b/research/gaussian-adaptive-header-tax/README.md @@ -0,0 +1,120 @@ +# A public routing header pays a Gaussian copy-cost penalty + +The fixed-support nonlinear Gaussian bound in [PR888](https://github.com/CrocSwap/integer-mult-bounds/pull/888) +explicitly excludes adaptive supports and variable-length messages. We extend +its observation model to a paid public prefix-free header which selects the +payload supports and their prefix-free codes. Payload encoders and receivers +may be nonlinear. This is an expected-cost theorem under uniform independent +input demands, not a pointwise bound or a native supplier. + +Write B = sum b_t, L = E[length of header], and H = entropy of the header. +Charge a header bit four Gaussian units (the full-space pairing rank), and +each payload bit its declared source/reader pairing rank. Then + + E[C] >= (2/3)B + 4L - (10/3)H >= (2/3)(B + L). + +For every nonorthogonal clique Q there is also a concentration inequality: + + E[C] >= sum_(t in Q) b_t + 4L - H + >= sum_(t in Q) b_t + 3L. + +Equal b-bit demands retain the floor 40b and incur at least 2L/3 extra Gaussian +units when a nonempty public routing code is used. The entropy form charges +a useless constant header its full 4L. An empty constant header recovers the +existing bound. Expected charges need not be integers: no ceiling is applied. + +The distinction from Jerry Chen's Hurwitz adaptive-routing argument is the +Gaussian geometry's strict gap: total weighted-clique weight 10/3 is less than +the full-space header rank 4. The entropy method is credited, not claimed new. +Variable prefix-free payloads are admitted as well as variable headers. The +precise model and all-width proof are in [PROOF.md](PROOF.md). + +## Reproduce + +Python3.12, standard library, from the repository root: + +``` +python3.12 -I -O -B research/gaussian-adaptive-header-tax/verify.py +python3.12 -B scripts/research_package.py --package research/gaussian-adaptive-header-tax +``` + +The replay checks exact SHA256/Git-blob source pins, runs PR738's unchanged +full geometry calculation in a separate assertion-enabled process, compares +its complete receipt, and checks all 640 weighted clique incidences. The child +ignores inherited PYTHONOPTIMIZE. No historical selected-result entry point +is used. The new actual-geometry fixture has 12 active independent bits, a +nonlinear AND header, adaptive payload supports and a variable-length prefix +payload. All 4096 inputs decode for all 12 receivers; every weighted clique's +conditional transcript injection is checked. + +Separate rational elimination checks the fixture's source/reader prices. +Controls reject omitted payloads, undeclared sources, illegal side information, +uncharged headers and non-prefix payloads. The last is an actually decoded +orthogonal-frame parity using an empty/one-bit code: apparent expected cost 2 +violates the 8/3 floor because termination is free. A valid variable header +costs 4 on the all-zero input, below expected floor 8, preventing a false +pointwise conclusion. These finite examples corroborate the written argument; +they do not prove the entropy theorem by enumeration. + +Default replay is read-only and offline. `--write NEW.json` writes the verified +receipt exclusively to a new file. The registered input list is the complete +external replay closure. Source or receipt changes need explicit review. + +## Limits and selection + +The rank 4 tariff requires the header's declared source and reader spans to be +the full four-dimensional Gaussian space. Localized or private headers have +a different contract. Additive per-bit pairing pricing remains an explicit +premise, not a physical cost theorem for arbitrary nonlinear circuits. Every +input-dependent choice of payload count, order, supports or codebooks must +come from the paid header. Payloads do not relay other payloads. Correlated +inputs, errors, uncharged termination, private routing, interactive relays, +sub-line operations and changed physical pricing are outside scope. + +Only with the additional inherited Gaussian Dfc stage identity does the +worst-case budget imply D/T <=40b(s-3) -(4s/3)L. A nonempty header therefore +makes the favorable three-stage screen strictly negative. This conditional +screen is not a completed construction or exponent improvement. No hosting, +all-size compilation, precision or whole multiplication theorem is admitted. + +Fresh base 0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2, priority 4, picker +822a27d6015294b31b90467ba9f189a5 selected complex mechanisms. The prescribed +P104 binding and complex-ceiling commands passed before this changed +helper-observation scope. P104 correction work was reserved by another worker. +The original ceiling is not applied to this different geometry. TASK.json +records the detour. The selected record is unchanged. + +## Open next questions + +Can localized paid headers beat this public-header penalty while preserving +a valid weighted transcript bound? Start with a single header whose source +and reader spans have rank below 4, and include every dependency of the payload +schedule. Receivers cannot obtain private schedule information for free. +The Gaussian nonlinear optimum between 40b and60b also remains open; this +result supplies no attaining 40b construction. + +## Credit + +Sagar Thakrar's PR738 supplies the Gaussian geometry and full flat-pair +certificate; ToikY's PR888 supplies its nonlinear transcript composition. +Alexander Templeton's PR785 and Michael Fischler's PR814 supply the underlying +conditional transcript method. Jerry Chen's Hurwitz adaptive-routing proof +supplies the paid-header entropy argument. Joel Pulikkan, Douglas Colkitt, +DreamingOfClouds and the retained lineage keep their original credit. +PR2607's adaptive affine Eisenstein theorem is distinct: these payload queries +may be nonlinear and use Gaussian costs. + +Prepared by ywz65 with substantial OpenAI Codex assistance in proof, code, +verification and writing. Apache-2.0; no independent human review or proof +assistant verification is claimed. + +## Revision5 expansion decision + +Before submission, main advanced to b4560d9e7216f72b73c5aa940ac099c05e33ccf9. +The changed guidance and family record were read and the branch fast-forwarded; +scientific inputs retain their unchanged historical pins. Decision: narrow and +finish this interface obstruction, without a dependent implementation campaign. +The bound rules out public adaptive routing as a repair of this stated +three-stage budget even when all other nonnegative costs are omitted. Native +tariff realization, consumer/hosting and restoration remain unknown; favorable +local examples do not admit a complete supplier. diff --git a/research/gaussian-adaptive-header-tax/RESULT.json b/research/gaussian-adaptive-header-tax/RESULT.json new file mode 100644 index 0000000000..8dcd3e660e --- /dev/null +++ b/research/gaussian-adaptive-header-tax/RESULT.json @@ -0,0 +1,184 @@ +{ + "adaptive_fixture": { + "average_cost": "13", + "conditional_checks": 2621440, + "cost_histogram": { + "12": 1024, + "16": 2048, + "8": 1024 + }, + "header_counts": { + "0": 3072, + "1": 1024 + }, + "header_length": "1", + "inputs": 4096, + "payload_codebooks": { + "(0, 0)": [ + "0", + "10", + "11" + ], + "(0, 1)": [ + "0", + "1" + ], + "(1, 0)": [ + "0", + "1" + ] + }, + "receiver_checks": 49152, + "tax_floor": "26/3", + "transcript_sha256": "bfb4a792b1682b0ba0c5404f24db4a1c8d0ccc6c09ed3a131b31f7d423ab9f96" + }, + "controls": 6, + "frames": [ + [ + 0, + 45, + 54, + 59 + ], + [ + 1, + 12, + 55, + 58 + ], + [ + 2, + 11, + 56, + 57 + ] + ], + "full_header_price": 4, + "header_tax": "2/3", + "incidence_per_port": 128, + "pointwise_boundary_mean": "13309/256", + "pointwise_boundary_minimum": 4, + "retained_geometry": { + "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 + }, + "schema": 1, + "sources_sha256": "d3828baa26d79497fe131e8074ddff72e4a60895148313e7fe5e5d65f474a230", + "status": "scoped expected-cost theorem; no supplier or kappa", + "unpaid_termination_cost": "2", + "unpaid_termination_floor": "8/3", + "weighted_cliques": 640 +} diff --git a/research/gaussian-adaptive-header-tax/SOURCES.json b/research/gaussian-adaptive-header-tax/SOURCES.json new file mode 100644 index 0000000000..45b43d8b40 --- /dev/null +++ b/research/gaussian-adaptive-header-tax/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "research/gaussian-clique-copy-bound/PROOF.md", + "usage": "input", + "git_blob": "748e6324394d53cf910836eb55e28578d8bc684a", + "sha256": "e33a3950f172bc93400fffd85df55236059f5391d4ed8a82e0f12bcd7f196812" + }, + { + "path": "research/gaussian-clique-copy-bound/certificate.json", + "usage": "input", + "git_blob": "cacb07d8e71177175c0702e5f455cc986dce5d42", + "sha256": "c50858aaab863b34c7533211ca07ae038ee000328bd5134b73219992ae078875" + }, + { + "path": "research/gaussian-clique-copy-bound/geometry.py", + "usage": "input", + "git_blob": "150762c7643a0ab5463a2b447d0541a32d7701fe", + "sha256": "4a3e2cee2e35ccebde346e63fd9869ed48b2d59de120f570650ecb9c8875f5e4" + }, + { + "path": "research/gaussian-clique-copy-bound/verify.py", + "usage": "input", + "git_blob": "71f0c21ecc2e9b0da7d0b0d937ab6ac0fe952db6", + "sha256": "966c5181f6a2d0865ae9a4be90ecb2a04cad8ca3b8acfc328fbe24ceaf9a7c6c" + }, + { + "path": "research/gaussian-nonlinear-copy-floor/PROOF.md", + "usage": "input", + "git_blob": "576d1094915711c639e3d17572a9dec2cc2cc5ee", + "sha256": "6ad0216af94aa09f988c09c5dbe8aad2a7b82535f7781a58ed8564b35eca6a8a" + }, + { + "path": "research/hurwitz-adaptive-routing/PROOF.md", + "usage": "input", + "git_blob": "915a91663e8ae2eb96a2c248224a40ec052e6fda", + "sha256": "612d1723fd855503384943217b78f18a80adaca074196aa677b7124845d9e4d1" + } + ] +} diff --git a/research/gaussian-adaptive-header-tax/TASK.json b/research/gaussian-adaptive-header-tax/TASK.json new file mode 100644 index 0000000000..a4c4807d4e --- /dev/null +++ b/research/gaussian-adaptive-header-tax/TASK.json @@ -0,0 +1,86 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?", + "starting_points": [ + "research/complex-local-word-ceiling/README.md", + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json", + "research/selected-k8-unrestricted-ends/README.md" + ], + "methods": [ + "Propose a changed helper inventory and derive an optimistic exact moment.", + "Design a small completed instance and independently verify its endpoint and rank bill." + ], + "acceptance_gate": "A new physically realizable contract outside the frozen catalogue whose per-call profile, screened with ceiling.ceiling(), beats the selected word's packing ceiling; a lower cap does not establish identical circuitry or order attainable optima, and is insufficient to pass the stronger-budget target under this model.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin.", + "bottleneck_link": "Packing of the selected word is capped at +0.87% (ceiling model); only a lower local excess spend or a changed coverage law raises the cap.", + "allowed_variations": [ + "Narrow to one changed boundary or helper type with explicit counts.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Mixing only providers already inside the pinned catalogue.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013." + ], + "overlap_terms": [ + "helper inventory", + "heterogeneous-owner", + "mutable leaver" + ] + }, + "scope_status": "changed", + "actual_scope": "Expected Gaussian copy-cost penalty for a full-space paid public routing header selecting nonlinear prefix-free payloads", + "scope_change_reason": "P104 correction reserved by another worker; investigate explicitly excluded adaptive helper-observation contract rather than repeat scalar decoding floors.", + "bottleneck_link": "Side result: a paid adaptive public-routing interface cannot escape the Gaussian nonlinear40b floor under explicit additive pairing pricing; retained Dfc3-stage screen becomes strictly negative for a nonempty header.", + "budget_minutes": 60, + "stop_rule": "Prove the stated entropy bound, replay exact geometric premise and a nonlinear adaptive code with failure controls; stop before supplier construction.", + "outcome": "negative-result", + "evidence": "PROOF.md; verify.py; RESULT.json", + "author": "ywz65", + "ai_assistance": "Substantial OpenAI Codex assistance in proof, implementation, verification and writing.", + "open_questions": [ + { + "question": "Can localized paid headers improve the public-header penalty?", + "why_it_matters": "It changes the full-space tariff premise without assuming free routing metadata.", + "first_step": "State one lower-rank header source/reader contract and charge all payload schedule dependencies.", + "blocked_by": "A valid weighted conditional-transcript bound with private observations." + } + ], + "selection_seed": "822a27d6015294b31b90467ba9f189a5", + "first_steps": [ + "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "PASS_COMPLEX_LOCAL_WORD_CEILING" + ], + "claim": "https://github.com/CrocSwap/integer-mult-bounds/pull/888#issuecomment-6196956825", + "freshness": { + "submission_base": "b4560d9e7216f72b73c5aa940ac099c05e33ccf9", + "priority_revision": 5, + "action": "read changed guidance and family status; fast-forwarded branch; scientific source pins unchanged" + }, + "declared_milestone": "scoped local interface obstruction", + "family_decision": { + "decision": "narrow", + "ledger": { + "proved": "Explicit abstract expected copy-cost lower bound and actual finite model witnesses", + "constructive_upper_bound": "Direct fixed-support messages cost60b; illustrative adaptive code costs13 for12activebits", + "unknown": "Native realization of additive tariff, hosting, restoration, all-size consumer; not counted as zero in any feasibility claim" + }, + "decision_changed": "Nonempty full-space public routing cannot repair the favorable three-stage Gaussian Dfc deficit even with other nonnegative costs omitted.", + "stop_rule": "Finish this changed-prefix/adaptive premise; no dependent construction or finer obstruction campaign." + } +} diff --git a/research/gaussian-adaptive-header-tax/VALIDATION.md b/research/gaussian-adaptive-header-tax/VALIDATION.md new file mode 100644 index 0000000000..6d3607f963 --- /dev/null +++ b/research/gaussian-adaptive-header-tax/VALIDATION.md @@ -0,0 +1,44 @@ +# Validation and coverage + +Executed on Windows, 2026-10-15: + +- Python 3.12.14 `-I -O -B verify.py --write RESULT.json`: full unchanged + PR738 geometry plus new finite controls passed and produced the receipt. +- Python 3.12.14 registered package replay: passed. The first metadata attempt + rejected an unsupported outcome spelling; it was corrected to the schema's + `negative-result` before the successful scientific replay. +- Python 3.14.5 `-I -O -B verify.py` in a Git-free export containing only this + package and its six declared inputs: passed with inherited PYTHONOPTIMIZE=2. + The retained geometry still ran in an assertion-enabled child. Every file's + SHA256 before/after matched, establishing read-only behavior for this run. +- The relocated entry point rejected a modified input source, an existing + `--write` destination and an unknown option. Six scientific controls are + recorded in RESULT.json and rerun by the default command. +- A separate Codex agent reviewed the full proof, including conditioning on + the branch, varying payload counts, the full-span tariff, both entropy bounds + and the expected/worst-case distinction; no remaining issue was reported. + +The retained geometry check covers 2,579,856 unordered nonempty flat pairs. +New checks cover 4,096 adaptive inputs, 49,152 receiver observations and +2,621,440 conditional clique projections. The average illustrative invoice is +13, with realized costs 8, 12 and 16; the proved simplified floor is 26/3. +Finite examples do not replace the written all-width entropy proof. No hosted +CI, independent human review, native supplier or full selected cold replay is +claimed. + +Initial source/selection base was0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2. +Before submission canonical main advanced to +b4560d9e7216f72b73c5aa940ac099c05e33ccf9, priority5. All changed guidance, +including the family expansion gate, was read. The branch was fast-forwarded; +the six scientific input blobs did not change. The contribution diff uses +b4560d9e as its base; SOURCES.json preserves historical scientific pins. + +Overlap used the fully paginated 817-open-PR snapshot at16:31:22 UTC and the +1,239-Discussion-record snapshot at15:22:22 UTC, plus a fresh REST page of the +newest100 open PRs before submission. The Gaussian nonlinear fixed-support, +Hurwitz paid-header and PR2607 adaptive affine Eisenstein scopes were read. +No matching Gaussian prefix-payload/header-tax result was located. Discussion +freshness is bounded, and metadata search is not a novelty guarantee. + +Claim and completion share the predecessor investigation: +https://github.com/CrocSwap/integer-mult-bounds/pull/888#issuecomment-6196956825 diff --git a/research/gaussian-adaptive-header-tax/VERIFY.json b/research/gaussian-adaptive-header-tax/VERIFY.json new file mode 100644 index 0000000000..fce67085f0 --- /dev/null +++ b/research/gaussian-adaptive-header-tax/VERIFY.json @@ -0,0 +1,25 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/gaussian-clique-copy-bound/PROOF.md", + "research/gaussian-clique-copy-bound/certificate.json", + "research/gaussian-clique-copy-bound/geometry.py", + "research/gaussian-clique-copy-bound/verify.py", + "research/gaussian-nonlinear-copy-floor/PROOF.md", + "research/hurwitz-adaptive-routing/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Full retained Gaussian geometry;4096 nonlinear adaptive inputs, all receiver observations and640 clique projections; prefix, source, decoding, tariff and side-information controls." + } + ] +} diff --git a/research/gaussian-adaptive-header-tax/geometry_check.py b/research/gaussian-adaptive-header-tax/geometry_check.py new file mode 100644 index 0000000000..8d67d2de86 --- /dev/null +++ b/research/gaussian-adaptive-header-tax/geometry_check.py @@ -0,0 +1,24 @@ +"""Run the unchanged geometric premise with assertions enabled.""" +import importlib.util +import json +from pathlib import Path +import sys + +if not __debug__: + raise RuntimeError('geometry premise requires assertions') +ROOT = Path(__file__).resolve().parents[2] +SOURCE = ROOT / 'research/gaussian-clique-copy-bound' +spec = importlib.util.spec_from_file_location('geometry', SOURCE / 'geometry.py') +geometry = importlib.util.module_from_spec(spec) +sys.modules['geometry'] = geometry +spec.loader.exec_module(geometry) +spec = importlib.util.spec_from_file_location('gaussian_retained', SOURCE / 'verify.py') +retained = importlib.util.module_from_spec(spec) +spec.loader.exec_module(retained) +receipt = retained.calculate() +if receipt != json.loads((SOURCE / 'certificate.json').read_text()): + raise RuntimeError('retained geometry receipt differs') +lines = geometry.gaussian_lines() +graph = geometry.nonorthogonality(lines) +cliques = geometry.maximal_cliques(graph) +print(json.dumps({'receipt': receipt, 'lines': lines, 'graph': graph, 'cliques': cliques})) diff --git a/research/gaussian-adaptive-header-tax/verify.py b/research/gaussian-adaptive-header-tax/verify.py new file mode 100644 index 0000000000..0e2a6114f1 --- /dev/null +++ b/research/gaussian-adaptive-header-tax/verify.py @@ -0,0 +1,287 @@ +#!/usr/bin/env python3 +"""Exact source-bound adaptive Gaussian controls; no numerical entropy oracle.""" +import argparse +from collections import Counter +from copy import deepcopy +from fractions import Fraction as Q +import hashlib +from itertools import combinations +import json +import os +from pathlib import Path +import subprocess +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE_NAMES = ('research/gaussian-clique-copy-bound/geometry.py', + 'research/gaussian-clique-copy-bound/verify.py', + 'research/gaussian-clique-copy-bound/certificate.json', + 'research/gaussian-clique-copy-bound/PROOF.md', + 'research/gaussian-nonlinear-copy-floor/PROOF.md', + 'research/hurwitz-adaptive-routing/PROOF.md') + + +def require(value, message): + if not value: + raise ValueError(message) + + +def pins(): + data = (HERE / 'SOURCES.json').read_bytes() + manifest = json.loads(data) + inputs = [x for x in manifest['files'] if x['usage'] == 'input'] + require({x['path'] for x in inputs} == set(SOURCE_NAMES), 'source inventory') + for item in inputs: + content = (ROOT / item['path']).read_bytes() + require(hashlib.sha256(content).hexdigest() == item['sha256'], 'source SHA256') + blob = b'blob ' + str(len(content)).encode() + b'\0' + content + require(hashlib.sha1(blob).hexdigest() == item['git_blob'], 'source Git blob') + return hashlib.sha256(data).hexdigest() + + +def geometry(): + env = os.environ.copy() + env.pop('PYTHONOPTIMIZE', None) + result = subprocess.run([sys.executable, '-I', '-B', str(HERE / 'geometry_check.py')], + env=env, capture_output=True, check=True, timeout=300) + return json.loads(result.stdout) + + +def rank(rows): + """Independent Fraction elimination; never imports retained rank code.""" + rows = [list(map(Q, row)) for row in rows] + n = 0 + for col in range(len(rows[0]) if rows else 0): + pivot = next((i for i in range(n, len(rows)) if rows[i][col]), None) + if pivot is None: + continue + rows[n], rows[pivot] = rows[pivot], rows[n] + divisor = rows[n][col] + rows[n] = [x / divisor for x in rows[n]] + for i in range(n + 1, len(rows)): + factor = rows[i][col] + rows[i] = [a - factor * b for a, b in zip(rows[i], rows[n])] + n += 1 + return n + + +def J(v): + return tuple(x for i in range(0, 8, 2) for x in (-v[i + 1], v[i])) + + +def charge(lines, sources, readers): + a = [v for i in sources for v in (lines[i], J(lines[i]))] + r = [v for i in readers for v in (lines[i], J(lines[i]))] + n = rank([[sum(x * y for x, y in zip(u, v)) for v in a] for u in r]) + require(n % 2 == 0, 'odd rational Gaussian pairing rank') + return n // 2 + + +def prefix(words): + words = set(words) + require(all(set(w) <= {'0', '1'} for w in words), 'nonbinary codeword') + require(all(not b.startswith(a) for a in words for b in words if a != b), + 'non-prefix codebook') + require(sum((Q(1, 2 ** len(w)) for w in words), Q()) <= 1, 'Kraft failure') + + +def frames(graph): + selected, used = [], set() + for frame in combinations(range(60), 4): + if used.intersection(frame): + continue + mask = sum(1 << t for t in frame) + if all(not (graph[t] & mask) for t in frame): + selected.append(list(frame)) + used.update(frame) + if len(selected) == 3: + return selected + raise ValueError('three disjoint orthogonal frames missing') + + +def fixture(frame): + ports = sum(frame, []) + first = frame[0] + frame[1] + branch = {0: [(first, first), (frame[2], frame[2])], + 1: [(frame[2], frame[2])]} + table = [] + for word in range(4096): + z = [(word >> (4 * f) & 15).bit_count() % 2 for f in range(3)] + m = z[0] & z[1] + pair = {(0, 0): '0', (0, 1): '10', (1, 0): '11'} + values = [str(z[2])] if m else [pair[z[0], z[1]], str(z[2])] + table.append((m, tuple(values))) + return {'ports': ports, 'branches': branch, 'headers': {0: '0', 1: '1'}, 'table': table} + + +_prices = {} + + +def charge_cache(lines, a, r): + key = tuple(map(tuple, lines)), tuple(a), tuple(r) + if key not in _prices: + _prices[key] = charge(lines, a, r) + return _prices[key] + + +def check_code(code, lines, graph, cliques, header_price=4): + ports, branch, table = code['ports'], code['branches'], code['table'] + n, size = len(ports), 1 << len(ports) + require(len(table) == size and len(set(ports)) == n, 'input domain') + require(header_price == charge_cache(lines, range(60), range(60)) == 4, + 'full-space header tariff') + prefix(code['headers'].values()) + require(len(set(code['headers'].values())) == len(code['headers']), 'ambiguous header') + local = {p: i for i, p in enumerate(ports)} + costs, lengths, counts = [], [], Counter() + source_maps, books = {}, {} + for word, (m, values) in enumerate(table): + require(m in code['headers'] and m in branch, 'undeclared header') + require(len(values) == len(branch[m]), 'payload count') + counts[m] += 1 + lengths.append(len(code['headers'][m])) + cost = header_price * lengths[-1] + for j, ((a, r), value) in enumerate(zip(branch[m], values)): + require(set(a + r) <= set(range(60)), 'invalid support') + mask = sum(1 << local[t] for t in a if t in local) + key = m, j, word & mask + require(key not in source_maps or source_maps[key] == value, 'undeclared source') + source_maps[key] = value + books.setdefault((m, j), set()).add(value) + cost += charge_cache(lines, a, r) * len(value) + costs.append(cost) + for words in books.values(): + prefix(words) + # Reader-conflict check uses no producer decoder or assumed inverse. + observations = [{} for _ in ports] + side_masks = [sum(1 << k for k, q in enumerate(ports) + if q != p and not (graph[p] >> q & 1)) for p in ports] + for word, (m, values) in enumerate(table): + for t, p in enumerate(ports): + received = tuple(values[j] for j, (_, readers) in enumerate(branch[m]) if p in readers) + key = m, word & side_masks[t], received + bit = word >> t & 1 + require(key not in observations[t] or observations[t][key] == bit, 'receiver conflict') + observations[t][key] = bit + projected = 0 + for clique in cliques: + inside = sum(1 << i for i, p in enumerate(ports) if clique >> p & 1) + outside, seen = (size - 1) ^ inside, {} + relevant_indices = {m: [j for j, (a, r) in enumerate(pairs) + if any(clique >> p & 1 for p in a) + and any(clique >> p & 1 for p in r)] + for m, pairs in branch.items()} + for word, (m, values) in enumerate(table): + relevant = tuple(values[j] for j in relevant_indices[m]) + key = word & outside, m, relevant + require(key not in seen or seen[key] == word & inside, 'conditional collision') + seen[key] = word & inside + projected += 1 + average, length = Q(sum(costs), size), Q(sum(lengths), size) + concentrated = max(sum(clique >> p & 1 for p in ports) for clique in cliques) + floor = max(Q(2, 3) * (n + length), concentrated + 3 * length) + require(average >= floor, 'header-tax bound') + return {'inputs': size, 'receiver_checks': size * n, 'conditional_checks': projected, + 'header_counts': {str(k): v for k, v in sorted(counts.items())}, + 'average_cost': str(average), 'header_length': str(length), + 'tax_floor': str(floor), 'cost_histogram': {str(k): v for k, v in sorted(Counter(costs).items())}, + 'payload_codebooks': {str(k): sorted(v) for k, v in sorted(books.items())}, + 'transcript_sha256': hashlib.sha256(json.dumps(table).encode()).hexdigest()} + + +def rejection(function, message): + try: + function() + except ValueError as error: + require(message in str(error), 'wrong rejection: ' + str(error)) + return + raise ValueError('negative control accepted: ' + message) + + +def calculate(): + source_hash = pins() + geo = geometry() + lines, graph = geo['lines'], geo['graph'] + cliques = [x for x in geo['cliques'] if x.bit_count() == 12] + require(len(lines) == 60 and len(cliques) == 640, 'geometry size') + require([sum(q >> t & 1 for q in cliques) for t in range(60)] == [128] * 60, + 'weighted clique incidence') + require(Q(640, 192) == Q(10, 3) and 4 - Q(640, 192) == Q(2, 3), 'header gap') + frame = frames(graph) + code = fixture(frame) + result = check_code(code, lines, graph, cliques) + require(result['average_cost'] == '13' and result['tax_floor'] == '26/3', 'fixture cost') + require(code['table'][0][0] ^ code['table'][1][0] ^ code['table'][16][0] + ^ code['table'][17][0] == 1, 'header is not nonlinear') + bad = deepcopy(code) + bad['table'][0] = (0, ('0', '1')) + rejection(lambda: check_code(bad, lines, graph, cliques), 'undeclared source') + bad = deepcopy(code) + bad['branches'][0][0] = ([], bad['branches'][0][0][1]) + rejection(lambda: check_code(bad, lines, graph, cliques), 'undeclared source') + bad = deepcopy(code) + bad['table'] = [(m, tuple('0' if j == len(v) - 1 else x for j, x in enumerate(v))) + for m, v in bad['table']] + rejection(lambda: check_code(bad, lines, graph, cliques), 'receiver conflict') + rejection(lambda: check_code(code, lines, graph, cliques, header_price=0), 'header tariff') + # Correct parity code with free termination violates the claimed floor. + frame_price = charge_cache(lines, frame[0], frame[0]) + require(frame_price == 4, 'orthogonal frame price') + free_end = ['' if w.bit_count() % 2 == 0 else '1' for w in range(16)] + for w, encoded in enumerate(free_end): + parity = int(encoded == '1') + for t in range(4): + require(parity ^ ((w & (15 ^ (1 << t))).bit_count() % 2) == (w >> t & 1), + 'termination boundary decode') + require(Q(sum(map(len, free_end)) * frame_price, 16) == 2 < Q(8, 3), 'termination boundary') + rejection(lambda: prefix(free_end), 'non-prefix') + # Extra nonorthogonal side information permits an inadmissible parity code. + clique_ports = [t for t in range(60) if cliques[0] >> t & 1] + require(len(clique_ports) == 12, 'clique boundary size') + def legal_side(): + require(all(not (graph[p] >> q & 1) for p in clique_ports + for q in clique_ports if p != q), 'illegal side information') + rejection(legal_side, 'illegal side information') + for w in range(4096): + parity = w.bit_count() % 2 + for t in range(12): + require(parity ^ ((w & (4095 ^ (1 << t))).bit_count() % 2) == (w >> t & 1), + 'illegal-side boundary decode') + require(4 < 12, 'illegal-side boundary cost') + # Valid prefix-free variable header violates a false pointwise strengthening. + headers = ['0' if w == 0 else '1' + format(w, '012b') for w in range(4096)] + prefix(headers) + require(len(set(headers)) == 4096 and 4 * len(headers[0]) == 4 < 8, 'pointwise boundary') + mean_header = Q(sum(map(len, headers)), 4096) + require(4 * mean_header >= Q(2, 3) * (12 + mean_header), 'variable header tax') + return {'schema': 1, 'status': 'scoped expected-cost theorem; no supplier or kappa', + 'sources_sha256': source_hash, 'retained_geometry': geo['receipt'], + 'frames': frame, 'full_header_price': 4, 'weighted_cliques': 640, + 'incidence_per_port': 128, 'header_tax': '2/3', 'adaptive_fixture': result, + 'unpaid_termination_cost': '2', 'unpaid_termination_floor': '8/3', + 'pointwise_boundary_minimum': 4, 'pointwise_boundary_mean': str(4 * mean_header), + 'controls': 6} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', type=Path) + args = parser.parse_args() + if args.write: + require(not args.write.exists(), 'output exists') + result = calculate() + expected = HERE / 'RESULT.json' + if expected.exists(): + require(result == json.loads(expected.read_text()), 'receipt mismatch') + else: + require(args.write is not None, 'missing committed receipt') + if args.write: + with args.write.open('x', encoding='utf-8', newline='\n') as stream: + json.dump(result, stream, indent=2, sort_keys=True) + stream.write('\n') + print('PASS_GAUSSIAN_ADAPTIVE_HEADER_TAX inputs=4096 receiver_checks=49152 cliques=640 controls=6') + + +if __name__ == '__main__': + main() From d4563baaffe2e417b56de9c9525e8332c8369afe Mon Sep 17 00:00:00 2001 From: ywz65 <154373401+ywz65@users.noreply.github.com> Date: Thu, 15 Oct 2026 09:42:11 -0700 Subject: [PATCH 2/2] Preserve discrete types when comparing the Gaussian receipt --- .../gaussian-adaptive-header-tax/VALIDATION.md | 4 ++++ research/gaussian-adaptive-header-tax/verify.py | 15 ++++++++++++++- 2 files changed, 18 insertions(+), 1 deletion(-) diff --git a/research/gaussian-adaptive-header-tax/VALIDATION.md b/research/gaussian-adaptive-header-tax/VALIDATION.md index 6d3607f963..e6c023da5b 100644 --- a/research/gaussian-adaptive-header-tax/VALIDATION.md +++ b/research/gaussian-adaptive-header-tax/VALIDATION.md @@ -42,3 +42,7 @@ freshness is bounded, and metadata search is not a novelty guarantee. Claim and completion share the predecessor investigation: https://github.com/CrocSwap/integer-mult-bounds/pull/888#issuecomment-6196956825 + +The final receipt comparator also rejects JSON Boolean/integer and float/integer +substitutions while accepting the unchanged parsed receipt. Scientific counts +and input bytes are unchanged by this type-preserving comparison. diff --git a/research/gaussian-adaptive-header-tax/verify.py b/research/gaussian-adaptive-header-tax/verify.py index 0e2a6114f1..9083be8a98 100644 --- a/research/gaussian-adaptive-header-tax/verify.py +++ b/research/gaussian-adaptive-header-tax/verify.py @@ -264,6 +264,19 @@ def legal_side(): 'controls': 6} +def same_receipt(actual, expected): + """Keep discrete proof counts distinct from JSON booleans and floats.""" + if type(actual) is not type(expected): + return False + if isinstance(actual, dict): + return actual.keys() == expected.keys() and all( + same_receipt(value, expected[key]) for key, value in actual.items()) + if isinstance(actual, list): + return len(actual) == len(expected) and all( + same_receipt(a, b) for a, b in zip(actual, expected)) + return actual == expected + + def main(): parser = argparse.ArgumentParser(description=__doc__) parser.add_argument('--write', type=Path) @@ -273,7 +286,7 @@ def main(): result = calculate() expected = HERE / 'RESULT.json' if expected.exists(): - require(result == json.loads(expected.read_text()), 'receipt mismatch') + require(same_receipt(result, json.loads(expected.read_text())), 'receipt mismatch') else: require(args.write is not None, 'missing committed receipt') if args.write: