From e07ed3d60124234d9805b789dbddd8c1badad3aa Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 13:34:17 +0000 Subject: [PATCH] feat(research): prove the exact integer carrier height --- .../integer-carrier-height/PREDECESSOR.json | 20 ++ research/integer-carrier-height/PROOF.md | 99 ++++++++++ research/integer-carrier-height/README.md | 135 +++++++++++++ research/integer-carrier-height/SOURCES.json | 18 ++ research/integer-carrier-height/TASK.json | 127 +++++++++++++ research/integer-carrier-height/VERIFY.json | 33 ++++ .../integer-carrier-height/independent.py | 66 +++++++ .../integer-carrier-height/retained/PROOF.md | 134 +++++++++++++ .../retained/frontier.py | 161 ++++++++++++++++ research/integer-carrier-height/verify.py | 178 ++++++++++++++++++ 10 files changed, 971 insertions(+) create mode 100644 research/integer-carrier-height/PREDECESSOR.json create mode 100644 research/integer-carrier-height/PROOF.md create mode 100644 research/integer-carrier-height/README.md create mode 100644 research/integer-carrier-height/SOURCES.json create mode 100644 research/integer-carrier-height/TASK.json create mode 100644 research/integer-carrier-height/VERIFY.json create mode 100644 research/integer-carrier-height/independent.py create mode 100644 research/integer-carrier-height/retained/PROOF.md create mode 100644 research/integer-carrier-height/retained/frontier.py create mode 100644 research/integer-carrier-height/verify.py diff --git a/research/integer-carrier-height/PREDECESSOR.json b/research/integer-carrier-height/PREDECESSOR.json new file mode 100644 index 0000000000..cd4167b9e9 --- /dev/null +++ b/research/integer-carrier-height/PREDECESSOR.json @@ -0,0 +1,20 @@ +{ + "repository": "CrocSwap/integer-mult-bounds", + "pull_request": 5787, + "commit": "08f0e5899254aa82288a91e70789049dc1f29690", + "author": "Richard Hoekstra", + "files": [ + { + "retained_path": "retained/PROOF.md", + "origin_path": "research/pr5413-carrier-frontier/PROOF.md", + "git_blob": "5a1148d936dc6c1783fc2f993306697b1f5af7a5", + "sha256": "7e6dbcd2937601b107de31c1c2f64be886a4dde6741a30b7cc99bd59cc5528c8" + }, + { + "retained_path": "retained/frontier.py", + "origin_path": "research/pr5413-carrier-frontier/frontier.py", + "git_blob": "8781900ee63d1e6191b382385733212784cd2686", + "sha256": "2d1837eed6e828298f4e02ca9105ed4595b2d305354477e42b97fb3ad20d27fc" + } + ] +} diff --git a/research/integer-carrier-height/PROOF.md b/research/integer-carrier-height/PROOF.md new file mode 100644 index 0000000000..177bca5e92 --- /dev/null +++ b/research/integer-carrier-height/PROOF.md @@ -0,0 +1,99 @@ +# The minimum integer height of the fixed logarithmic guard + +New proof produced by Nick Petalas. Apache-2.0. + +## Statement and provenance + +Fix p=322 and d=1/700000000000. For positive integer H, consider + + (H+1)^p < 2^(d H). (1) + +The minimum such H is + + H* = 12040587444441491. + +Every integer H>=H* satisfies (1), and every positive integer H8*1024 holds at H*. + +Richard Hoekstra's PR #5787, head +08f0e5899254aa82288a91e70789049dc1f29690, supplies this guard through the +logarithmic majorant in retained/PROOF.md sections 2 and 3. Its fixed-kappa +case in retained/frontier.py has p=322, tested saving .003027288245 and +declared saving .003027288235. Its rule d=(s-k)/7 gives the d above. +It supplies sufficient grid height 12040700000000000 and expressly does +not claim the minimum integer height. Those source statements are premises +for the compiler interpretation, not new results proved in this package. + +## Why two adjacent comparisons settle the whole domain + +For real x>0 put r(x)=ln(1+x)/x. Differentiation gives + + r'(x) = [x/(1+x) - ln(1+x)]/x^2 < 0. + +The strict sign follows directly from + + ln(1+x) = integral_0^x 1/(1+t) dt > x/(1+x). + +Taking logarithms in (1) and dividing by H shows that (1) holds exactly +when r(H)3/2 it uses +ln(a)=ln(2a/3)+ln(3/2), so every series argument remains in [1,3/2]. +It proves the same two strict signs using exact fractions, without sharing +the positive-series tail or dyadic rounding implementation. + +## Improvement and limits + +The difference from the cited sufficient grid height is exactly +112555558509. This improves the isolated logarithmic guard at fixed p and +d. It is not another evaluation of a paid-moment root or a review of the +predecessor's complete application. + +The result does not establish that the complete source compiler can be +instantiated at N=2^H*. In particular the changed finite-template counts, +precision and conjunction application, integer layout and physical +implementation need their own proof at that N. All source assumptions +remain. No global compiler optimum, complete multiplication theorem or +new kappa is claimed. diff --git a/research/integer-carrier-height/README.md b/research/integer-carrier-height/README.md new file mode 100644 index 0000000000..e34f4e4c9c --- /dev/null +++ b/research/integer-carrier-height/README.md @@ -0,0 +1,135 @@ +# Exact integer height for a logarithmic compiler guard + +Scoped mathematical proof, produced by Nick Petalas. Apache-2.0. + +For the fixed guard in Richard Hoekstra's +[PR #5787](https://github.com/CrocSwap/integer-mult-bounds/pull/5787), + +```text +(H+1)^322 < 2^(H/700000000000), H a positive integer, +``` + +the minimum height is exactly **12040587444441491**. Every larger integer +height passes, and every smaller positive integer height fails. This is +**112555558509** below the cited sufficient grid height 12040700000000000. +The separate guard H>8192 also holds. + +The new step removes the restriction H=ceil(j/d) for this inequality. It +does not audit the predecessor's complete caller, or claim that its full +application has already been instantiated at the smaller height. The +selected frontier and kappa do not change. + +## Proof and evidence + +[PROOF.md](PROOF.md) proves that ln(1+H)/H strictly decreases for H>0. +Consequently exact opposite signs at two adjacent integers settle the +entire positive integer domain. For D(H)=H/700000000000-322 log2(H+1), +the checker proves the rational brackets + +```text +-36/10^15 < D(12040587444441490) < -35/10^15 +1354/10^15 < D(12040587444441491) < 1355/10^15 +``` + +verify.py uses an exact positive odd-power logarithm series and outward +dyadic rounding. independent.py uses a separately implemented alternating +Mercator series and imports no primary or predecessor executable. + +Local CPython 3.12.15 warning-strict checks pass both adjacent comparisons, +1024 small exact integer-power comparisons, 65 exact power-of-two logarithms +and 17 rejection controls. These are finite checks supporting the written +all-height proof. They are not proof-kernel or independent human review. + +## Reproduce + +From the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/integer-carrier-height/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/integer-carrier-height/independent.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/integer-carrier-height +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/integer-carrier-height --check-source-history +``` + +Any CPython 3.12 interpreter can replace the local executable path. The +standalone scripts use only the standard library and work without Git. +An optional `verify.py --receipt /absolute/output/path` writes a generated +receipt binding every package file's SHA256. Ordinary checks write nothing. + +Expected markers: + +```text +PASS_INTEGER_CARRIER_HEIGHT minimum=12040587444441491 reduction=112555558509 small_exact=1024 controls=13 +PASS_INDEPENDENT_INTEGER_HEIGHT minimum=12040587444441491 adjacent_signs=2 exact_powers=65 controls=4 +``` + +## Sources and credit + +Richard Hoekstra's PR #5787 at exact head +08f0e5899254aa82288a91e70789049dc1f29690 supplies the fixed parameters, +the complete paid-tail application and the explicit unclaimed integer-height +boundary. Its PROOF.md and frontier.py are retained verbatim in retained/. +[PREDECESSOR.json](PREDECESSOR.json) records their origin paths, Git blobs +and SHA256 hashes. They were retrieved from the repository contents API at +that exact head. The checker verifies both hashes and source parameter +literals, but never executes the predecessor code or reruns its result. +Retaining these two interface sources makes replay independent of an +unmerged commit's availability. The source-history preflight separately +checks the ancestor provenance in SOURCES.json. + +The source retains zxv's logarithmic compiler, Jacob Alan Sussman's mixed +flow, Chris R/Clear1nsight's #5413 caller and exact arithmetic, Dillon +Amburgey's provider, Ali Romman's controller, Cao Yifan's native word, +Cinna Davis's helper/product lineage and their cumulative notices. +The new integer-height theorem and checkers are produced by Nick Petalas. +Independent human and formal proof-kernel review are unclaimed. + +The upstream checkpoint is de5ec2e7a6074068452f45b1a191b5c72832df4a, +priority revision 8. TASK.json records the changed scope from an audit card +to original parameter optimization, the overlap limits and next question. +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19217785) +states the same guard-only scope. + +## Limitations + +This proves the exact threshold of one fixed logarithmic inequality. It +does not minimize over p, d, compiler geometries, paid profiles or suppliers. +The full changed-height finite-template, precision, conjunction, layout and +physical implementation obligations remain open. No predecessor supplier +replay, selected cold replay, Lean build or complete multiplication theorem +is supplied. No scientific obligation is delegated to CI alone. + +The new checkers use managed Python fractions. Their fixed series lengths, +64-bit height domain, fixed small control domains and at-most-32-file receipt +inventory bound the work. Runtime allocation remains a managed-language +deviation from Power of Ten's static-storage rule. No recursion, dynamic +code execution, numerical logarithm library or optimization-sensitive Python +assertion is used in the new checkers. Retained code is an immutable cited +source and is not executed. + +## Open next questions + +Can the full PR #5787 finite-template and precision application be instantiated +at this exact height? Start by deriving its height-dependent counts, +rounding, precision and conjunction guards at H=12040587444441491, with every +paid tail retained. A complete changed-N application and any required layout +integrality are missing. This package's logarithmic threshold alone does +not settle those obligations. + +## Related open work + +- [#5787](https://github.com/CrocSwap/integer-mult-bounds/pull/5787) supplies + the complete #5413 carrier application and sufficient grid height. This + package proves the minimum integer height for its fixed logarithmic guard. +- [#5899](https://github.com/CrocSwap/integer-mult-bounds/pull/5899) determines + a different PR5756 tail-gate block-length threshold. It does not compute + this #5413 integer-height guard, and is not a predecessor of this result. + +Merged PRs #5462 and #5468 refine the #5413 saving and its gap-parametric +precision. They retain sufficient height grids and do not compute this +fixed guard's minimum integer height. This package changes neither result. + +## CI notes + +Hosted replay is pending. All registered scientific commands run locally; +no hosted scientific pass is claimed in advance. diff --git a/research/integer-carrier-height/SOURCES.json b/research/integer-carrier-height/SOURCES.json new file mode 100644 index 0000000000..fdb80ada25 --- /dev/null +++ b/research/integer-carrier-height/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ] +} diff --git a/research/integer-carrier-height/TASK.json b/research/integer-carrier-height/TASK.json new file mode 100644 index 0000000000..453e38abe4 --- /dev/null +++ b/research/integer-carrier-height/TASK.json @@ -0,0 +1,127 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "independent-moment", + "question": "Does a changed construction's serialized target/paid invoice independently support its claimed improvement?", + "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", + "docs/research/recursive-invoice-preflight.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": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "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": "Independently recount one changed emitted word and its complete caller, importing no constructor or pricing engine. Include target losses, owned lifetimes, native orientation and extra charges. Check existing #5633/#5708/#5717/#5719 coverage to avoid duplicate audits and preserve its exact head. Stop after the chosen missing implication; a correct root alone is not supplier admission.", + "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": [ + "invoice", + "signed moment", + "productive target", + "independent recount" + ], + "existing_checks": [ + { + "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.", + "evidence": "research/staged-fourth-mixture-ceiling/README.md", + "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.", + "status": "author-checked", + "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.", + "evidence": "research/r437-two-window-carrier/README.md", + "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.", + "status": "author-checked", + "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e", + "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": "Determine the minimum positive integer H for (H+1)^322 < 2^(H/700000000000), removing PR5787's rational-gap grid restriction.", + "scope_change_reason": "The donation requests original research, not an audit. After connector orientation and eligibility checks, take PR5787's explicit unclaimed integer-height boundary as a separate compiler-parameter optimization. No predecessor scientific replay is performed.", + "bottleneck_link": "A smaller logarithmic guard threshold removes rounding-grid slack in a finite compiler parameter. This is a local parameter theorem; the complete smaller-carrier caller application remains open.", + "budget_minutes": 60, + "stop_rule": "Stop at the first strict integer-height improvement with an adjacent-sign certificate and an all-positive-height minimality proof.", + "outcome": "completed", + "evidence": "PROOF.md, verify.py and independent.py certify minimum 12040587444441491 and reduction 112555558509 from the cited sufficient grid height.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can the complete PR5787 finite-template and precision application be instantiated at this exact integer height?", + "why_it_matters": "The isolated guard improvement does not itself certify a smaller complete conditional carrier.", + "first_step": "Re-derive the height-dependent counts, rounding, precision and conjunction guards at H=12040587444441491 while retaining every paid tail and caller obligation.", + "blocked_by": "A full changed-N application and any required layout integrality have not been supplied." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19217785", + "environment": { + "python": "3.12.15", + "implementation": "CPython", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12" + }, + "source": { + "pull_request": 5787, + "author": "RichardHoekstra", + "head": "08f0e5899254aa82288a91e70789049dc1f29690" + }, + "overlap": { + "upstream": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "priority_revision": 8, + "claim_checked_at": "2026-10-27T13:26:31Z", + "open_pr_records": 470, + "discussion_records": 5426, + "remote_pagination": "complete at cached times 13:22:06Z and 13:23:11Z", + "local_note_search": "225 materialized records; 7620 HEAD note paths omitted from cached local scan; separate full-Git README searches covered distinctive formulas and heights.", + "bounded_searches": [ + "All open PR title/author inventory; latest 30 handoff comments and active Discussions.", + "Own latest 200 PRs, with targeted last-seven-day source searches.", + "Merged searches for exact height, minimum logarithmic height and integer carrier height.", + "Full Git README searches for 12040587444441491, 112555558509, 322 with denominator 700000000000, and the cited grid height." + ], + "limits": "No exhaustive nested-code or historical-diff novelty proof; the focused checks found no earlier delivery of this guard threshold." + } +} diff --git a/research/integer-carrier-height/VERIFY.json b/research/integer-carrier-height/VERIFY.json new file mode 100644 index 0000000000..5c54fd608b --- /dev/null +++ b/research/integer-carrier-height/VERIFY.json @@ -0,0 +1,33 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Positive-series exact adjacent signs, all-integer proof brackets, 1024 independent integer-power comparisons, 13 invalid-claim/domain/source controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Independent alternating-series adjacent signs, 65 exact powers of two and four malformed input controls." + } + ] +} diff --git a/research/integer-carrier-height/independent.py b/research/integer-carrier-height/independent.py new file mode 100644 index 0000000000..0945eebef2 --- /dev/null +++ b/research/integer-carrier-height/independent.py @@ -0,0 +1,66 @@ +#!/usr/bin/env python3 +"""Alternating-series height certificate. Produced by Nick Petalas. Apache-2.0.""" + +from fractions import Fraction + + +def check(condition, message): + if not condition: + raise ValueError(message) + + +def mercator(value): + """Two successive partial sums bracket ln(value) on [1, 3/2].""" + check(Fraction(1) <= value <= Fraction(3, 2), "Mercator domain") + x = value - 1 + partial = Fraction(0) + power = x + for index in range(1, 257): + partial += (1 if index % 2 else -1) * power / index + power *= x + return partial, partial + power / 257 + + +def log2(value): + check(type(value) is int and 1 <= value <= 1 << 64, "positive bounded integer") + exponent = value.bit_length() - 1 + unit = Fraction(value, 1 << exponent) + three_low, three_high = mercator(Fraction(3, 2)) + four_low, four_high = mercator(Fraction(4, 3)) + base_low, base_high = three_low + four_low, three_high + four_high + if unit > Fraction(3, 2): + low, high = mercator(unit * Fraction(2, 3)) + low, high = low + three_low, high + three_high + else: + low, high = mercator(unit) + check(base_low > 0, "positive base") + return exponent + low / base_high, exponent + high / base_low + + +def main(): + height = 12040587444441491 + low, high = log2(height) + before = Fraction(height - 1, 700000000000) - 322 * low + check(before < 0, "preceding integer loses") + low, high = log2(height + 1) + after = Fraction(height, 700000000000) - 322 * high + check(after > 0, "new integer wins") + exact = 0 + for exponent in range(0, 65): + low, high = log2(1 << exponent) + check(low <= exponent <= high, "power-of-two logarithm") + exact += 1 + rejected = 0 + for bad in [0, -1, True, 1 << 65]: + try: + log2(bad) + except ValueError: + rejected += 1 + else: + raise ValueError("malformed logarithm input accepted") + print(f"PASS_INDEPENDENT_INTEGER_HEIGHT minimum={height} adjacent_signs=2 " + f"exact_powers={exact} controls={rejected}") + + +if __name__ == "__main__": + main() diff --git a/research/integer-carrier-height/retained/PROOF.md b/research/integer-carrier-height/retained/PROOF.md new file mode 100644 index 0000000000..5a1148d936 --- /dev/null +++ b/research/integer-carrier-height/retained/PROOF.md @@ -0,0 +1,134 @@ +# Changed-tuple carrier application to the frozen PR5413 caller + +This is a conditional application of the existing higher-moment and logarithmic +compiler theorems. The raw native word, all-column/owner contracts and the five +selected framework assumptions remain premises. No new raw profile or root is +claimed. Source paths, exact Git blobs and SHA256 are in SOURCES.json. + +## 1. Complete paid charge + +The source has 10,928 productive fields, 64,260 paid jobs and ambient rank 145. +For raw moments T_t and P_t, tested saving s, t=1-s, u>=s and integer v>=1, put + +``` +alpha=P_t/T_t, +gamma=P_(t+u)/(c^u*T_t), +delta=10928*b/(c^s*T_t), 1J, the final incomplete split block +is included in `q*J^t+r^t<=2*R*J^(-s)`; the higher moment is valid because +`t+u>=1`. Completion includes the same final-block allowance and every owner. +The final productive moment is at least the raw T_t^v, so normalization by that +smaller quantity is conservative. No new field or unpaid child is introduced. + +The old `.97` bounds and `4/2^32` debit were sufficient upper estimates of those +same charged jobs. The new certificate evaluates all three terms directly with +outward rational bounds. It does not add the old sufficient debit as a second +copy of physical work. In particular the fixed-kappa point has gamma>.97 but +its full paid bound is still strictly below one. The source's old conjunction +correctly rejects that point; its changed application is explicit here. + +The public `exact_moments.py` helper is authenticated and reused with attribution, +not called an independent implementation. Its rational logarithm/exponential +enclosures are rounded outward before integer powers; each positive paid term +is rounded upward again, and their exact sum must be below one. + +## 2. Logarithmic majorant + +For theta=A/D<1, the inherited theorem requires + +``` +c^D < b^A, +2^(D-A)*c^(v*D) <= 145^(v*A), +theta^p < (1-s)*145^(-v*s), +145^(v*s) < 2^p, p a positive integer. +``` + +All are checked with integers or directed rational bounds. They imply the +source compiler's normalized leaf bound +`L(n)<=n^(1-s)*(1+log2 n)^p`. For declared saving k use the inherited slack +family d=(s-k)/7, uniform=k+6d, b_outer=k+5d, a_outer=k+4d, q_outer=k+3d, +epsilon=1-d, beta=1-3d, r0=d/10 and stop=layout=d. The actual source ledger's +54 strict predicates, four functional guards and nine cost rows are recomputed. +The ordinary BIT saving .0034 and atom .004 remain fixed and funded. + +## 3. A rational-gap carrier grid + +Set `H_j=ceil(j/d)` for positive integers j. A successful grid point obeys +`H_j>8v` and `(H_j+1)^p<2^j<=2^(d*H_j)`. Thus at N=2^H_j the leaf bound is +strictly below `N^(1-s+d)=N^(1-uniform)`. The new construction does not require +the numerator of d to be one; every rank and program count remains integral. + +For the implemented domain `0=1/d>16`, hence `(H_j+1)^p>2^(4p)>=2^j`. +- For `j>=4p`, `H_(j+1)-H_j<=ceil(1/d)`. Therefore + `(H_(j+1)+1)/(H_j+1)<=1+(1+d)/j`. Raising this ratio to p gives less than + `exp(17/64)<2`, using `log 2>1/2`. The left comparison grows by less than + two while the right comparison doubles. Once the grid succeeds it stays + successful, and the preceding tested grid point fails exactly. + +No minimal integer H, global compiler optimum or maximal kappa is claimed. + +## 4. Fresh finite-template and precision application + +The original V16 application proof already counts the actual source's 145-axis +maps, 418 private fields, scalar/ordinary records and dyadic coefficient height +below A0=2^128. Those data and all raw source/field-ID/route bindings are unchanged. +For product v, the same strictified-unit overestimate becomes + +``` +2*(v*(2+2*128)+10+2*(8v))+6+3*(8v+1)=572v+29. +``` + +It remains below 1048576 on the declared v<=1024 domain. Keep the conservative +original `D0=2^1048576`, and reapply exactly the same constructive F16 recursion +at the new N. No count from the raw template is silently reused as an expanded +count. The resulting M=F16(N) bounds W,P,U,O,R,G, with the source's updated +ordinary/precision/parked-stock prescriptions. D0 and M enter eventual outer +constants, not a claim that they fit below N^d. All relevant outer gaps remain +strict. The tensor product, paid completion and disjoint splitting are the +retained finite algorithm, including their complete owners and whole-job adapters. + +`application.py` verifies seven numerical substitution sites in the accepted +V16 proof and inserts the preceding complete-charge/grid application paragraph. +It builds each full instance only in scratch and binds its SHA256 in the source +and conjunction manifests. The generated precision checker changes three exact +source sites: product/ambient-log parameters, positive rational gap, and the +positive-power ceiling-grid checks. On the original manifest it reproduces the +entire original precision payload except timing/checker/manifest hashes. + +The conjunction adapter changes six named applications: endpoint/gap, complete +moment funding, partial-block charging, carrier grid, fresh F16 count bound and +the instantiated proof hash. The old fixed-envelope minimum-reserve gate becomes +an explicit complete paid-sum gate. The other 19 conditions are compared in the +AST and stay unchanged, including complete profile equality, actual owners, +all-column source packet/phase/route bindings, ordinary BIT/stock and component +false flags. All 25 adapted conditions pass for each point. This is a new +conditional application receipt, not an upstream approval or proof-kernel result. + +## 5. Replay coverage and remaining premises + +Every registered replay first runs the unchanged complete PR5413 eight-engine +master and compares its frozen outputs. Those source-identical native, local, +whole-caller, field-ID and invoice results are reused across the five new tuples. +Each tuple then has fresh directed funding, full outer checks, generated written +application, precision check and conjunction. Meaningful controls reject the old +coarse application, a preceding carrier grid, product outside the declared safe +domain, a missing paid job, free completion and an invalid higher-moment offset. + +The five premises are unchanged: native_all_columns, owned_erasure, compiler, +precision_tape and analytic_recovery. No uniform word or physical Turing tape is +materialized, no independent human verification is claimed, and no practical +runtime improvement follows from the smaller sufficient carrier. + +Credit the source higher-moment/log compiler to zxv; mixed-target flow to Jacob +Alan Sussman; chronological products/completion and helpers to Cinna Davis and +the retained lineage; PR5413 application/checkers to Chris R/Clear1nsight, using +Dillon Amburgey's provider, Ali Romman's controller and Cao Yifan's native word. +Richard Hoekstra prepared this application with OpenAI Codex assistance. +New work is Apache-2.0; source-specific notices remain in the frozen inputs. diff --git a/research/integer-carrier-height/retained/frontier.py b/research/integer-carrier-height/retained/frontier.py new file mode 100644 index 0000000000..8781900ee6 --- /dev/null +++ b/research/integer-carrier-height/retained/frontier.py @@ -0,0 +1,161 @@ +#!/usr/bin/env python3 +"""Source-bound carrier certificates, retaining the complete PR5413 invoice. + +Apache-2.0. Richard Hoekstra, with substantial OpenAI Codex assistance. +The higher-moment/logarithmic compiler is zxv's; the mixed flow is Jacob +Alan Sussman's. Arithmetic helpers and the outer ledger are authenticated +public sources credited to Chris R/Clear1nsight and their retained lineage. +This module does not independently reimplement those arithmetic helpers. +""" +import copy +import hashlib +import json +from fractions import Fraction as Q +from pathlib import Path + +AGENTS = 'swarm-coupled-caller-sol-high-20261024/agents/' +INVOICE = AGENTS+'invoice/' +PRECISION = AGENTS+'precision/' +TEMPLATE = 'carrier-frontier/BASELINE-FUNDING.json' +TEMPLATE_SHA = '70ab7d13548962097ad83ad393b8482f52e827b8996869011ce6d071146bd3eb' +MOMENTS = INVOICE+'exact_moments.py' +MOMENTS_SHA = 'cf7439c9eb4095224126dd5eefc9f1c5dfe1968d6e8eca5b87d4a3897841182d' +OUTER = 'swarm-next-gain-sol-high-20261024/agents/numeric/exact_engine.py' +OUTER_SHA = '9ef7ee4082631566eb7903c3e21e517ef58039dca2a47104a2279c459589eb47' +BASE_K = Q('0.003027288235') +BASE_S = Q('0.003027288245') +CASES = [dict(name='fixed-kappa', k=BASE_K, s=BASE_S, v=1024, c=18, b=21, + u=Q(1, 10), theta=Q(61, 64), p=322, H=12040700000000000, j=17201)] +for name, k, v, p, H, j in [ + ('saving-003', Q('.003'), 512, 120, 1239850102, 3625), + ('saving-00275', Q('.00275'), 256, 59, 50859231, 1511), + ('saving-0025', Q('.0025'), 256, 58, 25258797, 1427), + ('saving-002', Q('.002'), 256, 55, 11738348, 1292), +]: + CASES.append(dict(name=name, k=k, s=k+Q(3, 4)*(BASE_S-k), v=v, c=17, b=21, + u=Q(1, 10), theta=Q(15, 16), p=p, H=H, j=j)) + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def sha(path): + return hashlib.sha256(Path(path).read_bytes()).hexdigest() + + +def encode(value): + if isinstance(value, Q): + return str(value) + if isinstance(value, dict): + return {str(k): encode(v) for k, v in value.items()} + if isinstance(value, (tuple, list)): + return [encode(v) for v in value] + return value + + +def load_source(root, relative, digest): + path = root/relative + need(sha(path) == digest, 'changed public arithmetic input: '+relative) + space = {'__name__': '_carrier_public_helper', '__file__': str(path)} + exec(compile(path.read_bytes(), str(path), 'exec', dont_inherit=True, optimize=0), space) + return space + + +def ceilq(x): + return -((-x.numerator)//x.denominator) + + +def upper(x): + scale = 2**192 + return Q(ceilq(x*scale), scale) + + +def grid(p, gap): + need(type(p) is int and p > 0 and 0 < gap < Q(1, 16), 'proved positive carrier-grid domain') + def at(j): + return ceilq(Q(j)/gap) + def wins(j): + return (at(j)+1)**p < 2**j + low, high = 1, 2 + while not wins(high): + low, high = high, 2*high + while high-low > 1: + mid = (low+high)//2 + if wins(mid): + high = mid + else: + low = mid + need(wins(high) and not wins(high-1), 'first successful sufficient height grid') + return at(high), high + + +def certify(root, case): + need(sha(root/TEMPLATE) == TEMPLATE_SHA, 'frozen complete source invoice') + baseline = json.loads((root/TEMPLATE).read_bytes()) + E = load_source(root, MOMENTS, MOMENTS_SHA) + ledger = load_source(root, OUTER, OUTER_SHA)['ledger'] + power, moment = E['power'], E['moment'] + P, T = ({int(r): n for r, n in baseline[key].items()} for key in ('paid', 'targets')) + need(sum(P.values()) == 64260 and sum(T.values()) == 10928, 'full source profile') + k, s, v, c, b, u, theta, p = (case[key] for key in ('k', 's', 'v', 'c', 'b', 'u', 'theta', 'p')) + t, d = 1-s, (s-k)/7 + target, paid = moment(T, t), moment(P, t) + alpha = upper(paid[1]/target[0]) + gamma = upper(moment(P, t+u)[1]/(power(c, u)[0]*target[0])) + delta = upper(Q(b*sum(T.values()))/(power(c, s)[0]*target[0])) + original_paid = upper(alpha**v) + higher_tail, completion_tail = upper(2*gamma**v), upper(2*delta**v) + complete = original_paid+higher_tail+completion_tail + eta = (1-s)*power(145, -v*s)[0] + H, j = grid(p, d) + n, den = theta.numerator, theta.denominator + predicates = dict( + ordered_savings=0 < k < s < Q('.0034'), raw_moment=target[0] > paid[1], + funded_alpha_reserve=alpha < 1-Q(1, 10**12), higher_moment_domain=u >= s, + positive_partial_block_charges=higher_tail > 0 and completion_tail > 0, + exact_completed_moment=complete < 1, split=1 < c < b < 145, + true_exit_exponent=c**den < b**n, + shifted_exits=2**(den-n)*c**(v*den) <= 145**(v*n), + eta=eta > theta**p, initial_range=power(145, v*s)[1] < 2**p, + height=H > 8*v and (H, j) == (case['H'], case['j'])) + need(all(predicates.values()), 'unfunded carrier predicates: '+str(predicates)) + parameters = dict(kappa=k, tested_saving=s, complex_uniform_saving=k+6*d, + b=k+5*d, a=k+4*d, q=k+3*d, bit_saving=Q('.0034'), + bit_atom=Q('.004'), epsilon=1-d, beta=1-3*d, r0=d/10, + stop=d, layout=d, d=d) + margins, strict, functional = ledger(parameters) + need(set(strict) == set(baseline['source_predicates']['strict']) and + set(functional) == set(baseline['source_predicates']['functional']), '54+4 source inventory') + need(len(strict) == 54 and len(functional) == 4 and + min(strict.values()) > 0 and min(functional.values()) > 0, 'strict full outer ledger') + result = copy.deepcopy(baseline) + for obsolete in ('strict_minimum_rounding_reserve', 'reserve_above_minimum', + 'reserve_slack', 'preceding_grid_fails'): + result.pop(obsolete, None) + result.update(case=case['name'], kappa=k, tested=s, gap=d, H=H, j=j, + tuple=dict(ambient=145, cutoff=c, floor=b, offset=u, tensor_power=v, + theta=theta, logarithm_power=p), + raw_tested_margin=(target[0]-paid[1], target[1]-paid[0]), + alpha_upper=alpha, gamma_upper=gamma, delta_upper=delta, eta_lower=eta, + normalized_paid_upper=complete, original_paid_upper=original_paid, + higher_tail_upper=higher_tail, completion_tail_upper=completion_tail, + completion_slack=1-complete, reserve_slack=1-Q(1, 10**12)-alpha, + predicates=predicates, outer=dict(parameters=parameters, margins=margins, + strict=strict, functional=functional, minimum_strict=min(strict.values()), + minimum_functional=min(functional.values())), + gain_over_comparison=k-Q('.00302728823'), + charging_model='complete-higher-moment-sum-with-both-partial-block-tails', + grid_success=True, preceding_grid_fails=True, + grid_scope='First j on H=ceil(j/gap) for this sufficient logarithmic majorant; no global template minimum.', + controls={}, possible_gain_type='smaller carrier at unchanged or explicitly weaker exponent saving', + scope='Source-bound numerical carrier certificate only; changed-tuple precision and physical conjunction are separate checks.') + return encode(result) + + +def verify_funding(root, received): + cases = [c for c in CASES if c['name'] == received.get('case')] + need(len(cases) == 1 and certify(root, cases[0]) == received, + 'complete changed-tuple funding certificate differs from exact rebuild') + return True diff --git a/research/integer-carrier-height/verify.py b/research/integer-carrier-height/verify.py new file mode 100644 index 0000000000..fe7b674a5f --- /dev/null +++ b/research/integer-carrier-height/verify.py @@ -0,0 +1,178 @@ +#!/usr/bin/env python3 +"""Exact integer-height certificate. Produced by Nick Petalas. Apache-2.0.""" + +import argparse +import hashlib +import json +from fractions import Fraction as Q +from pathlib import Path + + +HEIGHT = 12040587444441491 +GRID_HEIGHT = 12040700000000000 +DENOMINATOR = 700000000000 +POWER = 322 +TERMS = 80 +SCALE = 1 << 220 +PACKAGE = Path(__file__).resolve().parent + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def outward(low, high): + """Round a proved interval outwards onto a fixed dyadic grid.""" + require(low <= high, "reversed interval") + return Q((low * SCALE).__floor__(), SCALE), Q((high * SCALE).__ceil__(), SCALE) + + +def log_unit(value): + """Enclose ln(value), for 1 <= value <= 2, by a positive series.""" + require(Q(1) <= value <= Q(2), "logarithm unit domain") + z = (value - 1) / (value + 1) + term = z + total = Q(0) + for index in range(TERMS): + total += 2 * term / (2 * index + 1) + term *= z * z + tail = 2 * term / ((2 * TERMS + 1) * (1 - z * z)) + return outward(total, total + tail) + + +def log2_integer(value): + require(type(value) is int and 1 <= value <= 1 << 64, "integer log domain") + shift = value.bit_length() - 1 + low, high = log_unit(Q(value, 1 << shift)) + base_low, base_high = log_unit(Q(2)) + require(base_low > 0, "positive logarithm base") + return outward(shift + low / base_high, shift + high / base_low) + + +def margin(height, power=POWER, denominator=DENOMINATOR): + require(type(height) is int and 1 <= height < 1 << 64, "height domain") + require(type(power) is int and 1 <= power <= 1024, "power domain") + require(type(denominator) is int and 1 <= denominator <= 10**15, "gap domain") + low, high = log2_integer(height + 1) + return outward(Q(height, denominator) - power * high, + Q(height, denominator) - power * low) + + +def threshold(height=HEIGHT, power=POWER, denominator=DENOMINATOR): + require(type(height) is int and 2 <= height < 1 << 64, "threshold domain") + previous = margin(height - 1, power, denominator) + current = margin(height, power, denominator) + require(previous[1] < 0, "preceding height must lose strictly") + require(current[0] > 0, "candidate height must win strictly") + return {"height": height, "previous_margin": list(map(str, previous)), + "current_margin": list(map(str, current))} + + +def authenticate(data, digest, blob): + require(hashlib.sha256(data).hexdigest() == digest, "changed predecessor bytes") + header = f"blob {len(data)}\0".encode() + require(hashlib.sha1(header + data).hexdigest() == blob, "changed predecessor blob") + + +def sources(): + records = json.loads((PACKAGE / "PREDECESSOR.json").read_text()) + expected = { + "retained/PROOF.md": "7e6dbcd2937601b107de31c1c2f64be886a4dde6741a30b7cc99bd59cc5528c8", + "retained/frontier.py": "2d1837eed6e828298f4e02ca9105ed4595b2d305354477e42b97fb3ad20d27fc", + } + require(records["commit"] == "08f0e5899254aa82288a91e70789049dc1f29690", + "changed predecessor head") + require(len(records["files"]) == 2, "predecessor file inventory") + require({row["retained_path"] for row in records["files"]} == set(expected), + "duplicate or missing predecessor file") + for row in records["files"]: + path = row["retained_path"] + require(row["sha256"] == expected[path], "changed predecessor pin") + authenticate((PACKAGE / path).read_bytes(), expected[path], row["git_blob"]) + text = (PACKAGE / "retained/frontier.py").read_text() + for literal in ["BASE_K = Q('0.003027288235')", "BASE_S = Q('0.003027288245')", + "p=322, H=12040700000000000, j=17201)", "(s-k)/7"]: + require(literal in text, "missing cited fixed-height parameter") + require((Q('.003027288245') - Q('.003027288235')) / 7 == Q(1, DENOMINATOR), + "cited gap does not match the new guard") + + +def controls(): + rejected = 0 + for bad in [HEIGHT - 1, HEIGHT + 1, 2, 0, -1, True, 1 << 64]: + try: + threshold(bad) + except ValueError: + rejected += 1 + else: + raise ValueError("false minimum accepted") + for bad in [Q(0), Q(3)]: + try: + log_unit(bad) + except ValueError: + rejected += 1 + else: + raise ValueError("invalid logarithm domain accepted") + records = json.loads((PACKAGE / "PREDECESSOR.json").read_text()) + for row in records["files"]: + data = (PACKAGE / row["retained_path"]).read_bytes() + for digest, blob, payload in [(row["sha256"], row["git_blob"], data + b"\n"), + (row["sha256"], "0" * 40, data)]: + try: + authenticate(payload, digest, blob) + except ValueError: + rejected += 1 + else: + raise ValueError("source mutation accepted") + return rejected + + +def small_exact_cases(): + checked = 0 + for height in range(1, 65): + for power in range(1, 5): + for denominator in range(1, 5): + left = (height + 1) ** (power * denominator) + right = 1 << height + low, high = margin(height, power, denominator) + require(not (high < 0) or left > right, "false negative interval") + require(not (low > 0) or left < right, "false positive interval") + require(low <= 0 <= high or left != right, "lost exact equality") + require(left == right or high < 0 or low > 0, "unresolved small sign") + checked += 1 + return checked + + +def run(): + sources() + result = threshold() + before = tuple(map(Q, result["previous_margin"])) + after = tuple(map(Q, result["current_margin"])) + require(Q(-36, 10**15) < before[0] <= before[1] < Q(-35, 10**15), "losing bracket") + require(Q(1354, 10**15) < after[0] <= after[1] < Q(1355, 10**15), "winning bracket") + require(HEIGHT > 8 * 1024, "retained side guard") + result.update(reduction=GRID_HEIGHT - HEIGHT, controls=controls(), + small_exact_comparisons=small_exact_cases()) + return result + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path) + args = parser.parse_args() + result = run() + if args.receipt: + destination = args.receipt.resolve() + require(not destination.is_relative_to(PACKAGE), "receipt must be outside the package") + files = sorted(path for path in PACKAGE.rglob("*") if path.is_file()) + require(len(files) <= 32, "bounded package inventory") + result["package_sha256"] = {str(path.relative_to(PACKAGE)): + hashlib.sha256(path.read_bytes()).hexdigest() for path in files} + destination.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n") + print(f"PASS_INTEGER_CARRIER_HEIGHT minimum={HEIGHT} reduction={GRID_HEIGHT - HEIGHT} " + f"small_exact={result['small_exact_comparisons']} controls={result['controls']}") + + +if __name__ == "__main__": + main()