diff --git a/research/connector-chart-rank-repair/PROOF.md b/research/connector-chart-rank-repair/PROOF.md new file mode 100644 index 0000000000..5073f44b65 --- /dev/null +++ b/research/connector-chart-rank-repair/PROOF.md @@ -0,0 +1,146 @@ +# Minimum source repair for a changed connector chart + +Let B0,B1:X->Z be linear maps over any field, with finite dimensions n,m. +Let U,V be their row spaces in X*, with dimensions r0,r1 and intersection +dimension c. A chart is an arbitrary invertible linear map R:Z->Z. The +residual source correction is Delta=B1-R B0. Then + + min_(R invertible) rank(Delta) = max(r0,r1)-c. (1) + +This is a rank statement, not a minimum scalar circuit cost or a theorem +about a restricted native chart alphabet. The familiar equal-kernel criterion +in the credited predecessor is exactly the zero-residual case. The new +interface permits and charges the residual when kernels differ. + +## Lower bound + +The row space of R B0 is U. Modulo V, its rows equal the negatives of the +rows of Delta; therefore the image of row(Delta) in X*/V contains the image +of U, which has dimension r0-c. Likewise modulo U the rows of Delta project +onto the image of V, of dimension r1-c. Hence rank(Delta) is at least both +r0-c and r1-c, proving the lower bound in (1). + +This does not merely count unequal ranks. Two equal-rank maps can have +different row spaces and a positive minimum. For example the two rank-one +functionals x0 and x1 need one independent correction. + +## Attaining chart + +Choose a basis S of U intersect V, extend it by A to a basis of U, and by B +to a basis of V. The union S,A,B is independent: a relation between A and B +would put their common combination in U intersect V, contradicting either +extension. Choose invertible row-operation matrices Q0,Q1 taking B0,B1 to + + Q0 B0 = [S; A; 0], Q1 B1 = [S; B; 0]. + +Their common S rows occupy the first c positions; pair the exclusive rows in +the following positions, padding the shorter list with zeros. Set +R=Q1^-1 Q0. Then + + Q1 Delta = [0; B-A; unmatched rows; 0]. + +There are max(r0-c,r1-c) nonzero rows and they are independent by the +independence of S,A,B. Since Q1 is invertible, Delta attains (1). The same +argument covers zero maps, zero source dimension, full rank and unequal ranks. +It uses no generic-position, infinite-field or characteristic assumption. + +The binary constructor implements this argument by tracked elimination. It +extracts the common row basis from relations among independent bases of U,V, +extends that basis in each row space, solves for its preimages in the original +rows and appends the full relation basis. These preimages plus the relation +basis form the invertible Q matrices. The finite oracle independently forms +actual GL3 orbits rather than trusting the constructed R. + +More generally, consider any finite internal transport composed only of +invertible charts and additive source injections C_j x, with no intervening +output observation or source mutation. Its endpoint has the form R z+E x; +E is a sum of invertibly transported C_j. Thus rank(E)<=sum rank(C_j). +If it carries B0 x to B1 x, E=B1-R B0, so the same quantity in (1) lower-bounds +the **total injected rank**. One residual injection attains it. This statement +does not price the charts or the implementation of an injection. + +## Dirty endpoint and compulsory restoration + +Let x,z,y0,y1 be distinct arbitrary input rows, x immutable. A0,A1 are fixed +linear readers and can be singular, noncommuting and different. Complete +queries preserve every other row, private scratch and required head positions; +their increment is independent of the old target. Reserve z throughout. +For general characteristic execute, chronologically: + + y0 -= A0 z + z += B0 x + y0 += A0 z # first output delivered; never changed again + z = R z + z += Delta x # one paid source correction + y1 += A1 z + z -= B1 x + y1 -= A1 z # second output delivered + z = R^-1 z + +After the first delivery z=z_initial+B0 x. Chart plus correction makes it +R z_initial+B1 x. The second read/close/read adds A1 B1 x to y1 and leaves +z=R z_initial. The final inverse restores z exactly. Thus both outputs receive +their desired increments and all source/connector dirt restores. Nothing +requires R to fix the initial dirt. The source correction is cancelled by +the actual B1 close; it is not an unpaid obligation deferred to a consumer. +Reversing the word and inverting each complete operation gives its inverse. + +## Complete comparison and what rank does not buy + +For sign-symmetric complete query prices, or upper bounds valid in either +orientation, the two separately closed echoes cost + + C_closed = I0+P0+D0 + 2(c_B0+c_B1+c_A0+c_A1). + +The transported pair costs + + C_repair = I1+P1+D1 + c_B0+c_B1+2(c_A0+c_A1) + + c_R+c_Rinv+c_Delta. + +I,P,D charge admission/layout/reservation, preparation/synthesis and remaining +instruction/control work. Each complete c includes its real source/coefficient +access, arithmetic, scratch restoration, routing, frame obligations and heads. +For asymmetric signs or ports, sum the actual word prices instead. A saving +requires + + c_R+c_Rinv+c_Delta + (I1+P1+D1-I0-P0-D0) < c_B0+c_B1. + +A rank-r factorization Delta=UV does **not** implement U(Vx) for free. +Its observations, intermediate storage, dirty cancellation and restoration +must be included in c_Delta. Likewise arbitrary invertible R in (1) is a +mathematical search domain, not a free physical gate. Rank-minimizing R can +lose at actual tariffs; the receipt includes an explicit contrary tariff. + +The binary pilot uses B0=(7,6,1), B1=(1,6,5), R=(3,2,4), with bit j denoting +column j in each row. Delta=(0,0,4), a single source-coordinate XOR into the +third connector coordinate. The map ranks are2 and3, c=2, so this rank1 repair +is minimal. The identity chart leaves rank2. R and R^-1 are each the one-XOR +shear z0+=z1. With identity readers, all required source/read/chart/correction +operations are literally emitted:26 XORs versus34 for the separately closed +queries. There are no additional rows. The full4096 dirty states and inverses +pass, with first-output delivery checked at its actual cut. + +This is a fixed-call comparison. Opening the matrices and directly updating +the two outputs uses only11 XORs; that excluded-alphabet control is retained +and prevents a claim of general circuit optimality. The pilot therefore +demonstrates a complete adapter identity and price, not a practical optimizer. +Its same scalar gates act independently on length-L coordinate blocks, giving +26L versus34L scalar XORs; physical instruction/address costs still need a +backend. The fixed-port one-bit tariff explicitly counts movement plus five +units per XOR, matching the predecessor convention, without claiming a native +Turing-machine implementation. + +## Revision-5 expansion decision + +Declared milestone: **local module**. Retain the rank criterion and restored +adapter; narrow work to this single proof and discriminating example. General +native chart/repair prices, selected ownership, precision and a selected caller +remain unknown, not zero. Do not start a dependent optimization round until a +pinned caller supplies a strict complete allowance and legal connector lifetime. +The exact scope/boundary/cost ledger and reopening condition are in TASK.json. + +Credit woklerx's retained equal-kernel chart interface, Ross Richardson's PR943 +dirty-query accounting and the elementary row-space method. No priority claim +is made for rank inequalities or change of basis. The contribution is their +source-pinned residual-repair interface and executable evidence. Prepared by +ywz65 with substantial OpenAI Codex assistance; Apache-2.0. diff --git a/research/connector-chart-rank-repair/README.md b/research/connector-chart-rank-repair/README.md new file mode 100644 index 0000000000..298bf702a4 --- /dev/null +++ b/research/connector-chart-rank-repair/README.md @@ -0,0 +1,109 @@ +# Exact rank of a paid connector chart repair + +The retained dirty connector chart interface can move B0 x to B1 x without +another source observation exactly when the two maps have the same kernel. +This package permits a **paid residual source injection** Delta x and determines +its minimum rank: + + min_(R invertible) rank(B1-R B0) + = max(rank B0,rank B1) - dim(row B0 intersect row B1). + +The theorem holds over every field, including singular and unequal-rank maps. +A constructive change-of-basis proof supplies R and Delta. The same quantity +lower-bounds the total injected rank of any internal sequence of invertible +charts and additive source corrections without intermediate observations. +It does not minimize chart cost, scalar work or a physical native tariff. + +This extends woklerx's [equal-kernel chart criterion](../dirty-connector-chart-transport/README.md) +within Ross Richardson's [dirty-query model](../universal-connector-boundary/README.md). +Their boundary contracts, cancellation and price conventions retain credit. +The contribution is the residual-rank interface, its constructive certificate +and the restored/charged example; no novelty claim is made for elementary +row-space inequalities or change of basis. + +## Complete dirty-state example + +Read matrix rows as binary masks: + + B0=(7,6,1), B1=(1,6,5), R=(3,2,4), Delta=(0,0,4). + +The paid chart is z0+=z1 and its inverse is the same shear. The correction +is one XOR from source coordinate2 into connector coordinate2. It has rank1, +the proved minimum; the identity chart would leave rank2. Four distinct +three-bit rows x,z,y0,y1 are all arbitrary. Every source, chart, readout, +correction and final inverse is emitted explicitly; no extra row is needed. + +| Fixed one-bit implementation | XORs | Reads | Writes | Head moves | Declared tariff | +|---|---:|---:|---:|---:|---:| +| Two closed queries |34|68|34|444|614| +| Repaired chart pair |26|52|26|368|498| +| Direct matrices, outside this query alphabet |11|22|11|204|259| + +The tariff puts the12 bits at consecutive positions, starts/returns the data +head one cell before bit0, and charges `2*(max(source,target)+1)+5` for each +scalar XOR. Its five units are two reads, one write, XOR and dispatch. This +declared interpreter tariff is not a native tape-compiler certificate. +The11-gate direct control is deliberately retained:26 is **not** a minimum +over arbitrary circuits. No selected caller is claimed to need this alphabet. + +The first output is delivered before the chart change and never rewritten. +After the paid correction the connector is R z_initial+B1 x. The second +read/close/read cancels the charted dirt, and the final R inverse restores the +actual connector. The source correction is cancelled by the closing B1 call; +it is not deferred to a later consumer. [PROOF.md](PROOF.md) gives the exact +word over general characteristic and the full comparison, including admission, +preparation, instruction work and complete prices of all child operations. + +## Reproduce + +```sh +python3.12 scripts/research_package.py --package research/connector-chart-rank-repair +python -I -O -B research/connector-chart-rank-repair/verify.py +``` + +The external finite oracle enumerates all168 GL3 charts and their complete +orbits, then checks every262,144 pair of binary3-by-3 maps. It agrees with the +formula's minimum-rank histogram `0:40916, 1:187376, 2:33516, 3:336`. +The independent constructive method emits8,192 charts across all16 row-space +classes and512 destinations. No predecessor executable is imported. + +All4,096 dirty pilot inputs, literal inverses and first-output cuts pass. +Four altered programs fail semantically. A separate ordinary-matrix control +over F3 checks6,561 arbitrary dirty banks and inverses with noncommuting +readers, and rejects the wrong closing sign. Zero maps, unequal ranks, +equal-rank unequal kernels and an adverse chart tariff are explicit controls. +Four export groups cover Git-free read-only replay, source drift, typed/duplicate +receipt corruption and exclusive regeneration. + +Native CPython3.12.7 registered checks and optimized3.14.5 primary replay pass. +A separate OpenAI Codex agent checked the proof and independently minimized +4,454 smaller binary map pairs plus all168 charts for the pilot. Evidence is +finite where described; the all-field theorem relies on the written proof, +not on extrapolation from the finite checks. No human or formal-kernel review +or hosted CI result is claimed. + +## Expansion decision and limits + +Milestone: **local module**. The initial revision4 assignment was preserved +when main advanced to revision5 (`b4560d9e7216f72b73c5aa940ac099c05e33ccf9`). +The new family gate was read and the checkout fast-forwarded before packaging; +scientific predecessor blobs were unchanged. TASK.json contains the five-point +boundary/obligation ledger and the decision to **narrow** to this proof. + +A small rank is not a free observation or a cheap circuit. The general native +cost of R, R inverse and Delta, dynamic synthesis, selected ownership, precision +and an actual selected consumer remain unknown. Unknowns are not zero. The +complete improvement condition is that chart, inverse, correction and changed +admission/preparation/control cost less than the removed B0 and B1 calls. +No supplier, recursive contraction, selected-result change or new kappa follows. +Do not expand the family without a concrete consumer and that strict allowance. + +## Open next questions + +1. Find a pinned caller with this legal connector lifetime, actual source maps + and a favorable complete native repair invoice. Hosting and precision must + be included before using this module in a supplier. +2. For that caller only, optimize within its legal chart alphabet and actual + prices. The unrestricted rank optimum may be unavailable or more expensive. + +Prepared by ywz65 with substantial OpenAI Codex assistance. Apache-2.0. diff --git a/research/connector-chart-rank-repair/RESULT.json b/research/connector-chart-rank-repair/RESULT.json new file mode 100644 index 0000000000..7342ac0669 --- /dev/null +++ b/research/connector-chart-rank-repair/RESULT.json @@ -0,0 +1,469 @@ +{ + "schema_version": 1, + "source_pins": { + "research/dirty-connector-chart-transport/README.md": "c3d8b2fcc3485e267e25efc260b37ed7a2e8a0bc7d20294e9c79f0792a253d67", + "research/universal-connector-boundary/README.md": "23415f7829ab8d80a783142f10f7d31abbce84579362769984680af3df954476" + }, + "finite_oracle": { + "matrix_pairs": 262144, + "explicit_gl3_charts": 168, + "kernel_orbits": 16, + "constructive_charts": 8192, + "minimum_rank_histogram": { + "0": 40916, + "1": 187376, + "2": 33516, + "3": 336 + } + }, + "pilot": { + "b0": [ + 7, + 6, + 1 + ], + "b1": [ + 1, + 6, + 5 + ], + "chart": [ + 3, + 2, + 4 + ], + "delta": [ + 0, + 0, + 4 + ], + "minimum_rank": 1, + "identity_chart_rank": 2, + "candidate": [ + [ + 3, + 6 + ], + [ + 4, + 7 + ], + [ + 5, + 8 + ], + [ + 0, + 3 + ], + [ + 1, + 3 + ], + [ + 2, + 3 + ], + [ + 1, + 4 + ], + [ + 2, + 4 + ], + [ + 0, + 5 + ], + [ + 3, + 6 + ], + [ + 4, + 7 + ], + [ + 5, + 8 + ], + [ + 4, + 3 + ], + [ + 2, + 5 + ], + [ + 3, + 9 + ], + [ + 4, + 10 + ], + [ + 5, + 11 + ], + [ + 0, + 3 + ], + [ + 1, + 4 + ], + [ + 2, + 4 + ], + [ + 0, + 5 + ], + [ + 2, + 5 + ], + [ + 3, + 9 + ], + [ + 4, + 10 + ], + [ + 5, + 11 + ], + [ + 4, + 3 + ] + ], + "baseline": [ + [ + 3, + 6 + ], + [ + 4, + 7 + ], + [ + 5, + 8 + ], + [ + 0, + 3 + ], + [ + 1, + 3 + ], + [ + 2, + 3 + ], + [ + 1, + 4 + ], + [ + 2, + 4 + ], + [ + 0, + 5 + ], + [ + 3, + 6 + ], + [ + 4, + 7 + ], + [ + 5, + 8 + ], + [ + 0, + 3 + ], + [ + 1, + 3 + ], + [ + 2, + 3 + ], + [ + 1, + 4 + ], + [ + 2, + 4 + ], + [ + 0, + 5 + ], + [ + 3, + 9 + ], + [ + 4, + 10 + ], + [ + 5, + 11 + ], + [ + 0, + 3 + ], + [ + 1, + 4 + ], + [ + 2, + 4 + ], + [ + 0, + 5 + ], + [ + 2, + 5 + ], + [ + 3, + 9 + ], + [ + 4, + 10 + ], + [ + 5, + 11 + ], + [ + 0, + 3 + ], + [ + 1, + 4 + ], + [ + 2, + 4 + ], + [ + 0, + 5 + ], + [ + 2, + 5 + ] + ], + "outside_alphabet_direct": [ + [ + 0, + 6 + ], + [ + 1, + 6 + ], + [ + 2, + 6 + ], + [ + 1, + 7 + ], + [ + 2, + 7 + ], + [ + 0, + 8 + ], + [ + 0, + 9 + ], + [ + 1, + 10 + ], + [ + 2, + 10 + ], + [ + 0, + 11 + ], + [ + 2, + 11 + ] + ], + "candidate_bill": { + "xors": 26, + "reads": 52, + "writes": 26, + "dispatches": 26, + "head_moves": 368, + "fixed_port_tariff": 498 + }, + "baseline_bill": { + "xors": 34, + "reads": 68, + "writes": 34, + "dispatches": 34, + "head_moves": 444, + "fixed_port_tariff": 614 + }, + "direct_bill": { + "xors": 11, + "reads": 22, + "writes": 11, + "dispatches": 11, + "head_moves": 204, + "fixed_port_tariff": 259 + }, + "all_dirty_inputs": 4096, + "inverse_inputs": 4096, + "first_delivery_inputs": 4096, + "semantic_failure_witnesses": { + "omit_repair": 4, + "omit_final_inverse": 16, + "omit_initial_chart": 2, + "wrong_closing_source": 2 + }, + "rank_is_not_tariff_optimality": true + }, + "odd_characteristic_control": { + "field": 3, + "dimension": 2, + "dirty_inputs": 6561, + "inverse_inputs": 6561, + "wrong_closing_sign_rejected": true + }, + "boundary_cases": [ + { + "b0": [ + 1, + 0, + 0 + ], + "b1": [ + 2, + 0, + 0 + ], + "rank": 1, + "chart": [ + 1, + 2, + 4 + ], + "delta": [ + 3, + 0, + 0 + ] + }, + { + "b0": [ + 0, + 0, + 0 + ], + "b1": [ + 1, + 2, + 4 + ], + "rank": 3, + "chart": [ + 4, + 2, + 1 + ], + "delta": [ + 1, + 2, + 4 + ] + }, + { + "b0": [ + 1, + 2, + 4 + ], + "b1": [ + 0, + 0, + 0 + ], + "rank": 3, + "chart": [ + 4, + 2, + 1 + ], + "delta": [ + 4, + 2, + 1 + ] + }, + { + "b0": [ + 0, + 0, + 0 + ], + "b1": [ + 0, + 0, + 0 + ], + "rank": 0, + "chart": [ + 1, + 2, + 4 + ], + "delta": [ + 0, + 0, + 0 + ] + } + ], + "limits": "Rank minimum over all invertible row charts; no scalar/physical tariff minimum or selected supplier admission." +} diff --git a/research/connector-chart-rank-repair/SOURCES.json b/research/connector-chart-rank-repair/SOURCES.json new file mode 100644 index 0000000000..7826316c30 --- /dev/null +++ b/research/connector-chart-rank-repair/SOURCES.json @@ -0,0 +1,41 @@ +{ + "schema_version": 1, + "base_commit": "b4560d9e7216f72b73c5aa940ac099c05e33ccf9", + "files": [ + { + "path": "research/dirty-connector-chart-transport/README.md", + "usage": "input", + "sha256": "c3d8b2fcc3485e267e25efc260b37ed7a2e8a0bc7d20294e9c79f0792a253d67", + "git_blob": "2b161ebfccfc3867d3b6b74cc05c761ba1becfd2" + }, + { + "path": "research/universal-connector-boundary/README.md", + "usage": "input", + "sha256": "23415f7829ab8d80a783142f10f7d31abbce84579362769984680af3df954476", + "git_blob": "d277f7c5830b1f2bc42e1ff41ab86e7d7564929f" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "sha256": "7d185cd8c2af35988d638d969748ad7b670f902606444dbfc748e4402c340df6", + "git_blob": "889b95d936746df124872133ae1e7cc339adcb92" + }, + { + "path": "docs/research/research-family-status.md", + "usage": "provenance", + "sha256": "c37c7e0f6a1134983990e1b3efef55e65239b38be780e8a4cc10f5aefdaf2df5", + "git_blob": "1a2195004c5d681679279f0095b7964fb14a01e6" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11" + } + ], + "credit": [ + "woklerx: exact equal-kernel dirty connector chart criterion and paid pilot.", + "Ross Richardson: PR943 universal dirty-query model and complete-call accounting." + ], + "scientific_input_note": "These two predecessor README blobs are unchanged from initial main0fdd; revision5 updates guidance only. No predecessor executable imported." +} diff --git a/research/connector-chart-rank-repair/TASK.json b/research/connector-chart-rank-repair/TASK.json new file mode 100644 index 0000000000..0b4a8ee687 --- /dev/null +++ b/research/connector-chart-rank-repair/TASK.json @@ -0,0 +1,122 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 5, + "base_commit": "b4560d9e7216f72b73c5aa940ac099c05e33ccf9", + "original_card": { + "id": "connector-alphabet-change", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/universal-connector-boundary/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Construct and charge a legal extra operation on a minimal instance.", + "Prove a target-specific bound after adding one specified operation family." + ], + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. 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/universal-connector-boundary/verify.py" + ], + "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY", + "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "allowed_variations": [ + "Choose one additional operation and a small source count for its first counterexample." + ], + "scope_change_triggers": [ + "Keeping the alphabet and only increasing the source count; record this as a changed assignment." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ] + }, + "assignment_nonce": "fc48de8a055a955bfdc7a38a0308396d", + "initial_assignment_base": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "initial_priority_revision": 4, + "scope_status": "refined", + "actual_scope": "Minimum rank of one paid residual source injection between an invertible dirty connector chart and the second reader, with a restored, priced binary pilot.", + "scope_change_reason": "Adds exactly the residual correction family to the predecessor equal-kernel chart interface. Original assignment retained across revision5 refresh; current card and family gate read without rerolling.", + "bottleneck_link": "Equal kernels are an all-or-nothing criterion only when no source repair is allowed. A rank-minimum residual determines the observation dimension that a fixed-map caller must actually implement and pay before reusing the connector.", + "budget_minutes": 70, + "stop_rule": "One scoped rank theorem, constructive certificate, full-domain finite oracle and priced pilot; stop before any supplier or dependent optimization campaign.", + "outcome": "completed", + "declared_milestone": "local module", + "evidence": "PROOF.md, independently enumerated chart orbits, exact constructive charts, all dirty pilot inputs/inverse/cuts and semantic controls.", + "author": "ywz65", + "ai_assistance": "Substantial OpenAI Codex assistance, including separate agent formula/proof and independent finite checks. No human or formal-kernel review.", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/943#issuecomment-6197186784", + "first_step": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY pairings945; baseline bindings pass. Exact interface read.", + "overlap": { + "open_prs": 817, + "open_prs_utc": "2026-10-15T16:28:38.809260Z", + "discussion_records": 1279, + "discussions_utc": "2026-10-15T16:32:11.214527Z", + "complete_pagination": true, + "terms": [ + "chart transport", + "connector-only", + "same kernel", + "rank repair", + "rank-distance", + "kernel mismatch", + "dirty-connector-chart" + ], + "limit": "Metadata and local source notes only, not every diff. GraphQL quota exhausted after refresh; canonical claim posted through REST on PR943." + }, + "family_expansion_decision": { + "decision": "narrow", + "source_status": "Retained main predecessors independently read; new proof and pilot locally verified, separately reviewed before publication.", + "boundary": "Fixed source x; arbitrary dirty z,y0,y1; two chronological output requests; paid invertible R, one paid source correction \u0394x, final R inverse. No extra dirty row in the binary pilot.", + "obligation_ledger": { + "rank_minimum": "proved: max(r0,r1)-intersection dimension over arbitrary invertible row charts", + "fixed_pilot": "constructive upper bound:26 scalar XORs versus34 closed-query XORs; direct11-gate circuit lies outside the fixed-call alphabet", + "general_repair_cost": "unknown until R,R inverse and \u0394 have complete native implementations; rank is not their price", + "preparation_control_admission": "must be charged as actual differences in the complete comparison; no free dynamic synthesis", + "selected_consumer_hosting_precision": "unknown; no source-pinned selected caller identified" + }, + "decision_value": "The residual can replace one opening and one closing B call. Their costs disappear only if repair plus chart/inverse and admission differences cost less; the second B close cancels the repair so it does not recur at cleanup.", + "next_test": "Certify this interface once and retain it as a module. Do not expand the family until an actual caller and strict complete cost allowance are supplied.", + "reopen_trigger": "A pinned fixed-map caller with legal connector lifetime and a fully charged favorable repair/consumer invoice." + }, + "open_questions": [ + { + "question": "Does a pinned selected caller expose a cheap residual chart repair within this lifetime contract?", + "why_it_matters": "Only an actual complete invoice can turn a local rank repair into a supplier improvement.", + "first_step": "Extract B0,B1, readers, frame/owner boundaries and paid native chart/repair implementations.", + "blocked_by": "No selected consumer or hosting/precision invoice is supplied." + }, + { + "question": "What residual is cheapest in a specified restricted native chart alphabet?", + "why_it_matters": "The rank optimum over all invertible charts need not minimize actual price or remain attainable under native restrictions.", + "first_step": "Pin one caller and its legal chart generators, then compare complete tariffs only within the established allowance.", + "blocked_by": "No generic rank-to-price rule is valid; do not launch a chart search without that caller." + } + ], + "submission_refresh": { + "utc": "2026-10-15T16:54:53.985265+00:00", + "main": "b4560d9e7216f72b73c5aa940ac099c05e33ccf9", + "priority_revision": 5, + "compatibility": "Current main unchanged; two scientific predecessor blobs also unchanged from original revision4 base." + }, + "validation": { + "primary": "Native CPython3.12.7 registered primary and4 export groups PASS.", + "secondary": "Native CPython3.14.5 optimized primary PASS.", + "independent": "Separate AI proof/formula check and no-import4454 smaller binary-pair minima plus168 pilot charts; final source/chronology review recorded outside package.", + "unrun": [ + "Hosted CI", + "Human/formal-kernel review", + "Selected cold replay", + "Native supplier/physical compiler" + ] + } +} diff --git a/research/connector-chart-rank-repair/VERIFY.json b/research/connector-chart-rank-repair/VERIFY.json new file mode 100644 index 0000000000..226e0b762a --- /dev/null +++ b/research/connector-chart-rank-repair/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/dirty-connector-chart-transport/README.md", + "research/universal-connector-boundary/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact complete GL3 orbit minima, constructive rank repair, all dirty pilot endpoints/inverses/cuts and source/typed receipt binding." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 240, + "checks": "Git-free read-only export, source/typed evidence rejection and exclusive regeneration." + } + ] +} diff --git a/research/connector-chart-rank-repair/test_verify.py b/research/connector-chart-rank-repair/test_verify.py new file mode 100644 index 0000000000..f59210cd8f --- /dev/null +++ b/research/connector-chart-rank-repair/test_verify.py @@ -0,0 +1,67 @@ +"""Read-only Git-free replay, source/evidence rejection and exclusive output.""" +import hashlib +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE=Path(__file__).resolve().parent +ROOT=HERE.parents[1] + + +def require(ok,why): + if not ok: + raise ValueError(why) + + +def snapshot(root): + return {str(p.relative_to(root)):hashlib.sha256(p.read_bytes()).hexdigest() + for p in root.rglob('*') if p.is_file()} + + +def main(): + with tempfile.TemporaryDirectory(prefix='chart-rank-export-') as tmp: + root=Path(tmp)/'checkout' + pkg=root/'research'/HERE.name + shutil.copytree(HERE,pkg,ignore=shutil.ignore_patterns('__pycache__')) + for name in ('research/dirty-connector-chart-transport/README.md','research/universal-connector-boundary/README.md'): + target=root/name + target.parent.mkdir(parents=True,exist_ok=True) + target.write_bytes((ROOT/name).read_bytes()) + def run(*extra,ok=True,needle=None): + result=subprocess.run([sys.executable,'-I','-O','-B',str(pkg/'verify.py'),*map(str,extra)], + cwd=root,capture_output=True,text=True,encoding='utf-8',timeout=120) + require((result.returncode==0)==ok,result.stdout+result.stderr) + if needle: + require(needle in result.stdout+result.stderr,'wrong result: '+result.stdout+result.stderr) + before=snapshot(root) + run(needle='PASS_CONNECTOR_CHART_RANK_REPAIR') + require(snapshot(root)==before,'replay wrote files') + path=root/'research/dirty-connector-chart-transport/README.md' + raw=path.read_bytes() + path.write_bytes(raw+b'\n') + run(ok=False,needle='source binding') + path.write_bytes(raw) + result=pkg/'RESULT.json' + raw=result.read_bytes() + data=json.loads(raw) + data['pilot']['minimum_rank']=True + result.write_text(json.dumps(data),encoding='utf-8') + run(ok=False,needle='typed exact receipt mismatch') + result.write_text('{"schema_version":1,"schema_version":1}',encoding='utf-8') + run(ok=False,needle='duplicate JSON key') + result.write_bytes(raw) + new=Path(tmp)/'new-result.json' + run('--write-result',new) + require(json.loads(new.read_text())==json.loads(raw),'regeneration mismatch') + fresh=new.read_bytes() + run('--write-result',new,ok=False,needle='output already exists') + require(new.read_bytes()==fresh,'existing output changed') + require(snapshot(root)==before,'export changed') + print('PASS_CONNECTOR_CHART_RANK_EXPORT groups=4') + + +if __name__=='__main__': + main() diff --git a/research/connector-chart-rank-repair/verify.py b/research/connector-chart-rank-repair/verify.py new file mode 100644 index 0000000000..bb9cd8502c --- /dev/null +++ b/research/connector-chart-rank-repair/verify.py @@ -0,0 +1,317 @@ +"""Exact rank-repair certificates and a fully restored, paid binary pilot.""" +import argparse +from collections import Counter +import hashlib +from itertools import product +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def require(ok, why): + if not ok: + raise ValueError(why) + + +def read_json(path): + def pairs(items): + result = {} + for key, value in items: + require(key not in result, 'duplicate JSON key') + result[key] = value + return result + return json.loads(path.read_text(encoding='utf-8'), object_pairs_hook=pairs) + + +def canonical(value): + return json.dumps(value,sort_keys=True,separators=(',',':')) + + +def pins(): + out = {} + for row in read_json(HERE/'SOURCES.json')['files']: + if row['usage'] != 'input': + continue + raw = (ROOT/row['path']).read_bytes() + digest = hashlib.sha256(raw).hexdigest() + blob = hashlib.sha1(b'blob '+str(len(raw)).encode()+b'\0'+raw).hexdigest() + require(digest == row['sha256'] and blob == row['git_blob'],'source binding: '+row['path']) + out[row['path']] = digest + require(len(out) == 2,'two predecessor inputs') + return out + + +def xor(values): + out = 0 + for value in values: + out ^= value + return out + + +def solver(rows): + """Echelon image basis with input combinations and full relation basis.""" + basis = {} + relations = [] + for i, row in enumerate(rows): + value, combination = row, 1 << i + while value: + pivot = value.bit_length()-1 + if pivot not in basis: + basis[pivot] = value, combination + break + vector, earlier = basis[pivot] + value ^= vector + combination ^= earlier + if not value: + relations.append(combination) + return basis, relations + + +def rank(rows): + return len(solver(rows)[0]) + + +def express(basis, target): + result = 0 + while target: + pivot = target.bit_length()-1 + require(pivot in basis,'target outside span') + vector, combination = basis[pivot] + target ^= vector + result ^= combination + return result + + +def image_basis(rows): + basis, _ = solver(rows) + return [basis[p][0] for p in sorted(basis,reverse=True)] + + +def intersection(u,v): + _, relations = solver(u+v) + common = [xor(row for j,row in enumerate(u) if relation >> j & 1) for relation in relations] + require(rank(common) == len(common),'intersection independence') + return common + + +def adapted(common, rows): + result = common[:] + for row in rows: + if rank(result+[row]) > len(result): + result.append(row) + return result + + +def compose(a,b): + return tuple(xor(row for j,row in enumerate(b) if mask >> j & 1) for mask in a) + + +def inverse(a): + n = len(a) + left, right = list(a), [1 << i for i in range(n)] + for j in range(n): + pivot = next((i for i in range(j,n) if left[i] >> j & 1),None) + require(pivot is not None,'singular chart') + left[j],left[pivot] = left[pivot],left[j] + right[j],right[pivot] = right[pivot],right[j] + for i in range(n): + if i != j and left[i] >> j & 1: + left[i] ^= left[j] + right[i] ^= right[j] + require(left == [1 << i for i in range(n)],'inverse elimination') + return tuple(right) + + +def row_transform(rows, targets): + basis, relations = solver(rows) + require(len(targets) == len(basis),'target basis dimension') + result = tuple([express(basis,t) for t in targets]+relations) + require(rank(result) == len(rows),'invertible basis extension') + require(compose(result,rows) == tuple(targets+[0]*(len(rows)-len(targets))),'adapted form') + return result + + +def construct(b0,b1): + require(len(b0) == len(b1),'equal connector dimensions') + u,v = image_basis(b0),image_basis(b1) + common = intersection(u,v) + t0,t1 = adapted(common,u),adapted(common,v) + q0,q1 = row_transform(b0,t0),row_transform(b1,t1) + chart = compose(inverse(q1),q0) + moved = compose(chart,b0) + delta = tuple(x^y for x,y in zip(b1,moved)) + expected = max(len(u),len(v))-len(common) + require(rank(delta) == expected,'constructive minimum rank') + return chart,delta,expected + + +def vector(rows,value): + return sum(((row & value).bit_count() & 1) << i for i,row in enumerate(rows)) + + +def encode(rows): + return sum(row << (3*i) for i,row in enumerate(rows)) + + +def finite_oracle(): + matrices = list(product(range(8),repeat=3)) + # Independently classify left orbits by actual kernels; explicitly form each + # representative's entire GL3 orbit, with no constructor-derived witnesses. + groups = {} + for matrix in matrices: + key = tuple(x for x in range(8) if vector(matrix,x) == 0) + groups.setdefault(key,[]).append(matrix) + gl = [m for m in matrices if len({vector(m,x) for x in range(8)}) == 8] + require(len(gl) == 168 and len(groups) == 16,'finite domains') + ranks = {encode(m):rank(m) for m in matrices} + checked = 0 + histogram = Counter() + constructor_cases = 0 + for members in groups.values(): + representative = members[0] + orbit = {compose(g,representative) for g in gl} + require(orbit == set(members),'complete explicit chart orbit') + orbit_codes = [encode(m) for m in orbit] + for b1 in matrices: + minimum = min(ranks[encode(b1)^code] for code in orbit_codes) + for b0 in members: + c = rank(b0)+rank(b1)-rank(b0+b1) + formula = max(rank(b0),rank(b1))-c + require(minimum == formula,'independent full orbit minimum') + checked += 1 + histogram[minimum] += 1 + # All512 destinations for each of16 row-space orbits; the theorem + # and row_transform explicitly handle arbitrary representatives. + chart,delta,claim = construct(representative,b1) + require(claim == minimum and rank(chart) == 3,'constructed chart against orbit oracle') + require(compose(inverse(chart),compose(chart,representative)) == representative,'constructed inverse') + constructor_cases += 1 + require(checked == 262144 and constructor_cases == 8192,'coverage') + return {'matrix_pairs':checked,'explicit_gl3_charts':168,'kernel_orbits':16, + 'constructive_charts':constructor_cases,'minimum_rank_histogram':dict(sorted(histogram.items()))} + + +def gates(matrix,source,target): + return [(source+j,target+i) for i,row in enumerate(matrix) for j in range(3) if row >> j & 1] + + +def run(word,value): + for source,target in word: + require(source != target and 0 <= source < 12 and 0 <= target < 12,'valid distinct gate ports') + value ^= ((value >> source) & 1) << target + return value + + +def pilot(): + b0,b1,r = (7,6,1),(1,6,5),(3,2,4) + delta = tuple(x^y for x,y in zip(b1,compose(r,b0))) + require(delta == (0,0,4) and rank(delta) == 1,'literal rank-one repair') + require(rank(tuple(x^y for x,y in zip(b0,b1))) == 2,'identity-chart rank control') + identity = (1,2,4) + a0,a1 = gates(identity,3,6),gates(identity,3,9) + g0,g1 = gates(b0,0,3),gates(b1,0,3) + chart,repair = [(4,3)],gates(delta,0,3) + phases = [a0,g0,a0,chart,repair,a1,g1,a1,chart] + candidate = sum(phases,[]) + baseline = a0+g0+a0+g0+a1+g1+a1+g1 + direct = gates(b0,0,6)+gates(b1,0,9) + require((len(candidate),len(baseline),len(direct)) == (26,34,11),'paid scalar counts') + desired = lambda value:value ^ (vector(b0,value & 7)<<6) ^ (vector(b1,value & 7)<<9) + first_end = len(a0+g0+a0) + for value in range(4096): + expected = desired(value) + require(run(candidate,value) == expected and run(baseline,value) == expected,'full dirty endpoint') + require(run(direct,value) == expected,'outside-alphabet direct comparator') + require(run(list(reversed(candidate)),expected) == value,'literal inverse') + require((run(candidate[:first_end],value) >> 6) & 7 == (expected >> 6) & 7,'first delivery cut') + require(all(not(6 <= target < 9) for _,target in candidate[first_end:]),'no rewrite after first delivery') + mutants = { + 'omit_repair':sum(phases[:4]+phases[5:],[]), + 'omit_final_inverse':sum(phases[:-1],[]), + 'omit_initial_chart':sum(phases[:3]+phases[4:],[]), + 'wrong_closing_source':sum(phases[:6]+[g0]+phases[7:],[]), + } + failures = {} + for label,word in mutants.items(): + witness = next((x for x in range(4096) if run(word,x) != desired(x)),None) + require(witness is not None,'semantic mutation survived: '+label) + failures[label] = witness + # Rank optimization is not price optimization; a large chart tariff can lose. + require(10+10+1 > 2,'rank/cost distinction control') + def invoice(word): + return {'xors':len(word),'reads':2*len(word),'writes':len(word),'dispatches':len(word), + 'head_moves':sum(2*(max(s,t)+1) for s,t in word), + 'fixed_port_tariff':sum(2*(max(s,t)+1)+5 for s,t in word)} + return {'b0':b0,'b1':b1,'chart':r,'delta':delta,'minimum_rank':1,'identity_chart_rank':2, + 'candidate':candidate,'baseline':baseline,'outside_alphabet_direct':direct, + 'candidate_bill':invoice(candidate),'baseline_bill':invoice(baseline),'direct_bill':invoice(direct), + 'all_dirty_inputs':4096,'inverse_inputs':4096,'first_delivery_inputs':4096, + 'semantic_failure_witnesses':failures,'rank_is_not_tariff_optimality':True} + + +def odd_characteristic_control(): + # Independent ordinary integer matrix arithmetic, reduced modulo3. The + # noncommuting readers and signed close distinguish the general word from + # a cancellation that holds only in characteristic two. No tariff claimed. + b0,b1 = ((1,1),(0,0)),((1,0),(1,1)) + r,delta = ((0,1),(1,0)),((1,0),(0,0)) + a0,a1 = ((1,1),(0,1)),((1,0),(1,1)) + def mv(m,v):return tuple(sum(a*b for a,b in zip(row,v)) % 3 for row in m) + def add(a,b,sign=1):return tuple((x+sign*y) % 3 for x,y in zip(a,b)) + word = [('Q',2,1,a0,-1),('Q',1,0,b0,1),('Q',2,1,a0,1),('R',1,1,r,1), + ('Q',1,0,delta,1),('Q',3,1,a1,1),('Q',1,0,b1,-1),('Q',3,1,a1,-1),('R',1,1,r,1)] + def execute(program,bank): + bank = list(bank) + for op,target,source,m,sign in program: + bank[target] = mv(m,bank[source]) if op == 'R' else add(bank[target],mv(m,bank[source]),sign) + return tuple(bank) + inverse_word = [(op,t,s,m,-sign if op == 'Q' else sign) for op,t,s,m,sign in reversed(word)] + wrong = word[:] + wrong[6] = ('Q',1,0,b1,1) + rejected = False + cases = 0 + for values in product(range(3),repeat=8): + bank = tuple(tuple(values[2*j:2*j+2]) for j in range(4)) + x,z,y0,y1 = bank + expected = (x,z,add(y0,mv(a0,mv(b0,x))),add(y1,mv(a1,mv(b1,x)))) + require(execute(word,bank) == expected,'noncommuting odd-characteristic endpoint') + require(execute(inverse_word,expected) == bank,'signed literal inverse') + rejected |= execute(wrong,bank) != expected + cases += 1 + require(rejected,'wrong closing sign survived') + return {'field':3,'dimension':2,'dirty_inputs':cases,'inverse_inputs':cases,'wrong_closing_sign_rejected':True} + + +def calculate(): + source_pins = pins() + # Unequal kernels can share rank; zero/extreme ranks are included explicitly. + small = [] + for b0,b1 in (((1,0,0),(2,0,0)),((0,0,0),(1,2,4)),((1,2,4),(0,0,0)),((0,0,0),(0,0,0))): + r,d,k = construct(b0,b1) + small.append({'b0':b0,'b1':b1,'rank':k,'chart':r,'delta':d}) + require([x['rank'] for x in small] == [1,3,3,0],'boundary cases') + return {'schema_version':1,'source_pins':source_pins,'finite_oracle':finite_oracle(), + 'pilot':pilot(),'odd_characteristic_control':odd_characteristic_control(),'boundary_cases':small, + 'limits':'Rank minimum over all invertible row charts; no scalar/physical tariff minimum or selected supplier admission.'} + + +def main(): + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument('--write-result',type=Path,help='write only a NEW result') + args = ap.parse_args() + if args.write_result: + require(not args.write_result.exists(),'output already exists') + result = calculate() + if args.write_result: + with args.write_result.open('x',encoding='utf-8',newline='\n') as stream: + json.dump(result,stream,indent=2) + stream.write('\n') + else: + require(canonical(read_json(HERE/'RESULT.json')) == canonical(result),'typed exact receipt mismatch') + print('PASS_CONNECTOR_CHART_RANK_REPAIR pairs=262144 charts=8192 dirty=4096 scalar_xors=26_vs_34') + + +if __name__ == '__main__': + main()