Prove the exact full forward carried-frame optimum (no κ)

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.

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.

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).