diff --git a/research/frozen-snapshot-channel-capacity/README.md b/research/frozen-snapshot-channel-capacity/README.md new file mode 100644 index 0000000000..f2902416b2 --- /dev/null +++ b/research/frozen-snapshot-channel-capacity/README.md @@ -0,0 +1,244 @@ +# Sharp channel loss from frozen live snapshots + +This contribution was produced by Nick Petalas. Claim type: scoped algebraic +proof with exact finite corroboration. No new kappa is claimed. + +If an insertion must preserve a live copied value, its direction must lie in +the kernel of that snapshot map. Over D = Z[1/2], imposing constraints of +rational rank r removes at most r normalized unit channels. This bound is +sharp even when the rational rank of the eligible pairing does not change. +Thus rational pairing rank can miss the entire loss at a live-copy boundary. + +The new step combines a chronological frozen-snapshot contract with the +saturated dyadic pairing. It supplies a restriction formula, a sharp loss +bound and explicit extremizers. It does not validate a predecessor result. + +## Contract and theorem + +Let K be an m-by-n matrix over D. Its unrestricted unit-channel capacity is + +```text +c(K) = max { t : X K Y = I_t for matrices X,Y over D }. +``` + +Let C be any s-by-n matrix over D. The insertion columns must now satisfy +C Y = 0. Define + +```text +c_C(K) = max { t : X K Y = I_t and C Y = 0 }. +r = rank_Q(C). +``` + +All coefficient matrices are finite. A zero-dimensional identity is allowed. +Let Q have columns forming a full D-module basis of ker_D(C). Then + +```text +c_C(K) = c(K Q), +max(0, c(K) - r) <= c_C(K) <= c(K). +``` + +The exact value can therefore be obtained by applying the cited Smith +unit-block criterion to K Q. It is the number of unit Smith factors of K Q, +or equivalently its minimum rank modulo an odd prime. Q must be a saturated +module basis; a rational nullspace basis scaled column by column is insufficient. + +For every c,r >= 0 and every integer loss ell in [0,min(c,r)], there are K,C +with c(K)=rank_Q(K)=rank_Q(K Q)=c, rank_Q(C)=r, and c_C(K)=c-ell. +The ambient number of insertion coordinates in this construction is c+r. +These are sharp algebraic examples, not physical P104 cuts. + +## Why this is the frozen-copy equation + +At a nominated chronological comparison boundary, let z be the current cut +state and let the unchanged copied snapshot be t=S z. Suppose the allowed +insertions are z -> z+R0 Y a, where a is arbitrary source data. Keeping t +unchanged requires + +```text +S R0 Y = 0. +``` + +If eligible reader rows are L0, the normalized source-response condition is +X L0 R0 Y = I_t. Use K=L0 R0 and C=S R0 in the theorem. The rank in the loss +bound is rank_Q(S R0), which can be smaller than the number of copies. +Dependent copied functionals must not be counted repeatedly. + +This is an insertion interface with fixed eligible L0,R0 and frozen copied +slots. It does not classify all helper basis changes. It does not grant a +free read of dirty state, prove an arbitrary basis sequence legal at every +intermediate comparison, or permit an ERASE at an unverified intermediate +state. Every comparison boundary needs its actual equation. If the copied +slots also change, the contract changes and this restriction need not apply. + +## Proof + +First, ker_D(C) is saturated in D^n. If a nonzero d in D satisfies C(dv)=0, +then d C v=0 implies C v=0 because D is an integral domain. More explicitly, +D^n/ker_D(C) is isomorphic to im_D(C). This image is a free module of rank r, +because D is a principal ideal domain. The quotient is free, so the sequence +splits. Consequently Q extends to an invertible n-by-n matrix V=[Q P] over D, +where P has r columns. This splitting also covers zero C and a zero kernel. + +Every admissible column of Y lies in ker_D(C), so Y=Q Z for a unique matrix +Z over D. Conversely every Q Z is admissible. Substitution into X K Y=I_t +proves c_C(K)=c(K Q). Restricting admissible Y proves the upper bound. + +For the lower bound, reduce modulo any odd prime p. Every invertible D-matrix +remains invertible over F_p, so + +```text +rank_Fp(K mod p) = rank_Fp([K Q | K P] mod p) + <= rank_Fp(K Q mod p) + r. +``` + +The single-cut capacity theorem of Ali Romman's PR5615 states +c(A)=min_(odd primes p) rank_Fp(A mod p). Applying that cited theorem to K +and K Q gives c(K Q)>=c(K)-r. Capacity is nonnegative, which gives the stated +lower bound. This argument does not replace ker_D(C) by ker_Fp(C mod p). +Those two kernels can have different dimensions. + +For sharpness, choose any odd prime p and let K=[I_c | 0_r]. For j<=ell, +the j-th equation of C is + +```text +x_j + p y_j = 0. +``` + +For ell order[j] for i in range(n) + for j in range(i + 1, n)) + term = (-1) ** inversions + for i in range(n): + term *= a[i][order[i]] + total += term + return total + + +def divisors(a): + """All determinantal divisors, with d_0=1, in a bounded matrix.""" + result = [1] + for size in range(1, min(len(a), len(a[0])) + 1): + value = 0 + for rows in combinations(range(len(a)), size): + for cols in combinations(range(len(a[0])), size): + minor = [[a[i][j] for j in cols] for i in rows] + value = gcd(value, determinant(minor)) + result.append(value) + return result + + +def capacity(a): + d = divisors(a) + return max(k for k, value in enumerate(d) + if value > 0 and value & (value - 1) == 0) + + +def field_rank(a, prime=None): + """Independent elimination over Q or one of the declared prime fields.""" + require(prime is None or prime in PRIMES, 'prime domain') + b = [[Fraction(x) if prime is None else x % prime for x in row] + for row in a] + rank = 0 + for col in range(len(a[0])): + pivot = next((i for i in range(rank, len(a)) if b[i][col]), None) + if pivot is None: + continue + b[rank], b[pivot] = b[pivot], b[rank] + scale = 1 / b[rank][col] if prime is None else pow(b[rank][col], -1, prime) + b[rank] = [x * scale for x in b[rank]] + if prime is not None: + b[rank] = [x % prime for x in b[rank]] + for i in range(len(a)): + if i != rank: + factor = b[i][col] + b[i] = [x - factor * y for x, y in zip(b[i], b[rank])] + if prime is not None: + b[i] = [x % prime for x in b[i]] + rank += 1 + if rank == len(a): + break + return rank + + +def bezout(a, b): + """Bounded extended Euclid on signed integer inputs.""" + require(max(abs(a), abs(b)).bit_length() <= MAX_BITS, 'Euclid input bound') + old_r, r, old_s, s, old_t, t = abs(a), abs(b), 1, 0, 0, 1 + for _ in range(2 * MAX_BITS + 2): + if r == 0: + u = old_s if a >= 0 else -old_s + v = old_t if b >= 0 else -old_t + require(u * a + v * b == old_r, 'Bezout identity') + return old_r, u, v + q = old_r // r + old_r, r = r, old_r - q * r + old_s, s = s, old_s - q * s + old_t, t = t, old_t - q * t + raise ValueError('Euclid iteration bound') + + +def saturated_kernel(c): + """An integer basis, also a full D-basis, of ker(c).""" + q = identity(len(c[0])) + for equation in c: + if not q[0]: + break + row = multiply((equation,), q)[0] + if not any(row): + continue + width = len(row) + change = [list(r) for r in identity(width)] + current = list(row) + for j in range(1, width): + a, b = current[0], current[j] + g, u, v = bezout(a, b) + if g == 0: + continue + for i in range(width): + x, y = change[i][0], change[i][j] + change[i][0] = u * x + v * y + change[i][j] = -(b // g) * x + (a // g) * y + current[0], current[j] = g, 0 + if width == 1: + q = matrix([[] for _ in q]) + else: + reduced = matrix([r[1:] for r in change]) + q = multiply(q, reduced) + require(not any(x for row in multiply(c, q) for x in row), 'kernel equation') + return q + + +def check_pair(k, c): + require(len(k[0]) == len(c[0]), 'pair dimensions') + q = saturated_kernel(c) + r = field_rank(c) + width = len(q[0]) + require(width == len(c[0]) - r, 'kernel dimension') + require(divisors(q)[-1] == 1, 'kernel saturation') + constrained = multiply(k, q) + before, after = capacity(k), capacity(constrained) + require(max(0, before - r) <= after <= before, 'capacity envelope') + for a in (k, constrained): + profile = [field_rank(a)] + [field_rank(a, p) for p in PRIMES] + require(capacity(a) == min(profile), 'determinantal versus prime capacity') + return before, after + + +def census(): + counts = {'one_snapshot_pairs': 0, 'two_snapshot_pairs': 0, + 'strict_losses': 0, 'loss_without_rational_rank_drop': 0} + for values in product((-1, 0, 1, 3), repeat=4): + k = matrix((values[:2], values[2:])) + for row in product((-1, 0, 1, 3), repeat=2): + c = matrix((row,)) + before, after = check_pair(k, c) + counts['one_snapshot_pairs'] += 1 + if before > after: + counts['strict_losses'] += 1 + if field_rank(k) == field_rank(multiply(k, saturated_kernel(c))): + counts['loss_without_rational_rank_drop'] += 1 + for kv in product((-1, 0, 1), repeat=4): + k = matrix((kv[:2], kv[2:])) + for cv in product((-1, 0, 1), repeat=4): + check_pair(k, matrix((cv[:2], cv[2:]))) + counts['two_snapshot_pairs'] += 1 + return counts + + +def sharp_families(): + cases = 0 + for c in range(1, 4): + for r in range(1, 4): + for loss in range(min(c, r) + 1): + for p in (3, 5, 7): + k = matrix([[int(i == j) for j in range(c + r)] + for i in range(c)]) + constraints = [[0] * (c + r) for _ in range(r)] + for j in range(r): + constraints[j][c + j] = p if j < loss else 1 + if j < loss: + constraints[j][j] = 1 + constraints = matrix(constraints) + q = saturated_kernel(constraints) + require(field_rank(constraints) == r, 'sharp constraint rank') + require(field_rank(multiply(k, q)) == c, 'sharp rational rank') + require(capacity(k) == c, 'sharp initial capacity') + require(capacity(multiply(k, q)) == c - loss, 'sharp exact loss') + require(divisors(q)[-1] == 1, 'sharp saturated kernel') + cases += 1 + return cases + + +def dirty_word(): + cases = updates = 0 + for x, h0, h1 in product(range(-3, 4), repeat=3): + original = (h0, h1) + snapshot = h0 + 3 * h1 + for _ in range(3): + h0 += x + updates += 1 + h1 -= x + updates += 1 + require(h0 + 3 * h1 == snapshot, 'live snapshot at reading cut') + require(h0 - original[0] == 3 * x, 'restricted source response') + h1 += x + updates += 1 + for _ in range(3): + h0 -= x + updates += 1 + require((h0, h1) == original, 'arbitrary dirty restoration') + require(h0 + 3 * h1 == snapshot, 'live snapshot at ERASE') + cases += 1 + return {'dirty_inputs': cases, 'unit_add_updates': updates} + + +def controls(): + labels = [] + k = matrix(((1, 0),)) + c = matrix(((1, 3),)) + require(check_pair(k, c) == (1, 0), 'modular loss fixture') + labels.append('rational-rank-only overcounts') + require(capacity(multiply(k, matrix(((3,), (-1,))))) == 0, + 'unit-free constrained response') + labels.append('unconstrained direction violates snapshot') + require(multiply(c, matrix(((1,), (0,)))) == ((1,),), 'snapshot violation') + wrong_kernel = matrix(((0,), (3,))) + require(divisors(wrong_kernel)[-1] == 3, 'nonsaturated basis detectable') + require(capacity(multiply(matrix(((0, 1),)), wrong_kernel)) == 0, + 'nonsaturated false loss') + require(check_pair(matrix(((0, 1),)), matrix(((3, 0),))) == (1, 1), + 'primitive correct restriction') + labels.append('nonsaturated kernel gives false loss') + require(check_pair(k, matrix(((3, 0),))) == (1, 0), 'saturate before reduction') + require(field_rank(matrix(((3, 0),)), 3) == 0, 'reduction-first rank collapse') + labels.append('reduction before saturation overcounts') + require(check_pair(k, matrix(((0, 0),))) == (1, 1), 'zero snapshot') + labels.append('zero snapshot preserves capacity') + require(check_pair(identity(2), identity(2)) == (2, 0), 'full snapshot') + labels.append('full snapshot removes all directions') + require(check_pair(k, matrix(((1, 3), (2, 6)))) == (1, 0), 'dependent rows') + labels.append('dependent copies count by rank') + for label, rows in [('ragged matrix', ((1,), (1, 2))), + ('noninteger coefficient', ((Fraction(1, 2),),)), + ('dimension overflow', (tuple(range(7)),)), + ('coefficient overflow', ((1 << MAX_BITS,),))]: + try: + matrix(rows) + except ValueError: + labels.append(label) + else: + raise ValueError('failed input control: ' + label) + return labels + + +def main(): + result = census() + result['sharp_family_cases'] = sharp_families() + result.update(dirty_word()) + result['controls'] = controls() + result['environment'] = {'implementation': platform.python_implementation(), + 'python': platform.python_version()} + package = Path(__file__).resolve().parent + result['source_sha256'] = {p.name: sha256(p.read_bytes()).hexdigest() + for p in sorted(package.iterdir()) if p.is_file()} + print(json.dumps(result, sort_keys=True, indent=2)) + print('PASS_FROZEN_SNAPSHOT_CHANNEL_CAPACITY') + + +if __name__ == '__main__': + main()