diff --git a/research/pr626-root-moment/CERTIFICATE.json b/research/pr626-root-moment/CERTIFICATE.json new file mode 100644 index 0000000000..a59e2ff6d6 --- /dev/null +++ b/research/pr626-root-moment/CERTIFICATE.json @@ -0,0 +1,74 @@ +{ + "status": "PASS_PR626_ROOT_MOMENT", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "assignment_seed": 83, + "method": { + "dyadic_exponent_depth": 163, + "fixed_point_bits": 256 + }, + "profile": { + "1": 181659, + "2": 30016, + "3": 31104, + "4": 11520, + "5": 5040, + "6": 576, + "8": 576, + "37": 1, + "48": 2215 + }, + "calls": 72, + "children": 262707, + "rank_mass": 520704, + "live": 7168, + "m": 73, + "deficit": 2560, + "endpoints": [ + { + "model": "native", + "saving": "65528268492323474503/40000000000000000000000", + "surcharge": false, + "accept": true, + "moment_minus_one": [ + "-142148128976149550642076438100564568550607937383060524668453/60589831782675021682119447899586069414933465256081744101542733238316655867911471104", + "-142148128976149550642076422578022239048204750929254255060721/60589831782675021682119447899586069414933465256081744101542733238316655867911471104" + ] + }, + { + "model": "native", + "saving": "102387919519255428911/62500000000000000000000", + "surcharge": false, + "accept": false, + "moment_minus_one": [ + "39341639264698531015594468476523892300347883131076602280515/60589831782675021682119447899586069414933465256081744101542733238316655867911471104", + "4917704908087316376949310499883277725343883698117466480821/7573728972834377710264930987448258676866683157010218012692841654789581983488933888" + ] + }, + { + "model": "conservative", + "saving": "327641341885943404413/200000000000000000000000", + "surcharge": true, + "accept": true, + "moment_minus_one": [ + "-7584806818011483336044970520975726853599569129252809770770868404804637991/2704903204583706325094618209802949527452386841789363575961729162424850708388904960000000000000000", + "-5309364772608038335231478879603560999692429459824325047240653309000586691/1893432243208594427566232746862064669216670789252554503173210413697395495872233472000000000000000" + ] + }, + { + "model": "conservative", + "saving": "819103354714858511033/500000000000000000000000", + "surcharge": true, + "accept": false, + "moment_minus_one": [ + "724380969857440184294200186627014950008216568952753541271477820204572631/3786864486417188855132465493724129338433341578505109006346420827394790991744466944000000000000000", + "226369053080450057591937861495597045519610759456746973780156523470890111/1183395152005371517228895466788790418260419243282846564483256508560872184920145920000000000000000" + ] + } + ], + "controls": { + "integer_power_comparisons": 1743, + "kernel_mutants": 2, + "rejected_power_inputs": 5, + "mathematical_controls": 6 + } +} diff --git a/research/pr626-root-moment/CLAIM.json b/research/pr626-root-moment/CLAIM.json new file mode 100644 index 0000000000..cf0e0af23b --- /dev/null +++ b/research/pr626-root-moment/CLAIM.json @@ -0,0 +1,47 @@ +{ + "track": "independent verification or formalization", + "assignment_seed": 83, + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "claimed_at": "2026-10-13T01:28:00-03:00", + "expected_finish": "2026-10-13T02:05:00-03:00", + "object": "PR626 selected complex profile: native and conservative strict adjacent 10^-24 moment endpoints", + "method": "163-bit dyadic exponent brackets and 256-bit outward repeated integer square roots; independent integer qth-power controls", + "deliverable": "offline standard-library checker, exact certificate, proof of enclosure, mathematical and package negative controls", + "candidates_considered": [ + "selected complex recursive moment bracket", + "prime-power cyclic inverse identity from PR621", + "finite binary-frame admissibility" + ], + "choice": "The two latter areas have existing exact engines and related current reviews. PR678 audits only the bit profile with binomial series; PR667/672 optimize existing log/exp engines. A series-free algebraic check of the complex native and conservative models adds a distinct arithmetic method.", + "coordination": "GraphQL pinnedIssues returned an empty list; claim recorded locally.", + "initial_overlap": { + "open_prs": 520, + "through_pr": 700, + "metadata_file_local": "../open-prs.json (outside contribution)", + "related_prs": [ + 678, + 667, + 672, + 675 + ], + "query_terms": [ + "square.root", + "dyadic exponent", + "repeated.root", + "algebraic.*moment" + ] + }, + "stopping_rule": "one finite arithmetic verification package; no supplier search or selected-frontier edit", + "result": { + "status": "completed independent finite verification; no new kappa", + "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/706", + "completed_at": "2026-10-13T01:34:37-03:00", + "evidence": "CERTIFICATE.json; four native/conservative strict endpoint decisions; 1743 integer-power controls; test_verify.py four tests OK", + "overlap_refresh": { + "open_prs_through_704": 523, + "latest_metadata_through": 705, + "finding": "PR705 register-path determinant obstruction is distinct; PR678 bit binomial audit and PR667/672 pricing optimizations are credited, not imported." + } + }, + "seed_generation": "Four OS RandomNumberGenerator bytes interpreted as UInt32, remainder modulo 100; recorded before task selection." +} diff --git a/research/pr626-root-moment/PROOF.md b/research/pr626-root-moment/PROOF.md new file mode 100644 index 0000000000..b0d3784a32 --- /dev/null +++ b/research/pr626-root-moment/PROOF.md @@ -0,0 +1,134 @@ +# Exact rational-power enclosure and the checked obligation + +Prepared for arkfx with substantial OpenAI Codex assistance; Apache-2.0. + +## The precise finite statement + +Let `H[r]` be the complete paid child profile in the selected #626 assembly, +`m=73`, `W=7168`, and let `b` be the supplier saving. The native moment is + +```text +M(b) = sum_r H[r]/W * (r/m)^(1-b) + = sum_r r*H[r]/(m*W) * (m/r)^b. +``` + +The conservative model adds + +```text +F(b) = (32*m^2*sum_r H[r])/10^16 * (1/W) * (1/m)^(1-b) + = 32*m*sum_r H[r]/(W*10^16) * m^b. +``` + +This is the rank-one exceptional-set profile charged by `check_moment` in the +base commit's `research/complex-k492-owner-repair/code/assemble.py`. The native +complex model omits that charge under the reviewed #559 exact-cover recurrence +correction. The construction-level correctness of both models is inherited. + +For the source-recorded `b_N = 65528268492323474503 / 40000000000000000000000` +and `b_C = 327641341885943404413 / 200000000000000000000000`, the package proves +these particular real-number inequalities through rational enclosures: + +```text +M(b_N) < 1 < M(b_N + 10^-24) +M(b_C) + F(b_C) < 1 < M(b_C + 10^-24) + F(b_C + 10^-24). +``` + +These are the local moment obligations. They are not the assembled κ claim. +All profile coefficients are positive and every `m/r > 1`, so each model is +strictly increasing in `b`; the adjacent-endpoint decisions enclose its unique +threshold within the recorded interval. Existence follows here from continuity +and the opposing strict signs. No claim of global supplier optimality follows. + +## Enclosure argument + +Take an exact rational base `a >= 1` and exponent `0 <= b <= 1`. Set +`D=2^K`, `k_L=floor(bD)` and `k_U=ceil(bD)`. Monotonicity gives + +```text +a^(k_L/D) <= a^b <= a^(k_U/D). +``` + +Thus no analytic tail estimate is needed. The binary digits of an integer +`0 <= k < D` write `k/D` as a sum of selected `2^-i`, for `1 <= i <= K`. +Consequently `a^(k/D)` is a product of selected repeated roots +`a^(2^-i)`. At `k=D`, use `a` directly. At `k=0`, the empty product is one. + +All intermediate intervals use a fixed scale `S=2^B`. An integer pair `(L,U)` +denotes the real interval `[L/S,U/S]`. Initially use +`L=floor(aS)`, `U=ceil(aS)`. Given such an enclosing pair, define + +```text +L' = floor(sqrt(L*S)) +U' = ceil(sqrt(U*S)). +``` + +Then `[L'/S,U'/S]` encloses the square root of every element of the original +interval. `isqrt(n)` gives the exact lower integer; add one for the upper +integer precisely when that lower integer's square is smaller than `n`. +This proves the root invariant for every step by induction. + +For nonnegative enclosing pairs `(L1,U1)` and `(L2,U2)`, multiplication gives + +```text +floor(L1*L2/S)/S <= product <= ceil(U1*U2/S)/S. +``` + +Induction over the selected binary factors proves that `dyadic(k)` encloses +`a^(k/D)`. Take only the lower endpoint of `dyadic(k_L)` and upper endpoint of +`dyadic(k_U)` to enclose `a^b`. This argument holds for any supported positive +depth and precision. An overly coarse grid may fail to decide a moment; it +cannot justify acceptance when the strict rational comparison fails. + +The implementation uses `K=163`, `B=256`, sums all terms with `Fraction`, and +does not round the final sum. Multiplying by nonnegative rational weights and +adding intervals preserves containment. The four final certified intervals +lie strictly on their required sides of one; their exact endpoints are stored +in `CERTIFICATE.json` and reproduced on every run. + +## Independent comparisons and failure distinctions + +For each kernel fixture `a` and `b=p/q`, the checker separately evaluates + +```text +lower^q <= a^p <= upper^q +``` + +with exact integer/rational exponentiation. Positive qth powers are strictly +increasing, so these comparisons independently establish containment for the +fixture without using the root enclosure's logic. Fixtures cover all 72 +ratios `73/r`, denominators 2 through 13 with numerators 1 and `q-1`, four +endpoint cases, and 83 seed-83 additional integer bases with denominators +2 through 31. Duplicate fractions across denominators are retained as distinct +test fixtures; this is 1,743 comparisons, not 1,743 distinct rationals. + +The two coarse kernel controls are concrete failures of unsafe enclosures: +using only `85/256` to approximate `1/3` from below omits the true cube root of +`73/48`; rounding the upper bound for `sqrt(2)` down omits `sqrt(2)` itself. +The separate package tests mutate the actual implementation and require +rejection. These controls corroborate the general invariant; they are not a +formal proof that every possible implementation error is detected. + +The equal-count/rank-mass control replaces two rank-two children with one +rank-one and one rank-three child. Both totals are preserved, but the upper +native saving endpoint becomes accepted. Strict concavity of `r^(1-b)` for +`0= 1 and 0 <= exponent <= 1, 'power domain') + require(type(depth) is int and 1 <= depth <= 4096, 'depth domain') + require(type(bits) is int and 8 <= bits <= 4096, 'precision domain') + scale = 1 << bits + initial = (base.numerator * scale // base.denominator, + ceil_div(base.numerator * scale, base.denominator)) + denominator = 1 << depth + lower_n = exponent.numerator * denominator // exponent.denominator + upper_n = ceil_div(exponent.numerator * denominator, exponent.denominator) + roots = [] + current = initial + for _ in range(depth): + current = root_bounds(current, scale) + roots.append(current) + + def dyadic(n): + if n == denominator: + return initial + result = (scale, scale) + for i, bounds in enumerate(roots, 1): + if n & (1 << (depth - i)): + result = mul_bounds(result, bounds, scale) + return result + + return Q(dyadic(lower_n)[0], scale), Q(dyadic(upper_n)[1], scale) + + +def moment(profile, m, live, saving, surcharge=False): + require(type(m) is int and m > 1 and type(live) is int and live > 0, 'parent domain') + require(type(surcharge) is bool, 'surcharge domain') + require(profile and all(type(r) is int and 0 < r < m and + type(n) is int and n > 0 for r, n in profile.items()), 'child domain') + lo = hi = Q(0) + for r, count in sorted(profile.items()): + lower, upper = power_bounds(Q(m, r), saving) + weight = Q(r * count, m * live) + lo += weight * lower + hi += weight * upper + if surcharge: + lower, upper = power_bounds(m, saving) + weight = Q(32 * m * sum(profile.values()), live * 10**16) + lo += weight * lower + hi += weight * upper + return lo, hi + + +def profile_dict(data): + require(type(data) is dict and data, 'profile object required') + result = {} + for rank, count in data.items(): + require(type(rank) is str and str(int(rank)) == rank and + type(count) is int and count > 0, 'invalid profile entry') + result[int(rank)] = count + return result + + +def load_inputs(): + sources = json.loads((HERE / 'SOURCES.json').read_text(encoding='utf-8')) + data = {} + for label, item in sources['files'].items(): + path = (ROOT / item['path']).resolve() + require(path.is_relative_to(ROOT), 'source path escapes checkout') + raw = path.read_bytes() + require(sha256(raw).hexdigest() == item['sha256'], 'source hash: ' + label) + data[label] = json.loads(raw) + assembly, owner, invoice, idle, selected = [data[n] for n in + ('assembly', 'owner', 'invoice', 'idle', 'selected')] + require(selected['audited_source_head'] == sources['selected_source_head'], 'selected source head') + require(selected['certificate'] == sources['files']['assembly']['path'], 'selected certificate path') + require(selected['certificate_sha256'] == sources['files']['assembly']['sha256'], 'selected certificate hash') + require(selected['kappa'] == assembly['kappa'], 'selected kappa') + local = Counter() + counts = Counter() + calls = invoice['selected_calls'] + require(len(calls) == 72 and len({(c['stage'], c['replica']) for c in calls}) == 72, + 'selected calls') + require({(c['stage'], c['replica']) for c in calls} == + {(s, r) for s in range(9) for r in range(8)}, 'call domain') + for call in calls: + require(call['orientation'] == ('forward' if call['stage'] % 2 == 0 else 'backward'), + 'call orientation') + provider = invoice['providers'][call['provider_id']] + local.update(profile_dict(provider['paid_profile'])) + counts[call['provider_id']] += 1 + require(dict(counts) == invoice['provider_counts'] == assembly['provider_counts'] == + {'ck': 8, 'jp8': 64}, 'provider multiplicities') + require(dict(local) == profile_dict(invoice['selected_local_paid_profile']), 'local profile') + profile = local + Counter(profile_dict(idle['rank_profile'])) + require(dict(profile) == profile_dict(owner['paid_profile']) == + profile_dict(assembly['complex_profile']), 'complete profile') + require(sum(idle['rank_profile'].values()) == idle['children'] == + owner['explicit_idle_remainder_children'], 'idle count') + require(owner['template_sha256'] == invoice['template_sha256'] == idle['template_sha256'], + 'receipt template binding') + require(owner['live'] == invoice['live'] == 7168 and owner['physical'] == invoice['physical'] == 7670, + 'live and physical stocks') + mass = sum(r * n for r, n in profile.items()) + require(mass == owner['rank_mass'] == 520704 and 73 * owner['live'] - mass == + owner['deficit'] == 2560, 'rank mass and deficit') + require(assembly['surcharge_model']['complex'] is False, 'native complex charge') + return assembly, dict(profile), dict(local), sources + + +def algebraic_controls(): + """Integer qth-power comparisons use no root/power enclosure algorithm.""" + rng = random.Random(83) + fixtures = [(Q(73, r), Q(p, q)) for r in range(1, 73) + for q in range(2, 14) for p in sorted({1, q - 1})] + fixtures += [(Q(1), Q(0)), (Q(1), Q(1)), (Q(73), Q(0)), (Q(73), Q(1))] + fixtures += [(Q(rng.randrange(2, 200)), Q(rng.randrange(1, q), q)) + for q in [rng.randrange(2, 32) for _ in range(83)]] + for base, exponent in fixtures: + lo, hi = power_bounds(base, exponent) + require(lo**exponent.denominator <= base**exponent.numerator <= hi**exponent.denominator, + 'integer-power oracle') + # Coarse depth forces a visible exponent bracket. Using the lower exponent + # for both endpoints incorrectly excludes this rational-power value. + lo, hi = power_bounds(Q(73, 48), Q(1, 3), depth=8, bits=32) + require(lo**3 < Q(73, 48) < hi**3, 'coarse exponent bracket') + lower_dyadic_hi = power_bounds(Q(73, 48), Q(85, 256), depth=8, bits=32)[1] + require(lower_dyadic_hi**3 < Q(73, 48), 'truncated exponent mutant not detected') + # Rounding the upper root down fails even at an exact dyadic exponent. + scale = 1 << 32 + bad_upper = Q(isqrt(2 * scale * scale), scale) + require(bad_upper**2 < 2 <= power_bounds(2, Q(1, 2), bits=32)[1]**2, + 'upper-root rounding mutant not detected') + bad = [(Q(1, 2), Q(1, 2)), (Q(2), Q(-1)), (Q(2), Q(2)), (2.0, Q(1, 2)), + (Q(2), 0.5)] + for base, exponent in bad: + try: + power_bounds(base, exponent) + except ValueError: + pass + else: + raise ValueError('invalid power accepted') + return {'integer_power_comparisons': len(fixtures), 'kernel_mutants': 2, + 'rejected_power_inputs': len(bad)} + + +def build_certificate(): + assembly, profile, local, sources = load_inputs() + rows = [] + for label, key, surcharge in [('native', 'complex_lower', False), + ('conservative', 'conservative_complex_lower', True)]: + lower = Q(assembly[key]) + for saving, accepted in [(lower, True), (lower + Q(1, 10**24), False)]: + lo, hi = moment(profile, 73, 7168, saving, surcharge) + require(hi < 1 if accepted else lo > 1, 'strict endpoint: ' + label) + recorded = (assembly['moments'] if label == 'native' else assembly['conservative_moments']) + original = next(x for x in recorded if x['side'] == + ('complex' if label == 'native' else 'conservative_complex') and + Q(x['endpoint']) == saving) + require(original['accept'] is accepted and original['surcharge'] is surcharge, + 'recorded endpoint decision') + rows.append({'model': label, 'saving': str(saving), 'surcharge': surcharge, + 'accept': accepted, 'moment_minus_one': [str(lo - 1), str(hi - 1)]}) + native = Q(assembly['complex_lower']) + conservative = Q(assembly['conservative_complex_lower']) + require(moment(profile, 73, 7168, native, True)[0] > 1, 'old surcharge at native endpoint') + require(moment(profile, 73, 7168, conservative + Q(1, 10**24), False)[1] < 1, + 'omitted conservative charge') + require(moment(local, 73, 7168, native + Q(1, 10**24))[1] < 1, 'omitted idle children') + require(moment(profile, 73, 7670, native + Q(1, 10**24))[1] < 1, 'physical stock denominator') + changed = Counter(profile) + changed[2] -= 2 + changed[1] += 1 + changed[3] += 1 + require(sum(changed.values()) == sum(profile.values()) and + sum(r*n for r, n in changed.items()) == sum(r*n for r, n in profile.items()), + 'equal mass/count control') + require(moment(dict(changed), 73, 7168, native + Q(1, 10**24))[1] < 1, + 'equal mass/count profile must change decision') + require(moment(profile, 73, 7168, Q(0)) == (Q(520704, 73*7168),) * 2, + 'zero-saving exact moment') + controls = algebraic_controls() + controls['mathematical_controls'] = 6 + return {'status': 'PASS_PR626_ROOT_MOMENT', 'base_commit': sources['base_commit'], + 'assignment_seed': 83, 'method': {'dyadic_exponent_depth': DEPTH, 'fixed_point_bits': BITS}, + 'profile': {str(r): n for r, n in sorted(profile.items())}, + 'calls': 72, 'children': sum(profile.values()), 'rank_mass': 520704, + 'live': 7168, 'm': 73, 'deficit': 2560, 'endpoints': rows, 'controls': controls} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write-certificate', action='store_true', + help='explicitly replace this package certificate after recomputing all checks') + args = parser.parse_args() + certificate = build_certificate() + path = HERE / 'CERTIFICATE.json' + if args.write_certificate: + path.write_text(json.dumps(certificate, indent=2) + '\n', encoding='utf-8') + else: + require(json.loads(path.read_text(encoding='utf-8')) == certificate, 'certificate differs') + print(certificate['status']) + print(f"4 strict endpoints; 72 calls; {certificate['children']} children; " + f"{certificate['controls']['integer_power_comparisons']} integer-power controls; " + '2 kernel mutants; 6 mathematical controls.') + + +if __name__ == '__main__': + main()