diff --git a/research/a3-d5-decoder-floor/README.md b/research/a3-d5-decoder-floor/README.md new file mode 100644 index 0000000000..0f971cf3bc --- /dev/null +++ b/research/a3-d5-decoder-floor/README.md @@ -0,0 +1,242 @@ +# The fixed A3+D5 nine-normal decoder has exact COPY cost 72 + +This contribution was produced by Nick Petalas. Apache-2.0. + +Scoped algebraic proof with exhaustive finite premises. For the fixed +`A3 weights + D5 root basis` family in +[joaqcoo's PR1224](https://github.com/CrocSwap/integer-mult-bounds/pull/1224), +the minimum separate-term binary pairing-rank cost on all 120 E8 root lines +is exactly **72**, allowing arbitrary independent complex row shifts. +An exact nine-active-term witness has ranks `(1,8,9,9,9,9,9,9,9)`. + +The source gives a sparsest-row cost-81 example and records three bounded +searches whose best cost is 81 for this unpunctured family. The new result +replaces that upper bound with a sharp optimum. Its ratio `72/120 = 3/5` +equals the ordinary eight-term P120 COPY bill. It does not improve the P112 +ratio `4/7`, supply a physical supplier, change kappa or prove a complete +multiplication theorem. No literature-priority claim is intended. + +## Exact model + +Let `r_i` run over the 120 E8 root lines of squared norm two in eight +coordinates. Use the representative with first nonzero coordinate positive. +The doubled roots `x_i=2r_i` are the 56 vectors `2e_a +/- 2e_b`, `a` in `K_j`, put + +```text +H_k(U) = {z : z is compatible with every member of U}, k!=j. +``` + +This is the annihilator of the labels on +`(supp(a) union supp(b)) intersect {i:d_ij!=d_ik}`. Checking the two basis +characters therefore checks the entire plane. Necessarily `K_k subset H_k(U)`. + +The exhaustive finite premises are: + +1. At every anchor j and every binary plane U, each of its three partner + spaces `H_k(U)` has dimension at most one. +2. For every subset J of the nonzero partner spaces, let z_k be its unique + nonzero character and let F be the span of all labels on + `supp(z_k) intersect {i:d_ij!=d_ik}`, for k in J. Then `dim F >= |J|`. + +If every delta is at most one, their sum is at most four. Otherwise choose +an anchor j with `delta_j>=2` and a plane U in `K_j`. Premise 1 makes every +other nonzero `K_k` one-dimensional; let J be exactly these k. Compatibility +forces all of `K_j` to annihilate F, so + +```text +sum delta_k = delta_j + |J| <= 9-dim F+|J| <= 9. +``` + +This proves cost at least 72 for every complex shift assignment. The proof +adapts the deficiency-plane method of Philipp / mightyOil #1248 and the +forced-space argument of Adam Gall #2062, with their credit retained. +Their different normal families are not replayed or assumed to imply these +finite premises. + +### Complete finite coverage + +Characters are exactly the 512 nine-bit vectors. Every plane has three +nonzero vectors and the unique ordered representation `0> column) & 1) << j + for j, column in enumerate(columns)) for row in pairing) + require(len(binary_basis(labels)) == 9, "label projection") + readers = tuple(sum((dot(line, normal) != 0) << i + for i, line in enumerate(lines)) for normal in NORMALS) + require(all(len(binary_basis(row & mask for row in pairing)) == 9 + for mask in readers), "reader ranks") + return grams, pairing, labels, readers + + +def selected_rows(values, mask): + return tuple(value for i, value in enumerate(values) if (mask >> i) & 1) + + +def character_supports(labels): + supports = tuple(sum(((label & w).bit_count() % 2) << i + for i, label in enumerate(labels)) for w in range(512)) + require(len(set(supports)) == 512 and supports[0] == 0, "character coverage") + return supports + + +def partner_tables(anchor, base, labels, supports): + tables, forced = {}, {} + for k in range(4): + if k == anchor: + continue + difference = sum((row[anchor] != row[k]) << i for i, row in enumerate(base)) + tables[k] = tuple(sum((not (left & right & difference)) << z + for z, right in enumerate(supports[1:], 1)) + for left in supports) + forced[k] = tuple(binary_basis(selected_rows(labels, mask & difference)) + for mask in supports) + return tables, forced + + +def plane_certificate(anchor, tables): + histogram, signatures, count = Counter(), set(), 0 + for a in range(1, 512): + for b in range(a + 1, 512): + if b >= (a ^ b): + continue + count += 1 + signature = [] + for table in tables.values(): + nonzero = table[a] & table[b] + require(nonzero.bit_count() <= 1, "partner dimension exceeds one") + signature.append(nonzero.bit_length() - 1 if nonzero else 0) + signatures.add(tuple(signature)) + histogram[sum(z != 0 for z in signature)] += 1 + require(count == 43435, "plane coverage") + require(dict(histogram) == {0: 18211, 1: 18144, 2: 6237, 3: 843}, + "plane histogram") + require(len(signatures) == 767, "signature count") + return signatures, {"anchor": anchor, "planes": count, + "nonzero_partner_histogram": dict(sorted(histogram.items())), + "signatures": len(signatures)} + + +def forced_certificate(signatures, tables, forced): + maximum, cases, missing_constraint_witness = 0, 0, False + for signature in sorted(signatures): + active = tuple((k, z) for k, z in zip(tables, signature, strict=True) if z) + for mask in range(1 << len(active)): + chosen = tuple(pair for j, pair in enumerate(active) if (mask >> j) & 1) + rows = tuple(row for k, z in chosen for row in forced[k][z]) + rank = len(binary_basis(rows)) + bound = 9 - rank + len(chosen) + require(bound <= 9, "deficiency bound") + maximum = max(maximum, bound) + cases += 1 + missing_constraint_witness |= bool(chosen) and bound == 9 + require(maximum == 9 and missing_constraint_witness, "sharp finite bound") + literal_checks = 0 + for k, table in tables.items(): + for z in range(1, 512): + equations = forced[k][z] + annihilator = sum(all((w & row).bit_count() % 2 == 0 for row in equations) + << w for w in range(1, 512)) + require(annihilator == table[z], "literal annihilator disagreement") + literal_checks += 1 + return {"subset_cases": cases, "maximum_deficiency_bound": maximum, + "literal_annihilator_checks": literal_checks, + "missing_constraint_bound_exceeds_nine": missing_constraint_witness} + + +def exact_identity(coeffs, lines, grams, normals=NORMALS): + readers = tuple(tuple(Fraction(dot(line, normal), 16) for normal in normals) + for line in lines) + return all(dot(row, reader) == 2 * grams[i][j] + for i, row in enumerate(coeffs) for j, reader in enumerate(readers)) + + +def rank_profile(coeffs, pairing, readers): + profile = [] + for k in range(9): + rows = tuple(pairing[i] & readers[k] for i, row in enumerate(coeffs) if row[k]) + profile.append(len(binary_basis(rows))) + return profile + + +def witness_certificate(base, lines, grams, pairing, readers): + require(exact_identity(base, lines, grams), "eight-active witness") + inactive = rank_profile(base, pairing, readers) + require(inactive == [0] + [9] * 8, "eight-active ranks") + active = [list(row) for row in base] + require(lines[0] == (2, 2, 0, 0, 0, 0, 0, 0) and base[0][1] == -4, + "active-witness row") + for k in range(4): + active[0][k] += 4 + require(exact_identity(active, lines, grams), "nine-active witness") + profile = rank_profile(active, pairing, readers) + require(profile == [1, 8] + [9] * 7, "nine-active ranks") + return active, {"eight_active_profile": inactive, "nine_active_profile": profile, + "identity_entries_per_witness": 14400, "optimum": 72} + + +def controls(active, lines, grams): + changed = [row[:] for row in active] + changed[0][0] += 1 + require(not exact_identity(changed, lines, grams), "coefficient control") + missing = [row[:] for row in active] + for row in missing: + row[4] = 0 + require(not exact_identity(missing, lines, grams), "forced-term control") + swapped = list(NORMALS) + swapped[0], swapped[4] = swapped[4], swapped[0] + require(not exact_identity(active, lines, grams, tuple(swapped)), "reader control") + generic_shift = [row[:] for row in active] + for k in range(4): + generic_shift[0][k] += Fraction(1, 3) + require(exact_identity(generic_shift, lines, grams), "noncritical-shift control") + return {"rejected_identity_mutations": 3, "noncritical_shift_identity": True} + + +def run(): + lines = roots() + base = coefficients(lines) + grams, pairing, labels, readers = geometry(lines) + supports = character_supports(labels) + anchors = [] + for anchor in range(4): + tables, forced = partner_tables(anchor, base, labels, supports) + signatures, record = plane_certificate(anchor, tables) + record.update(forced_certificate(signatures, tables, forced)) + anchors.append(record) + active, witnesses = witness_certificate(base, lines, grams, pairing, readers) + return {"marker": "PASS_A3_D5_DECODER_FLOOR", "claim_type": "scoped proof", + "root_lines": len(lines), "anchors": anchors, "witnesses": witnesses, + "controls": controls(active, lines, grams), "no_new_kappa": True} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path, help="write a generated receipt outside the package") + args = parser.parse_args() + package = Path(__file__).resolve().parent + if args.receipt: + require(not args.receipt.resolve().is_relative_to(package), "receipt inside package") + result = run() + filenames = ("README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") + hashes = {} + for name in filenames: + path = package / name + require(path.is_file() and not path.is_symlink(), "package source file") + require(path.stat().st_size <= 1048576, "package source size") + hashes[name] = hashlib.sha256(path.read_bytes()).hexdigest() + result["source_sha256"] = hashes + payload = json.dumps(result, indent=2, sort_keys=True) + "\n" + if args.receipt: + with args.receipt.open("x", encoding="utf-8") as stream: + require(stream.write(payload) == len(payload), "receipt write") + print(payload, end="") + + +if __name__ == "__main__": + main()