From 49fb8b2c3d5abbcba16f819f2d52d84ee735c7a9 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 22 Oct 2026 23:23:50 +0100 Subject: [PATCH] feat(research): prove four-frame concave subspace pricing --- .../subspace-three-contact-pricing/README.md | 245 ++++++++++++++++ .../RESULT.json | 106 +++++++ .../SOURCES.json | 30 ++ .../subspace-three-contact-pricing/TASK.json | 114 +++++++ .../VERIFY.json | 37 +++ .../subspace-three-contact-pricing/verify.py | 277 ++++++++++++++++++ 6 files changed, 809 insertions(+) create mode 100644 research/subspace-three-contact-pricing/README.md create mode 100644 research/subspace-three-contact-pricing/RESULT.json create mode 100644 research/subspace-three-contact-pricing/SOURCES.json create mode 100644 research/subspace-three-contact-pricing/TASK.json create mode 100644 research/subspace-three-contact-pricing/VERIFY.json create mode 100644 research/subspace-three-contact-pricing/verify.py diff --git a/research/subspace-three-contact-pricing/README.md b/research/subspace-three-contact-pricing/README.md new file mode 100644 index 0000000000..86d6611267 --- /dev/null +++ b/research/subspace-three-contact-pricing/README.md @@ -0,0 +1,245 @@ +# Four frames suffice for concave three-contact subspace pricing + +This contribution is produced by Nick Petalas. It gives a **scoped proof with +finite corroboration**, with no new kappa or native supplier claim. + +For three fixed subspaces, the exact minimum sum of nondecreasing concave +rank-distance prices is attained at one of four explicit frames. The fourth +frame is the sum of the three pairwise intersections. Thus this local search +needs no enumeration of all intermediate subspaces, at any ambient dimension +or over any field. The theorem also respects a common mandatory subspace and +receiver cap when the entire interval between them is allowed. + +The distance is exactly the schematic charge declared in Chrisbryan17's +[PR #2844](https://github.com/CrocSwap/integer-mult-bounds/pull/2844), +`research/p104-signed-mixed-carrier-bank/README.md`. That package leaves physical +lowering separate from its frame experiment. Cinna Davis's +[PR #4447](https://github.com/CrocSwap/integer-mult-bounds/pull/4447), +`research/missing-join-frame/README.md`, supplies the distinct motivation to +close contact catalogues under spans and intersections. Neither predecessor +executable or numerical result is rechecked here. The new result is an exact +local optimization rule in the explicitly stated distance model. The metric +median construction and elementary concavity argument are standard ingredients; +no claim of literature priority for those ingredients is made. + +## Exact contract and formula + +Let V be a finite-dimensional vector space over any field. Fix three subspaces +A, B, C of V, and allow every subspace X of V. Define + +``` +d(U,W) = dim(U) + dim(W) - 2 dim(U intersect W). +M = (A intersect B) + (B intersect C) + (C intersect A). +F(X) = phi_A(d(X,A)) + phi_B(d(X,B)) + phi_C(d(X,C)). +``` + +Each phi is a nonnegative, nondecreasing concave function on `[0, dim V]`. +The functions can differ, so arbitrary nonnegative contact weights are covered. +Discrete tariffs are allowed when their nonnegative successive increments are +nonincreasing; use their piecewise linear interpolation. An additive constant +in any tariff has no effect on the minimizing frame. In particular, the result +covers `phi_i(r)=w_i*r^t` for any `w_i>=0` and `0= alpha+beta, +x+z >= alpha+gamma, +y+z >= beta+gamma. +``` + +If each coordinate is at least its median radius, monotonicity gives +`F(X)>=F(M)`. Otherwise at most one coordinate is below its radius. Suppose +`x0` and + +``` +(x,y,z) >= (x, beta+alpha-x, gamma+alpha-x) + = (x/alpha)*(alpha,beta,gamma) + + (1-x/alpha)*(0,alpha+beta,alpha+gamma). +``` + +The inequality is coordinatewise. Monotonicity followed by concavity gives + +``` +F(X) >= (x/alpha)*F(M) + (1-x/alpha)*F(A) + >= min(F(M),F(A)). +``` + +Thus every X costs at least the cheapest candidate. Every candidate is itself +allowed, which proves equality. For the interval version, meets and joins of +subspaces between L and H remain between L and H. All four candidates are +therefore feasible, and the same argument applies. This completes the scoped +all-field proof; the finite checks below corroborate it. + +## Sharp scope boundaries + +All three terminal candidates are necessary when contact tariffs may differ, +by permuting a price that places sufficient weight on one contact. The median +can also be strictly necessary. For three distinct lines in `F2^2`, the median +zero frame has distances `(1,1,1)` and each terminal has a permutation of +`(0,2,2)`. With tariff `(phi(0),phi(1),phi(2))=(0,3,5)`, the median costs 9 +and every terminal costs 10. With tariff `(0,1,1)`, a terminal costs 2 and the +median costs 3. Neither a terminals-only nor a median-only rule suffices. + +Concavity matters. In `F2^4`, take + +``` +A=span(e1,e2), B=span(e3,e4), C=span(e1+e3,e2+e4). +phi_A(r)=5*r^2, phi_B(r)=phi_C(r)=r^2. +``` + +Here M is zero and the cheapest of the four candidates costs 28. The frame +`span(e1)` has distance vector `(1,3,3)` and costs 23. This explicit convex +counterexample prevents extending the rule to arbitrary increasing prices. + +The candidate set also depends on allowing unequal frame dimensions. If only +lines in `F2^2` are allowed, the zero median of three distinct lines is absent; +the linear-price minimum is 4 rather than the unrestricted minimum 3. These +lines are Lagrangian in the two-dimensional alternating space, so the theorem +cannot be transferred to Lagrangian-only charts by merely rescaling d. +No native Clifford tariff is identified with this schematic charge. + +## Finite evidence and reproduction + +From the repository root, using the standard library and CPython 3.12: + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B scripts/research_package.py --package research/subspace-three-contact-pricing +~/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -B research/subspace-three-contact-pricing/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -O -B research/subspace-three-contact-pricing/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/subspace-three-contact-pricing --check-source-history +``` + +The direct verifier is read-only and works without Git, network access or +predecessor files. `--emit` generates the deterministic receipt on stdout; +ordinary verification recomputes it and compares every field with +[RESULT.json](RESULT.json), including the hashes of all five other package +files. A receipt is generated from computation, never handwritten. +The metadata commands additionally check the contextual source pins in +[SOURCES.json](SOURCES.json); those sources are not runtime dependencies of +the mathematical verifier. + +The RREF enumeration includes every subspace of `F2^2`, `F2^3`, `F2^4`, +`F3^2` and `F3^3`. Vector-set addition constructs joins; vector-set intersection +constructs meets. For every unordered triple, the verifier checks the proposed +median and segment domination against every possible competing frame. Ordered +triples differ only by contact permutation, and independently varying all +three tariff tables covers these permutations. + +For direct optimum comparisons, tariffs have nonincreasing increments in +`{0,1,2}`. Every independent triple of such tables is tested. Equivalent +finite optimization problems with identical candidate vectors and identical +sets of attainable distance vectors are checked once. This lossless grouping +is reported explicitly, with exact transcript hashes. It is not a sampling +argument. The verifier also checks every common subspace interval in `F2^3`, +the strict candidate examples, the convex counterexample and invalid tariffs. +Across the five domains, this checks 57,361 unordered contact triples against +3,637,645 competing frames, then makes 388,002 exact optimum comparisons +after the stated signature grouping. The interval check adds 66 intervals, +1,462 contact triples and 15,802 competing frames. These are separate coverage +counts. +The written proof covers arbitrary dimensions, fields and admissible tariffs; +finite enumeration alone does not establish that universal statement. + +## Limits and implementation discipline + +This package supplies no new scalar word, native realization, profitable paid +consumer, compiler, ownership scheme, precision bound, physical tape cost, +supplier admission or multiplication exponent. It does not optimize a graph +with several variable frames. It does not assert that the actual native +rank of a Clifford transport equals d. Predecessor operators, source numbers +and the selected construction are cited context and are not replayed. +Independent human and formal proof-kernel review are unclaimed. + +The verifier has no recursion or dynamic code loading. Every loop is bounded +by the five fixed domains, at most 67 subspaces, 81 vectors, 15 tariffs per +contact and the corresponding finite products. Receipt reads are limited to +1 MiB per file. Functions stay within 60 physical lines. Checks use explicit +exceptions and survive optimized Python. Warning-strict normal and optimized +registered replays are the available recurring diagnostics; no repository +Python static analyzer is configured for this package. + +Power-of-Ten rule 3 deviation: CPython and its standard library allocate +managed objects during the exact enumeration. Replacing those allocations +requires a different runtime. The scope is this one bounded verifier; +geometry tables have at most 67 squared entries, there are at most 52,394 +contact triples per domain, and all tariff checks stream over fixed finite +products. Only distinct optimization signatures are retained. Both local +modes exercise these limits. A move to larger domains must establish new +capacity bounds before changing these guards. Runtime/library allocations +are not independently instrumented or claimed allocation-free. + +## Open next questions + +- Can a comparable finite candidate rule handle a four-contact junction in + this same schematic distance model? First inspect all quadruples in + `F2^3` and identify which extra distance vectors are essential. The + three-coordinate proof does not supply such a rule. +- Can a physical P104 frame operation realize a useful instance with these + exact prices? First name a literal carrier, its three contacts, all allowed + frames and a fully paid preparation/restoration word. The native realization + gap of PR #2844 remains a blocker; this local theorem does not close it. + +## Credit + +The new theorem application, exact optimization reduction and checker are +produced by Nick Petalas. Credit Chrisbryan17 / PR #2844 for the declared +schematic distance and signed-carrier context; Ali Romman / PR #1125, the +PR #968 frame-pair decoder contributors and Chrisbryan17 / PR #2820 for its +retained geometry lineage; Cinna Davis / PR #4447 and PR #4440/#4441, zxv, +Jacob Alan Sussman and the retained native/controller/bit/transfer contributors +for the separate span/intersection contact motivation. Their results and +credit lines are unchanged. New material is Apache-2.0. diff --git a/research/subspace-three-contact-pricing/RESULT.json b/research/subspace-three-contact-pricing/RESULT.json new file mode 100644 index 0000000000..3ea0e46fb6 --- /dev/null +++ b/research/subspace-three-contact-pricing/RESULT.json @@ -0,0 +1,106 @@ +{ + "binary_dimension_three_intervals": { + "contact_triples": 1462, + "frame_comparisons": 15802, + "intervals": 66 + }, + "claim_type": "scoped proof with finite corroboration", + "controls": { + "best_terminal_mild": 10, + "convex_counterexample": { + "four_candidate_price": 28, + "witness_price": 23 + }, + "essential_median": 9, + "essential_terminal": 2, + "fixed_dimension_counterexample": "three lines of F2^2 have no median within the lines", + "median_strong": 3, + "rejected_tariffs": [ + "decreasing", + "convex", + "negative", + "wrong_length" + ], + "weighted_terminal_prices": [ + 4, + 8, + 8, + 5 + ] + }, + "domains": [ + { + "all_frame_comparisons": 175, + "distinct_optimization_signatures": 11, + "exact_optimum_comparisons": 2376, + "independent_tariff_triples": 216, + "n": 2, + "optimum_transcript_sha256": "f41f3f32e67a024f9c98fbf6ad127b1c209cc61fe54aed83106d594bfb92721b", + "q": 2, + "segment_cases": 59, + "spaces": 5, + "tariffs_per_contact": 6, + "unordered_contact_triples": 35 + }, + { + "all_frame_comparisons": 13056, + "distinct_optimization_signatures": 33, + "exact_optimum_comparisons": 33000, + "independent_tariff_triples": 1000, + "n": 3, + "optimum_transcript_sha256": "d90aa9ebf8a29522c6616bce6083c484015b684acd546e7c31cabd37601fac8c", + "q": 2, + "segment_cases": 4020, + "spaces": 16, + "tariffs_per_contact": 10, + "unordered_contact_triples": 816 + }, + { + "all_frame_comparisons": 3510398, + "distinct_optimization_signatures": 94, + "exact_optimum_comparisons": 317250, + "independent_tariff_triples": 3375, + "n": 4, + "optimum_transcript_sha256": "65385ae570968a5b002f254cd768823222d11f4ee87dd76b7866629b490f97e1", + "q": 2, + "segment_cases": 795397, + "spaces": 67, + "tariffs_per_contact": 15, + "unordered_contact_triples": 52394 + }, + { + "all_frame_comparisons": 336, + "distinct_optimization_signatures": 11, + "exact_optimum_comparisons": 2376, + "independent_tariff_triples": 216, + "n": 2, + "optimum_transcript_sha256": "f41f3f32e67a024f9c98fbf6ad127b1c209cc61fe54aed83106d594bfb92721b", + "q": 3, + "segment_cases": 106, + "spaces": 6, + "tariffs_per_contact": 6, + "unordered_contact_triples": 56 + }, + { + "all_frame_comparisons": 113680, + "distinct_optimization_signatures": 33, + "exact_optimum_comparisons": 33000, + "independent_tariff_triples": 1000, + "n": 3, + "optimum_transcript_sha256": "d90aa9ebf8a29522c6616bce6083c484015b684acd546e7c31cabd37601fac8c", + "q": 3, + "segment_cases": 26132, + "spaces": 28, + "tariffs_per_contact": 10, + "unordered_contact_triples": 4060 + } + ], + "schema_version": 1, + "source_sha256": { + "README.md": "aa650555e3074e1ea599c833396253140d5684e4fb5fe92190a33d0d4e3acfa5", + "SOURCES.json": "8f324e4ec1292c398908366d2d02c9ea183e48f0658bcc7c702bc11f9b38c68c", + "TASK.json": "edd575936a1474c51a4499f2f9b603422c3aacc0ef2037a1f4264fc9f205a936", + "VERIFY.json": "fc5e48ac7f0ffc8f24a6379f6f31a05ccaacafb63892567b559bbc2008fc4d9d", + "verify.py": "a39f7a7e99ff851072b259ad28b5b5581244e34680f417e8b5e50fe309e50e97" + } +} diff --git a/research/subspace-three-contact-pricing/SOURCES.json b/research/subspace-three-contact-pricing/SOURCES.json new file mode 100644 index 0000000000..b525294822 --- /dev/null +++ b/research/subspace-three-contact-pricing/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/missing-join-frame/README.md", + "usage": "input", + "git_blob": "3de79ebc9badae792e4a0197b7083537a0bf6b9e", + "sha256": "b35f8ed70a3493056a37ab2b18bf55b2457c1e9411795aa5958f2323ee1d0439" + }, + { + "path": "research/p104-signed-mixed-carrier-bank/README.md", + "usage": "input", + "git_blob": "98688fbbe913da8e8bb0a5036d8f56bdad04f094", + "sha256": "80e5d89e311c8fa5bb0663ed4c031d109013c7ebc15c1c46955076e6da3ba64b" + } + ] +} diff --git a/research/subspace-three-contact-pricing/TASK.json b/research/subspace-three-contact-pricing/TASK.json new file mode 100644 index 0000000000..89144a37e5 --- /dev/null +++ b/research/subspace-three-contact-pricing/TASK.json @@ -0,0 +1,114 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact four-candidate optimization of a three-contact subspace frame under nonnegative nondecreasing concave distance tariffs, over every field and inside common subspace intervals.", + "scope_change_reason": "The open-ended original-work assignment excludes audits; PR2844 declares a concrete schematic distance model, while PR4447 motivates span/intersection contact closure. This is a self-contained local optimization side result rather than formalizing existing endpoint arithmetic.", + "bottleneck_link": "Exact local candidate reduction in the explicitly relaxed P104 frame-distance model; no native or supplier saving is inferred.", + "budget_minutes": 60, + "stop_rule": "Ship the first proved and exactly corroborated original local reduction; do not extend to four contacts or native synthesis.", + "outcome": "completed", + "evidence": "Written all-field proof; complete finite subspace and concave-tariff comparisons; source-bound generated RESULT.json.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does a finite candidate rule exist for four-contact junctions in this schematic metric?", + "why_it_matters": "Four incident transitions are outside the three-contact reduction.", + "first_step": "Enumerate quadruples of subspaces in F2^3 and characterize essential distance vectors.", + "blocked_by": "The one-depressed-coordinate argument is specific to three coordinates." + }, + { + "question": "Can a physical P104 carrier realize a useful instance with these exact tariffs?", + "why_it_matters": "A schematic optimum alone does not remove paid recursive work.", + "first_step": "Name a carrier and three literal contacts and price complete preparation and restoration.", + "blocked_by": "PR2844 leaves native realization, phases, ownership and complete consumer costs open." + } + ], + "claim_type": "scoped proof with finite corroboration", + "predecessors": [ + { + "pr": 2844, + "author": "Chrisbryan17", + "role": "Explicit schematic subspace distance, signed-carrier context and physical-realization boundary" + }, + { + "pr": 4447, + "author": "Cinna Davis", + "role": "Span/intersection contact catalogue motivation, not a source algorithm replay" + } + ] +} diff --git a/research/subspace-three-contact-pricing/VERIFY.json b/research/subspace-three-contact-pricing/VERIFY.json new file mode 100644 index 0000000000..b433ec33f3 --- /dev/null +++ b/research/subspace-three-contact-pricing/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/missing-join-frame/README.md", + "research/p104-signed-mixed-carrier-bank/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Exact full finite subspace enumeration, median/segment identities, exhaustive independent concave-price optima, common intervals, semantic controls and generated source-bound receipt." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Exact full finite subspace enumeration, median/segment identities, exhaustive independent concave-price optima, common intervals, semantic controls and generated source-bound receipt." + } + ] +} diff --git a/research/subspace-three-contact-pricing/verify.py b/research/subspace-three-contact-pricing/verify.py new file mode 100644 index 0000000000..1e5d9e626a --- /dev/null +++ b/research/subspace-three-contact-pricing/verify.py @@ -0,0 +1,277 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the scoped three-contact pricing theorem.""" +import argparse +import hashlib +import json +from itertools import combinations, combinations_with_replacement, product +from pathlib import Path + +ROOT = Path(__file__).resolve().parent +SOURCE_FILES = ('README.md', 'SOURCES.json', 'TASK.json', 'VERIFY.json', 'verify.py') + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def read_package_file(name): + path = ROOT / name + require(path.stat().st_size <= 1024 * 1024, 'package file exceeds 1 MiB') + return path.read_bytes() + + +def vector_add(a, b, q, n): + result, place = 0, 1 + for _ in range(n): + result += ((a % q + b % q) % q) * place + a, b, place = a // q, b // q, place * q + return result + + +def vector_scale(a, scalar, q, n): + result, place = 0, 1 + for _ in range(n): + result += ((a % q * scalar) % q) * place + a, place = a // q, place * q + return result + + +def members(mask, size): + return tuple(v for v in range(size) if (mask >> v) & 1) + + +def enumerate_spaces(q, n): + """All RREF bases, encoded independently as sets of actual vectors.""" + require(q in (2, 3) and 1 <= n <= (4 if q == 2 else 3), 'finite domain') + masks = set() + for rank in range(n + 1): + for pivots in combinations(range(n), rank): + free = tuple((i, j) for i, pivot in enumerate(pivots) + for j in range(pivot + 1, n) if j not in pivots) + for entries in product(range(q), repeat=len(free)): + rows = [q ** pivot for pivot in pivots] + for (i, j), value in zip(free, entries): + rows[i] += value * q ** j + mask = 0 + for coefficients in product(range(q), repeat=rank): + value = 0 + for row, coefficient in zip(rows, coefficients): + value = vector_add(value, vector_scale(row, coefficient, q, n), q, n) + mask |= 1 << value + require(mask.bit_count() == q ** rank, 'RREF independence') + require(mask not in masks, 'distinct RREF bases must give distinct subspaces') + masks.add(mask) + return tuple(sorted(masks)) + + +def geometry(q, n): + spaces = enumerate_spaces(q, n) + size = q ** n + index = {mask: i for i, mask in enumerate(spaces)} + dimension = {q ** d: d for d in range(n + 1)} + dims = tuple(dimension[mask.bit_count()] for mask in spaces) + vectors = tuple(members(mask, size) for mask in spaces) + meets, joins, distances = [], [], [] + for i, left in enumerate(spaces): + meet_row, join_row, distance_row = [], [], [] + for j, right in enumerate(spaces): + meet = index[left & right] + span = 0 + for a in vectors[i]: + for b in vectors[j]: + span |= 1 << vector_add(a, b, q, n) + meet_row.append(meet) + join_row.append(index[span]) + distance_row.append(dims[i] + dims[j] - 2 * dims[meet]) + meets.append(tuple(meet_row)) + joins.append(tuple(join_row)) + distances.append(tuple(distance_row)) + return spaces, tuple(meets), tuple(joins), tuple(distances) + + +def median(a, b, c, meets, joins): + return joins[joins[meets[a][b]][meets[b][c]]][meets[c][a]] + + +def branches(a, b, c, distances): + ab, bc, ca = distances[a][b], distances[b][c], distances[c][a] + require((ab + bc + ca) % 2 == 0, 'integer median radii') + return ((ab + ca - bc) // 2, (ab + bc - ca) // 2, (bc + ca - ab) // 2) + + +def domination(actual, radii): + """Return the median or one median-to-terminal segment dominated by actual.""" + depressed = tuple(i for i in range(3) if actual[i] < radii[i]) + require(len(depressed) <= 1, 'two depressed radii violate triangle inequality') + if not depressed: + return None + i = depressed[0] + delta = radii[i] - actual[i] + point = tuple(actual[i] if j == i else radii[j] + delta for j in range(3)) + require(all(point[j] <= actual[j] for j in range(3)), 'segment domination') + return i + + +def collect_domain(q, n): + spaces, meets, joins, distances = geometry(q, n) + signatures = set() + triples = comparisons = segments = 0 + for a, b, c in combinations_with_replacement(range(len(spaces)), 3): + contacts = (a, b, c) + radii = branches(a, b, c, distances) + m = median(a, b, c, meets, joins) + require(tuple(distances[m][v] for v in contacts) == radii, 'median identity') + attainable = set() + for x in range(len(spaces)): + actual = tuple(distances[x][v] for v in contacts) + segments += domination(actual, radii) is not None + attainable.add(actual) + comparisons += 1 + candidates = tuple(tuple(distances[x][v] for v in contacts) for x in (a, b, c, m)) + signatures.add((candidates, tuple(sorted(attainable)))) + triples += 1 + report = {'q': q, 'n': n, 'spaces': len(spaces), 'unordered_contact_triples': triples, + 'all_frame_comparisons': comparisons, 'segment_cases': segments, + 'distinct_optimization_signatures': len(signatures)} + return report, tuple(sorted(signatures)), (spaces, meets, joins, distances) + + +def tariffs(n): + result = [] + for increasing in combinations_with_replacement(range(3), n): + values = [0] + for increment in reversed(increasing): + values.append(values[-1] + increment) + result.append(tuple(values)) + return tuple(result) + + +def validate_tariff(values, n): + require(len(values) == n + 1 and all(type(v) is int and v >= 0 for v in values), + 'nonnegative integer tariff table') + steps = tuple(values[i + 1] - values[i] for i in range(n)) + require(all(step >= 0 for step in steps), 'nondecreasing tariff') + require(all(steps[i] >= steps[i + 1] for i in range(n - 1)), 'concave tariff') + + +def price(point, tables): + return sum(tables[i][point[i]] for i in range(3)) + + +def audit_prices(n, signatures): + tables = tariffs(n) + for table in tables: + validate_tariff(table, n) + checks = 0 + digest = hashlib.sha256() + for family in product(tables, repeat=3): + for candidates, attainable in signatures: + predicted = min(price(point, family) for point in candidates) + exhaustive = min(price(point, family) for point in attainable) + require(predicted == exhaustive, 'four-frame optimum differs from exhaustive search') + digest.update(f'{exhaustive},'.encode('ascii')) + checks += 1 + return {'tariffs_per_contact': len(tables), 'independent_tariff_triples': len(tables) ** 3, + 'exact_optimum_comparisons': checks, 'optimum_transcript_sha256': digest.hexdigest()} + + +def audit_intervals(data): + spaces, meets, joins, distances = data + intervals = triples = comparisons = 0 + for low, low_mask in enumerate(spaces): + for high, high_mask in enumerate(spaces): + if low_mask & high_mask != low_mask: + continue + allowed = tuple(i for i, mask in enumerate(spaces) + if low_mask & mask == low_mask and mask & high_mask == mask) + for a, b, c in combinations_with_replacement(allowed, 3): + m = median(a, b, c, meets, joins) + require(m in allowed, 'median left mandatory-subspace/cap interval') + radii = branches(a, b, c, distances) + require(tuple(distances[m][v] for v in (a, b, c)) == radii, 'interval radii') + for x in allowed: + domination(tuple(distances[x][v] for v in (a, b, c)), radii) + comparisons += 1 + triples += 1 + intervals += 1 + return {'intervals': intervals, 'contact_triples': triples, 'frame_comparisons': comparisons} + + +def controls(): + rejected = [] + for label, table in [('decreasing', (0, 2, 1)), ('convex', (0, 1, 4)), + ('negative', (0, -1, 0)), ('wrong_length', (0, 1))]: + try: + validate_tariff(table, 2) + except ValueError: + rejected.append(label) + else: + raise ValueError('invalid tariff accepted: ' + label) + # Three different lines in F2^2: both terminals and a median can be essential. + spaces, meets, joins, distances = geometry(2, 2) + a, b, c = (spaces.index(mask) for mask in (3, 5, 9)) + m = median(a, b, c, meets, joins) + points = tuple(tuple(distances[x][v] for v in (a, b, c)) for x in (a, b, c, m)) + mild = ((0, 3, 5),) * 3 + strong = ((0, 1, 1),) * 3 + require(price(points[3], mild) < min(price(p, mild) for p in points[:3]), 'median is essential') + require(min(price(p, strong) for p in points[:3]) < price(points[3], strong), 'terminal is essential') + weighted = ((0, 3, 6), (0, 1, 2), (0, 1, 2)) + weighted_prices = tuple(price(p, weighted) for p in points) + require(weighted_prices == (4, 8, 8, 5), 'a specified terminal can be uniquely optimal') + # Fixed-dimensional/Lagrangian frames exclude the zero median in this same fixture. + require(all(spaces[m].bit_count() != spaces[v].bit_count() for v in (a, b, c)), + 'fixed-dimension restriction must not be silently imposed') + # A concrete convex price is cheaper strictly between a median and a terminal. + spaces4, meets4, joins4, distances4 = geometry(2, 4) + contacts = tuple(spaces4.index(sum(1 << v for v in values)) for values in + ((0, 1, 2, 3), (0, 4, 8, 12), (0, 5, 10, 15))) + middle = median(*contacts, meets4, joins4) + convex = ((0, 5, 20, 45, 80), (0, 1, 4, 9, 16), (0, 1, 4, 9, 16)) + candidate_price = min(price(tuple(distances4[x][v] for v in contacts), convex) + for x in (*contacts, middle)) + witness = spaces4.index(3) + witness_price = price(tuple(distances4[witness][v] for v in contacts), convex) + require((witness_price, candidate_price) == (23, 28), 'convex counterexample') + return {'rejected_tariffs': rejected, 'essential_median': 9, 'best_terminal_mild': 10, + 'essential_terminal': 2, 'median_strong': 3, + 'weighted_terminal_prices': list(weighted_prices), + 'convex_counterexample': {'witness_price': witness_price, 'four_candidate_price': candidate_price}, + 'fixed_dimension_counterexample': 'three lines of F2^2 have no median within the lines'} + + +def result(): + reports = [] + interval_report = None + for q, n in ((2, 2), (2, 3), (2, 4), (3, 2), (3, 3)): + report, signatures, data = collect_domain(q, n) + report.update(audit_prices(n, signatures)) + reports.append(report) + if (q, n) == (2, 3): + interval_report = audit_intervals(data) + return {'schema_version': 1, 'claim_type': 'scoped proof with finite corroboration', + 'domains': reports, 'binary_dimension_three_intervals': interval_report, + 'controls': controls(), 'source_sha256': { + name: hashlib.sha256(read_package_file(name)).hexdigest() for name in SOURCE_FILES}} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--emit', action='store_true', help='emit a generated source-bound receipt to stdout') + args = parser.parse_args() + actual = result() + if args.emit: + print(json.dumps(actual, indent=2, sort_keys=True)) + return + expected = json.loads(read_package_file('RESULT.json')) + require(actual == expected, 'generated result or source hashes differ from RESULT.json') + print('PASS_THREE_CONTACT_PRICING ' + json.dumps({ + 'contact_triples': sum(d['unordered_contact_triples'] for d in actual['domains']), + 'frame_comparisons': sum(d['all_frame_comparisons'] for d in actual['domains']), + 'exact_optimum_comparisons': sum(d['exact_optimum_comparisons'] for d in actual['domains'])}, + sort_keys=True)) + + +if __name__ == '__main__': + main()