From dab7aa7706bbdcb95483589f90d2981639d09c39 Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Fri, 23 Oct 2026 12:10:19 -0500 Subject: [PATCH 1/2] Prove an all-height source telescope and selected width floor --- research/separated-source-telescope/README.md | 173 +++++++++++++++++ .../separated-source-telescope/RESULT.json | 98 ++++++++++ .../separated-source-telescope/SOURCES.json | 48 +++++ research/separated-source-telescope/TASK.json | 90 +++++++++ .../separated-source-telescope/VERIFY.json | 40 ++++ research/separated-source-telescope/verify.py | 176 ++++++++++++++++++ 6 files changed, 625 insertions(+) create mode 100644 research/separated-source-telescope/README.md create mode 100644 research/separated-source-telescope/RESULT.json create mode 100644 research/separated-source-telescope/SOURCES.json create mode 100644 research/separated-source-telescope/TASK.json create mode 100644 research/separated-source-telescope/VERIFY.json create mode 100644 research/separated-source-telescope/verify.py diff --git a/research/separated-source-telescope/README.md b/research/separated-source-telescope/README.md new file mode 100644 index 0000000000..4db725326f --- /dev/null +++ b/research/separated-source-telescope/README.md @@ -0,0 +1,173 @@ +# An all-height source telescope for separated nested flows + +**Scoped proof with exact source checks.** For the unchanged selected #4470 +product, completion and split rule in #4436's nested divisible-width compiler, +this package proves `K/N > 3.054`. The previous lower coefficient was 2.943. +Together with Nick Petalas's [PR #5109](https://github.com/CrocSwap/integer-mult-bounds/pull/5109) +upper proof, the interval is + +```text +3.054 < K/N < 3.0694, +H = 64215200000000, N = 2^H, K = ceil(log2 B_N)/H. +``` + +Its endpoint ratio is less than 1.0051. This is a tighter estimate of a +permitted compiler's width. It does not reduce that width or improve kappa. +The selected conditional kappa remains `60403/20000000`. Physical stock, +owned storage, routing, native realization and supplier admission remain open. + +## Exact count at every height + +Let positive integer target multiplicities `T_k` have minimum rank `L>=2` +and maximum rank `M`. Let positive integer paid multiplicities `P_r` have +`max r < L`. Set `W=sum T_k`, `Q=sum P_r`, `c=floor(n/M)` and +`g=max{j:L^j<=c}`, for `n>=M`. Use the unchanged default height. + +Let `F_d(c)` count ordered words with `d` paid choices and `g-d` target +choices whose rank product is at most c. Count each choice with its actual +multiplicity. The paid choices form the chronological path. The target +choices give the ordered form of the source's multinomial unit weights. +Thus `0<=F_d<=Q^d W^(g-d)` and `F_g=Q^g`, since every paid rank is below L. + +The exact source count is + +```text +S_n = W F_0 + sum_(d=1..g) (W F_d - Q F_(d-1)) + = W Q^g + (W-Q) sum_(d=0..g-1) F_d. (1) +``` + +To prove the first equality, start with the root's `W F_0` target slots. +At depth d, eligible child units have `W F_d` target slots. An eligible +parent point contributes all its Pascal demand: replacing its last target +factor k by any paid factor r preserves eligibility because `r=W`, then `S_n>=W^(g+1)` at every height and width. +If `Q>W`, equality holds exactly when `c>=M^g`. Sufficiency follows because +every mixed word then fits. Necessity follows from the `d=0` term: the +all-maximum target word has positive multiplicity and fails when `cW`, constant when `Q=W`, and nondecreasing +when `QW` without +expanding the final paid histogram. Every final paid rank is at most +`20^1024=M L^(hlo-1)`, the default height is at least `hlo-1`, so (2) gives +`log2 S_n>=hlo log2 W>=Xlo`. There are at least `N(1-1/L)` such indices +through N. The nested recurrence `B_n=B_(n-1) S_n`, with base width one, +therefore gives + +```text +log2 B_N >= N(1-1/L) Xlo, +1000 (L-1) Xlo > 3054 L H, +K/N >= (L-1) Xlo/(L H) > 3054/1000. +``` + +The comparison uses only integers with thousands of bits. It never +constructs N, B_N, or the power-1024 histogram. The inherited 3.0694 upper +proof is pinned as a source premise, not independently reproved here. +This exact lower estimate does not prove a 3.055 endpoint. + +## Evidence and reproduction + +[RESULT.json](RESULT.json) records the arithmetic and finite checks. +[SOURCES.json](SOURCES.json) pins every consumed input at main +`ff3cc58e370d0f678e529246f8c73e8094e18fcf`. No pending branch is required. +The verifier authenticates input bytes before execution and checks them again +after it finishes. It loads the pinned flow from source bytes, without using +cached bytecode. Its independent counter uses scalar product convolutions; +the predecessor uses multivariate Pascal points and chronological matching. + +From the repository root, Python 3.12 and standard library only: + +```sh +python3 -I -W error -B research/separated-source-telescope/verify.py +python3 -I -O -W error -B research/separated-source-telescope/verify.py +python3 -B scripts/research_package.py --package research/separated-source-telescope +``` + +Expected direct marker: `PASS_SEPARATED_SOURCE_TELESCOPE K/N>3.054 no_new_kappa`. +The deterministic receipt covers 864 small merged flows, 12 complete literal +source/exit comparisons, 708 within-height monotonicity checks and 16 distinct +selected `v=1` boundary cases through height four. Six controls distinguish +omitted root/nonroot terms, omitted subtraction, `Q= 1, 'separated default-height domain') + height, power = 0, 1 + while power * low <= cap: + height += 1 + power *= low + tp, pp = powers(targets, height, cap), powers(paid, height, cap) + counts = [sum(a * b for r, a in pp[d].items() for k, b in tp[height-d].items() + if r * k <= cap) for d in range(height+1)] + w, q = sum(targets.values()), sum(paid.values()) + need(counts[-1] == q**height, 'every all-paid word is eligible') + total = w*q**height + (w-q)*sum(counts[:-1]) + deficits = [q**d*w**(height-d)-counts[d] for d in range(height)] + need(total-w**(height+1) == (q-w)*sum(deficits), 'deficit identity') + need(all(value >= 0 for value in deficits), 'negative eligibility deficit') + need(all(w*counts[d] >= q*counts[d-1] for d in range(1, height+1)), + 'negative missing-parent count') + if q > w: + need(total >= w**(height+1), 'all-height lower bound') + need((total == w**(height+1)) == (cap >= width**height), 'equality threshold') + return height, total, counts + + +def clear(flow): + for method in (flow.column, flow.points, flow.units, flow.demand): + method.cache_clear() + + +def completed(raw): + targets, paid = Counter(), Counter() + for rank, count in raw['targets'].items(): + rank = int(rank) + targets[max(21, rank)] += count + if rank < 21: + paid[21-rank] += count + paid.update({int(rank): count for rank, count in raw['paid'].items()}) + split = Counter() + for rank, count in paid.items(): + whole, remainder = divmod(rank, 20) + split[20] += whole * count + if remainder: + split[remainder] += count + return targets, +split + + +def verify(): + source = inputs() + name = 'research/direct-mixed-flow/flow.py' + namespace = {'__file__': str(ROOT/name), '__name__': 'pinned_flow'} + exec(compile(source[name], name, 'exec'), namespace) + flow_type = namespace['Flow'] + tiny, literal, monotone = 0, 0, 0 + for ranks in ((2, 3), (2, 4), (3, 4)): + for weights in product((1, 2), repeat=2): + targets = dict(zip(ranks, weights)) + for count in (1, 2, 4): + paid = {1: count, min(ranks)-1: count} + previous = None + for cap in range(1, 25): + height, expected, _ = telescope(targets, paid, cap) + flow = flow_type(targets, paid, max(targets)*cap) + result = flow.merged() + need(result['height'] == height and result['source_count'] == expected, + 'independent ordered products differ from pinned flow') + if cap in (1, 2, 3, 4) and weights == (1, 1) and count == 1: + word = [r for r, c in paid.items() for _ in range(c)] + exact = flow.literal(word) + need(exact['sources'] == result['sources'] and exact['exits'] == result['exits'], + 'literal chronological flow differs') + literal += 1 + if previous is not None and previous[0] == height: + sign = sum(paid.values())-sum(targets.values()) + need(sign*(expected-previous[1]) <= 0, 'fixed-height monotonicity') + monotone += 1 + previous = height, expected + tiny += 1 + clear(flow) + raw = json.loads(source['research/joint-helper-lattice/RESULT.json']) + need(raw['productive_fields'] == 10928 and raw['paid_calls'] == 64620, 'raw field/call counts') + need(raw['strictification']['floor'] == 21 and raw['strictification']['cutoff'] == 20 + and raw['strictification']['power'] == 1024, 'selected completion and split rule') + targets, paid = completed(raw) + need(sum(targets.values()) == 10928 and sum(paid.values()) == 77564, 'reduced invoice') + selected = [] + caps = {cap for height in range(1, 5) + for cap in (21**height-1, 21**height, 21**height+1, + 21**(height+1)-1, 145**height) if cap < 21**5} + for cap in sorted(caps): + h, total, _ = telescope(targets, paid, cap) + flow = flow_type(targets, paid, 145*cap) + need(flow.merged()['source_count'] == total, 'selected reduced-power source count') + selected.append({'cap': cap, 'height': h, 'sources': total}) + clear(flow) + # Concrete false extensions and omissions must disagree with actual counts. + _, full, f = telescope({2: 1, 4: 1}, {1: 4}, 2) + need(full != 2*f[0], 'root-only control did not distinguish missing sources') + need(full != 2*sum(f), 'missing subtraction control did not distinguish') + _, below, _ = telescope({2: 1, 4: 1}, {1: 1}, 2) + need(below == 3 and below < 2**2, 'Q 3054*low*h, 'strict selected 3.054 lower coefficient') + need(1000*(low-1)*xlo < 3055*low*h, 'rounded 3.055 claim must fail') + need(10000*30694 < 10051*30540, 'combined bracket ratio below 1.0051') + need(inputs() == source, 'source changed during verification') + return {'schema_version': 1, 'tiny_flows': tiny, 'literal_flows': literal, + 'fixed_height_comparisons': monotone, 'selected_reduced_flows': selected, + 'negative_controls': 6, 'H': h, 'hlo': hlo, 'Xlo': xlo, + 'W_bit_length': w.bit_length(), 'L_bit_length': low.bit_length(), + 'M_bit_length': ambient.bit_length(), 'strict_lower_K_over_N': '3054/1000', + 'inherited_upper_K_over_N': '30694/10000', 'selected_kappa': raw['kappa']} + + +if __name__ == '__main__': + result = verify() + if sys.argv[1:] == ['--emit']: + print(json.dumps(result, indent=2, sort_keys=True)) + else: + need(not sys.argv[1:], 'use no arguments or --emit') + need(result == json.loads((PACKAGE/'RESULT.json').read_text()), 'result receipt changed') + print('PASS_SEPARATED_SOURCE_TELESCOPE K/N>3.054 no_new_kappa') From cf7c21187a9d2d0ea689902b8727617affe70cde Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Fri, 23 Oct 2026 12:11:45 -0500 Subject: [PATCH 2/2] Record portable proof replay and source-history limit --- research/separated-source-telescope/README.md | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/research/separated-source-telescope/README.md b/research/separated-source-telescope/README.md index 4db725326f..cd2b4ec1d6 100644 --- a/research/separated-source-telescope/README.md +++ b/research/separated-source-telescope/README.md @@ -135,6 +135,14 @@ omitted root/nonroot terms, omitted subtraction, `Q