Program for the three demonstrations
Run and edit these examples in your browser
Exact integer calculations using Python 3.10 or later and its standard library. The program checks reconstruction, refinement, and a recovery witness.
Download Python program Revision and checksum
From the download folder, run python -B komorebi_demonstrations.py all. Each demonstration page provides its expected output and mathematical explanation.
1 #!/usr/bin/env python3
2 """Three fixed, exact integer demonstrations for the Komorebi reading guide.
3
4 Python 3.10 or later. Standard library only. No files or network are used.
5 These calculations illustrate existing tutorials. They do not run Lean,
6 qualify production software or verify the collection's general theorems.
7 """
8 import argparse
9
10
11 def require(condition, message):
12 if not condition:
13 raise AssertionError(message)
14
15
16 def multiply(a, b):
17 return tuple(tuple(sum(x*y for x, y in zip(row, column))
18 for column in zip(*b)) for row in a)
19
20
21 def apply(a, vector):
22 return tuple(sum(x*y for x, y in zip(row, vector)) for row in a)
23
24
25 def add_matrices(matrices):
26 return tuple(tuple(sum(a[i][j] for a in matrices)
27 for j in range(len(matrices[0][0])))
28 for i in range(len(matrices[0])))
29
30
31 def add_vectors(vectors):
32 return tuple(map(sum, zip(*vectors)))
33
34
35 def packets():
36 x = (2, 3)
37 p = (((1, 0), (0, 0)), ((0, 0), (0, 1)))
38 identity, zero = ((1, 0), (0, 1)), ((0, 0), (0, 0))
39 t = ((1, 2), (3, 4))
40 require(add_matrices(p) == identity, 'Packets must sum to the identity')
41 for j in range(2):
42 for i in range(2):
43 require(multiply(p[j], p[i]) == (p[i] if i == j else zero),
44 'Packet multiplication identity failed')
45 # Rows are target packets and columns are source packets.
46 blocks = tuple(multiply(multiply(p[j], t), p[i])
47 for j in range(2) for i in range(2))
48 require(add_matrices(blocks) == t, 'Block reconstruction failed')
49 direct = apply(t, x)
50 rebuilt = add_vectors(tuple(apply(b, x) for b in blocks))
51 missing = add_vectors(tuple(apply(b, x) for b in blocks[:-1]))
52 require(direct == rebuilt == (8, 18), 'Unexpected reconstructed result')
53 require(missing == (8, 6) and missing != direct, 'Missing-block control failed')
54 return '\n'.join([
55 f'Input: {x}',
56 f'Packet parts: {tuple(apply(q, x) for q in p)}',
57 f'Block contributions: {tuple(apply(b, x) for b in blocks)}',
58 f'Direct result: {direct}',
59 f'Reconstructed result: {rebuilt}',
60 f'Without the final block: {missing}',
61 'PASS: packets',
62 ])
63
64
65 def refinement():
66 x = tuple(range(1, 9))
67 coarse = tuple(x[r::2] for r in range(2))
68 fine = tuple(x[r::4] for r in range(4))
69 # Interleave by original addresses. No padding or boundary extension.
70 rebuilt = tuple(fine[i % 4][i // 4] for i in range(len(x)))
71 lifted = tuple(tuple(v if i % 4 == r else 0 for i, v in enumerate(x))
72 for r in range(4))
73 for r in range(2):
74 require(add_vectors((lifted[r], lifted[r+2])) ==
75 tuple(v if i % 2 == r else 0 for i, v in enumerate(x)),
76 'Coarse packet differs from its fine children')
77 kept = add_vectors((lifted[0], lifted[1], lifted[3]))
78 residual = tuple(a-b for a, b in zip(x, kept))
79 energy = sum(v*v for v in residual)
80 require(rebuilt == x, 'Interleaving failed')
81 require(residual == lifted[2] and energy == 58, 'Discarded-packet control failed')
82 return '\n'.join([
83 f'Input: {x}', f'Two packets: {coarse}', f'Four packets: {fine}',
84 f'Interleaved: {rebuilt}', f'Without remainder 2: {kept}',
85 f'Residual: {residual}', f'Squared residual norm: {energy}',
86 'PASS: refinement',
87 ])
88
89
90 def recovery():
91 r, f, h = ((1, 1),), ((1, 0),), ((2, 2),)
92 u, v = (1, 0), (0, 1)
93 summary = apply(r, u)[0]
94 answers = (apply(f, u)[0], apply(f, v)[0])
95 w = tuple(a-b for a, b in zip(u, v))
96 rw, fw = apply(r, w)[0], apply(f, w)[0]
97 require(summary == apply(r, v)[0] == 1, 'Collision is missing')
98 require(answers == (1, 0) and rw == 0 and fw == 1, 'Witness failed')
99 # The matrix identity proves the compatible linear rule for every vector.
100 require(multiply(((2,),), r) == h, 'Compatible observation identity failed')
101 return '\n'.join([
102 f'Inputs: {u} and {v}', f'Same summary: {summary}',
103 f'Requested first coordinates: {answers}', f'Kernel witness: {w}',
104 f'R(w): {rw}', f'F(w): {fw}',
105 f'Compatible observation coefficients: {h[0]}',
106 'PASS: recovery',
107 ])
108
109
110 DEMOS = {'packets': packets, 'refinement': refinement, 'recovery': recovery}
111
112
113 def main():
114 parser = argparse.ArgumentParser(description=__doc__)
115 parser.add_argument('demo', nargs='?', choices=(*DEMOS, 'all'), default='all')
116 args = parser.parse_args()
117 names = DEMOS if args.demo == 'all' else (args.demo,)
118 print('\n\n'.join(DEMOS[name]() for name in names))
119
120
121 if __name__ == '__main__':
122 main()