diff --git a/research/pair-consistent-frame-optimum/CERTIFICATE.json.gz b/research/pair-consistent-frame-optimum/CERTIFICATE.json.gz new file mode 100644 index 0000000000..2591c96ad6 Binary files /dev/null and b/research/pair-consistent-frame-optimum/CERTIFICATE.json.gz differ diff --git a/research/pair-consistent-frame-optimum/IMPLEMENTATION.md b/research/pair-consistent-frame-optimum/IMPLEMENTATION.md new file mode 100644 index 0000000000..627b53287d --- /dev/null +++ b/research/pair-consistent-frame-optimum/IMPLEMENTATION.md @@ -0,0 +1,65 @@ +# Verification boundaries + +`model.py` authenticates eight fixed inputs, reuses the predecessor's frame +construction definitions, and builds the new pair-consistent equality model. +`powers.py` provides directed integer bounds. `verify.py` checks the supplied +primal and symbolic dual, the actual integral frame assignment, and rejection +controls. No scientific predecessor replay or solver executes. + +The certificate is a generated proof witness, not a handwritten receipt. +Its mathematical model hash is regenerated from the complete rows, right-hand +sides, costs, fixed constant, source profile, domains, node variable inventory +and mapped-edge count. Gzip container bytes are not a mathematical invariant; +the decoded certificate and freshly checked equations define acceptance. + +## Power of Ten inspection + +New functions stay within 60 physical lines. All loops range over explicit +finite collections or fixed Taylor truncations. Guards enforce at most 100,000 +source events, 5,000 source frames, dimension nine, 16,000 graph nodes, 30,000 +mapped edges, quotient gap five, 5,000 marginal choices, 25,000 columns and +16,000 equality rows. This is a fixed authenticated input, not a general input +service. Checks raise explicit exceptions and remain enabled under `-O`. +All new data is local to one run. Input files and certificate bytes are read +only; file operations use `Path` methods with normal error propagation. + +Rule 3, managed allocation deviation. CPython, arbitrary-precision arithmetic, +standard containers and the retained frame caches allocate during verification. +These cannot meet a fixed-memory native execution rule. The scope is one bounded +read-only certificate replay, with the enforced inventories above and a 120-second +registered timeout. The largest LP table has 59,077 nonzero coefficients; dual +vectors have five integer entries. No fixed-memory physical caller is claimed. +A native port would need fixed-capacity arithmetic and storage before such use. + +Rule 8, authenticated source-loading deviation. Preserving the pinned source +requires compiling its frame definitions and the single unchanged `construct` +function selected by AST name. The whole native verifier must not run, since +that would spend the assignment on predecessor verification. Eight hashes are +checked before loading. No source text is modified, and no arbitrary module or +callback path is accepted. The retained constructor's globals are explicitly +bound to its original canonical data, Fraction, copy and an exception guard. +The verifier exercises the actual graph produced by those definitions. A future +upstream definition-only module would remove the need for AST extraction. + +Rule 9, managed dispatch deviation. Standard-library operations and the +predecessor's `NativeSchedule` methods dispatch through a fixed, authenticated +module. The eight test-only rejection callables have explicit local targets. +No callback registry, network or subprocess exists in the scientific checker. +Changing the loader to a native static interface would be needed for a literal +no-indirect-call execution model. + +Rule 10. Registered normal and optimized replays enable warnings as errors. +The available interpreter supplies syntax and runtime diagnostics. No separate +static analyzer is installed in the declared standard-library environment. +Frozen predecessor code is preserved; no repository-wide analyzer configuration +or historical suite is changed. + +## Meaningful controls + +Eight controls reject a missing integral pair variable, an invalid index, +a duplicated selected variable, a changed dual coefficient, an omitted dual +row, an omitted model row, a false optimum histogram and an invalid power rank. +They exercise the same acceptance functions as the certificate. The proof's +Taylor remainders and reduced-cost signs are executable acceptance obligations. +The direct stdout receipt records source hashes, exact counts, interpreter, +all rejection reasons and the minimum certified positive sign bound. diff --git a/research/pair-consistent-frame-optimum/PROOF.md b/research/pair-consistent-frame-optimum/PROOF.md new file mode 100644 index 0000000000..547108fc9f --- /dev/null +++ b/research/pair-consistent-frame-optimum/PROOF.md @@ -0,0 +1,128 @@ +# The pair-consistent certificate + +Put `p=4984891121/5000000000` and `f(r)=r^p`, with `f(0)=0`. +All objects below refer to the authenticated forward graph from #4994. +The predecessor's graph/realization and complete marginal-interval theorems +are cited premises. No native endpoint or physical phase theorem is reproved. + +## 1. A relaxation containing every legal frame assignment + +A vertex v carries a binary subspace U_v. Each mapped edge e:u->v imposes +`G_e U_u contained in U_v`. Its paid rank is `dim U_v-dim U_u` because G_e +is invertible. Repeated identical edges retain their multiplicity. Fixed +vertices and eight rank-eight center jobs retain the source charges. + +The predecessor interval theorem gives the least and greatest feasible +subspaces L_v,H_v and proves that every subspace between them is an attainable +single-vertex marginal. Enumerate each complete interval D_v by enumerating +all subspaces of H_v/L_v. This does not assume that arbitrary simultaneous +marginal choices are feasible. + +Introduce nonnegative x_(v,a), for a in D_v, with sum_a x_(v,a)=1. +For every edge with two flexible ends, introduce nonnegative +z_(e,a,b) only for pairs satisfying `G_e a contained in b`. Impose + +```text +sum_b z_(e,a,b) = x_(u,a) for every a in D_u +sum_a z_(e,a,b) = x_(v,b) for every b in D_v. +``` + +When an end is fixed, charge its edge price directly to the remaining +x variable. When both ends are fixed, add its price to the constant. +For a two-flexible-end edge, charge z_(e,a,b) by its multiplicity times +`f(dim b-dim a)`. Include all eight center jobs in the constant. + +Every legal integral frame assignment induces a feasible point by choosing +its one node marginal and compatible edge pair. It has exactly the same bill. +No assumption that every fractional point has a global frame realization is +needed. Therefore the LP minimum is a lower bound on the legal minimum. + +The deterministic builder gives A x=b, x>=0, objective c^T x+c0, with +24,788 columns and 15,524 rows. It retains all 29,790 mapped edges and all +4,684 subspace choices across all 1,339 flexible contacts. This includes the +large component as well as the previously settled small components. + +## 2. Symbolic weak duality + +The certificate gives one vector d_i in Z^5 for every equality row. Set + +```text +y_i = d_i1*f(1) + ... + d_i5*f(5). +``` + +All variable costs use ranks zero through five; the verifier checks that +condition explicitly. The remaining fixed costs are in c0. For each column j +it computes the coefficient vector + +```text +s_j = c_j - sum_i A_ij*y_i. +``` + +Here c_j and s_j denote exact linear combinations of the five prices. +For every distinct nonzero s_j the directed bounds in section 3 prove +`s_j>0` at the stated p. The zero vector evaluates exactly to zero. +Consequently A^T y<=c, so for every feasible x, + +```text +c^T x + c0 >= y^T A x + c0 = y^T b + c0. +``` + +This uses only nonnegativity of x and the explicitly checked equalities. +It does not rely on a solver's status or on LP strong duality. + +The certificate also gives the indices of an integral feasible x. Every row +and index bound is checked exactly, and the associated node assignment passes +every original mapped containment and fixed vertex. Its objective, the dual +objective and the source objective are equal coefficient by coefficient to + +```text +2201*f(1) + 412*f(2) + 510*f(3) + 127*f(4) + 40*f(5) + 8*f(8). +``` + +Thus the LP and legal integral problems both attain this exact minimum. +The attained frame labels need not be unique. This proof says nothing about +other tariffs, the backward graph or different native words/boundaries. + +## 3. Exact directed power bounds + +Let S=2^192. First write r=2^k a with 1<=a<2, and use + +```text +log(a) = 2*sum_(j>=0) t^(2j+1)/(2j+1), t=(a-1)/(a+1). +``` + +The first 128 summands, each rounded down in units 1/S, give a lower bound. +Their total rounding loss is below 128/S. The remaining positive tail is at +most `2*t^257/[257*(1-t^2)]`, which the checker proves is less than 1/S. +Thus adding 129 units gives a rigorous upper bound. The same construction +bounds log(2); combine it with k and multiply by the exact rational p, +rounding the lower product down and the upper product up. + +The resulting interval [l/S,u/S] for p log r lies in [0,3]. Expand its +exponential through degree 256. Recur on integer lower terms with floor +multiplication by l/(S*j), and upper terms with ceiling multiplication by +u/(S*j). Each recurrence encloses the corresponding exact Taylor term. +Their sums therefore enclose the partial series. The positive remaining +series is at most + +```text +(3^257/257!) / (1-3/258) < 1/S, +``` + +which is checked exactly as a rational inequality. Add one unit to the upper +sum. For r=1 use the exact interval [S,S]. This proves every returned power +interval contains S*f(r). + +Evaluate each signed reduced-cost polynomial by using the lower endpoint +for positive coefficients and the upper endpoint for negative coefficients. +All 383 distinct nonzero coefficient vectors have strictly positive lower +bounds. The arithmetic uses integers and Fraction throughout. Finite bound +widths and Taylor remainders are checked, not assumed from decimal precision. + +## 4. What the certificate establishes + +This is a finite exact optimization certificate for a specified source-bound +frame contract. Its consequences for any native schedule use #4994's inherited +graph contract. No predecessor scientific verifier runs. No independent human +review, formal proof kernel, physical implementation, complete supplier invoice +or multiplication theorem is claimed. The current selected frontier is unchanged. diff --git a/research/pair-consistent-frame-optimum/README.md b/research/pair-consistent-frame-optimum/README.md new file mode 100644 index 0000000000..87d9288a5b --- /dev/null +++ b/research/pair-consistent-frame-optimum/README.md @@ -0,0 +1,137 @@ +# Exact full forward carried-frame optimum at the declared tariff + +This contribution was produced by Nick Petalas. Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. + +Claim type: **finite exact optimization certificate**, with a written +weak-duality argument. For the complete forward contact domain of Cinna Davis / +1337isnot1337's [#4994](https://github.com/CrocSwap/integer-mult-bounds/pull/4994) +and [#5016](https://github.com/CrocSwap/integer-mult-bounds/pull/5016), put + +```text +C = 15108879/5000000000 = .0030217758 +p = 1-C = 4984891121/5000000000 +f(0) = 0, f(r) = r^p for r >= 1. +``` + +The exact global minimum of the stated forward frame bill is + +```text +2201 + 412*2^p + 510*3^p + 127*4^p + 40*5^p + 8*8^p. +``` + +This covers all 1,339 flexible contacts and all 4,684 marginal choices, +including the previously unresolved 1,271-contact component. The scalar word, +carried native maps, fixed entrances/exits and owned-center contacts remain +fixed. The eight rank-eight center jobs are included. The original source +attains the minimum; the certificate also contains an integral attainer with +31 changed contact frames. No uniqueness is claimed. + +The new step answers the forward fixed-tariff part of JoyboyBrian's +[#5091 open question](https://github.com/CrocSwap/integer-mult-bounds/pull/5091). +A genuine pair-consistent relaxation has an exactly matching symbolic dual. +Its 24,788 nonnegative columns satisfy 15,524 equality rows with 59,077 nonzero +coefficients. The dual uses integer coefficients in the five prices +`f(1),...,f(5)`. Directed integer arithmetic proves all 383 distinct nonzero +reduced costs strictly positive. The other reduced-cost polynomial is zero. +The primal and dual objectives agree coefficient by coefficient, with the +source histogram above. [PROOF.md](PROOF.md) explains why this is sufficient. + +This closes a missing exact optimization step. It does not improve kappa or +replay a predecessor's numerical or scientific result. The original +marginal/rank-selector relaxation in #5091 is a different, weaker model; +its fractional witness is not rerun. Chris R / Clear1nsight's +[#5068](https://github.com/CrocSwap/integer-mult-bounds/pull/5068) already settles +18 small components with the large one fixed and rejects an all-concave +extension. Krzysztof Wójt's +[#5024](https://github.com/CrocSwap/integer-mult-bounds/pull/5024) settles the +intact-region model. Those results are cited, not rechecked or claimed here. + +## Reproduce + +From the repository root, with the Python 3.12 standard library only: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/pair-consistent-frame-optimum/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/pair-consistent-frame-optimum/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/pair-consistent-frame-optimum +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/pair-consistent-frame-optimum --check-source-history +``` + +Another CPython 3.12 path may replace the displayed interpreter. Expected +marker: `PASS_PAIR_CONSISTENT_FRAME_OPTIMUM`. Both registered commands are +read-only. The generated stdout receipt includes the actual interpreter and +SHA256 of every package file. No receipt is handwritten. No solver, NumPy, +SciPy, network or Git is needed by the scientific verifier. + +The checker authenticates eight predecessor inputs, executes only the retained +constructor definition and frame-graph definitions, constructs every marginal +subspace and compatible pair, and checks the entire primal and dual. It also +checks every mapped containment for the integral attainer and eight mutation +controls. The retained native verifier's top-level scientific program is never +executed. Source construction and its frame-contract semantics are inherited +from #4971/#4994. They are not independently audited here. + +Discovery used numerical linear programming to select a basis. Acceptance +uses the committed symbolic certificate and exact arithmetic only. The +22,668-byte compressed certificate is generated data; reproduction reconstructs +the mathematical model and binds it to the certificate by SHA256. + +## Limits and provenance + +This result is for the **forward orientation and this one tariff**. It does +not certify the backward graph, another exponent, a changed scalar/native +word, split ownership, arbitrary frame descents, or a changed boundary. +It prices the source's recursive frame bill, not routing, precision, stock, +absolute phases, the complete physical caller or the multiplication theorem. +The current selected #7000 and its five framework assumptions are unchanged. +The tariff here is historical and is not asserted to be the current supplier's +saving. Native, selected cold-replay, Lean and Docker checks were not run. + +The `p104-side-correction` card is explicitly changed to this optimization +interface. The first source-binding control passed against canonical base +`e54523517d0f03e58352e647c403a5af3e525a57`, whose selected conditional kappa is +`.00363005817`. This is a local obstruction to improving a fixed older word, +not the card's complete changed-helper supplier. Further construction must +change a hypothesis and price its complete invoice. + +The overlap check included live PRs, this account's earlier submissions, the +latest handoffs, active Discussions, batch reservations, merged searches and +main-tree README searches for the full-contact and pair-consistent model. +The broad card cache covered 545 open PRs and 7,207 Discussion records, with +incomplete sparse local coverage. Targeted Git searches also read the omitted +matching packages. These checks exclude neither unpublished work nor arbitrary +unsearched code diffs. The advance claim is +[here](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19541785). + +## Open next questions + +1. Does the same exact minimum hold on the backward contact graph? Start by + building its pair-consistent model and seeking a separately checked dual. + This forward certificate does not establish the needed correspondence. +2. On which interval of exponents do the committed reduced-cost polynomials + remain nonnegative? Start with their 383 distinct expressions. The present + directed bounds certify only the stated exponent; #5068 already shows that + an unrestricted all-concave extension fails. +3. Can a changed word or boundary beat this fixed-model bill while preserving + arbitrary-input correctness and paying every new fee? First name the + changed contract and complete productive/paid ledger. Physical delivery, + restoration and supplier admission are unresolved here. + +## Credit + +Cinna Davis / 1337isnot1337 supplies #4994's carried-frame model and interval +completeness theorem and #5016's full-domain numerical screen. JoyboyBrian +supplies #5091's explicit stronger-relaxation question and its original-model +obstruction. Chris R / Clear1nsight #5068 and Krzysztof Wójt #5024 retain their +distinct exact partial optima. Dugongue / David Ganz #4971 supplies the signed +frame-carrying swaps, following Cao Yifan / intqwq's round-three word. Cinna +Davis #4440/#4470, zxv, Jacob Alan Sussman, James Reed and the retained +native/controller/compiler authors keep their predecessor credit. The source +LICENSE and NOTICE are unchanged declared inputs. + +Local marginal polytopes, linear programming duality and directed Taylor bounds +are classical. The new result is the source-bound full-forward certificate, +its exact verifier and the resulting fixed-tariff optimum. No literature-wide +priority for those methods is claimed. Implementation bounds and justified +Power of Ten deviations are in [IMPLEMENTATION.md](IMPLEMENTATION.md). diff --git a/research/pair-consistent-frame-optimum/SOURCES.json b/research/pair-consistent-frame-optimum/SOURCES.json new file mode 100644 index 0000000000..d20f7bb50f --- /dev/null +++ b/research/pair-consistent-frame-optimum/SOURCES.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/carried-warp-frame-intervals/README.md", + "usage": "input", + "git_blob": "15af4809991fc192717bfbf38136f24c34240a6b", + "sha256": "1186b6c09480bd40b2b6d71105ad9d4582d83eb51ff31bfacd69b3a589468cd6" + }, + { + "path": "research/carried-warp-frame-intervals/discovery/README.md", + "usage": "input", + "git_blob": "92e69475bdc1d83c84bab2840938a5195a9fcbd5", + "sha256": "4408fef72b0e1f86ff939b3cc366bbeb95679f6698d760d5bf90a2784a4a587c" + }, + { + "path": "research/carried-warp-frame-intervals/frame_dag.py", + "usage": "input", + "git_blob": "307934bb58765d80043f6901d250f370a95c686f", + "sha256": "2f1277c6467b7219d2a0988138386c2ec5efdfbf6a5c106da6d479b0ede7abd5" + }, + { + "path": "research/full-contact-exact-native-optimum/README.md", + "usage": "input", + "git_blob": "0c065137bdedec8ce9cc2f9890a79b6d610720c6", + "sha256": "73e8a4dc2d7327bb449e9396a355c1bb7653f960745d5dff7d07e46c606dd1b1" + }, + { + "path": "research/native-frame-carrying-swaps/LICENSE", + "usage": "input", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4" + }, + { + "path": "research/native-frame-carrying-swaps/NOTICE", + "usage": "input", + "git_blob": "faa0f8ce7f3dfb9b7095302d60a37469cea91da4", + "sha256": "57d5bcf4f205d6d4c16eb81f37c5a1ab0c99185de26978cab99f0ce82b3147f0" + }, + { + "path": "research/native-frame-carrying-swaps/SOURCE-WORD.json.gz", + "usage": "input", + "git_blob": "46d929df83817b85a5387bcdb9745e0627d6366e", + "sha256": "7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05" + }, + { + "path": "research/native-frame-carrying-swaps/verify.py", + "usage": "input", + "git_blob": "88aa08b7d54cdae5b2c6696fe96a73a9ae89debf", + "sha256": "9e536497b6bf5a1162a933c1aef0ff079f1ec21996095ccfeda40252e0b7b3dd" + } + ] +} diff --git a/research/pair-consistent-frame-optimum/TASK.json b/research/pair-consistent-frame-optimum/TASK.json new file mode 100644 index 0000000000..1f08bb9831 --- /dev/null +++ b/research/pair-consistent-frame-optimum/TASK.json @@ -0,0 +1,129 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "p104-side-correction", + "question": "Can joint helper bases and a legal causal split improve the complete P104 productive/paid invoice?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "research/p104-helper-subspace-splits/README.md", + "research/dyadic-helper-channel-capacity/README.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. 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", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Start with the selected #5599 emitted word and review pending #5718 distinct input/output bases plus #5717/#5719 coverage before claiming work. Pick one uncovered source word, helper group and cut region. Prove the arbitrary-input relation and legal entry/exit corrections, then compare full target and paid profiles. Reject if completion, owned lifetimes or consumer costs repay the gain. A static pairing rank alone is not a physical split.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "P104", + "helper basis", + "helper split", + "5718", + "dyadic capacity" + ], + "existing_checks": [ + { + "scope": "PR #4133: literal-slot defect", + "evidence": "research/p104-literal-slot-defect/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "88666f1dee93fbd85b31fd5d6f91a219e111b5f4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4136: uniform commutation gap", + "evidence": "research/p104-uniform-commutation-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "281ce601a8be9db470de630759179c23e1dfaa88", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4140: uniform encoding gap", + "evidence": "research/p104-uniform-encoding-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "de25c6525aa866962309df5d107b32d55e6e5628", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4153: source-chart shortcut exhausts its optimistic allowance", + "evidence": "research/p104-source-chart-shortcut/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "9123241fea53df77e51ffe30d9aca1625d4bf3a8", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4154: fiber-tag seam mismatch", + "evidence": "research/p104-fiber-tag-seam/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "4ffcdaee5d6255a9cea1fe53a5424435068089d0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove the exact minimum of the full forward carried-frame contact problem at C=15108879/5000000000 using a genuine pair-consistent LP and an exact symbolic dual.", + "scope_change_reason": "The card is changed from constructing a selected helper split to resolving the full-forward exact optimization question left by PR5091 and PR5016. No native supplier or current-frontier gain is claimed.", + "bottleneck_link": "A fixed source word cannot gain at this tariff by any legal contact-frame assignment in the inherited contract. Changed words, boundaries and complete physical invoices remain open; this historical tariff does not certify the current frontier.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified full-forward finite optimization certificate. Do not extend to the backward graph or other exponents.", + "outcome": "completed", + "evidence": "24,788 nonnegative LP columns, 15,524 equalities and 59,077 nonzero coefficients; integer-coefficient symbolic dual, 383 strict nonzero reduced-cost signs, a matching integral primal, eight controls and all original mapped containments for that attainer.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does the same optimum hold on the backward graph?", + "why_it_matters": "A forward certificate does not establish the dual-orientation optimum.", + "first_step": "Build the backward pair-consistent model and seek its own exact dual.", + "blocked_by": "No backward certificate or correspondence is supplied." + }, + { + "question": "For which exponents is this symbolic dual feasible?", + "why_it_matters": "This identifies whether the fixed-tariff obstruction persists under a changed price.", + "first_step": "Certify an interval for the 383 distinct nonzero reduced-cost expressions.", + "blocked_by": "Only one exponent is enclosed here; PR5068 already disproves an all-concave extension." + }, + { + "question": "Can a changed source word or boundary lower a complete signed invoice?", + "why_it_matters": "The fixed-forward model is now exactly closed at the stated tariff.", + "first_step": "Name a changed contract and every new productive and paid fee.", + "blocked_by": "Physical delivery, restoration and full supplier admission are unpriced." + } + ] +} diff --git a/research/pair-consistent-frame-optimum/VERIFY.json b/research/pair-consistent-frame-optimum/VERIFY.json new file mode 100644 index 0000000000..d1a0ffb99e --- /dev/null +++ b/research/pair-consistent-frame-optimum/VERIFY.json @@ -0,0 +1,41 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/carried-warp-frame-intervals/README.md", + "research/carried-warp-frame-intervals/discovery/README.md", + "research/carried-warp-frame-intervals/frame_dag.py", + "research/full-contact-exact-native-optimum/README.md", + "research/native-frame-carrying-swaps/LICENSE", + "research/native-frame-carrying-swaps/NOTICE", + "research/native-frame-carrying-swaps/SOURCE-WORD.json.gz", + "research/native-frame-carrying-swaps/verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Reconstruct all forward domains and compatible pairs; check the complete integral primal, symbolic weak dual, directed power signs, mapped attainer and eight mutations." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Reconstruct all forward domains and compatible pairs; check the complete integral primal, symbolic weak dual, directed power signs, mapped attainer and eight mutations." + } + ] +} diff --git a/research/pair-consistent-frame-optimum/model.py b/research/pair-consistent-frame-optimum/model.py new file mode 100644 index 0000000000..4cb2b50fce --- /dev/null +++ b/research/pair-consistent-frame-optimum/model.py @@ -0,0 +1,145 @@ +"""Pair-consistent carried-frame model. New work produced by Nick Petalas. + +The authenticated construction and frame graph are credited to Cinna Davis; +only their definitions run, without any predecessor scientific replay. +""" +import ast +import copy +import gzip +import hashlib +import json +from collections import Counter +from fractions import Fraction +from pathlib import Path +from types import ModuleType, SimpleNamespace + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def digest(value): + normalized = json.loads(json.dumps(value)) + raw = json.dumps(normalized, sort_keys=True, separators=(",", ":")).encode() + return hashlib.sha256(raw).hexdigest() + + +def authenticate(): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + paths = [row for row in manifest["files"] if row["usage"] == "input"] + need(len(paths) == 8, "Declared input inventory") + result = {} + for row in paths: + payload = (ROOT / row["path"]).read_bytes() + need(hashlib.sha256(payload).hexdigest() == row["sha256"], "Input hash") + result[row["path"]] = payload + return result + + +def load_graph(inputs): + prefix = "research/native-frame-carrying-swaps/" + data = json.loads(gzip.decompress(inputs[prefix + "SOURCE-WORD.json.gz"])) + need(data["canonical"]["h"] == 9, "Fixed nine-dimensional source") + need(len(data["programs"]["forward"]) <= 100000, "Source event bound") + frame = ModuleType("authenticated_frame_definitions") + source = inputs["research/carried-warp-frame-intervals/frame_dag.py"] + exec(compile(source, "authenticated_frame_dag.py", "exec"), frame.__dict__) + tree = ast.parse(inputs[prefix + "verify.py"]) + definitions = [node for node in tree.body + if isinstance(node, ast.FunctionDef) and node.name == "construct"] + need(len(definitions) == 1, "Unique retained constructor") + canonical = data["canonical"] + need(len(canonical["frames"]) <= 5000, "Source frame inventory bound") + masks = [frame.space(vectors) for vectors in canonical["frames"]] + spaces = [{x for x in range(512) if mask >> x & 1} for mask in masks] + namespace = {"c": canonical, "spaces": spaces, "Q": Fraction, + "copy": copy, "V": SimpleNamespace(need=need)} + exec(compile(ast.Module(body=definitions, type_ignores=[]), + "authenticated_construct.py", "exec"), namespace) + program, _, _ = namespace["construct"](data["programs"]["forward"]) + schedule = frame.NativeSchedule(canonical, program) + return frame, schedule + + +def domain(frame, lower, upper, cache): + complement, generated = [], lower + for vector in frame.basis(upper): + if not generated >> vector & 1: + complement.append(vector) + generated = frame.join(generated, frame.space([vector])) + gap = len(complement) + need(gap <= 5, "Fixed-source quotient bound") + if gap not in cache: + values = {1} + for vector in range(1, 1 << gap): + values |= {frame.join(value, frame.space([vector])) for value in tuple(values)} + cache[gap] = sorted(values) + return sorted({frame.join(lower, frame.space( + [frame.linear(complement, v) for v in frame.basis(value)])) + for value in cache[gap]}) + + +def compatible_pairs(frame, left, right, columns): + result = [] + for a, av in enumerate(left): + moved = frame.image(columns, av) + for b, bv in enumerate(right): + if moved & bv == moved: + result.append((a, b, frame.dimension(bv) - frame.dimension(av))) + return result + + +def build_model(frame, schedule): + graph = schedule.graph + lower, upper = graph.bounds() + need(len(lower) <= 16000, "Graph node bound") + cache = {} + domains = {i: domain(frame, a, b, cache) + for i, (a, b) in enumerate(zip(lower, upper)) if a != b} + need(sum(map(len, domains.values())) <= 5000, "Marginal domain bound") + counts, rows, rhs, variables = [], [], [], {} + for i, values in domains.items(): + variables[i] = list(range(len(counts), len(counts) + len(values))) + counts.extend({} for _ in values) + rows.append(dict.fromkeys(variables[i], 1)) + rhs.append(1) + edges = Counter((a, b, m) for b, parents in enumerate(graph.parents) for a, m in parents) + need(sum(edges.values()) <= 30000, "Mapped edge bound") + constant = Counter({8: 8}) + for (a, b, columns), multiplicity in sorted(edges.items()): + if a not in domains and b not in domains: + constant[frame.dimension(lower[b]) - frame.dimension(lower[a])] += multiplicity + elif a not in domains or b not in domains: + i = b if b in domains else a + for j, value in zip(variables[i], domains[i]): + rank = (frame.dimension(value) - frame.dimension(lower[a]) if i == b + else frame.dimension(lower[b]) - frame.dimension(value)) + counts[j][rank] = counts[j].get(rank, 0) + multiplicity + else: + pairs = [] + for ia, ib, rank in compatible_pairs(frame, domains[a], domains[b], columns): + pairs.append((ia, ib, len(counts))) + counts.append({rank: multiplicity}) + for side, i in ((0, a), (1, b)): + for k, variable in enumerate(variables[i]): + row = {j: 1 for ia, ib, j in pairs if (ia if side == 0 else ib) == k} + row[variable] = -1 + rows.append(row) + rhs.append(0) + source = Counter({8: 8}) + for (a, b, _), multiplicity in edges.items(): + rank = frame.dimension(schedule.original_values[b]) - frame.dimension(schedule.original_values[a]) + source[rank] += multiplicity + need(len(counts) <= 25000 and len(rows) <= 16000, "LP size bound") + return {"rows": rows, "rhs": rhs, "counts": counts, "constant": dict(constant), + "source": dict(source), "domains": domains, "variables": variables, + "mapped_edges": sum(edges.values())} + + +def mathematical_digest(model): + keys = ("rows", "rhs", "counts", "constant", "source", "domains", "variables", "mapped_edges") + return digest({key: model[key] for key in keys}) diff --git a/research/pair-consistent-frame-optimum/powers.py b/research/pair-consistent-frame-optimum/powers.py new file mode 100644 index 0000000000..9721ccd7a8 --- /dev/null +++ b/research/pair-consistent-frame-optimum/powers.py @@ -0,0 +1,59 @@ +"""Directed integer bounds for r^(4984891121/5000000000), 1 <= r <= 9. + +Produced by Nick Petalas. Only exact integer and rational arithmetic is used. +""" +from fractions import Fraction +from math import factorial + +SCALE = 1 << 192 +NUMERATOR = 4984891121 +DENOMINATOR = 5000000000 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def log_series(value): + require(Fraction(1) <= value <= 2, "Reduced logarithm domain") + t = (value - 1) / (value + 1) + term, lower = t, 0 + for index in range(128): + summand = 2 * term / (2 * index + 1) + lower += summand.numerator * SCALE // summand.denominator + term *= t * t + tail = 2 * term / (257 * (1 - t * t)) + require(0 <= tail < Fraction(1, SCALE), "Logarithm remainder") + return lower, lower + 129 + + +def price_interval(rank): + require(type(rank) is int and 1 <= rank <= 9, "Rank domain") + if rank == 1: + return SCALE, SCALE + shift = rank.bit_length() - 1 + lower, upper = log_series(Fraction(rank, 1 << shift)) + low_two, high_two = log_series(Fraction(2)) + lower = (lower + shift * low_two) * NUMERATOR // DENOMINATOR + upper = ((upper + shift * high_two) * NUMERATOR + DENOMINATOR - 1) // DENOMINATOR + require(0 <= lower <= upper <= 3 * SCALE, "Exponential domain") + term_low = term_high = total_low = total_high = SCALE + for index in range(1, 257): + divisor = SCALE * index + term_low = term_low * lower // divisor + term_high = (term_high * upper + divisor - 1) // divisor + total_low += term_low + total_high += term_high + remainder = Fraction(3**257, factorial(257)) / (1 - Fraction(3, 258)) + require(remainder < Fraction(1, SCALE), "Exponential remainder") + return total_low, total_high + 1 + + +def polynomial_interval(coefficients, prices): + lower = upper = 0 + for rank, value in enumerate(coefficients, 1): + a, b = prices[rank] + lower += value * (a if value >= 0 else b) + upper += value * (b if value >= 0 else a) + return lower, upper diff --git a/research/pair-consistent-frame-optimum/verify.py b/research/pair-consistent-frame-optimum/verify.py new file mode 100644 index 0000000000..79022e5e76 --- /dev/null +++ b/research/pair-consistent-frame-optimum/verify.py @@ -0,0 +1,145 @@ +#!/usr/bin/env python3 +"""Check the full forward pair-consistent frame optimum without a solver. + +Produced by Nick Petalas. Claim type: finite exact optimization certificate. +""" +import copy +import gzip +import hashlib +import json +import platform +from collections import Counter + +from model import HERE, authenticate, build_model, load_graph, mathematical_digest, need +from powers import SCALE, polynomial_interval, price_interval + + +def histogram(counts, selected, constant): + result = Counter(constant) + for variable in selected: + result.update(counts[variable]) + return [result[rank] for rank in range(1, 10)] + + +def primal_check(model, selected): + need(isinstance(selected, list) and len(selected) <= len(model["counts"]), "Primal inventory") + need(all(type(j) is int and 0 <= j < len(model["counts"]) for j in selected), "Primal index") + need(len(set(selected)) == len(selected), "Primal uniqueness") + support = set(selected) + for row, rhs in zip(model["rows"], model["rhs"]): + need(sum(value for j, value in row.items() if j in support) == rhs, "Primal marginal equation") + return histogram(model["counts"], selected, model["constant"]) + + +def dual_remainders(model, dual): + need(len(dual) == len(model["rows"]), "Dual row inventory") + need(all(isinstance(row, list) and len(row) == 5 for row in dual), "Dual price basis") + need(all(type(x) is int and abs(x) <= 256 for row in dual for x in row), "Dual coefficient bound") + reduced = [[hist.get(rank, 0) for rank in range(1, 6)] for hist in model["counts"]] + for row, vector in zip(model["rows"], dual): + for variable, value in row.items(): + for k in range(5): + reduced[variable][k] -= value * vector[k] + return reduced + + +def dual_check(model, dual, prices): + need(all(set(hist) <= set(range(6)) for hist in model["counts"]), "Variable rank basis") + reduced = dual_remainders(model, dual) + distinct = Counter(tuple(row) for row in reduced) + positive = [] + for vector in distinct: + if any(vector): + lower, _ = polynomial_interval(vector, prices) + need(lower > 0, "Dual reduced-cost sign") + positive.append(lower) + objective = [model["constant"].get(rank, 0) for rank in range(1, 10)] + for rhs, vector in zip(model["rhs"], dual): + for k, value in enumerate(vector): + objective[k] += rhs * value + return objective, {"distinct_reduced_costs": len(distinct), + "zero_reduced_cost_columns": distinct[(0, 0, 0, 0, 0)], + "strict_signs": len(positive), + "minimum_positive_lower_over_scale": [min(positive), SCALE]} + + +def certificate_check(model, certificate, prices): + need(certificate["schema_version"] == 1, "Certificate schema") + need(certificate["model_sha256"] == mathematical_digest(model), "Mathematical model digest") + primal = primal_check(model, certificate["primal_ones"]) + dual, signs = dual_check(model, certificate["dual"], prices) + source = [model["source"].get(rank, 0) for rank in range(1, 10)] + need(primal == dual == source, "Coefficientwise primal-dual-source equality") + need(primal == certificate["optimum_histogram"], "Certificate objective") + return primal, signs + + +def rejection(action, message): + try: + action() + except ValueError as error: + need(message in str(error), "Unexpected rejection reason") + return message + raise ValueError("Mutation accepted: " + message) + + +def controls(model, certificate, prices): + results = [] + changed = certificate["primal_ones"][:-1] + results.append(rejection(lambda: primal_check(model, changed), "Primal marginal equation")) + results.append(rejection(lambda: primal_check(model, [-1]), "Primal index")) + changed = certificate["primal_ones"] + certificate["primal_ones"][:1] + results.append(rejection(lambda: primal_check(model, changed), "Primal uniqueness")) + dual = copy.deepcopy(certificate["dual"]) + dual[0][0] += 1 + results.append(rejection(lambda: dual_check(model, dual, prices), "Dual reduced-cost sign")) + dual = copy.deepcopy(certificate["dual"]) + dual.pop() + results.append(rejection(lambda: dual_check(model, dual, prices), "Dual row inventory")) + changed = dict(model) + changed["rows"] = model["rows"][:-1] + results.append(rejection(lambda: certificate_check(changed, certificate, prices), "Mathematical model digest")) + changed = dict(certificate) + changed["optimum_histogram"] = certificate["optimum_histogram"][:] + changed["optimum_histogram"][0] -= 1 + results.append(rejection(lambda: certificate_check(model, changed, prices), "Certificate objective")) + results.append(rejection(lambda: price_interval(0), "Rank domain")) + return results + + +def actual_assignment(schedule, model, selected): + support = set(selected) + values = schedule.original_values[:] + for i, variables in model["variables"].items(): + chosen = [k for k, j in enumerate(variables) if j in support] + need(len(chosen) == 1, "Integral frame marginal") + values[i] = model["domains"][i][chosen[0]] + schedule.graph.check(values) + return sum(a != b for a, b in zip(values, schedule.original_values)) + + +def main(): + inputs = authenticate() + frame, schedule = load_graph(inputs) + model = build_model(frame, schedule) + raw_certificate = gzip.decompress((HERE / "CERTIFICATE.json.gz").read_bytes()) + need(len(raw_certificate) <= 1048576, "Certificate size") + certificate = json.loads(raw_certificate) + prices = {rank: price_interval(rank) for rank in range(1, 10)} + optimum, signs = certificate_check(model, certificate, prices) + changed = actual_assignment(schedule, model, certificate["primal_ones"]) + rejected = controls(model, certificate, prices) + hashes = {path.name: hashlib.sha256(path.read_bytes()).hexdigest() + for path in sorted(HERE.iterdir()) if path.is_file()} + result = {"status": "PASS_PAIR_CONSISTENT_FRAME_OPTIMUM", "claim_type": "finite exact optimization certificate", + "orientation": "forward", "saving": "15108879/5000000000", "optimum_histogram_ranks_1_to_9": optimum, + "nodes": len(schedule.graph.fixed), "mapped_edges": model["mapped_edges"], + "flexible_contacts": len(model["domains"]), "marginal_choices": sum(map(len, model["domains"].values())), + "columns": len(model["counts"]), "equalities": len(model["rows"]), + "nonzero_coefficients": sum(map(len, model["rows"])), "attainer_changed_frames": changed, + "dual": signs, "controls": rejected, "python": platform.python_version(), "sha256": hashes} + print(json.dumps(result, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()