diff --git a/research/odd-cycle-query-capacity/PROOF.md b/research/odd-cycle-query-capacity/PROOF.md new file mode 100644 index 0000000000..5130e487b8 --- /dev/null +++ b/research/odd-cycle-query-capacity/PROOF.md @@ -0,0 +1,141 @@ +# Every unequal odd-cycle query mask + +JoyboyBrian, substantial OpenAI Codex assistance; Apache-2.0. Credit Tekalign +PR3362's C5 proof/interface, Nick Petalas PR4909's bipartite interface, and +classical finite linear-programming duality and capacitated matching methods. +No literature-priority claim is made for odd-cycle coding or matching. + +## Contract and exact answer + +Let n=2k+1, k>=2, and d_i be any nonnegative integers, S=sum d_i. Over any +field F take an S by S fitting matrix M with M_ii=I_(d_i), and M_ij=0 for +distinct nonadjacent vertices of C_n. The two allowed ordered blocks at every +edge are arbitrary rectangular matrices. They need not be symmetric, invertible, +commuting, or simultaneously diagonalizable. A zero-width block is empty. +Let alpha be the largest sum of d_i on an independent vertex set. Then + + min rank(M) = max(alpha, ceil(S/2)). (1) + +For linear query factorizations M=AB this is the exact minimum intermediate +field-coordinate dimension. It is not a native call count, physical COPY cost, +Gaussian rank, admitted supplier, or multiplication exponent. No assertion is +made about nonlinear encoders, changed zero masks, or a physical embedding of +these cycles inside the P112 geometry. + +## Lower bound for arbitrary directed blocks + +Factor M=AB through r=rank(M) dimensions. Let B_i be its i-th column block, +A_i its i-th row block, and U_i=im B_i. Because A_i B_i=I, B_i is injective, +dim U_i=d_i, and A_i is injective on U_i. Because both ordered forbidden blocks +are zero, A_i annihilates the sum of all nonneighbor U_j. Thus + + U_i intersect sum_(j nonadjacent to i, j!=i) U_j = 0. (2) + +For every independent set the U_i form a direct sum, by applying A_i to a +putative relation. Therefore r>=alpha. + +Put t_i=dim(U_i intersect U_(i+1)). The two subspaces U_i intersect U_(i-1) +and U_i intersect U_(i+1) lie in U_i and have zero intersection: i-1 and i+1 +are nonadjacent when n>=5. Hence + + t_(i-1)+t_i <= d_i; 2 sum_i t_i <= S. (3) + +For each i take J_i={i,i+1,i+3,i+5,...,i+2k-1} modulo n. The subgraph on +J_i consists of exactly the edge {i,i+1} and k-1 isolated vertices. Applying +each isolated A_j kills all the other subspaces. Their sum is therefore direct +with U_i+U_(i+1), so + + r >= sum_(j in J_i) d_j - t_i. + +Every vertex lies in exactly k+1 of these n rotated sets. Sum the inequalities +and use (3): + + n r >= (k+1) S - sum_i t_i >= (k+1/2) S = n S/2. + +Integer dimensions give r>=ceil(S/2), in every characteristic. This proves the +entire lower bound, including arbitrary noncommuting payload blocks. Finite +matrix tests are corroboration of this argument rather than its justification. + +## Exact integral sharing + +An edge count x_i>=0 reserves x_i distinct coordinates at both endpoints. +Private count p_i=d_i-x_(i-1)-x_i must be nonnegative. One shared coordinate +uses the rank-one all-ones two-by-two block; one private coordinate uses a +scalar identity. These disjoint groups fit the full ordered zero mask over every +field and have rank sum_i(x_i+p_i)=S-sum_i x_i. + +For completeness the needed cycle matching fact is proved here. Consider the +finite LP max sum_i x_i with x_i>=0 and x_(i-1)+x_i<=d_i. Its dual is min +sum_i d_i y_i with y_i>=0 and y_i+y_(i+1)>=1. Truncating y_i at one preserves +feasibility and cannot increase the objective. An extreme dual point is either +an integral vertex cover or all y_i=1/2. Indeed a proper component of fractional +vertices connected by active edge equalities is a path, whose alternating +plus/minus perturbation preserves all active equalities for a sufficiently small +amount; an endpoint cannot be pinned by an adjacent integral value without +becoming integral itself. Such a path is not extreme. If the component is the +whole odd cycle, its alternating equations force all values to one half. +Finite LP strong duality therefore gives the fractional optimum + + min(S-alpha, S/2). (4) + +Here integral covers have minimum weight S-alpha because their complements +are independent sets. To pass to integers, choose an extreme optimal primal +point. Any positive-support component that is a proper path has integer edge +values: a full-rank active system is solved from a zero edge/end or a tight +endpoint constraint and then successively along integer vertex capacities. +Equivalently the path incidence matrix has every nonsingular square minor +0 or +/-1 by removing a leaf. Fractionality can consequently occur only when +all n edges are positive and every vertex constraint is tight. The cyclic +system x_(i-1)+x_i=d_i has determinant two; any fractional solution has all +x_i integer-plus-one-half. Round x_0,x_2,...,x_(n-1) down and the intervening +edges up. Every vertex keeps its total except vertex 0, whose total drops by +one. Nonnegativity remains valid, and the objective loses exactly one half. +Thus the maximum *integral* sharing is + + min(S-alpha, floor(S/2)). (5) + +When (4) is integer, the fractional extreme case cannot be optimal: the sum of +an odd number of half-integers is a noninteger. This also covers zero widths +and zero total. Equations (5) and the channel construction attain (1). +The LP argument is a classical matching method, not a new general LP theorem. + +## Compressed deterministic construction + +The implementation does not call an LP solver or expand d_i coordinates. +Fix the closing edge x_(n-1)=t with 0<=t<=D=min(d_0,d_(n-1)). The remaining +capacities on endpoints are reduced by t. A path maximum matching is obtained +by saturating the leftmost remaining edge as far as possible and continuing. +An exchange proves this greedy rule: if an optimum uses fewer copies at the +left edge, an unused copy at its right endpoint can be taken directly, or one +copy on the next edge can be moved left without reducing the number of edges. +After fixing the left edge repeat on the shorter path. + +Let g(t)=t+the optimum path sharing. The capacitated path matching/cover dual +is integral, either by the leaf argument above or ordinary weighted bipartite +matching duality. Thus for integer t it equals the minimum of the path-cover +affine functions + + cover_weight + t*(1 - number_of_endpoints_in_cover). + +Those slopes are -1,0,1. The same LP expression on real t is concave, so g on +integers is discretely concave. Binary search for the first index satisfying +g(t)>=g(t+1) finds a maximum, including an arbitrary long flat plateau and +D=0. It uses at most 2 ceil(log2(D+1))+1 greedy path evaluations; each takes +O(n) integer operations and O(n) compressed integers. The maximum arithmetic +operand bit length is O(log(S+1)); source/target coordinate expansion and any +physical index/bit-operation costs are separate. `validate` checks every +coverage equation and exact answer, and emits a weighted independent witness using linear-space backpointer +reconstruction, without quadratic prefix-tuple copying. + +## Discriminating cases and stop + +Seven width-two vertices need seven query coordinates, rather than twice the +scalar optimum four. For d=(2,1,2,1,2,1,1), alpha=6 exceeds S/2=5; the actual +answer is six. For seven unit vertices alpha=3 but ceil(S/2)=4. Both terms +are essential. The C5 predecessor is recovered exactly, not claimed again. + +The proof closes this cycle-mask dimension contract. It does not fund copying, +dirty compensation/restoration, owner access, source coefficient preparation, +frames, hosting, stock, finite precision, physical tapes, compiler or outer +transfer. A new physical construction needs those contracts before another +implementation campaign. No selected frontier is changed. diff --git a/research/odd-cycle-query-capacity/README.md b/research/odd-cycle-query-capacity/README.md new file mode 100644 index 0000000000..55514f7ff0 --- /dev/null +++ b/research/odd-cycle-query-capacity/README.md @@ -0,0 +1,76 @@ +# Exact query capacity for every unequal odd cycle + +For every C_(2k+1), k>=2, arbitrary nonnegative payload widths d_i and every +field, the exact fitting rank is + + max(maximum independent-set payload weight, ceil(total payload/2)). + +Allowed ordered edge blocks may be rectangular, nonsymmetric and noncommuting. +[PROOF.md](PROOF.md) proves the all-field lower bound and an attaining integral +edge/private-channel factorization. The compressed deterministic constructor +uses O(n log(max(d)+2)) integer operations, without expanding payload coordinates. +This is a query-dimension contract, not a physical supplier or new kappa. + +Seven width-two payloads need seven coordinates, while two separate scalar +rank-four solutions would need eight. The unequal C7 (2,1,2,1,2,1,1) needs six +coordinates: its weight-six independent set is stronger than half-total five. +Seven unit payloads instead need four, stronger than independent-set weight three. + +## Scope and family decision + +This extends Tekalign #3362's C5 interface to all odd cycle lengths, alongside +Nick Petalas #4909's bipartite-mask result. It changes the mask class, retaining +the same complete ordered zero and identity-block contracts. All rotated +one-edge-plus-isolates subspaces establish the new general lower-bound step. +Classical matching, vertex-cover/LP and odd-cycle index-coding methods retain +credit; no literature priority or new general matching algorithm is claimed. +The bounded finite census does not establish the universal theorem by itself. + +Family decision: EXPAND once to close this exact mask contract, then STOP at +that result. No source-bound P112 realization is asserted. Physical reads, +copies, dirty restoration, frames, ownership, hosting, preparation, numerical +stock/precision, fixed tapes, compiler and outer recovery remain UNKNOWN. +A dimension optimum does not price them as free or improve the selected result. + +## Reproduction + +Use Python 3.12 and only its standard library: + +```sh +python3.12 -B scripts/research_package.py --package research/odd-cycle-query-capacity +python3.12 -I -O -B research/odd-cycle-query-capacity/verify.py +``` + +The read-only replay checks every width vector in {0,1,2,3}^5, {0,1,2}^7 +and {0,1}^9 against independently enumerated coordinate sharing and independent +sets. It checks all attaining matrix entries and ranks over GF(2), GF(3) and +GF(101), every directed binary scalar fitting matrix on C5/C7, malformed inputs, +underpaid/incorrect channel recipes and a forbidden ordered block. An eleven- +vertex fixture uses 4097-bit widths while retaining only O(n) integers. Exact +counts and the deterministic recipe digest are in [RESULT.json](RESULT.json). +An independent column-span implementation checks 288 directed rectangular-block +fitting matrices, all rotated subspace inequalities and a sharp seven-width-two +attainer with noncommuting allowed blocks. Source/receipt corruption must fail. Hosted CI and independent mathematical +acceptance are not asserted here. + +Canonical base bee95ce88f9f19802f0613f92838895cd0e14a1f, priority revision 7, +selected conditional kappa 0.00302015 unchanged. Initial overlap covered 310 +open PRs, 4096 Discussion records and all 6690 tracked package notes, with +reported complete inventories; absence of a match is not proof of novelty. +The canonical investigation is Discussion #1587. Exact predecessor bytes and +the original card are retained in SOURCES.json and TASK.json. + +## Open next questions + +1. Determine a named triangle-free mask with overlapping odd cycles for which + arbitrary fitting blocks improve on integral coordinate pairing. First + compare its rank-factor subspace constraints with its complete edge-sharing + LP; no physical decoder should be assumed. +2. Exhibit an actual recursive caller whose admitted ordered read mask is one + of these longer odd cycles, with all query/source/copy and cleanup costs. + A geometric/matching realization and complete consumer tariff are blockers. + +Credit Tekalign #3362, Sagar Thakrar #2484, ywz65 #2471, Nick Petalas #4909, +Cinna Davis, Adam Gall, ctoth, Philippe Van Velzen and the retained P112/native +lineage. New scoped proof, constructor and checks: JoyboyBrian, with substantial +OpenAI Codex assistance. Apache-2.0. No human or proof-kernel review claimed. diff --git a/research/odd-cycle-query-capacity/RESULT.json b/research/odd-cycle-query-capacity/RESULT.json new file mode 100644 index 0000000000..2ad741b8dd --- /dev/null +++ b/research/odd-cycle-query-capacity/RESULT.json @@ -0,0 +1,294 @@ +{ + "binary_completions": [ + { + "histogram": { + "3": 45, + "4": 537, + "5": 442 + }, + "length": 5, + "matrices": 1024, + "minimum": 3 + }, + { + "histogram": { + "4": 49, + "5": 2226, + "6": 9235, + "7": 4874 + }, + "length": 7, + "matrices": 16384, + "minimum": 4 + } + ], + "controls": [ + "invalid dimensions rejected", + "invalid dimensions rejected", + "invalid dimensions rejected", + "invalid dimensions rejected", + "invalid dimensions rejected", + "invalid dimensions rejected", + "omitted shared channel", + "unpaid rank", + "bool channel", + "false independent witness", + "forbidden directed block" + ], + "field_rank_checks": 11169, + "fixtures": [ + { + "alpha": 6, + "dimensions": [ + 2, + 1, + 2, + 1, + 2, + 1, + 1 + ], + "edge": [ + 1, + 0, + 1, + 0, + 1, + 0, + 1 + ], + "independent": [ + 0, + 2, + 4 + ], + "path_evaluations": 3, + "private": [ + 0, + 0, + 1, + 0, + 1, + 0, + 0 + ], + "rank": 6 + }, + { + "alpha": 6, + "dimensions": [ + 2, + 2, + 2, + 2, + 2, + 2, + 2 + ], + "edge": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "independent": [ + 1, + 3, + 5 + ], + "path_evaluations": 5, + "private": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "rank": 7 + }, + { + "alpha": 3, + "dimensions": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "edge": [ + 1, + 0, + 1, + 0, + 1, + 0, + 0 + ], + "independent": [ + 1, + 3, + 5 + ], + "path_evaluations": 3, + "private": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1 + ], + "rank": 4 + }, + { + "alpha": 102, + "dimensions": [ + 100, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "edge": [ + 1, + 0, + 1, + 0, + 1, + 0, + 1 + ], + "independent": [ + 0, + 2, + 4 + ], + "path_evaluations": 3, + "private": [ + 98, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "rank": 102 + }, + { + "alpha": 10, + "dimensions": [ + 0, + 2, + 0, + 3, + 1, + 0, + 4, + 0, + 1 + ], + "edge": [ + 0, + 0, + 0, + 1, + 0, + 0, + 0, + 0, + 0 + ], + "independent": [ + 1, + 3, + 6, + 8 + ], + "path_evaluations": 1, + "private": [ + 0, + 2, + 0, + 2, + 0, + 0, + 4, + 0, + 1 + ], + "rank": 10 + } + ], + "large": { + "length": 11, + "path_evaluations": 8193, + "rank_bits": 4099, + "width_bits": 4097 + }, + "live_inputs": 4, + "recipe_sha256": "a184c90a400006e189a1e22d7f842418f89736d4b3f1001cda4d196c9b11e1f0", + "scope": "All-field proof with finite corroboration; query dimension only, no physical supplier or kappa.", + "status": "PASS_ODD_CYCLE_QUERY_CAPACITY", + "subspace": { + "cases": 288, + "noncommuting_blocks": [ + [ + [ + 1, + 0 + ], + [ + 0, + 0 + ] + ], + [ + [ + 0, + 0 + ], + [ + 1, + 0 + ] + ] + ], + "sha256": "3c069361c7d7204197f841b4b49d00b7c765188587da6a04f0e72573b77ed31b", + "sharp": { + "cuts": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "field": 101, + "intersections": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "length": 7, + "rank": 7, + "total": 14 + } + }, + "width_cases": 3723 +} diff --git a/research/odd-cycle-query-capacity/SOURCES.json b/research/odd-cycle-query-capacity/SOURCES.json new file mode 100644 index 0000000000..66438ed69c --- /dev/null +++ b/research/odd-cycle-query-capacity/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "bee95ce88f9f19802f0613f92838895cd0e14a1f", + "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/bipartite-query-capacity/README.md", + "usage": "input", + "git_blob": "6f233535ea861fbda9c93da23cd07c3b4ea87146", + "sha256": "6631ce35debbe51bb991d27eac4c609901f79ee4eefb95fa1673aa6b2f7cd56d" + }, + { + "path": "research/unequal-cycle-payloads/PROOF.md", + "usage": "input", + "git_blob": "e407a81af930a1b218f899f244edb303547f3d5c", + "sha256": "684d0281bd0308a6c3eeea602b0d6ac4e35a66a0ff740e3aeb6d5d2309805753" + }, + { + "path": "research/unequal-cycle-payloads/README.md", + "usage": "input", + "git_blob": "8e1e01bb308b7a9147847446a7070b0c7bb9f354", + "sha256": "834cd8c46c3893962afe96bdf13eccf21f698fcf26e8fe0ac3c9efd1cea1e4c4" + }, + { + "path": "research/unequal-cycle-payloads/cycle.py", + "usage": "input", + "git_blob": "4ea7ecc07fd86209e9cbae83402d9d252311016c", + "sha256": "a95fbd2e27951d47abca16793f64a3eb9ed13c4bb68b32d48babd5459527d976" + } + ] +} diff --git a/research/odd-cycle-query-capacity/TASK.json b/research/odd-cycle-query-capacity/TASK.json new file mode 100644 index 0000000000..fc8b5ce2fb --- /dev/null +++ b/research/odd-cycle-query-capacity/TASK.json @@ -0,0 +1,79 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 7, + "base_commit": "bee95ce88f9f19802f0613f92838895cd0e14a1f", + "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": "Exact all-field unequal-payload query capacity for every odd cycle with compressed attaining constructor", + "scope_change_reason": "Extend PR3362 C5 and PR4909 bipartite mask contracts to every odd length; fixed geometry and physical tariffs remain outside scope", + "bottleneck_link": "A precise query-dimension bound determines whether mixing can beat coordinate pairing under this changed ordered read mask", + "budget_minutes": 60, + "stop_rule": "Stop at the exact cycle contract; no automatic physical implementation expansion", + "outcome": "completed", + "evidence": "PROOF.md and RESULT.json; independent edge/subset enumeration, matrix ranks and all directed binary C5/C7 fits", + "author": "JoyboyBrian", + "ai_assistance": "Substantial OpenAI Codex assistance; parallel research and independent proof/code review; no independent human acceptance", + "open_questions": [ + { + "question": "Can a named triangle-free mask with overlapping odd cycles beat integral coordinate pairing?", + "why_it_matters": "The local Count/linear query interface alone cannot admit the recursive supplier", + "first_step": "Derive its subspace lower bound and compare the complete edge-sharing optimum", + "blocked_by": "A named changed mask and complete ordered-block contract" + } + ], + "overlap": { + "open_prs": 310, + "discussions": 4096, + "local_notes": 6690, + "complete_pagination": true, + "limits": "Arbitrary diffs, unindexed prose and unpublished work may overlap." + } +} diff --git a/research/odd-cycle-query-capacity/VERIFY.json b/research/odd-cycle-query-capacity/VERIFY.json new file mode 100644 index 0000000000..58223429e8 --- /dev/null +++ b/research/odd-cycle-query-capacity/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bipartite-query-capacity/README.md", + "research/unequal-cycle-payloads/PROOF.md", + "research/unequal-cycle-payloads/README.md", + "research/unequal-cycle-payloads/cycle.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 90, + "checks": "Independent bounded edge/subset enumeration, full directed C5/C7 binary completions, exact attaining ranks over three fields and rejection controls" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 90, + "checks": "Same complete finite domains under optimization" + } + ] +} diff --git a/research/odd-cycle-query-capacity/cycle.py b/research/odd-cycle-query-capacity/cycle.py new file mode 100644 index 0000000000..9eb0162afb --- /dev/null +++ b/research/odd-cycle-query-capacity/cycle.py @@ -0,0 +1,81 @@ +"""Compressed exact query factorization for every unequal odd-cycle mask. + +JoyboyBrian; substantial OpenAI Codex assistance. Apache-2.0. +Credit Tekalign PR3362 and classical matching/vertex-cover methods. +""" + +def need(ok,message): + if not ok: raise ValueError(message) + +def dimensions(values): + need(type(values) in (list,tuple) and len(values)>=5 and len(values)%2==1, + 'odd cycle length at least five') + need(all(type(x) is int and x>=0 for x in values),'nonnegative integer widths') + return tuple(values) + +def independent(values): + d=dimensions(values) + def path(start,stop): + weights=[0,0];taken=[] + for i in range(start,stop): + take=weights[-2]+d[i] + taken.append(take>weights[-1]) + weights.append(max(weights[-1],take)) + witness=[];j=stop-start-1 + while j>=0: + if taken[j]:witness.append(start+j);j-=2 + else:j-=1 + return weights[-1],tuple(reversed(witness)) + omitted=path(1,len(d));weight,vertices=path(2,len(d)-1) + included=(weight+d[0],(0,)+vertices) + return max(omitted,included) + +def minimum(values): + d=dimensions(values) + return max(independent(d)[0],(sum(d)+1)//2) + +def construct(values): + """Use logarithmically many greedy path matchings; never expand widths.""" + d=dimensions(values);n=len(d) + def path(t): + capacity=list(d);capacity[0]-=t;capacity[-1]-=t + edge=[0]*n;edge[-1]=t + for i in range(n-1): + edge[i]=min(capacity[i],capacity[i+1]) + capacity[i]-=edge[i];capacity[i+1]-=edge[i] + return sum(edge),edge,capacity + low,high=0,min(d[0],d[-1]);evaluations=0 + while low=0 for x in edge+private),'integer channel counts') + need(all(edge[i-1]+edge[i]+private[i]==d[i]for i in range(n)), + 'complete disjoint coordinate coverage') + need(type(recipe['rank']) is int and recipe['rank']==sum(edge)+sum(private)==minimum(d), + 'sharp complete query capacity') + witness=recipe['independent'] + need(type(witness) is list and all(type(i) is int and 0<=i=(k+1)*s-sum(intersections) and 2*sum(intersections)<=s, + 'summed rotated rank inequality') + return dict(length=n,field=q,total=s,rank=r,intersections=intersections,cuts=cuts) diff --git a/research/odd-cycle-query-capacity/verify.py b/research/odd-cycle-query-capacity/verify.py new file mode 100644 index 0000000000..d4e13156b6 --- /dev/null +++ b/research/odd-cycle-query-capacity/verify.py @@ -0,0 +1,148 @@ +#!/usr/bin/env python3 +"""Independent bounded corroboration of the all-field odd-cycle proof.""" +import argparse,copy,hashlib,itertools,json,sys +from functools import lru_cache +from pathlib import Path +HERE=Path(__file__).resolve().parent;ROOT=HERE.parents[1] +sys.path.insert(0,str(HERE)) +from cycle import construct,minimum,validate +from subspace import audit +def need(ok,message): + if not ok:raise ValueError(message) +def authenticate(): + rows=json.loads((HERE/'SOURCES.json').read_text())['files'] + for row in rows: + if row['usage']=='input': + need(hashlib.sha256((ROOT/row['path']).read_bytes()).hexdigest()==row['sha256'], + 'source hash '+row['path']) + return sum(x['usage']=='input'for x in rows) +def brute_alpha(d): + n=len(d) + return max(sum(d[i]for i in range(n)if mask>>i&1)for mask in range(1<>i&1 and mask>>((i+1)%n)&1)for i in range(n))) +def brute_sharing(d): + n=len(d) + @lru_cache(None) + def extend(i,previous,first): + if i==n-1:return 0 if previous+first<=d[-1]else -10**9 + return max(x+extend(i+1,x,first)for x in range(min(d[i]-previous,d[i+1])+1)) + return max(x+extend(0,x,x) for x in range(min(d[0],d[-1])+1)) +def matrix(recipe): + d=recipe['dimensions'];n=len(d);offset=[sum(d[:i])for i in range(n)] + used=[0]*n;groups=[] + for i,count in enumerate(recipe['edge']): + j=(i+1)%n + for _ in range(count): + groups.append((offset[i]+used[i],offset[j]+used[j]));used[i]+=1;used[j]+=1 + for i,count in enumerate(recipe['private']): + for _ in range(count):groups.append((offset[i]+used[i],));used[i]+=1 + need(used==d,'independent coordinate partition') + out=[[0]*sum(d)for _ in range(sum(d))] + for group in groups: + for i in group: + for j in group:out[i][j]=1 + return out + +def fits(a,d): + owner=[i for i,x in enumerate(d)for _ in range(x)];n=len(d);s=sum(d) + need(len(a)==s and all(len(row)==s for row in a),'full fitting shape') + for i in range(s): + for j in range(s): + x,y=owner[i],owner[j] + if x==y or (x-y)%n not in(1,n-1):need(a[i][j]==int(i==j),'complete ordered fitting mask') +def rank(a,q): + a=[[x%q for x in row]for row in a];r=0 + for c in range(len(a)): + pivot=next((i for i in range(r,len(a))if a[i][c]),None) + if pivot is None:continue + a[r],a[pivot]=a[pivot],a[r];scale=pow(a[r][c],-1,q) + a[r]=[v*scale%q for v in a[r]] + for i in range(r+1,len(a)): + factor=a[i][c] + if factor:a[i]=[(x-factor*y)%q for x,y in zip(a[i],a[r])] + r+=1 + return r + +def binary_rank(rows): + pivots={} + for row in rows: + while row: + bit=row.bit_length()-1 + if bit not in pivots:pivots[bit]=row;break + row^=pivots[bit] + return len(pivots) +def run(): + inputs=authenticate();cases=0;field_checks=0;digest=hashlib.sha256() + fixtures=[] + for n,limit in [(5,3),(7,2),(9,1)]: + for d in itertools.product(range(limit+1),repeat=n): + recipe=construct(d);alpha=brute_alpha(d);sharing=brute_sharing(d) + need(recipe['alpha']==alpha and recipe['rank']==sum(d)-sharing, + 'independent subset/edge enumeration') + need(recipe['rank']==max(alpha,(sum(d)+1)//2),'exact capacity formula') + a=matrix(recipe);fits(a,d) + for q in (2,3,101):need(rank(a,q)==recipe['rank'],'attaining field rank');field_checks+=1 + digest.update(json.dumps(recipe,sort_keys=True,separators=(',',':')).encode());cases+=1 + completions=[] + for n in(5,7): + best=n;hist={} + for bits in range(1<<(2*n)): + rows=[(1<>(2*i))&1)<<((i-1)%n))| + (((bits>>(2*i+1))&1)<<((i+1)%n))for i in range(n)] + r=binary_rank(rows);need(r>=(n+1)//2,'all directed binary fitting completions') + best=min(best,r);hist[r]=hist.get(r,0)+1 + need(best==(n+1)//2,'scalar sharp rank') + completions.append(dict(length=n,matrices=1<<(2*n),minimum=best,histogram=hist)) + for d in [(2,1,2,1,2,1,1),(2,2,2,2,2,2,2),(1,1,1,1,1,1,1), + (100,1,1,1,1,1,1),(0,2,0,3,1,0,4,0,1)]: + fixtures.append(construct(d)) + huge=[(1<<4096)+i for i in range(11)];large=construct(huge) + need(large['path_evaluations']<=2*4097+1,'logarithmic compressed search') + span_digest=hashlib.sha256();span_cases=0 + for n in(5,7,9): + for q in(2,3,101): + for seed in range(32): + d=[(seed+2*i+i*i)%3 for i in range(n)] + owner=[i for i,width in enumerate(d)for _ in range(width)] + a=[[int(i==j)if x==y else ((seed+17*i+31*j)%q if (x-y)%n in(1,n-1)else 0) + for j,y in enumerate(owner)]for i,x in enumerate(owner)] + fits(a,d);witness=audit(a,d,q) + need(witness['rank']==rank(a,q),'independent column/row elimination') + span_digest.update(json.dumps(witness,sort_keys=True).encode());span_cases+=1 + sharp=construct([2]*7);sharp_matrix=matrix(sharp);sharp_span=audit(sharp_matrix,[2]*7,101) + need(sharp_span['rank']==7 and sharp_span['intersections']==[1]*7 and + sharp_span['cuts']==[7]*7,'every subspace bound is attained') + # Actual allowed 2x2 blocks can fail to commute even in a sharp attainer. + x=[[sharp_matrix[i][2+j]for j in range(2)]for i in range(2)] + y=[[sharp_matrix[2+i][4+j]for j in range(2)]for i in range(2)] + product=lambda a,b:[[sum(a[i][h]*b[h][j]for h in range(2))for j in range(2)]for i in range(2)] + need(product(x,y)!=product(y,x),'noncommuting permitted block fixture') + controls=[] + for bad in [[],[1]*3,[1]*6,[True]*5,[1,-1,1,1,1],[1.0]*5]: + try:construct(bad) + except ValueError:controls.append('invalid dimensions rejected') + else:raise ValueError('invalid dimensions accepted') + good=construct([2]*7) + for name,mutate in [('omitted shared channel',lambda r:r['edge'].__setitem__(0,r['edge'][0]+1)), + ('unpaid rank',lambda r:r.__setitem__('rank',r['rank']-1)), + ('bool channel',lambda r:r['private'].__setitem__(0,False)), + ('false independent witness',lambda r:r.__setitem__('independent',[0,1]))]: + bad=copy.deepcopy(good);mutate(bad) + try:validate(bad) + except ValueError:controls.append(name) + else:raise ValueError('mutant accepted '+name) + a=matrix(good);a[0][4]=1 + try:fits(a,good['dimensions']) + except ValueError:controls.append('forbidden directed block') + else:raise ValueError('forbidden directed block accepted') + return dict(status='PASS_ODD_CYCLE_QUERY_CAPACITY',live_inputs=inputs,width_cases=cases, + field_rank_checks=field_checks,recipe_sha256=digest.hexdigest(),binary_completions=completions, + fixtures=fixtures,subspace=dict(cases=span_cases,sha256=span_digest.hexdigest(),sharp=sharp_span,noncommuting_blocks=[x,y]),large=dict(length=11,width_bits=4097,rank_bits=large['rank'].bit_length(), + path_evaluations=large['path_evaluations']),controls=controls, + scope='All-field proof with finite corroboration; query dimension only, no physical supplier or kappa.') +def main(): + parser=argparse.ArgumentParser();parser.add_argument('--write',action='store_true');a=parser.parse_args();result=run() + if a.write:(HERE/'RESULT.json').write_text(json.dumps(result,indent=2,sort_keys=True)+'\n') + else:need(json.dumps(json.loads((HERE/'RESULT.json').read_text()),sort_keys=True)==json.dumps(result,sort_keys=True),'typed deterministic receipt') + print(result['status']) +if __name__=='__main__':main()