diff --git a/research/idle-four-site-rigidity/PROOF.md b/research/idle-four-site-rigidity/PROOF.md new file mode 100644 index 0000000000..ad09eae2db --- /dev/null +++ b/research/idle-four-site-rigidity/PROOF.md @@ -0,0 +1,197 @@ +# Four idle positions cannot exchange rank across the fixed schedule + +This is a scoped mathematical proof under the inherited completed-call +contract, with a finite source check. It is not a proof-assistant verification +or an audit of the native implementation of that contract. + +## Statement and assumptions + +Fix one replica, one port, and cover identity in the pinned data schedule. +Number its streams `(X0,Y0,X1,Y1,X2,Y2,X3,Y3)` by `0,...,7`. +Allow simultaneous replacements of idle children **8, 10, 12, 13** only. +At each position, both the original and replacement child have a linearly +independent axis set in `F_2^m`, followed by an optional address translation. +An orthonormal axis set, as required by the source construction, is sufficient. + +Assume: + +1. A completed child with axes `A` and translation `t` acts on its one physical + stream as the product of the `C_v` for `v in A`, followed by `X_t`, in the + source convention below. The number of independent axes is its rank. +2. Every operation outside the four positions is fixed. The completed local + data calls are the source F/B shears conjugated by diagonal Fourier frames; + completed hosted-helper actions on this replica/port are nonzero diagonal + multipliers. They keep the character fixed. In particular, a replacement + cannot silently alter a hosted helper, its frame, or its scheduling. +3. The unchanged prefix, intervening operator and suffix are invertible on + arbitrary inputs to the eight streams. Equality means equality of these + physical operators, not equality on a proper subspace of inputs. + +**Theorem.** If the replacements preserve the physical operator for every +Fourier character at cover identity, then each child separately preserves +its Fourier phase function and its rank. In particular, arbitrary matched +swaps, cycles and simultaneous changes confined to these four positions +cannot change any of their individual ranks. + +There is no assumption that different children's axis sets are orthogonal, +that the combined multiset of axes is retained, or that only a few axes move. +Preserving the operator over every cover implies preserving it at cover +identity, so this necessary condition suffices to rule out a rank change. +No claim that cover identity alone suffices for full admission is needed. + +## 1. The schedule separates the two phase positions + +All event indices below are zero-based. `verify.py` derives them from +`TEMPLATE.json.gz` and checks the physical child mappings against `PLAN.json.gz`. +The exact input pins are in [SOURCES.json](SOURCES.json). + +| Event | Operation | Streams mixed | +|---|---|---| +| 14 | idle children 8, 10 on pair 3 | diagonal on 6, 7 | +| 15 | bridge, pair 2 receiving from pair 3 | 4, 5, 6, 7 | +| 16 | local stage 6 on pair 2 | 4, 5 | +| 17 | idle children 9, 11 on pair 3 | diagonal | +| 18 | inverse bridge, pairs 2 and 3 | 4, 5, 6, 7 | +| 19 | local stage 7 on pair 3 | 6, 7 | +| 20 | local stage 8 on pair 3 | 6, 7 | +| 21 | idle children 12, 13 on pair 0 | diagonal on 0, 1 | + +For a fixed character `u`, write `M(u)` for everything strictly between events +14 and 21, including any interleaved completed hosted-helper phases. Put +`V = span(e_0,e_1)`. Every listed factor preserves `V`; so does every diagonal +frame or helper factor allowed by the contract. The factors are invertible: +F/B and bridges are elementary shears and the diagonal factors are nonzero. +Consequently `M` is invertible and `M(V)=V`. Neither the values of its phases +nor the actual hosted occupancy are needed for this fact. + +Write the original interval as `D_B M D_A`, where `D_A` acts only on streams +6, 7, and `D_B` only on streams 0, 1. Primes denote the replacement factors. +Cancel the unchanged invertible prefix and suffix from physical equality. +Then multiply on the left by `D_B^(-1)` and on the right by `D_A^(-1)`: + +``` +D'_B M D'_A = D_B M D_A +E_B M E_A = M, +E_B = D_B^(-1) D'_B, E_A = D'_A D_A^(-1). +``` + +For every `v in V`, `E_A v = v`, so `E_B M v = M v`. Since `M(V)=V`, +`E_B` is identity on `V`. It is identity off `V` by its support, hence +`E_B=I`. Invertibility of `M` then gives `E_A=I`. The four diagonal entries +are individual child multipliers, so **each of the four phases is unchanged**. +Apply the same argument separately at every `u`. + +This strengthens the single-stream interval argument in Nick Petalas's +[PR #3187](https://github.com/CrocSwap/integer-mult-bounds/pull/3187), following +Gareth Davidson's physical-stream obstruction in +[PR #1387](https://github.com/CrocSwap/integer-mult-bounds/pull/1387). +The two-coordinate invariant subspace makes the argument simultaneous and +removes the need to isolate one moved axis by choosing a character. + +## 2. Polarization recovers rank from a child's phase + +In the source convention, + +``` +X_v f(x) = f(x+v), +C_v = ((1+i) I + (1-i) X_v)/2. +``` + +For `chi_u(x)=(-1)^(u dot x)`, the multiplier of `C_v` is +`i^(u dot v mod 2)`, and that of `X_t` is `(-1)^(u dot t mod 2)`. +Thus a child has multiplier `i^q(u)`, where + +``` +q_A,t(u) = sum_{v in A} (u dot v mod 2) + 2(u dot t mod 2) (mod 4). +``` + +For bits `a,b`, `a+b-(a xor b)=2ab`. Therefore the even residue +`q(u)+q(w)-q(u+w)` can be divided by two as a map from `{0,2}` in `Z/4` +to `F_2`, giving + +``` +B_q(u,w) = (q(u)+q(w)-q(u+w))/2 + = sum_{v in A} (u dot v)(w dot v) + = u^T P_A w (over F_2), +P_A = sum_{v in A} v v^T. +``` + +The translation term disappears: its contribution before reduction is +`4(u dot t)(w dot t)`. Let `R` be the `r by m` binary matrix with the axes +as rows. Then `P_A=R^T R`. Because the rows are independent, `R:F_2^m -> F_2^r` +is surjective and `R^T:F_2^r -> F_2^m` is injective. The image of `R^T R` +is exactly the image of `R^T`, which has dimension `r`. Hence + +``` +rank_F2(P_A) = r = |A|. +``` + +Equal phase functions have equal polar forms. If both axis sets are +independent, their ranks are therefore equal, even if their translations +and their bases differ. Combining this with section 1 proves the theorem. +Notice that this rank argument does not require a nondegenerate restriction +of the dot product to the axis span. + +## 3. An exact, small representation of phase equality + +Expanding a binary parity modulo four gives + +``` +q(u) = sum_j d_j u_j + 2 sum_{j= 1, 'positive dimension') + require(type(translation) is int and 0 <= translation < 1 << dimension, 'translation domain') + linear = [2 * ((translation >> j) & 1) for j in range(dimension)] + polar = [0] * dimension + for axis in axes: + require(type(axis) is int and 0 < axis < 1 << dimension, 'axis domain') + for j in range(dimension): + if axis >> j & 1: + linear[j] = (linear[j] + 1) % 4 + polar[j] ^= axis + return {'linear_mod4': linear, 'polar_rows': polar} + + +def signature_value(s, x): + return (sum(c for j, c in enumerate(s['linear_mod4']) if x >> j & 1) + + 2 * sum(parity(row & ~((1 << (j + 1)) - 1), x) + for j, row in enumerate(s['polar_rows']) if x >> j & 1)) % 4 + + +def direct_phase(axes, x, translation=0): + return (sum(parity(v, x) for v in axes) + 2 * parity(translation, x)) % 4 + + +def input_rank_certificate(recipes): + require(len(recipes) == 112, 'complete port catalogue') + signatures = [] + for port, recipe in enumerate(recipes): + require(recipe['port'] == port, 'ordered unique port catalogue') + for child in EARLY + LATE: + entry = recipe['idle_children'][child] + axes = list(map(int, entry['orthogonal_axes'])) + require(len(axes) == 48, 'source full child rank') + require(all(parity(v, w) == int(i == j) for i, v in enumerate(axes) + for j, w in enumerate(axes)), 'source orthonormality') + s = phase_signature(axes, 73, translation=int(entry['translation_after'])) + require(binary_rank(axes) == binary_rank(s['polar_rows']) == 48, 'phase recovers source rank') + signatures.append([port, child, s]) + return {'ports': 112, 'child_positions': list(EARLY + LATE), 'full_axis_sets': len(signatures), + 'ranks_per_port': [48] * 4, 'signature_sha256': hashlib.sha256(canonical(signatures)).hexdigest(), + 'nonzero_character_signature_probes': 73 + 73 * 72 // 2} + + +def phase_controls(): + sets = checks = 0 + for n in range(1, 5): + for size in range(n + 1): + for axes in itertools.combinations(range(1, 1 << n), size): + # Independent explicit-span oracle, distinct from binary elimination. + span = {0} + for a in axes: + span |= {x ^ a for x in span} + if len(span) != 1 << size: + continue + sets += 1 + s = phase_signature(axes, n) + require(binary_rank(s['polar_rows']) == size, 'independent-set polar rank') + for x in range(1 << n): + require(signature_value(s, x) == direct_phase(axes, x), 'quadratic phase identity') + checks += 1 + standard6 = [1 << j for j in range(6)] + changed6 = [63 ^ a for a in standard6] + require(phase_signature(standard6, 6) == phase_signature(changed6, 6), 'nontrivial basis positive control') + require(all(direct_phase(standard6, x) == direct_phase(changed6, x) for x in range(64)), 'basis-change oracle') + standard4 = [1 << j for j in range(4)] + changed4 = [15 ^ a for a in standard4] + a, b = phase_signature(standard4, 4), phase_signature(changed4, 4) + require(a['polar_rows'] == b['polar_rows'] and a != b, 'polar-only false-positive control') + require(direct_phase(standard4, 1) != direct_phase(changed4, 1), 'linear phase witness') + require(a == phase_signature(changed4, 4, translation=15), 'translation repair preserves rank') + require(phase_signature([1] * 4, 1) == phase_signature([], 1), 'dependent-axis boundary') + require(binary_rank([1] * 4) != 4, 'independence is required') + return {'independent_axis_sets': sets, 'all_character_checks': checks, + 'nontrivial_same_phase_basis_change': [standard6, changed6], + 'polar_only_false_positive': [standard4, changed4], 'translation_repair': 15, + 'dependent_axis_control': [1] * 4} + + +def rotate(z, k): + a, b = z + return ((a, b), (-b, a), (-a, -b), (b, -a))[k % 4] + + +def identity(): + return [[(int(i == j), 0) for j in range(8)] for i in range(8)] + + +def add_row(matrix, dst, src, coefficient): + matrix[dst] = [(a + coefficient * c, b + coefficient * d) + for (a, b), (c, d) in zip(matrix[dst], matrix[src])] + + +def interval_matrix(template, cut, rng): + matrix = identity() + local = {e['stage']: e for e in template['recipe'] if e['kind'] == 'local'} + for index in range(cut['early_event'] + 1, cut['late_event']): + # Arbitrary invertible diagonal fixtures include frame/host phase effects. + for row in range(8): + k = rng.randrange(4) + matrix[row] = [rotate(z, k) for z in matrix[row]] + event = template['execution_schedule'][index] + if event['kind'] == 'bridge': + dst, src, c = event['dst'], event['src'], event['coefficient'] + add_row(matrix, 2 * dst, 2 * src, c) + add_row(matrix, 2 * src + 1, 2 * dst + 1, -c) + elif event['kind'] == 'local_cover_sweep': + op = local[event['stage']] + x, y = 2 * op['pair'], 2 * op['pair'] + 1 + add_row(matrix, x if op['reverse'] else y, y if op['reverse'] else x, + -1 if op['reverse'] else 1) + return matrix + + +def phase_relation(matrix, changes): + """Direct exact entry test of E_late M E_early = M.""" + early, late = {6: changes[0], 7: changes[1]}, {0: changes[2], 1: changes[3]} + return all(rotate(matrix[i][j], late.get(i, 0) + early.get(j, 0)) == matrix[i][j] + for i in range(8) for j in range(8)) + + +def cut_controls(template, plan, cut): + rng = random.Random(40) + for _ in range(32): + matrix = interval_matrix(template, cut, rng) + solutions = [x for x in itertools.product(range(4), repeat=4) if phase_relation(matrix, x)] + require(solutions == [(0, 0, 0, 0)], 'four independent phases are rigid') + crossing = identity() + crossing[0], crossing[6] = crossing[6], crossing[0] + require(phase_relation(crossing, (3, 0, 1, 0)), 'crossing-cut positive transfer') + require(phase_relation([[(0, 0)] * 8 for _ in range(8)], (1, 1, 1, 1)), 'singular boundary control') + def rejected(t, p, message): + try: + schedule_cut(t, p) + except ValueError as error: + require(message in str(error), 'wrong rejecting rule: ' + str(error)) + return + raise ValueError('mutated schedule accepted') + clone = lambda x: json.loads(json.dumps(x)) + t = clone(template) + t['execution_schedule'][cut['early_event'] + 1]['src'] = 0 + rejected(t, plan, 'late coordinate subspace is mixed') + t = clone(template) + next(e for e in t['recipe'] if e.get('stage') == 6)['pair'] = 0 + rejected(t, plan, 'late coordinate subspace is mixed') + t = clone(template) + t['execution_schedule'][cut['early_event'] + 1]['kind'] = 'erase' + rejected(t, plan, 'unproved intervening operation') + p = clone(plan) + p['sides']['8'] ^= 1 + rejected(template, p, 'plan/event physical stream mismatch') + t = clone(template) + t['execution_schedule'].append(t['execution_schedule'][cut['early_event']]) + rejected(t, plan, 'duplicate child event') + return {'seed': 40, 'diagonal_fixtures': 32, 'phase_tuples_per_fixture': 256, + 'nonidentity_tuples_rejected': 32 * 255, 'source_schedule_mutations_rejected': 5, + 'crossing_cut_transfer_accepted': True, 'singular_boundary_exhibited': True} + + +def calculate(): + x = read_inputs() + cut = schedule_cut(x['template'], x['plan']) + return {'base_commit': BASE, 'status': 'scoped-written-proof-with-exact-finite-hypotheses', + 'schedule_cut': cut, 'source_axes': input_rank_certificate(x['phases']['recipes']), + 'phase_controls': phase_controls(), 'cut_controls': cut_controls(x['template'], x['plan'], cut), + 'claim': 'Each of the four child ranks is invariant under operator-preserving independent-axis replacements with the remaining schedule fixed.', + 'new_kappa': False, 'formal_kernel_proof': False} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--emit-result', action='store_true') + args = parser.parse_args() + result = calculate() + if args.emit_result: + print(json.dumps(result, sort_keys=True, indent=2)) + return + require(canonical(result) == canonical(json.loads((PACKAGE / 'RESULT.json').read_bytes())), 'stored result mismatch') + print('PASS_IDLE_FOUR_SITE_RIGIDITY ports=112 axesets=448 full_recipe_ranks=48,48,48,48 phase_tuples=8192') + + +if __name__ == '__main__': + main()