nx_lattice.nx source
↩ module page · 99 lines · 3533 B
1// nx_lattice.nx -- 2D integer lattice primitives.
2//
3// Foundation for Minkowski's fundamental theorem (Freek #40) and
4// related geometry of numbers results.
5//
6// genealogy_id: minkowski_1896_geometrie_der_zahlen
7// lineage_id: zfc_separation + lattice + symmetric_convex_set
8// axioms: NX_AX_ZFC_SEPARATION, NX_AX_GEO_TWO_POINTS_DETERMINE_LINE
9
10// nx_safety_envelope:
11// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
12// sil_target: SIL1
13// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
14// verdict: NOT_YET_EVALUATED
15
16import "syscalls.nx"
17import "nx_axioms.nx"
18import "nx_i128.nx"
19
20// Count integer lattice points (i, j) with |i| <= R and |j| <= R AND
21// (i, j) satisfies a*i + b*j with |i|^2 + |j|^2 <= R^2 (disk).
22func nx_lattice_disk_point_count(R: i64) -> i64 {
23 if R < 0 { return 0 }
24 let R2: i64 = R * R
25 var count: i64 = 0
26 var i: i64 = -R
27 while i <= R {
28 var j: i64 = -R
29 while j <= R {
30 if i * i + j * j <= R2 { count = count + 1 }
31 j = j + 1
32 }
33 i = i + 1
34 }
35 return count
36}
37
38// Count integer lattice points in a centered axis-aligned rectangle
39// [-A, A] x [-B, B].
40func nx_lattice_rect_point_count(A: i64, B: i64) -> i64 {
41 if A < 0 { return 0 }
42 if B < 0 { return 0 }
43 return (2 * A + 1) * (2 * B + 1)
44}
45
46// Minkowski's fundamental theorem (rectangle case):
47// If a centered, symmetric, convex set in R^2 has area > 4, then it
48// contains a non-zero lattice point.
49// Substrate verifier: for a 2A x 2B rectangle (area = 4AB), area > 4
50// iff AB > 1. In this case, the rectangle [-A, A] x [-B, B] contains
51// lattice points other than origin (e.g., (1,0) if A >= 1).
52//
53// Returns 1 if Minkowski conclusion holds: rectangle of area > 4
54// has a nonzero lattice point inside.
55func nx_lattice_minkowski_rect_check(A: i64, B: i64) -> i64 {
56 if A * B <= 1 { return 0 } // area <= 4
57 // Find any nonzero (i, j) with |i| <= A, |j| <= B.
58 if A >= 1 { return 1 } // (1, 0) is in there
59 if B >= 1 { return 1 } // (0, 1) is in there
60 return 0
61}
62
63// L_p norm squared (p=2) of a lattice vector.
64func nx_lattice_norm_sq(x: i64, y: i64) -> i64 {
65 return x * x + y * y
66}
67
68// Shortest non-zero vector in a 2D lattice generated by (a1, a2), (b1, b2)
69// with both vectors having coordinates in [-K, K]. Brute search up to
70// linear combinations |c| <= search_max.
71func nx_lattice_shortest_vector_search(a1: i64, a2: i64, b1: i64, b2: i64,
72 search_max: i64) -> i64 {
73 var min_norm: i64 = -1
74 var c: i64 = -search_max
75 while c <= search_max {
76 var d: i64 = -search_max
77 while d <= search_max {
78 if c != 0 {
79 let x: i64 = c * a1 + d * b1
80 let y: i64 = c * a2 + d * b2
81 let n: i64 = nx_lattice_norm_sq(x, y)
82 if min_norm < 0 { min_norm = n }
83 if n < min_norm { min_norm = n }
84 }
85 if c == 0 {
86 if d != 0 {
87 let x: i64 = d * b1
88 let y: i64 = d * b2
89 let n: i64 = nx_lattice_norm_sq(x, y)
90 if min_norm < 0 { min_norm = n }
91 if n < min_norm { min_norm = n }
92 }
93 }
94 d = d + 1
95 }
96 c = c + 1
97 }
98 return min_norm
99}