structure ISAR.Matrix4 : Type

A concrete 4x4 matrix over the integers Int. Using a structure allows automatic derivation of decidable equality, meaning equality of computed matrices is decidable by computation (via rfl/decide).

• m00 : Int
• m01 : Int
• m02 : Int
• m03 : Int
• m10 : Int
• m11 : Int
• m12 : Int
• m13 : Int
• m20 : Int
• m21 : Int
• m22 : Int
• m23 : Int
• m30 : Int
• m31 : Int
• m32 : Int
• m33 : Int

def ISAR.instDecidableEqMatrix4.decEq (x✝ x✝¹ : Matrix4) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance ISAR.instDecidableEqMatrix4 : DecidableEq Matrix4

Equations

• ISAR.instDecidableEqMatrix4 = ISAR.instDecidableEqMatrix4.decEq

@[implicit_reducible]

instance ISAR.instReprMatrix4 : Repr Matrix4

Equations

• ISAR.instReprMatrix4 = { reprPrec := ISAR.instReprMatrix4.repr }

def ISAR.instReprMatrix4.repr : Matrix4 → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def ISAR.mul (A B : Matrix4) : Matrix4

Matrix multiplication.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance ISAR.instMulMatrix4 : Mul Matrix4

Equations

• ISAR.instMulMatrix4 = { mul := ISAR.mul }

def ISAR.zero : Matrix4

The zero matrix.

Equations

• ISAR.zero = { m00 := 0, m01 := 0, m02 := 0, m03 := 0, m10 := 0, m11 := 0, m12 := 0, m13 := 0, m20 := 0, m21 := 0, m22 := 0, m23 := 0, m30 := 0, m31 := 0, m32 := 0, m33 := 0 }

@[implicit_reducible]

instance ISAR.instZeroMatrix4 : Zero Matrix4

Equations

• ISAR.instZeroMatrix4 = { zero := ISAR.zero }

def ISAR.I1 : Matrix4

Invariant layer projection matrix (I).

Equations

• ISAR.I1 = { m00 := 1, m01 := 0, m02 := 0, m03 := 0, m10 := 0, m11 := 0, m12 := 0, m13 := 0, m20 := 0, m21 := 0, m22 := 1, m23 := 0, m30 := 0, m31 := 0, m32 := 0, m33 := 0 }

def ISAR.R1 : Matrix4

Rotation matrix (R).

Equations

• ISAR.R1 = { m00 := 1, m01 := 0, m02 := 0, m03 := 0, m10 := 0, m11 := 0, m12 := 0, m13 := 0, m20 := 0, m21 := 1, m22 := 0, m23 := 0, m30 := 0, m31 := 0, m32 := 1, m33 := 0 }

def ISAR.A1 : Matrix4

Adjacency matrix (A).

Equations

• ISAR.A1 = { m00 := 0, m01 := 0, m02 := 0, m03 := 0, m10 := 1, m11 := 0, m12 := 0, m13 := 0, m20 := 0, m21 := 1, m22 := 0, m23 := 0, m30 := 0, m31 := 0, m32 := 0, m33 := 0 }

def ISAR.S1 : Matrix4

Selection matrix (S).

Equations

• ISAR.S1 = { m00 := 1, m01 := 1, m02 := 0, m03 := 0, m10 := 0, m11 := 1, m12 := 0, m13 := 0, m20 := 0, m21 := 0, m22 := 1, m23 := 0, m30 := 0, m31 := 0, m32 := 0, m33 := 1 }

theorem ISAR.I1_idempotent : I1 * I1 = I1

Theorem: The invariant projection matrix I1 is idempotent.

theorem ISAR.K1_nilpotent : I1 * R1 * A1 * S1 * (I1 * R1 * A1 * S1) = zero

Theorem: The core rewrite operator K1 = I1 * R1 * A1 * S1 is nilpotent (K1² = 0).

def ISAR.I2 : Matrix4

Invariant layer projection matrix (I) - version 2.

Equations

• ISAR.I2 = { m00 := 1, m01 := 0, m02 := 0, m03 := 0, m10 := 0, m11 := 0, m12 := 0, m13 := 0, m20 := 0, m21 := 0, m22 := 1, m23 := 0, m30 := 0, m31 := 0, m32 := 0, m33 := 0 }

def ISAR.R2 : Matrix4

Rotation matrix (R) - version 2.

Equations

• ISAR.R2 = { m00 := 1, m01 := 0, m02 := 0, m03 := 0, m10 := 0, m11 := 0, m12 := 0, m13 := 1, m20 := 0, m21 := 0, m22 := 1, m23 := 0, m30 := 0, m31 := 0, m32 := 0, m33 := 0 }

def ISAR.A2 : Matrix4

Adjacency matrix (A) - version 2.

Equations

• ISAR.A2 = { m00 := 0, m01 := 0, m02 := 0, m03 := 0, m10 := 1, m11 := 0, m12 := 0, m13 := 0, m20 := 0, m21 := 1, m22 := 0, m23 := 0, m30 := 0, m31 := 0, m32 := 0, m33 := 0 }

def ISAR.S2 : Matrix4

Selection matrix (S) - version 2.

Equations

• ISAR.S2 = { m00 := 1, m01 := 1, m02 := 0, m03 := 0, m10 := 0, m11 := 1, m12 := 0, m13 := 0, m20 := 0, m21 := 0, m22 := 1, m23 := 0, m30 := 0, m31 := 0, m32 := 0, m33 := 1 }

theorem ISAR.I2_idempotent : I2 * I2 = I2

Theorem: The invariant projection matrix I2 is idempotent.

theorem ISAR.K2_nilpotent : I2 * R2 * A2 * S2 * (I2 * R2 * A2 * S2) = zero

Theorem: The core rewrite operator K2 = I2 * R2 * A2 * S2 is nilpotent (K2² = 0).

def ISAR.I_id : Matrix4

The 4D Identity matrix.

Equations

• ISAR.I_id = { m00 := 1, m01 := 0, m02 := 0, m03 := 0, m10 := 0, m11 := 1, m12 := 0, m13 := 0, m20 := 0, m21 := 0, m22 := 1, m23 := 0, m30 := 0, m31 := 0, m32 := 0, m33 := 1 }

def ISAR.P : Matrix4

Lower-triangular gauge transformation matrix (P).

Equations

• ISAR.P = { m00 := 1, m01 := 0, m02 := 0, m03 := 0, m10 := 1, m11 := 1, m12 := 0, m13 := 0, m20 := 0, m21 := 0, m22 := 1, m23 := 0, m30 := 0, m31 := 0, m32 := 0, m33 := 1 }

def ISAR.P_inv : Matrix4

Inverse gauge transformation matrix (P_inv).

Equations

• ISAR.P_inv = { m00 := 1, m01 := 0, m02 := 0, m03 := 0, m10 := -1, m11 := 1, m12 := 0, m13 := 0, m20 := 0, m21 := 0, m22 := 1, m23 := 0, m30 := 0, m31 := 0, m32 := 0, m33 := 1 }

theorem ISAR.P_inv_left : P_inv * P = I_id

Theorem: P_inv is the left inverse of P.

theorem ISAR.P_inv_right : P * P_inv = I_id

Theorem: P_inv is the right inverse of P.

theorem ISAR.K1_K2_gauge_equiv : P * (I1 * R1 * A1 * S1) * P_inv = I2 * R2 * A2 * S2

Theorem: Gauge Equivalence. The two kernel representations are conjugate (similar) via the gauge matrix P. This formally unifies the two inconsistent representations of R used in the python scripts.