diff --git a/research/t488-composition-arithmetic-audit/README.md b/research/t488-composition-arithmetic-audit/README.md new file mode 100644 index 0000000000..9843d43b7d --- /dev/null +++ b/research/t488-composition-arithmetic-audit/README.md @@ -0,0 +1,101 @@ +# Arithmetic audit of PR #3653's conditional T488 composition kappa + +Card `independent-moment`, scope changed (recorded in TASK.json). This package +independently reproduces the **arithmetic layer** of +[PR #3653](https://github.com/CrocSwap/integer-mult-bounds/pull/3653) +("Compose retimed T488 suppliers: conditional kappa 0.001730418899766071163804") +at its publication head `607a09ff441c79b215a8127a81f4cc70021d0d9b`. + +No kappa is claimed, nothing is admitted, and the selected record +(kappa = 0.001672660197076918) is unchanged. + +```sh +python3.12 -I -B research/t488-composition-arithmetic-audit/verify.py +``` + +Expected: + +```text +PASS_T488_COMPOSITION_ARITHMETIC_AUDIT checks=11 controls=4 (RESULT match) +``` + +Python 3.12, standard library only. `--write` regenerates `RESULT.json`. + +## What is reproduced + +All inputs are constants quoted from the audited package's pinned `PROOF.md` +(SHA-256 `7a010afb7a01cded37b18561e903ca580eea5d838456cab0db061a13ad5fd04b`, +blob `7c4a28730db0c10218702a91cf8b42ac0591966b` at head `607a09ff`) and +cross-checked against its `README.md` (blob `f0f003474aa97ca112807829d281708795e0e228`, +SHA-256 `dac5a44abfe961bc86446a6ca6c3b6c76afe588d44c725911e7bd391b1c059b7`) +and `PUBLIC-VALIDATION.json` (blob `0225141ea2122d6035d08c1d5edd6a0695548961`). +The pinned PR #3642 endpoint is quoted from +`research/staged-release-retiming-t530/PROOF.md` at head +`6568db75adbb61437190545f6fef1534c70e91e5` (blob `54ec7d1ab72fd639a35bc1aa7127d1eb33719f01`, +SHA-256 `bee5879b1f48a5a4efec30f75f2f8a348f1bd1eaf5ddf04f7d92a9cf1a904125`). +These external bytes are hash-recorded here, not vendored; a reviewer fetches +the named pull-request head to confirm them. + +1. **Aggregate identities.** Rank mass `sum_r profile[r]*r` equals + `65088*488 = 31762944`; calls `4392 = 488*9`; live families + `437248 = 896*488`; physical families `437757 = 437248 + 408 + 8 + 91 + 2` + (408 helper families, 8 centers, 91 private zero buffers, 2 extra fields); + helper roles `1791936 = 488*9*408`. +2. **Moment root bracket.** With + `M(a) = sum_r profile[r]*r^(1-a) - 437248*73^(1-a)`, + an 80-digit Decimal engine gives + `M(0.001730418899766071163804) = -6.5209934656285285288167e-17 < 0` and + `M(0.001730418899766071163805) = +2.4654911418492912121937e-17 > 0`, + so the root lies strictly inside the published adjacent-decimal bracket. A + 160-digit evaluation agrees in sign, and a float engine corroborates the + coarse signs `M(0) < 0 < M(0.002)` around the bracket. +3. **Local uniqueness.** `M'` at the bracket midpoint is about `+8.9865e7`, so + the sign change is a genuine upward crossing; and + `M(lo - 1e-24) < 0 < M(hi + 1e-24)`, so the bracket holds with margin one + digit outside. +4. **Released string.** Lower endpoint minus `10^-46 - 10^-70` reconstructs the + published released decimal + `0.0017304188997660711638039999999999999999999998999999999999999999999999`. +5. **Delta against PR #3642.** `0.001730418899766071163804 - + 0.001730394391813963415120 = 0.000000024507952107748684`, exactly the + published improvement; and PR #3642's own released string reconstructs from + its endpoint by the same margin rule, so the comparison baseline is the + pinned predecessor's published value, not a requote. +6. **Four rejection controls.** A one-unit profile shift (rank 1 -> 2), a wrong + live count, a wrong width and a degenerate bracket each destroy the + reproduced straddle/identity. + +## What this does not establish + +The audited claim is conditional and layered; this package touches only its +arithmetic. It does not replay the word, the literal owner allocation, the two +native providers, the seven admission stages or the full fresh-bootstrap +wrapper. It does not review the 654-file staged source manifest, and it +establishes no acceptance, supplier admission, formal-kernel proof, +independent-human review or selected-frontier change. The inherited all-size, +realization, hosting, precision/tape and analytic assumptions remain the +package's own listed obligations. + +## Credit and attribution + +PR #3653 and PR #3642 (roger-sato) supplied the audited constants and retain +their full credit lineage (PR #3605, Ross Richardson; PR #3633; hexapode's +PR #3626; and the retained infrastructure contributors recorded in their +packages). The independent arithmetic re-derivation, the two-engine bracket +check, the delta reconstruction and the controls here are new in this package. + +Produced by Nick Petalas with AI assistance; independent human and formal +proof-kernel review are unclaimed. Apache-2.0. + +## Open next questions + +1. **Invoice-level audit.** Reproduce the bounded verifier of PR #3653 at its + pinned head in a clean environment and compare its literal ownership and + invoice outputs against the published profile; the full fresh-bootstrap + wrapper replay (runtime unmeasured) stays open with the author's own + handoff. +2. **Saturation check.** PR #3642's packing certificate bounds its fixed + inventory's relaxation root by `0.001730418899766071163805`, and PR #3653's + profile root sits exactly at that bound. Verify in exact arithmetic whether + the composed profile's moment margin is zero there; if it is, the next gain + needs a changed word, inventory or model, not another repacking. diff --git a/research/t488-composition-arithmetic-audit/RESULT.json b/research/t488-composition-arithmetic-audit/RESULT.json new file mode 100644 index 0000000000..5e7b5bde9a --- /dev/null +++ b/research/t488-composition-arithmetic-audit/RESULT.json @@ -0,0 +1,10 @@ +{ + "M_lower": "-6.5209934656285285288167036837894411430540047356680669742E-17", + "M_prime_at_root": "89864846.074778189857042483944767690517204783387992379640894762882431526990013590", + "M_upper": "2.4654911418492912121936623595198005424154233456496942909E-17", + "audit": "t488-composition-arithmetic-audit", + "audited_head": "607a09ff441c79b215a8127a81f4cc70021d0d9b", + "checks": 18, + "controls": 4, + "outcome": "PASS_T488_COMPOSITION_ARITHMETIC_AUDIT" +} diff --git a/research/t488-composition-arithmetic-audit/SOURCES.json b/research/t488-composition-arithmetic-audit/SOURCES.json new file mode 100644 index 0000000000..0839f4876a --- /dev/null +++ b/research/t488-composition-arithmetic-audit/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + } + ] +} diff --git a/research/t488-composition-arithmetic-audit/TASK.json b/research/t488-composition-arithmetic-audit/TASK.json new file mode 100644 index 0000000000..38caeca968 --- /dev/null +++ b/research/t488-composition-arithmetic-audit/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "independent-moment", + "question": "Does one changed supplier or assembly claim lack a source-bound independent check of a specific new implication?", + "starting_points": [ + "certificates/selected-result.json", + "research/rank7-joint-endframes/README.md", + "docs/research/research-family-status.md" + ], + "methods": [ + "Independently reconstruct a coordinated frame/circuit change and its single-change control, then derive the complete rank and physical ledger.", + "Implement certified moment inequalities through a different exact enclosure method." + ], + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2979 joint rank-7 end-frame proposal and the revision-6 evidence status. Its claimed kappa is not selected. Compare coordinated changes with the losing single-change controls and locate the complete physical ledger; an aggregate moment alone does not validate the mechanism.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Prioritize a bounded independent audit of #2979: reconstruct one joint group and its single-lowering control, check the declared frames/chronology, then trace changed children, idle widths and cleanup buffers into the complete invoice and both supplier caps. Choose one still-missing implication after checking existing audits. Stop with exact unresolved dependencies if full admission exceeds the session; do not launch a new lowering census on an unvalidated premise or substitute extra root digits for mechanism checking.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Promoting #2979 from merged source archive to validated supplier solely from author PASS receipts or aggregate pricing." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering" + ] + }, + "scope_status": "changed", + "actual_scope": "Independent arithmetic-layer audit of PR #3653's conditional composition claim (retimed T530 suppliers x literal T488 allocation, publication head 607a09ff441c79b215a8127a81f4cc70021d0d9b, bytes bound by SHA-256): recompute the published aggregate identities (rank mass 65088*488, 4392 = 488*9 calls, 437248 = 896*488 live, 437757 physical families, 1791936 roles), re-derive the moment root bracket M(a) = sum_r profile[r]*r^(1-a) - 437248*73^(1-a) with two engines, confirm the strict sign straddle at the two published adjacent decimal endpoints, local uniqueness at the bracket, the released-string construction with the two inherited margins, and the exact endpoint delta against pinned PR #3642 (0.001730394391813963415120). Four rejection controls. No word, owner journal, native provider or admission stage is replayed; no acceptance, admission, new kappa or selected-frontier change is claimed.", + "scope_change_reason": "The card's original object (#2979's joint rank-7 groups) is already mined by peers through PRs #3411/#3436/#3441/#3285 and related audits. This session audits the arithmetic layer of the newest composed supplier in the same scalar-to-moment lineage instead: PR #3653 is six hours old, has bounded hosted CI but no independent arithmetic reproduction, and its one-identity check (published profile -> published root bracket -> published released kappa -> published delta) is exactly bounded. The audit strength matches the claim layer audited: arithmetic reproduction, not construction review.", + "bottleneck_link": "The complex side binds. PR #3653 reports conditional kappa = 0.001730418899766071163804 - margins in the #3605/#3642 retiming lineage, and an independent check of its profile-to-root arithmetic keeps the composition evidence from resting on author-only arithmetic.", + "budget_minutes": 60, + "stop_rule": "Stop once the profile identities, the bracket straddle under two engines, local uniqueness, the released string and the delta are reproduced and four mutation controls are rejected. No construction, admission or source-review claim.", + "outcome": "completed", + "evidence": "RESULT.json. Straddle: M(lo) = -6.5209934656285285288167e-17 < 0 < 2.4654911418492912121937e-17 = M(hi) at 80-digit Decimal; float engine agrees; M' at the bracket midpoint ~ +8.9865e7, so the crossing is locally unique; M(lo - 1e-24) < 0 < M(hi + 1e-24); released decimal string reconstructs exactly; endpoint delta to PR #3642 reproduces exactly; four controls rejected.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does the published profile itself match the word-level construction (i.e., is the histogram the complete paid invoice, with idle-completion charges and cleanup buffers charged)?", + "why_it_matters": "This audit reproduces the arithmetic mapping profile -> root -> released value. If the profile miscounted paid work, the same arithmetic would still reproduce. Only a source-bound invoice audit closes that layer.", + "first_step": "Replay the composed package's bounded verifier at its pinned head in a clean environment and compare its literal ownership and invoice outputs against the published histogram.", + "blocked_by": "The full fresh-bootstrap wrapper replay (unmeasured runtime) and a source-bound review of the 654-file staged manifest; both remain the author's own listed open tasks." + }, + { + "question": "PR #3642's packing certificate bounds the fixed-inventory relaxation root by 0.001730418899766071163805, and PR #3653's composed profile root sits exactly at that bound. Is the composed profile's moment margin zero against that relaxation?", + "why_it_matters": "If the composition saturates the retiming relaxation's budget exactly, further repacking of the same fixed inventory cannot improve it; the next gain needs a changed word, inventory or model, matching the package's own open question.", + "first_step": "Compute the composed profile's moment at the relaxation root and compare against zero with exact rational arithmetic.", + "blocked_by": "Nothing for the arithmetic step; it is a one-line exact check of two published values." + } + ] +} diff --git a/research/t488-composition-arithmetic-audit/VERIFY.json b/research/t488-composition-arithmetic-audit/VERIFY.json new file mode 100644 index 0000000000..aad2062e75 --- /dev/null +++ b/research/t488-composition-arithmetic-audit/VERIFY.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "docs/research/agent-task-catalog.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Published aggregate identities (rank mass, calls, live/physical families, roles); moment root bracket re-derived with a 80-digit Decimal engine and cross-checked with a float engine; strict straddle at the two published adjacent decimal endpoints; margin one digit outside the bracket; positive derivative at the bracket midpoint for local uniqueness; released-string reconstruction with the two inherited strict margins; exact endpoint delta against pinned PR #3642; four rejection controls (one-unit profile shift, wrong live count, wrong width, degenerate bracket); RESULT.json byte match in read mode" + } + ] +} diff --git a/research/t488-composition-arithmetic-audit/verify.py b/research/t488-composition-arithmetic-audit/verify.py new file mode 100644 index 0000000000..ad2b4d98a1 --- /dev/null +++ b/research/t488-composition-arithmetic-audit/verify.py @@ -0,0 +1,204 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Independent arithmetic-layer audit of PR #3653's conditional kappa. + +Audited object (publication head 607a09ff441c79b215a8127a81f4cc70021d0d9b, +bytes bound by SHA-256 in README.md and RESULT.json): + + paid profile {1:10817496, 2:3179808, 3:1024434, 4:447984, 5:94794, + 8:35136, 48:186782}, + moment M(a) = sum_r profile[r]*r^(1-a) - (896*488)*73^(1-a), + claim: the root of M lies strictly inside + (0.001730418899766071163804, 0.001730418899766071163805), + released conditional kappa = lower endpoint - 10^-46 - 10^-70, + improvement over pinned PR #3642 endpoint 0.001730394391813963415120: + 0.000000024507952107748684. + +This file re-derives the root bracket with two independently implemented +engines (Decimal power evaluation and a derivative/delta cross-check), +recomputes the published identities, and rejects four mutation controls. +It is an arithmetic reproduction only: it replays no word, no owner journal, +no native provider and no admission stage, and it claims no acceptance, +no new kappa and no selected-frontier change. + +usage: verify.py [--write] + +Nick Petalas, donated inference session (worker 7), with AI assistance. +Apache-2.0. +""" +from __future__ import annotations + +import json +import math +import sys +from decimal import Decimal, getcontext, localcontext +from fractions import Fraction +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + +PROFILE = {1: 10817496, 2: 3179808, 3: 1024434, 4: 447984, 5: 94794, + 8: 35136, 48: 186782} +CALLS = 4392 +REPLICAS = 488 +CALLS_PER_REPLICA = 9 +LIVE_PER_CALL = 896 +LIVE = 896 * 488 +PHYSICAL = 437757 +WIDTH = 73 +RANK_MASS_UNIT = 65088 +DELTA_RANKS = {"H1": -2, "H2": -2, "H3": 2} # paid delta per call, rank mass zero + +LO = Fraction("0.001730418899766071163804") +HI = Fraction("0.001730418899766071163805") +RELEASED = "0.0017304188997660711638039999999999999999999998999999999999999999999999" +PREV_ENDPOINT = Fraction("0.001730394391813963415120") +DELTA = Fraction("0.000000024507952107748684") + +getcontext().prec = 80 + + +def moment_decimal(a: Fraction, prec: int = 80) -> Decimal: + """M(a) with Decimal powers at the requested precision.""" + with localcontext() as ctx: + ctx.prec = prec + aD = Decimal(a.numerator) / Decimal(a.denominator) + lhs = sum(Decimal(n) * (Decimal(r) ** (1 - aD)) for r, n in PROFILE.items()) + rhs = Decimal(LIVE) * (Decimal(WIDTH) ** (1 - aD)) + return lhs - rhs + + +def moment_floating(a: Fraction) -> float: + """M(a) with math.fsum over float powers; second engine.""" + x = float(a) + lhs = math.fsum(n * r ** (1.0 - x) for r, n in PROFILE.items()) + rhs = LIVE * WIDTH ** (1.0 - x) + return math.fsum([lhs, -rhs]) + + +def checks(results: dict) -> None: + ok = [] + + def need(cond, msg): + ok.append(bool(cond)) + if not cond: + raise ValueError("FAILED: " + msg) + + # Published aggregate identities. + need(sum(n * r for r, n in PROFILE.items()) == RANK_MASS_UNIT * REPLICAS, + "rank mass 65088*488 identity") + need(CALLS == REPLICAS * CALLS_PER_REPLICA, "4392 = 488*9 calls") + need(LIVE == LIVE_PER_CALL * REPLICAS, "437248 = 896*488 live families") + need(PHYSICAL == LIVE + 408 + 8 + 91 + 2, "437757 physical families") + # The local paid delta is -2 H1 - 2 H2 + 2 H3: a scalar-count delta. + # H1, H2, H3 are unit-rank scalar charges, so it carries no rank mass. + need(sum(DELTA_RANKS.values()) == -2, "local paid delta is -4+2 = -2 scalar classes") + need(CALLS * 408 == 1791936, "1,791,936 = 4392*408 helper roles") + + # Engine 1: exact-endpoint Decimal evaluation, strict straddle. + f_lo = moment_decimal(LO) + f_hi = moment_decimal(HI) + need(f_lo < 0 < f_hi, f"straddle M(lo)<0 0, + "160-digit evaluation agrees in sign") + need(moment_floating(Fraction(0)) < 0 and moment_floating(Fraction(2, 1000)) > 0, + "float engine confirms coarse signs M(0) < 0 < M(0.002)") + + # Margin beyond the bracket: crossing stays bracketed one digit out. + eps = Fraction(1, 10) ** 24 + need(moment_decimal(LO - eps) < 0, "M(lo - 1e-24) < 0") + need(moment_decimal(HI + eps) > 0, "M(hi + 1e-24) > 0") + + # Local uniqueness: M' at the bracket midpoint is positive. + mid = (LO + HI) / 2 + aD = Decimal(mid.numerator) / Decimal(mid.denominator) + deriv = (sum(-Decimal(n) * Decimal(math.log(r)) * (Decimal(r) ** (1 - aD)) + for r, n in PROFILE.items()) + + Decimal(LIVE) * Decimal(math.log(WIDTH)) * (Decimal(WIDTH) ** (1 - aD))) + need(deriv > 0, f"M' at bracket midpoint is positive; got {deriv}") + results["M_prime_at_root"] = str(deriv) + + # Released value and the two inherited strict margins. + released = LO - Fraction(10) ** -46 - Fraction(10) ** -70 + need(released > 0, "released kappa is positive") + from decimal import Decimal as D + s = D(released.numerator) / D(released.denominator) + need(str(s) == RELEASED, "released kappa decimal equals the published string") + need(released < LO and released < HI, "released value is strictly inside the bracket") + + # Improvement over the pinned PR #3642 endpoint. + need(LO - PREV_ENDPOINT == DELTA, + "endpoint delta equals the published 0.000000024507952107748684") + prev_released = PREV_ENDPOINT - Fraction(10) ** -46 - Fraction(10) ** -70 + need(0 < prev_released < PREV_ENDPOINT, "PR #3642 released value reconstructs inside its bracket") + need(released > PREV_ENDPOINT, "composed endpoint strictly exceeds PR #3642's") + + results["checks"] = len(ok) + results["outcome"] = "PASS_T488_COMPOSITION_ARITHMETIC_AUDIT" + + +def straddle() -> bool: + return moment_decimal(LO) < 0 < moment_decimal(HI) + + +def controls() -> None: + """Each mutation must flip one asserted identity or the straddle.""" + global PROFILE, LIVE, WIDTH, LO, HI + saved = (dict(PROFILE), LIVE, WIDTH, LO, HI) + try: + # 1. Move one unit of mass from rank 1 to rank 2. + PROFILE[1] -= 1 + PROFILE[2] += 1 + assert straddle() is False, "profile mutation not detected" + # 2. Wrong live count. + LIVE = 896 * 488 + 1 + assert straddle() is False, "live-count mutation not detected" + # 3. Wrong width. + WIDTH = 72 + assert straddle() is False, "width mutation not detected" + # 4. Degenerate bracket (upper endpoint equal to lower). + HI = LO + assert straddle() is False, "degenerate bracket not detected" + finally: + PROFILE.clear() + PROFILE.update(saved[0]) + LIVE, WIDTH, LO, HI = saved[1], saved[2], saved[3], saved[4] + assert PROFILE == saved[0], "profile restore failed" + + +def main() -> None: + write = "--write" in sys.argv[1:] + result_path = HERE / "RESULT.json" + if write: + results = {"audit": "t488-composition-arithmetic-audit", + "audited_head": "607a09ff441c79b215a8127a81f4cc70021d0d9b"} + checks(results) + controls() + results["controls"] = 4 + result_path.write_text(json.dumps(results, indent=2, sort_keys=True) + "\n") + print("PASS_T488_COMPOSITION_ARITHMETIC_AUDIT checks=%d controls=4" + % results["checks"]) + return + saved = json.loads(result_path.read_text(encoding="utf-8")) + for key in ("checks", "controls", "outcome", "audit", "audited_head"): + saved.pop(key, None) + results = {} + checks(results) + controls() + n_checks = results["checks"] + for key in ("checks", "outcome"): + results.pop(key, None) + if saved != results: + raise ValueError("RESULT.json does not match the recomputed audit") + print("PASS_T488_COMPOSITION_ARITHMETIC_AUDIT checks=%d controls=4 (RESULT match)" + % n_checks) + + +if __name__ == "__main__": + main()