diff --git a/research/p104-prefix-birth-obstruction/PROOF.md b/research/p104-prefix-birth-obstruction/PROOF.md new file mode 100644 index 0000000000..1999f0d78c --- /dev/null +++ b/research/p104-prefix-birth-obstruction/PROOF.md @@ -0,0 +1,122 @@ +# A birth-lowered market needs a paid deletion + +This is a scoped accounting obstruction, with new finite continuation fixtures. +It does not re-prove or audit the source construction. + +## Contract + +Fix the PR6030 word stored by DreamingOfClouds's PR6170 toolkit. Write +`t = 1-C`, with `00 and lowering its birth +adds dimension d>0. Before its first original MOVE it must ascend from the +new birth to the old birth. Let the positive ranks of those new MOVEs be +`d_1,...,d_k`. Nesting gives `sum_i d_i=d`. + +For `0= d^t, + (s+d)^t < s^t+d^t. + +Its target-credit increase is `18((s+d)^t-s^t)`. Every original paid MOVE +remains, and the extra ascents cost at least `18d^t`. Hence + + Delta F(t) <= -18 [s^t+d^t-(s+d)^t] < 0. (1) + +Summing (1) over selected helpers proves the same strict loss for any +nonempty simultaneous choice. Extra paid work can only decrease F further. +This argument does not inspect scalar coefficients, row contents, event +order between different registers, or independence of the proposed targets. +It already rejects the optimistic invoice. Correctness and native delivery +cannot make that invoice better without changing the stated contract. + +For completeness, strict subadditivity follows by fixing s>0 and observing +that `g(d)=(s+d)^t-d^t` has negative derivative for d>0, with limiting value +`s^t` at zero. Iterating the non-strict form proves the path inequality. + +## Exact P104 specialization and sharpness + +The checker enumerates the fourteen manifest markets. Each G has dimension +five; its orthogonal O has dimension four; and I=O intersect G has dimension +two. The helpers born at these G and ending at the full frame form a disjoint +set of 62 roles. These extracted source facts select the new candidate family; +they are not a replay of the original arithmetic or invoice. + +A binary plane has exactly five subspaces: zero, its three lines, and itself. +Thus there are 310 single-helper choices (h,B). Their added dimensions are +five, four and three respectively, and every old helper span is four. +For fixed s and t, the deficit + + D(s,d,t)=s^t+d^t-(s+d)^t + +strictly increases with d, since its d derivative is +`t[d^(t-1)-(s+d)^(t-1)]>0`. Consequently every changed helper loses at least + + 18 [4^t+3^t-7^t], (2) + +and a nonempty m-helper change loses at least m times (2). +The bound holds throughout the open power interval, including the selected +complex supplier's power, without a numerical root search. + +The optimistic lower bound is attained as an invoice difference: take +B=I, change only h's initial frame, and prepend the single MOVE B->G. +This MOVE changes no logical row. At the old entry boundary, every register +again has precisely its old frame and arbitrary unit row. Keeping the entire +old program therefore preserves its arbitrary-input continuation identity, +conditional on the source's identity. No arithmetic replay of that source is +needed or claimed. The new recursive bill is exactly (2) worse. Scalar or +physical overhead can add cost; attainment here concerns this recursive bill. + +The checker constructs all 310 such continuation splices, checks their +new prefix and literal unchanged suffix, and derives their changed target and +paid entries. It does not claim to enumerate every possible scalar coupling. + +## What this excludes and what remains + +The result excludes obtaining a gain solely by lowering market births and +resynthesizing scalars while preserving the original paid transitions and +other target endpoints. A prospective coupled word must remove an original +paid transition or obtain another justified target/boundary gain worth more +than its strict preparation deficit. Replacing, splitting or deleting old +MOVEs, changing helper final frames, adding productive targets, owned/native +interfaces and actual consumer costs require a new comparison. + +No universal helper-split barrier, supplier admission, complete multiplication +theorem, selected-frontier change or new kappa is proved. No source result was +independently audited. The source's arbitrary-input identity and recursive +pricing convention are cited premises. Independent human and formal +proof-kernel review are unclaimed. + +The argument uses classical concavity and monotone dimension accounting. +The contribution is this quantified changed-boundary obstruction, its sharp +P104 preparation bill and the explicit new continuation family. Credit +DreamingOfClouds for PR6170's geometry, Lemma 11 opening, word and ledger, Ali +Romman and the retained P104/native/helper/caller/compiler/BIT contributors. +This contribution was produced by Nick Petalas. diff --git a/research/p104-prefix-birth-obstruction/README.md b/research/p104-prefix-birth-obstruction/README.md new file mode 100644 index 0000000000..981a6c87c8 --- /dev/null +++ b/research/p104-prefix-birth-obstruction/README.md @@ -0,0 +1,94 @@ +# A paid-deletion requirement for birth-lowered P104 markets + +Claim type: scoped accounting proof with finite continuation certificates. +No new kappa, supplier admission or selected-frontier change. + +For the PR6030 geometry retained in DreamingOfClouds's PR6170 toolkit, lowering +a market helper's birth into its associated hub cannot improve the recursive +moment if every old paid MOVE and all other productive endpoints remain. +This holds even with arbitrary scalar resynthesis. Each changed helper loses +at least + + 18 [4^t + 3^t - 7^t] > 0, for every 0> i & 1}) + if all(a ^ b in subset for a in subset for b in subset): + candidates.append(subset) + require(len(candidates) == 5, 'wrong plane lattice') + return candidates + + +def read_inputs(): + manifest = json.loads((PACKAGE / 'SOURCES.json').read_text()) + paths = [] + for entry in manifest['files']: + if entry.get('usage') == 'input': + name = entry['path'] + data = (ROOT / name).read_bytes() + require(hashlib.sha256(data).hexdigest() == entry['sha256'], 'source hash: ' + name) + paths.append(name) + require(len(paths) == 3, 'wrong live input inventory') + raw = (ROOT / (TOOLKIT + 'words/6030.json.gz')).read_bytes() + require(len(raw) < 2_000_000, 'source container too large') + word_data = gzip.decompress(raw) + require(len(word_data) < 16_000_000, 'source word too large') + word = json.loads(word_data) + plan = json.loads((ROOT / (TOOLKIT + 'alignbuild/data/manifest_6030.json')).read_text()) + require(len(word['initial']) == word['public'] == 770, 'wrong public interface') + require(len(word['frames']) <= 1200 and len(word['program']) < 26000, 'word bounds') + require(len(plan['plan']) <= 32, 'manifest bound') + return word, plan, paths + + +def market_rows(word, plan, frames): + markets = [g for block in plan['plan'] if block['side'] == 'markets' for g in block['items']] + require(len(markets) == len(set(markets)) == 14, 'wrong market inventory') + main = set(word['live']) | {r + 112 for r in word['live']} + rows = [] + all_roles = set() + for market in markets: + birth = frames[market] + require(len(birth) == 32, 'market dimension') + hub = frozenset(x for x in range(512) if all((x & g).bit_count() % 2 == 0 for g in birth)) + intersection = hub & birth + require(len(hub) == 16 and len(intersection) == 4, 'hub/intersection dimension') + roles = [r for r, f in enumerate(word['initial']) if f == market and r not in main] + require(0 < len(roles) <= 8, 'market role bound') + require(not all_roles.intersection(roles), 'duplicate market role') + for role in roles: + require(len(frames[word['final'][role]]) == 512, 'helper final is not full') + moves = [e for e in word['program'] if e[0] == 'MOVE' and e[1] == role] + require(moves and moves[0][2] == market, 'first original MOVE is not from G') + all_roles.update(roles) + rows.append((market, roles, intersection)) + require(len(all_roles) == 62, 'changed helper inventory') + return rows + + +def splice(word, frames, market, role, lower): + require(lower < frames[market], 'birth must be a strict subspace') + require(word['initial'][role] == market, 'wrong source birth') + require(all((x & g).bit_count() % 2 == 0 for x in lower for g in frames[market]), + 'lower birth is outside the associated hub') + index = next((f for f, space in enumerate(frames) if space == lower), len(frames)) + initial = list(word['initial']) + initial[role] = index + program = [['MOVE', role, index, market]] + word['program'] + table = list(word['frames']) + if index == len(table): + basis = [] + covered = frozenset({0}) + for value in sorted(lower): + if value not in covered: + basis.append(value) + covered = span(basis) + require(covered == lower, 'new frame basis') + table.append(basis) + return dict(word, initial=initial, program=program, frames=table, lower=lower, index=index) + + +def check_splice(word, frames, market, role, edited): + prefix = edited['program'][0] + require(prefix == ['MOVE', role, edited['index'], market], 'missing or wrong paid ascent') + require(edited['lower'] < frames[market], 'non-nested paid ascent') + require(span(edited['frames'][edited['index']]) == edited['lower'], 'dangling frame') + require(edited['final'] == word['final'], 'final boundary changed') + require(edited['program'][1:] == word['program'], 'old suffix changed') + current = list(edited['initial']) + require(current[role] == edited['index'], 'wrong edited entry') + current[role] = market # MOVE transports a value unchanged; no row operation occurs. + require(current == word['initial'], 'old entry boundary not restored') + added = len(word['frames'][market]) - (len(edited['lower']).bit_length() - 1) + old_span = len(word['frames'][word['final'][role]]) - len(word['frames'][market]) + require(old_span == 4 and added in (3, 4, 5), 'wrong changed ranks') + return (old_span, added, old_span + added) + + +def sqrt_bounds(value): + scale = 10**12 + floor = isqrt(value * scale * scale) + return Fraction(floor, scale), Fraction(floor + 1, scale) + + +def power_controls(): + # Exact interval arithmetic at t=1/2 corroborates the written all-power proof. + count = 0 + for added in (3, 4, 5): + root_lo, root_hi = sqrt_bounds(added) + total_lo, total_hi = sqrt_bounds(4 + added) + require(2 + root_lo - total_hi > 0, 'preparation deficit not positive') + require(total_lo - 2 > 0, 'paid-deletion escape control must gain') + for mask in range(1 << (added - 1)): + cuts = [0] + [i + 1 for i in range(added - 1) if mask >> i & 1] + [added] + parts = [b - a for a, b in zip(cuts, cuts[1:])] + require(sum(parts) == added, 'composition mass') + # Equality for one jump; a strict lower enclosure suffices otherwise. + if len(parts) > 1: + require(sum(sqrt_bounds(x)[0] for x in parts) > root_hi, 'path bound') + count += 1 + require(count == 28, 'composition inventory') + return count + + +def rejection_controls(word, frames, row): + market, roles, lower = row + role = roles[0] + good = splice(word, frames, market, role, lower) + bad = [] + empty_prefix = dict(good, program=good['program'][1:]) + bad.append(lambda: check_splice(word, frames, market, role, empty_prefix)) + wrong_rank = dict(good, program=[['MOVE', role, good['index'], 0]] + word['program']) + bad.append(lambda: check_splice(word, frames, market, role, wrong_rank)) + deleted = dict(good, program=good['program'][:-1]) + bad.append(lambda: check_splice(word, frames, market, role, deleted)) + wrong_entry = dict(good, initial=list(word['initial'])) + bad.append(lambda: check_splice(word, frames, market, role, wrong_entry)) + bad.append(lambda: splice(word, frames, market, role, frames[market])) + bad.append(lambda: splice(word, frames, market, role, frozenset(range(512)))) + outside = next(x for x in frames[market] if x not in lower) + bad.append(lambda: splice(word, frames, market, role, frozenset({0, outside}))) + for operation in bad: + try: + operation() + except ValueError: + continue + raise ValueError('rejection control accepted') + return len(bad) + + +def main(): + word, plan, inputs = read_inputs() + frames = [span(basis) for basis in word['frames']] + rows = market_rows(word, plan, frames) + counts = Counter() + details = [] + for market, roles, intersection in rows: + spaces = plane_subspaces(intersection) + for role in roles: + for lower in spaces: + edited = splice(word, frames, market, role, lower) + old, added, new = check_splice(word, frames, market, role, edited) + counts[added] += 1 + require((old, new) == (4, 4 + added), 'changed target entry') + details.append({'market': market, 'roles': roles, 'intersection': sorted(intersection)}) + require(dict(counts) == {5: 62, 4: 186, 3: 62}, 'new splice inventory') + controls = rejection_controls(word, frames, rows[0]) + compositions = power_controls() + files = sorted(PACKAGE.glob('*')) + receipt = {str(path.relative_to(ROOT)): hashlib.sha256(path.read_bytes()).hexdigest() + for path in files if path.is_file()} + receipt.update({name: hashlib.sha256((ROOT / name).read_bytes()).hexdigest() for name in inputs}) + result = {'schema': 'p104-birth-obstruction/1', 'markets': details, + 'splices': sum(counts.values()), 'added_rank_counts': dict(sorted(counts.items())), + 'compositions': compositions, 'rejections': controls, 'python': platform.python_version(), + 'minimum_loss': '18*(4^t+3^t-7^t), 0