File size: 4,792 Bytes
9425aed | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 | theory MOCJordanRoundtrip
imports Main
begin
(* ═══════════════════════════════════════════════════════════════════════════
MOCJordanRoundtrip.thy — Closes gap 2: MOC 108-dim ↔ Jordan 10×10 roundtrip
Ahmad Ali Parr · SnapKitty Collective · 2026
Zero sorry. Pure arithmetic. simp + metis only.
═══════════════════════════════════════════════════════════════════════════ *)
definition MOC_DIM :: nat where "MOC_DIM = 108"
definition JORDAN_N :: nat where "JORDAN_N = 10"
(* 100 ≤ 108: the matrix fits in the MOC array *)
lemma jordan_fits_in_moc: "JORDAN_N * JORDAN_N ≤ MOC_DIM"
by (simp add: MOC_DIM_def JORDAN_N_def)
(* Every valid matrix index is a valid MOC index *)
lemma index_bound:
assumes "i < JORDAN_N" "j < JORDAN_N"
shows "i * JORDAN_N + j < MOC_DIM"
using assms by (simp add: MOC_DIM_def JORDAN_N_def)
(* The data region: i*10 + j < 100 *)
lemma in_data_region:
assumes "i < JORDAN_N" "j < JORDAN_N"
shows "i * JORDAN_N + j < JORDAN_N * JORDAN_N"
using assms by (simp add: JORDAN_N_def)
(* Row recovery: (i*10 + j) div 10 = i *)
lemma decode_row:
assumes "j < JORDAN_N"
shows "(i * JORDAN_N + j) div JORDAN_N = i"
using assms by (simp add: JORDAN_N_def)
(* Column recovery: (i*10 + j) mod 10 = j *)
lemma decode_col:
assumes "j < JORDAN_N"
shows "(i * JORDAN_N + j) mod JORDAN_N = j"
using assms by (simp add: JORDAN_N_def)
(* Encoding: (i,j) ↦ i*10 + j *)
definition encode_idx :: "nat ⇒ nat ⇒ nat" where
"encode_idx i j = i * JORDAN_N + j"
(* Encoding is injective on valid indices *)
lemma encode_injective:
assumes "i1 < JORDAN_N" "j1 < JORDAN_N"
"i2 < JORDAN_N" "j2 < JORDAN_N"
"encode_idx i1 j1 = encode_idx i2 j2"
shows "i1 = i2 ∧ j1 = j2"
proof
show "i1 = i2"
using assms
by (metis decode_row encode_idx_def)
show "j1 = j2"
using assms
by (metis decode_col encode_idx_def)
qed
(* Encoding + decoding as functions over an arbitrary type 'a *)
definition encode_matrix :: "(nat ⇒ nat ⇒ 'a) ⇒ 'a ⇒ nat ⇒ 'a" where
"encode_matrix m pad_val k =
(if k < JORDAN_N * JORDAN_N
then m (k div JORDAN_N) (k mod JORDAN_N)
else pad_val)"
definition decode_matrix :: "(nat ⇒ 'a) ⇒ nat ⇒ nat ⇒ 'a" where
"decode_matrix f i j = f (encode_idx i j)"
(* ═══════════════════════════════════════════════════════
MAIN THEOREM: decode ∘ encode = id ZERO SORRY
═══════════════════════════════════════════════════════ *)
theorem moc_jordan_roundtrip:
assumes "i < JORDAN_N" "j < JORDAN_N"
shows "decode_matrix (encode_matrix m pad_val) i j = m i j"
proof -
have h_lt : "encode_idx i j < JORDAN_N * JORDAN_N"
using assms by (simp add: encode_idx_def JORDAN_N_def)
have h_row : "(encode_idx i j) div JORDAN_N = i"
using assms by (simp add: encode_idx_def decode_row)
have h_col : "(encode_idx i j) mod JORDAN_N = j"
using assms by (simp add: encode_idx_def decode_col)
show ?thesis
by (simp add: decode_matrix_def encode_matrix_def h_lt h_row h_col)
qed
(* COROLLARY: encode is injective — no information lost *)
corollary moc_encode_no_collision:
assumes "i1 < JORDAN_N" "j1 < JORDAN_N"
"i2 < JORDAN_N" "j2 < JORDAN_N"
"encode_matrix m pad_val (encode_idx i1 j1) =
encode_matrix m pad_val (encode_idx i2 j2)"
shows "m i1 j1 = m i2 j2"
proof -
have h1: "encode_idx i1 j1 < JORDAN_N * JORDAN_N"
using assms by (simp add: encode_idx_def JORDAN_N_def)
have h2: "encode_idx i2 j2 < JORDAN_N * JORDAN_N"
using assms by (simp add: encode_idx_def JORDAN_N_def)
have h_row1: "(encode_idx i1 j1) div JORDAN_N = i1"
using assms(2) by (simp add: encode_idx_def decode_row)
have h_col1: "(encode_idx i1 j1) mod JORDAN_N = j1"
using assms(2) by (simp add: encode_idx_def decode_col)
have h_row2: "(encode_idx i2 j2) div JORDAN_N = i2"
using assms(4) by (simp add: encode_idx_def decode_row)
have h_col2: "(encode_idx i2 j2) mod JORDAN_N = j2"
using assms(4) by (simp add: encode_idx_def decode_col)
show ?thesis
using assms(5)
by (simp add: encode_matrix_def h1 h2 h_row1 h_col1 h_row2 h_col2)
qed
end
|