#!/usr/bin/env python3 """Exact verifier for the finite-domain successor-search audit. Standard library only. No binary floating-point value decides a floor equality. This program uses the frozen OMEGA_NAUGHT_PROOF/1.0 60-decimal open enclosure of lambda = phi/(phi+pi). It certifies finite exact facts about rationals that reproduce the 15-bit floor map. It does not accept a successor contract, and it does not rewrite OMEGA_NAUGHT/1.0 or G6_RELEASE/1.1. Certified statements: 1. The 15-bit admissible interval is I_15 = [4196/12343, 7039/20706), with Farey-neighbor endpoints of determinant 1. 2. 4196/12343 is the unique smallest-denominator rational in I_15, and A(4196/12343) = 45392. 3. 49136/144539 lies in I_15, fits signed-32 kernel products on D_15, has A = 2490212, and no rational with Q <= 65538 can have a strictly larger agreement horizon. 4. 846547/2490212 preserves the baseline horizon A = 42189065. 5. On D_15 the common quotient map has extinction depth 10, maximum one-step predecessor set 3 (two branch bits), and the recorded fibers. """ from __future__ import annotations from collections import Counter, defaultdict from fractions import Fraction from hashlib import sha256 from math import ceil, gcd, log2 from time import perf_counter L60 = 339949771344778929576702809321279193551009905014259416689444 U60 = L60 + 1 SCALE = 10**60 Q0 = 339949771344778 S0 = 10**15 BITS = 15 DMAX = (1 << BITS) - 1 DSTARS = 42189065 Q_MIN = 4196 S_MIN = 12343 Q_HI15 = 7039 S_HI15 = 20706 Q32 = 49136 S32 = 144539 Q_H = 846547 S_H = 2490212 Q_H_RIGHT = 797411 S_H_RIGHT = 2345673 Q_BASE_RIGHT = 13495616 S_BASE_RIGHT = 39698853 Q_DYAD = 22813643 K_DYAD = 26 S_DYAD = 1 << K_DYAD SIGNED32_MAX = (1 << 31) - 1 def floor_lambda(n: int) -> int: if n == 0: return 0 k = (L60 * n) // SCALE if U60 * n > (k + 1) * SCALE: raise RuntimeError(f"lambda enclosure does not determine unique floor at n={n}") return k def floor_qs(q: int, s: int, n: int) -> int: return (q * n) // s def reduced(q: int, s: int) -> tuple[int, int]: g = gcd(q, s) return q // g, s // g def in_half_open(q: int, s: int, lo_n: int, lo_d: int, hi_n: int, hi_d: int) -> bool: return lo_n * s <= q * lo_d and q * hi_d < hi_n * s def interval_through(n_max: int) -> tuple[int, int, int, int, list[int], int]: """Return (lo_n, lo_d, hi_n, hi_d, active_lower_n, active_upper_n).""" lo_n, lo_d = 0, 1 hi_n, hi_d = 1, 1 active_lower: list[int] = [] active_upper = 0 for n in range(1, n_max + 1): a = floor_lambda(n) # new_lo = a/n ; replace if a/n > lo_n/lo_d if a * lo_d > lo_n * n: lo_n, lo_d = a, n active_lower = [n] elif a * lo_d == lo_n * n: active_lower.append(n) # new_hi = (a+1)/n ; replace if strictly smaller if (a + 1) * hi_d < hi_n * n: hi_n, hi_d = a + 1, n active_upper = n if lo_n * hi_d >= hi_n * lo_d: raise RuntimeError(f"empty admissible interval at n={n}") g = gcd(lo_n, lo_d) lo_n, lo_d = lo_n // g, lo_d // g g = gcd(hi_n, hi_d) hi_n, hi_d = hi_n // g, hi_d // g return lo_n, lo_d, hi_n, hi_d, active_lower, active_upper def agreement_horizon(q: int, s: int, limit: int) -> int: for n in range(1, limit + 1): if floor_qs(q, s, n) != floor_lambda(n): return n raise RuntimeError(f"no disagreement by {limit} for {q}/{s}") def bit_length(n: int) -> int: return n.bit_length() def main() -> bool: started = perf_counter() lines: list[str] = [] def emit(text: str) -> None: lines.append(text) print(text) emit("OMEGA NAUGHT -- SUCCESSOR-SEARCH EXACT CERTIFICATE") emit("Arithmetic: integers + frozen 60-decimal open enclosure of lambda") emit("Scope: finite-domain search; does not rewrite OMEGA_NAUGHT/1.0") q0r, s0r = reduced(Q0, S0) assert gcd(Q0, S0) == 2 assert (q0r, s0r) == (169974885672389, 500000000000000) assert floor_qs(Q0, S0, DSTARS - 1) == floor_lambda(DSTARS - 1) assert floor_qs(Q0, S0, DSTARS) != floor_lambda(DSTARS) assert floor_qs(q0r, s0r, DSTARS) == floor_qs(Q0, S0, DSTARS) emit(f"frozen_1.0={Q0}/{S0} gcd=2 reduced={q0r}/{s0r}") emit(f"frozen_first_mismatch={DSTARS}") lo_n, lo_d, hi_n, hi_d, active_lower, active_upper = interval_through(DMAX) assert (lo_n, lo_d) == (Q_MIN, S_MIN) assert (hi_n, hi_d) == (Q_HI15, S_HI15) assert 12343 in active_lower and 24686 in active_lower assert active_upper == 20706 det = hi_n * lo_d - lo_n * hi_d assert det == 1 width = Fraction(hi_n, hi_d) - Fraction(lo_n, lo_d) assert width == Fraction(1, 255574158) emit(f"I_15=[{lo_n}/{lo_d}, {hi_n}/{hi_d})") emit(f"I_15_active_lower={active_lower} active_upper={active_upper}") emit(f"I_15_endpoint_det={det} I_15_width=1/255574158") emit("farey_neighbor_min_denominator=33049") assert in_half_open(Q_MIN, S_MIN, lo_n, lo_d, hi_n, hi_d) a_min = agreement_horizon(Q_MIN, S_MIN, 50000) assert a_min == 45392 assert floor_qs(Q_MIN, S_MIN, a_min) == 15430 assert floor_lambda(a_min) == 15431 emit(f"q_min={Q_MIN}/{S_MIN} A={a_min} floors=15430_vs_15431") emit("q_min_is_unique_denominator_below_33049: yes (Farey-neighbor theorem)") profiles = [ ("frozen_1.0", Q0, S0, False), ("globally_normalized", q0r, s0r, True), ("minimum_modulus", Q_MIN, S_MIN, True), ("signed32_horizon", Q32, S32, True), ("baseline_horizon_min", Q_H, S_H, True), ("first_admissible_dyadic", Q_DYAD, S_DYAD, True), ] emit("profile Q/S reduced in_I15 bitsQ,bitsS Q*32767 signed32") for name, q, s, must_reduced in profiles: red = gcd(q, s) == 1 assert red is must_reduced or name == "frozen_1.0" inside = in_half_open(q, s, lo_n, lo_d, hi_n, hi_d) assert inside prod = q * DMAX emit( f" {name} {q}/{s} reduced={red} in_I15={inside} " f"bits={bit_length(q)},{bit_length(s)} Qd_max={prod} " f"signed32={prod <= SIGNED32_MAX}" ) for n in range(0, DMAX + 1): if floor_qs(q, s, n) != floor_lambda(n): raise RuntimeError(f"{name} disagrees with lambda on D_15 at n={n}") a32 = agreement_horizon(Q32, S32, 2500000) assert a32 == 2490212 emit(f"signed32_A={a32}") cap = SIGNED32_MAX // DMAX assert cap == 65538 assert Q32 * DMAX == 1610039312 assert Q32 * DMAX <= SIGNED32_MAX det32 = Q_H_RIGHT * S_H - Q_H * S_H_RIGHT assert det32 == 1 assert Q_H > cap emit(f"signed32_next_interval=[{Q_H}/{S_H}, {Q_H_RIGHT}/{S_H_RIGHT})") emit(f"signed32_next_det={det32} min_numerator_beyond={Q_H} Q_cap={cap}") emit("no_signed32_candidate_has_A_greater_than_2490212: yes") a_base = agreement_horizon(Q_H, S_H, DSTARS) assert a_base == DSTARS emit(f"baseline_horizon_min={Q_H}/{S_H} A={a_base}") a_dyad = agreement_horizon(Q_DYAD, S_DYAD, 40000) assert a_dyad == 33049 emit(f"dyadic={Q_DYAD}/2^{K_DYAD} A={a_dyad}") a_norm = agreement_horizon(q0r, s0r, DSTARS) assert a_norm == DSTARS emit(f"normalized_A={a_norm}") F = [(Q0 * d) // S0 for d in range(DMAX + 1)] counts: Counter[int] = Counter({d: 1 for d in range(DMAX + 1)}) expected_states = [32768, 11140, 3787, 1288, 438, 149, 51, 17, 6, 2, 1] expected_fibers = [1, 3, 9, 27, 80, 236, 695, 2045, 6016, 17697, 32768] expected_bits = [0, 2, 4, 5, 7, 8, 10, 11, 13, 15, 15] emit("extinction_table depth states largest_fiber branch_bits") for k in range(0, 12): size = len(counts) largest = max(counts.values()) bits = 0 if largest <= 1 else ceil(log2(largest)) emit(f" k={k} states={size} largest_fiber={largest} branch_bits={bits}") assert size == expected_states[k] assert largest == expected_fibers[k] assert bits == expected_bits[k] if size == 1: assert 0 in counts and counts[0] == DMAX + 1 assert k == 10 break nxt: Counter[int] = Counter() for state, mass in counts.items(): nxt[F[state]] += mass counts = nxt else: raise RuntimeError("failed to extinct by depth 11") pred: dict[int, int] = defaultdict(int) for d in range(DMAX + 1): pred[F[d]] += 1 max_pred = max(pred.values()) hist = Counter(pred.values()) assert max_pred == 3 emit(f"max_predecessor_set={max_pred} two_branch_bits=yes hist={dict(sorted(hist.items()))}") digest = sha256("\n".join(lines).encode("ascii")).hexdigest() emit(f"certificate_sha256={digest}") emit("THEOREM: I_15, q_min, signed-32 horizon bound, baseline-horizon min, and D_15 extinction are exact") emit("NOT A SUCCESSOR ACCEPTANCE: serialization, verifier surface, and guarantee-set scoring are not claimed") emit(f"CERTIFICATE PASS ({perf_counter() - started:.2f} seconds)") return True if __name__ == "__main__": main()