Transfer.lean

1 import MachineTheory.Behavior
2 import Mathlib.Algebra.Module.LinearMap.End
3 import Mathlib.Algebra.Field.Defs
4 
5 /-! Core v0.2, 2.1 and 2.3. Exact algebra and left-to-right forward transport. -/
6 namespace Komorebi.MachineTheory
7 
8 /-- Local intertwining composes along arbitrary finite, left-to-right action words. -/
9 theorem forward_transport {X Y A B : Type*} (F : A → X → X) (G : B → Y → Y)
10     (T : X → Y) (τ : A → B) (h : ∀ a x, T (F a x) = G (τ a) (T x))
11     (word : List A) (x : X) : T (run F word x) = run G (word.map τ) (T x) := by
12   induction word generalizing x with
13   | nil => rfl
14   | cons a word ih =>
15     change T (run F word (F a x)) = run G (word.map τ) (G (τ a) (T x))
16     rw [ih, h]
17 
18 /-- Matched readouts must be an additional premise. -/
19 theorem forward_output {X Y A B O : Type*} (F : A → X → X) (G : B → Y → Y)
20     (T : X → Y) (τ : A → B) (q : X → O) (qbar : Y → O)
21     (h : ∀ a x, T (F a x) = G (τ a) (T x)) (hq : ∀ x, q x = qbar (T x))
22     (word : List A) (x : X) : q (run F word x) = qbar (run G (word.map τ) (T x)) := by
23   rw [hq, forward_transport F G T τ h]
24 
25 /-- Restricting to an invariant subtype makes domain closure explicit. -/
26 theorem invariant_forward_transport {X Y A B : Type*} (D : Set X)
27     (F : A → X → X) (G : B → Y → Y) (T : X → Y) (τ : A → B)
28     (hD : ∀ a x, x ∈ D → F a x ∈ D)
29     (h : ∀ a x, x ∈ D → T (F a x) = G (τ a) (T x))
30     (word : List A) (x : X) (hx : x ∈ D) :
31     T (run F word x) = run G (word.map τ) (T x) := by
32   induction word generalizing x with
33   | nil => rfl
34   | cons a word ih =>
35     change T (run F word (F a x)) = run G (word.map τ) (G (τ a) (T x))
36     rw [ih (F a x) (hD a x hx), h a x hx]
37 
38 /-- Output preservation on an invariant domain, including domain-restricted readout agreement. -/
39 theorem invariant_forward_output {X Y A B O : Type*} (D : Set X)
40     (F : A → X → X) (G : B → Y → Y) (T : X → Y) (τ : A → B)
41     (q : X → O) (qbar : Y → O)
42     (hD : ∀ a x, x ∈ D → F a x ∈ D)
43     (h : ∀ a x, x ∈ D → T (F a x) = G (τ a) (T x))
44     (hq : ∀ x, x ∈ D → q x = qbar (T x))
45     (word : List A) (x : X) (hx : x ∈ D) :
46     q (run F word x) = qbar (run G (word.map τ) (T x)) := by
47   have hi : ∀ (w : List A) (y : X), y ∈ D → run F w y ∈ D := by
48     intro w
49     induction w with
50     | nil => intro y hy; exact hy
51     | cons a w ih => intro y hy; exact ih (F a y) (hD a y hy)
52   rw [hq _ (hi word x hx), invariant_forward_transport D F G T τ hD h word x hx]
53 
54 section Split
55 variable {𝕜 V Z : Type*} [Field 𝕜] [AddCommGroup V] [Module 𝕜 V]
56   [AddCommGroup Z] [Module 𝕜 Z]
57 
58 /-- Full split encoding has the compatible-image projector as its identity. -/
59 theorem split_projector_idempotent (A : V →ₗ[𝕜] Z) (S : Z →ₗ[𝕜] V)
60     (hSA : S.comp A = LinearMap.id) : (A.comp S).comp (A.comp S) = A.comp S := by
61   ext z
62   have h : ∀ v, S (A v) = v := fun v => LinearMap.congr_fun hSA v
63   simp only [LinearMap.comp_apply, h]
64 
65 /-- Core 2.1: whole-state encoding preserves multiplication. -/
66 theorem split_encoding_comp (A : V →ₗ[𝕜] Z) (S : Z →ₗ[𝕜] V)
67     (hSA : S.comp A = LinearMap.id) (T U : V →ₗ[𝕜] V) :
68     (A.comp (T.comp S)).comp (A.comp (U.comp S)) = A.comp ((T.comp U).comp S) := by
69   ext z
70   have h : ∀ v, S (A v) = v := fun v => LinearMap.congr_fun hSA v
71   simp only [LinearMap.comp_apply, h]
72 
73 /-- The discarded-return identity itself does not need C R = identity. -/
74 theorem hidden_return_identity (C : V →ₗ[𝕜] Z) (R : Z →ₗ[𝕜] V)
75     (T U : V →ₗ[𝕜] V) :
76     C.comp ((T.comp U).comp R) - (C.comp (T.comp R)).comp (C.comp (U.comp R)) =
77       C.comp (T.comp ((LinearMap.id - R.comp C).comp (U.comp R))) := by
78   ext z
79   simp only [LinearMap.sub_apply, LinearMap.comp_apply, LinearMap.id_apply, map_sub]
80 
81 /-- Core 2.1: exact composition iff the named discarded excursion vanishes. -/
82 theorem compressed_comp_iff_no_return (C : V →ₗ[𝕜] Z) (R : Z →ₗ[𝕜] V)
83     (T U : V →ₗ[𝕜] V) :
84     C.comp ((T.comp U).comp R) = (C.comp (T.comp R)).comp (C.comp (U.comp R)) ↔
85       C.comp (T.comp ((LinearMap.id - R.comp C).comp (U.comp R))) = 0 := by
86   rw [← hidden_return_identity]
87   exact sub_eq_zero.symm
88 
89 /-- Under the compression split, the reconstructed retained part is a projector. -/
90 theorem compression_projector_idempotent (C : V →ₗ[𝕜] Z) (R : Z →ₗ[𝕜] V)
91     (hCR : C.comp R = LinearMap.id) : (R.comp C).comp (R.comp C) = R.comp C := by
92   exact split_projector_idempotent R C hCR
93 end Split
94 end Komorebi.MachineTheory

Back to source controls