mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
allaun
475f6319ea
This squashes all local history (768 commits) onto the scrubbed PR #90 baseline. Individual commits were lost during filter-repo corruption; the working tree content is preserved intact. Build: N/A (working tree state only)
105 lines
3.1 KiB
Python
105 lines
3.1 KiB
Python
#!/usr/bin/env python3
|
|
"""
|
|
compute_adjugate_identity.py — DSP shim for Lean kernel offload
|
|
|
|
Computes the 8x8 adjugate of the identity matrix and all 64 cofactor
|
|
product entries as Lean #eval-verified constants. This bypasses the
|
|
kernel's isDefEq timeout on 322K-operation determinant trees.
|
|
|
|
Output: Lean code snippet with pre-computed constants and #eval checks.
|
|
"""
|
|
|
|
Q16 = 65536
|
|
N = 8
|
|
|
|
def identity_matrix():
|
|
return [[Q16 if i == j else 0 for j in range(N)] for i in range(N)]
|
|
|
|
def det2(m):
|
|
return m[0][0]*m[1][1] - m[0][1]*m[1][0]
|
|
|
|
def minor(m, skip_row, skip_col):
|
|
return [[m[i][j] for j in range(N) if j != skip_col]
|
|
for i in range(N) if i != skip_row]
|
|
|
|
def det_rec(m, n):
|
|
if n == 1:
|
|
return m[0][0]
|
|
total = 0
|
|
for j in range(n):
|
|
sign = 1 if j % 2 == 0 else -1
|
|
sub = [[m[i][col] for col in range(n) if col != j] for i in range(1, n)]
|
|
total += sign * m[0][j] * det_rec(sub, n - 1)
|
|
return total
|
|
|
|
def det(m):
|
|
return det_rec(m, len(m))
|
|
|
|
def cofactor(m, i, j):
|
|
sub = minor(m, i, j)
|
|
sign = 1 if (i + j) % 2 == 0 else -1
|
|
return sign * det_rec(sub, len(m) - 1)
|
|
|
|
def adjugate(m):
|
|
n = len(m)
|
|
return [[cofactor(m, j, i) // Q16 for i in range(n)] for j in range(n)]
|
|
|
|
def matrix_multiply(a, b):
|
|
n = len(a)
|
|
result = [[0]*n for _ in range(n)]
|
|
for i in range(n):
|
|
for j in range(n):
|
|
total = 0
|
|
for k in range(n):
|
|
total += a[i][k] * b[k][j]
|
|
result[i][j] = total // Q16
|
|
return result
|
|
|
|
def cofactor_product_entry(m, i, j):
|
|
adj = adjugate(m)
|
|
total = 0
|
|
for k in range(N):
|
|
total += m[i][k] * adj[k][j]
|
|
return total // Q16
|
|
|
|
def to_q16_raw(val):
|
|
return max(-2147483648, min(2147483647, val))
|
|
|
|
def main():
|
|
I = identity_matrix()
|
|
|
|
print("// -- DSP-computed: adjugate(identity8) = identity8")
|
|
adj_I = adjugate(I)
|
|
for i in range(N):
|
|
for j in range(N):
|
|
expected = Q16 if i == j else 0
|
|
computed = adj_I[i][j]
|
|
assert computed == expected, f"adj(I)[{i}][{j}] = {computed}, expected {expected}"
|
|
print("// VERIFIED: adjugate(identity8) = identity8")
|
|
print()
|
|
|
|
print("// -- DSP-computed: cofactorProductEntry identity8 i j for all 64 (i,j)")
|
|
cpe = [[0]*N for _ in range(N)]
|
|
for i in range(N):
|
|
for j in range(N):
|
|
val = cofactor_product_entry(I, i, j)
|
|
cpe[i][j] = val
|
|
print()
|
|
|
|
print("// Lean #eval witnesses for all 64 entries:")
|
|
print("// (These are fast — just array lookups, no kernel unfolding)")
|
|
for i in range(N):
|
|
for j in range(N):
|
|
val = cpe[i][j]
|
|
print(f"#eval cofactorProductEntry identity8 {i} {j} -- expect {val}")
|
|
print()
|
|
|
|
print("// Lean lemma: all entries verified by DSP")
|
|
print("// (Replace native_decide calls with these constants)")
|
|
for i in range(N):
|
|
for j in range(N):
|
|
val = cpe[i][j]
|
|
print(f"theorem cpe_identity_{i}_{j} : cofactorProductEntry identity8 {i} {j} = ofRawInt {val} := by native_decide")
|
|
|
|
if __name__ == "__main__":
|
|
main()
|