diff --git a/research/gaussian-localized-header-tax/README.md b/research/gaussian-localized-header-tax/README.md new file mode 100644 index 0000000000..c5e4662c21 --- /dev/null +++ b/research/gaussian-localized-header-tax/README.md @@ -0,0 +1,209 @@ +# Gaussian public headers with localized sources pay a strict surcharge + +**Scoped proof with exact finite corroboration.** In the Gaussian nonlinear +message model of ywz65's [PR2641](https://github.com/CrocSwap/integer-mult-bounds/pull/2641), +allow the public routing header M to depend only on inputs at a declared +nonempty source set A. Charge each header bit its actual declared source-span +rank r, rather than the predecessor's full-space price four. Then + +```text +E[C] >= (2/3) B + r L - lambda(A) H(M) + >= (2/3) B + L/3, +``` + +where B is total independent uniform demand, L is expected header length, +and lambda(A) is the total weight of the retained nonorthogonal cliques +meeting A. For equal b-bit demands this is `40b + L/3`. Localizing the header +source can reduce the predecessor's `2L/3` guaranteed surcharge, but cannot +eliminate a positive surcharge under this public-observation contract. + +This answers the **localized-source, public-reader** part of PR2641's Open next +question. It leaves private readers open. The new step is to retain the header's +source support in every conditional entropy term, then use the credited flat +census to obtain a uniform positive gap. Geometry, clique weights, transcript +injectivity and prefix-coding entropy are cited predecessor results. No +predecessor verifier or census is replayed here. + +## Model and cited premises + +There are 60 Gaussian E8 lines. Port t has an independent uniform b_t-bit +input X_t, and receiver t must recover it exactly on every input. Its free side +information consists only of orthogonal ports. Source and receiver roles are +distinct. The header is a deterministic function `M=h(X_A)` with a finite +prefix-free code. All receivers and payload encoders receive it. Its price +per bit is `c(All,A)=r`, the Gaussian rank of the span of A. + +Conditional on M, payload count, order, source/reader supports and prefix-free +codebooks are fixed. Payload encoders use M and their declared original source +inputs, without relays. Arbitrary nonlinear encoding and decoding are allowed. +A payload bit costs its source/reader pairing rank, additively. Encoding, +decoding and source access remain free in this abstract relaxation. + +Sagar Thakrar's [PR738](https://github.com/CrocSwap/integer-mult-bounds/pull/738) +supplies 640 nonorthogonal cliques, each of weight 1/192, with incidence 128 +at every line, and the support inequality + +```text +sum_Q [Q meets R and S]/192 <= c(R,S). +``` + +Its unchanged [certificate](../gaussian-clique-copy-bound/certificate.json) +also supplies the root-generated flat census used below. These are mathematical +premises of this extension; source hashes authenticate retained bytes, not +independent acceptance of their geometry. PR2641 supplies the conditional +transcript argument and paid prefix-code model. + +## Proof + +Fix a clique Q and the inputs outside Q. Let Z_Q be the tuple of payloads +whose source and reader sets both meet Q. The pair `(M,Z_Q)` determines X_Q: +other payloads received by Q have sources outside Q and are determined by M +and the fixed outside inputs; all permitted side information is outside Q. +Exact recovery therefore gives the inherited entropy inequality + +```text +sum_(t in Q) b_t + <= H(M | X_outside_Q) + + E[sum_j length(Y_j) [Q meets R_j(M) and S_j(M)]]. +``` + +If Q does not meet A, its outside inputs determine the header, so the first +term is zero. Otherwise it is at most H(M). Multiply by 1/192 and sum over Q. +The 128 incidences at every port and the cited support inequality imply + +```text +(2/3) B <= lambda(A) H(M) + E[payload charge]. +``` + +Adding the actual header price rL proves the first displayed bound. No +conditional independence after observing M was assumed. Kraft's inequality +and the entropy bound for prefix codes give `H(M)<=L`. + +Let F be the Gaussian span closure of A among the 60 lines. Then +`lambda(A)<=lambda(F)` and `rank(F)=r`. The following table transforms the +**inherited** flat census; it does not claim new flat enumeration. + +| r | Lines in F | lambda(F) | r-lambda(F) | +|---:|---:|---:|---:| +| 1 | 1 | 2/3 | 1/3 | +| 2 | 2 | 4/3 | 2/3 | +| 2 | 3 | 77/48 | 19/48 | +| 2 | 6 | 5/3 | 1/3 | +| 3 | 4 | 109/48 | 35/48 | +| 3 | 6 | 41/16 | 7/16 | +| 3 | 15 | 8/3 | 1/3 | +| 4 | 60 | 10/3 | 2/3 | + +Every nonempty source set consequently has `r-lambda(A)>=1/3`. Thus +`rL-lambda(A)H(M)>=(r-lambda(A))L>=L/3`, proving the theorem for every finite +block width and every finite prefix-coded payload list. When r=4 the stronger +`2L/3` bound survives even if A is a proper spanning subset. A positive-length +constant header has H(M)=0 and pays its full rL. + +The support-sensitive entropy estimate is exact as an information-loss bound. +Take one independent bit at every port of any nonempty A and let M be their +parity. Conditional on outside-Q inputs, this parity has entropy one precisely +when Q meets A. Therefore the total conditional header entropy is exactly +lambda(A), while `H(M)=L=1`. Singleton, six-line rank-two and fifteen-line +rank-three flats attain the geometric gap 1/3. **This does not establish an +attaining complete communication code at charge `(2/3)B+L/3`.** The Gaussian +nonlinear optimum itself remains open. + +## Exact corroboration and reproduction + +From the repository root, using the available CPython 3.12 interpreter: + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -B research/gaussian-localized-header-tax/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/gaussian-localized-header-tax +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/gaussian-localized-header-tax --check-source-history +``` + +The registered replay runs both ordinary and optimized Python. The verifier +reads cited data, transforms its eight flat types, and performs new bounded +information checks: + +- All 65,536 Boolean headers on four independent bits at orthogonal lines. + Each clique meets at most one of those lines. Conditional header entropy + at a singleton cut equals its Boolean edge influence. The support-sensitive + entropy bound is checked using integer powers; no floating logarithm decides + an inequality. The 32 equality cases are exactly the affine headers. +- All 63 nonempty cuts of a six-input parity, with 4,032 input/cut pairs, + confirming the exact support-loss witness. +- Three literal public-observation protocols on the credited six-line rank-two + flat with source indices `(0,1,2,11,12,45)`: parity header, nonlinear header + `x0 XOR (x1 AND x2)`, and variable header code `{0,10,11}`. All 64 inputs and + six receiver demands are checked for each protocol. Header-dependent payload + orders and counts are included. Their expected charges are 7, 7 and 8; + these corroborate correctness and pricing, not optimality. +- Eight rejection controls: an invalid surcharge table, three invalid prefix + codes, three missing-payload protocols and an undeclared header source. + +`RESULT.json` is generated by `verify.py --output NEW_PATH` and binds every +package source file and live predecessor input by SHA256. Default replay +regenerates and compares the entire result. Exclusive output refuses an +existing path. The all-width theorem is the written proof, not an extrapolation +from these finite examples or a proof-kernel result. + +## Scope and implementation limits + +The result bounds expected and hence worst-case charge, not each execution. +All receivers see the paid header; private schedule knowledge, interactive +relays, correlated or restricted demands, errors, non-prefix termination, +cheaper physical sharing and changed stage accounting are excluded. The +nonempty declared-source premise excludes a free empty-source constant header. +No physical supplier, helper-restoration implementation, native caller, +precision/tape bound, improved kappa or complete multiplication theorem follows. +The selected frontier is unchanged. + +The verifier is a finite standard-library calculation. Its scientific loops have fixed +bounds: 65,536 headers, four variables with eight edges each, 64 inputs, 63 cuts, +three protocols and eight cited flat types. The source manifest has four entries; +five fixed package source files are hashed. Each file read is capped at 256 KiB. +No recursion, dynamic code or network is used. The verifier authenticates before +reading live data and does not execute predecessor code. Warning-strict normal +and optimized replay are the recurring Python diagnostics; no unavailable +static analyzer is claimed. + +Power of Ten deviations are confined to this verifier: + +- Rule 3, managed allocation: Python allocates integers, JSON and dictionaries + during execution. Reads are capped; the header loop is 65,536 iterations; + each receiver map has at most 64 entries and each cut has at most 64 fibers. + The equality list has capacity at most 65,536 identifiers. Normal/optimized + full replay verifies the finite bounds' path. Resources are process-local and + files use context managers. Follow-up: if the domain grows, retain explicit + input/collection caps and measure peak allocation before enlarging the limit. +- Rule 9, indirect calls: the rejection helper invokes only four fixed local + targets (table, prefix, protocol and source-support checks). This is confined + to eight deliberate fault controls and exposes each failure. Normal/optimized + replay exercises them. Follow-up: replace this helper with explicit cases if + external callbacks or stateful targets are ever introduced. + +## Open next questions + +1. Can localized **private-reader** headers preserve a useful transcript + bound? This changes who knows the payload schedule. Start with one rank-one + header and specify every recipient's observation and routing information. + The blocker is avoiding uncharged schedule leakage to other receivers. +2. Does a chronological sequence of public headers with source supports chosen + by earlier headers retain the `L_total/3` surcharge? Start with two rounds + and condition the support-sensitive entropy argument on the first paid + header. Branch-dependent source ranks and stopping information need an + explicit contract. No multi-header theorem is claimed here. + +## Provenance and credit + +Base `624de9dc66858af0945e5f8a0942488d62280d43`, priority revision 7. TASK.json +records the changed card scope. SOURCES.json pins the unchanged geometric +certificate and predecessor proof as live inputs and the task/selected context +as historical provenance. The claim is [here](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19134282). + +This contribution is **produced by Nick Petalas**. Credit ywz65 / PR2641 for +the public-header argument and open localized-header question; Sagar Thakrar / +PR738 for the Gaussian geometry, clique weights, flat census and support bound; +ToikY / PR888, Alexander Templeton / PR785, Michael Fischler / PR814 and Jerry +Chen / PR912 for the nonlinear transcript and paid-header lineage, retaining +Joel Pulikkan, Douglas Colkitt and DreamingOfClouds's prior credit. Entropy, +Kraft's inequality and Boolean influence are standard methods. Independent +human and formal proof-kernel review are unclaimed. Apache-2.0. diff --git a/research/gaussian-localized-header-tax/RESULT.json b/research/gaussian-localized-header-tax/RESULT.json new file mode 100644 index 0000000000..1ff256207c --- /dev/null +++ b/research/gaussian-localized-header-tax/RESULT.json @@ -0,0 +1,111 @@ +{ + "boolean_headers": { + "equality_headers": 32, + "headers": 65536, + "nonlinear_headers": 65504, + "support_census": { + "0": 2, + "1": 8, + "2": 60, + "3": 872, + "4": 64594 + } + }, + "claim_type": "scoped proof", + "flat_tax_table": [ + { + "leakage_coefficient": "2/3", + "lines": 1, + "rank": 1, + "surcharge_coefficient": "1/3" + }, + { + "leakage_coefficient": "4/3", + "lines": 2, + "rank": 2, + "surcharge_coefficient": "2/3" + }, + { + "leakage_coefficient": "77/48", + "lines": 3, + "rank": 2, + "surcharge_coefficient": "19/48" + }, + { + "leakage_coefficient": "5/3", + "lines": 6, + "rank": 2, + "surcharge_coefficient": "1/3" + }, + { + "leakage_coefficient": "109/48", + "lines": 4, + "rank": 3, + "surcharge_coefficient": "35/48" + }, + { + "leakage_coefficient": "41/16", + "lines": 6, + "rank": 3, + "surcharge_coefficient": "7/16" + }, + { + "leakage_coefficient": "8/3", + "lines": 15, + "rank": 3, + "surcharge_coefficient": "1/3" + }, + { + "leakage_coefficient": "10/3", + "lines": 60, + "rank": 4, + "surcharge_coefficient": "2/3" + } + ], + "geometry_status": "cited premise; not replayed", + "parity_witness": { + "conditional_entropy_each_nonempty_cut": "1", + "input_cut_pairs": 4032, + "nonempty_cuts": 63 + }, + "protocols": [ + { + "certified_lower_bound": "13/3", + "expected_charge": "7", + "expected_header_length": "1", + "header_entropy": "1", + "inputs": 64, + "mode": "parity", + "receiver_observations": 384 + }, + { + "certified_lower_bound": "13/3", + "expected_charge": "7", + "expected_header_length": "1", + "header_entropy": "1", + "inputs": 64, + "mode": "nonlinear", + "receiver_observations": 384 + }, + { + "certified_lower_bound": "5", + "expected_charge": "8", + "expected_header_length": "7/4", + "header_entropy": "3/2", + "inputs": 64, + "mode": "variable", + "receiver_observations": 384 + } + ], + "rejecting_controls": 8, + "schema": "localized-gaussian-header/v1", + "source_hashes": { + "package/README.md": "8a6ac33f9de5fc1ebb43a1a1e0cb16b3e769694dcd8d859fa50aaca968a9ab0b", + "package/SOURCES.json": "4233ea8699f2ed564e23b39a30cf133ec2c5a3dabb9cdf716741179d4f3f7854", + "package/TASK.json": "8f2917b84ad4df9ab4e9326111d86028a82121c2e2e3f63fb88d2663e85719ab", + "package/VERIFY.json": "fb3db3d2d3285c63975a282651b8e7de8115ca221f22d609ca08cd23f7b40d8c", + "package/verify.py": "398dcc75fc0e6f306bd3d18cd39397a6dcf777d074ec367d6068d36c7e658ac6", + "research/gaussian-adaptive-header-tax/PROOF.md": "af3c143c50a4290033ff5f585c58ddf205ce7c15a2faf1998c73282aed56ea34", + "research/gaussian-clique-copy-bound/certificate.json": "c50858aaab863b34c7533211ca07ae038ee000328bd5134b73219992ae078875" + } +} diff --git a/research/gaussian-localized-header-tax/SOURCES.json b/research/gaussian-localized-header-tax/SOURCES.json new file mode 100644 index 0000000000..ce586db986 --- /dev/null +++ b/research/gaussian-localized-header-tax/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/gaussian-adaptive-header-tax/PROOF.md", + "usage": "input", + "git_blob": "317d8324c2e89e1073238b21f3801c723de00ee4", + "sha256": "af3c143c50a4290033ff5f585c58ddf205ce7c15a2faf1998c73282aed56ea34" + }, + { + "path": "research/gaussian-clique-copy-bound/certificate.json", + "usage": "input", + "git_blob": "cacb07d8e71177175c0702e5f455cc986dce5d42", + "sha256": "c50858aaab863b34c7533211ca07ae038ee000328bd5134b73219992ae078875" + } + ] +} diff --git a/research/gaussian-localized-header-tax/TASK.json b/research/gaussian-localized-header-tax/TASK.json new file mode 100644 index 0000000000..fdf6b72da0 --- /dev/null +++ b/research/gaussian-localized-header-tax/TASK.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "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. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "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": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "Source-sensitive Gaussian public-header entropy tax with localized source span and all receivers.", + "scope_change_reason": "Answer the explicit localized-header question of ywz65 PR2641; this is a scoped nonlinear observation-contract obstruction, not decoder synthesis.", + "bottleneck_link": "Localizing paid routing sources lowers header rank; the new strict surcharge shows that this change alone cannot remove the Gaussian public-routing penalty. No physical supplier is inferred.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved source-sensitive tax with bounded exact corroboration; do not extend to private or multi-header protocols.", + "outcome": "completed", + "evidence": "Written all-width proof conditional on credited Gaussian geometry; deterministic integer entropy checks, exact receiver observations and a generated source-bound receipt.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can localized private-reader headers satisfy a comparable lower bound?", + "why_it_matters": "Private routing changes the observation contract and may escape the public-header argument.", + "first_step": "Specify one rank-one header with all recipients and every payload schedule observation.", + "blocked_by": "No uncharged schedule leakage is allowed; the common public transcript proof does not apply." + }, + { + "question": "Does a sequence of publicly observed adaptive headers retain L_total/3?", + "why_it_matters": "Multiple rounds permit source supports and rank prices to depend on earlier information.", + "first_step": "Write a two-round support-sensitive conditional entropy argument.", + "blocked_by": "Branch-dependent source ranks, codebooks and stopping metadata require a precise contract." + } + ] +} diff --git a/research/gaussian-localized-header-tax/VERIFY.json b/research/gaussian-localized-header-tax/VERIFY.json new file mode 100644 index 0000000000..7915314e81 --- /dev/null +++ b/research/gaussian-localized-header-tax/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/gaussian-adaptive-header-tax/PROOF.md", + "research/gaussian-clique-copy-bound/certificate.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Source-bound receipt; localized tax arithmetic; all four-bit Boolean headers; parity cuts; exact adaptive protocol observations; eight rejection controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same complete check with assertions disabled; every check uses explicit runtime failures." + } + ] +} diff --git a/research/gaussian-localized-header-tax/verify.py b/research/gaussian-localized-header-tax/verify.py new file mode 100644 index 0000000000..644091fea4 --- /dev/null +++ b/research/gaussian-localized-header-tax/verify.py @@ -0,0 +1,216 @@ +"""Exact corroboration of the localized public-header argument; stdlib only.""" + +import argparse +from collections import Counter +from fractions import Fraction +from hashlib import sha256 +import json +from pathlib import Path + + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def read_bytes(path): + with path.open("rb") as stream: + data = stream.read(262145) + require(len(data) <= 262144, "input exceeds 256 KiB bound") + return data + + +def source_hashes(): + manifest = json.loads(read_bytes(PACKAGE / "SOURCES.json")) + require(len(manifest["files"]) == 4, "four source entries") + hashes = {} + for entry in manifest["files"]: + if entry["usage"] == "input": + path = entry["path"] + digest = sha256(read_bytes(ROOT / path)).hexdigest() + require(digest == entry["sha256"], "source hash: " + path) + hashes[path] = digest + for name in ("README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py"): + hashes["package/" + name] = sha256(read_bytes(PACKAGE / name)).hexdigest() + return hashes + + +def tax_table(certificate): + """Transform cited flat data, without replaying or certifying its geometry.""" + table = [] + for rank_text, entries in certificate["flat_census"].items(): + rank = int(rank_text) + if rank == 0: + continue + for entry in entries: + leakage = Fraction(entry["cliques_hit"], 192) + gap = rank - leakage + require(gap >= Fraction(1, 3), "nonempty-source surcharge") + table.append({"rank": rank, "lines": entry["lines"], + "leakage_coefficient": str(leakage), + "surcharge_coefficient": str(gap)}) + require(len(table) == 8, "eight cited nonempty flat types") + require(min(Fraction(row["surcharge_coefficient"]) for row in table) + == Fraction(1, 3), "attained geometric coefficient") + return table + + +def influence_edges(table, variables): + return tuple(sum(((table >> word) ^ (table >> (word | (1 << bit)))) & 1 + for word in range(1 << variables) if not (word >> bit) & 1) + for bit in range(variables)) + + +def boolean_headers(): + """Check entropy exactly by exponentiating, never by floating point.""" + census = Counter() + equality = [] + for table in range(1 << 16): + ones = table.bit_count() + edges = influence_edges(table, 4) + support = sum(value != 0 for value in edges) + # 16 H(M) = 64 - log2(k^k (16-k)^(16-k)). + entropy_denominator = ones ** ones * (16 - ones) ** (16 - ones) + exponent = 64 * support - 2 * sum(edges) + left = 1 << exponent + right = entropy_denominator ** support + require(left >= right, "source-sensitive entropy inequality") + if left == right: + equality.append(table) + census[support] += 1 + affine = set() + for mask in range(16): + for offset in range(2): + affine.add(sum((((word & mask).bit_count() + offset) % 2) << word + for word in range(16))) + require(set(equality) == affine, "equality is exactly affine headers") + return {"headers": 65536, "support_census": {str(key): value for key, value in sorted(census.items())}, + "equality_headers": len(equality), "nonlinear_headers": 65504} + + +def check_prefix(words): + require(len(set(words)) == len(words), "duplicate codeword") + require(all(not right.startswith(left) for left in words for right in words + if left != right), "non-prefix code") + + +def header(word, mode): + bits = tuple((word >> bit) & 1 for bit in range(6)) + if mode == "parity": + return str(sum(bits) % 2) + if mode == "nonlinear": + return str(bits[0] ^ (bits[1] & bits[2])) + if bits[0]: + return "11" + return "10" if bits[1] else "0" + + +def protocol(mode, omit=False): + """Literal public observations; six sources occupy one cited rank-2 flat.""" + words = ("0", "10", "11") if mode == "variable" else ("0", "1") + check_prefix(words) + observations = tuple({} for _ in range(6)) + costs = [] + for word in range(64): + code = header(word, mode) + indices = tuple(range(1, 6)) + if mode == "variable" and code != "11": + indices = tuple(range(2, 6)) + if code.endswith("1"): + indices = tuple(reversed(indices)) + if omit: + indices = tuple(bit for bit in indices if bit != 5) + payload = tuple((word >> bit) & 1 for bit in indices) + observation = (code, payload) + for bit in range(6): + value = (word >> bit) & 1 + previous = observations[bit].setdefault(observation, value) + require(previous == value, "receiver conflict") + costs.append(2 * len(code) + len(payload)) + expected = Fraction(sum(costs), 64) + length = Fraction(sum(len(header(word, mode)) for word in range(64)), 64) + entropy = Fraction(3, 2) if mode == "variable" else Fraction(1) + lower = 4 + 2 * length - Fraction(5, 3) * entropy + require(expected >= lower >= 4 + length / 3, "cost inequality") + return {"mode": mode, "inputs": 64, "receiver_observations": 384, + "expected_charge": str(expected), "expected_header_length": str(length), + "header_entropy": str(entropy), "certified_lower_bound": str(lower)} + + +def parity_cuts(): + checked = 0 + for inside in range(1, 64): + fibers = {} + for word in range(64): + outside = word & (63 ^ inside) + counts = fibers.setdefault(outside, [0, 0]) + counts[word.bit_count() % 2] += 1 + checked += 1 + require(all(zero == one for zero, one in fibers.values()), + "parity is conditionally uniform at each nonempty cut") + return {"nonempty_cuts": 63, "input_cut_pairs": checked, + "conditional_entropy_each_nonempty_cut": "1"} + + +def rejected(function, *arguments): + try: + function(*arguments) + except ValueError: + return 1 + raise ValueError("negative control was accepted") + + +def check_header_support(mode, source_mask): + for word in range(64): + for bit in range(6): + if not (source_mask >> bit) & 1: + require(header(word, mode) == header(word ^ (1 << bit), mode), + "undeclared header source") + + +def controls(certificate): + corrupted = json.loads(json.dumps(certificate)) + corrupted["flat_census"]["1"][0]["cliques_hit"] = 200 + count = rejected(tax_table, corrupted) + count += rejected(check_prefix, ("0", "01")) + count += rejected(check_prefix, ("", "1")) + count += rejected(check_prefix, ("0", "0")) + for mode in ("parity", "nonlinear", "variable"): + count += rejected(protocol, mode, True) + count += rejected(check_header_support, "nonlinear", 3) + return count + + +def calculate(): + hashes = source_hashes() + certificate = json.loads(read_bytes( + ROOT / "research/gaussian-clique-copy-bound/certificate.json")) + return {"schema": "localized-gaussian-header/v1", "claim_type": "scoped proof", + "geometry_status": "cited premise; not replayed", + "source_hashes": hashes, "flat_tax_table": tax_table(certificate), + "boolean_headers": boolean_headers(), "parity_witness": parity_cuts(), + "protocols": [protocol(mode) for mode in ("parity", "nonlinear", "variable")], + "rejecting_controls": controls(certificate)} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, help="write a generated receipt exclusively") + arguments = parser.parse_args() + result = calculate() + if arguments.output: + with arguments.output.open("x") as stream: + stream.write(json.dumps(result, indent=2, sort_keys=True) + "\n") + else: + committed = json.loads(read_bytes(PACKAGE / "RESULT.json")) + require(committed == result, "generated receipt mismatch") + print("PASS_GAUSSIAN_LOCALIZED_HEADER_TAX surcharge=1/3 " + "boolean_headers=65536 protocols=3 controls=8 no_new_kappa") + + +if __name__ == "__main__": + main()