InstrumentRealization.lean

1 import KomorebiLSM.InstrumentCoordinates
2 
3 /-! Known finite instruments have minimal mass-anchored predictive coordinates.
4 Signed coordinates are interpreted on the image of genuine beliefs, not as
5 independent nonnegative probabilities. No unknown-model learning is asserted. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.FiniteInstruments
8 open scoped BigOperators
9 open Module FiniteBayes
10 universe u v w
11 variable {I : Type u} {U : Type v} {O : Type w} [Fintype I] [Fintype O]
12 variable {E : Type*} [AddCommGroup E] [Module ℝ E]
13 
14 /-- The admissible predictive states are images of actual priors. -/
15 def realizableBeliefs (R : (I → ℝ) →ₗ[ℝ] E) : Set E :=
16   {z | ∃ p, IsPrior p ∧ R p = z}
17 
18 section Semantics
19 variable (T : Instrument I U O) (R : (I → ℝ) →ₗ[ℝ] E)
20 variable (B : U × O → E →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ)
21 variable (hmass : l.comp R = mass)
22 variable (hB : ∀ s, (B s).comp R = R.comp (T.branch s))
23 include hmass hB
24 
25 /-- The scalar prediction is exactly the fine joint branch mass. -/
26 theorem reduced_likelihood (s : U × O) (p : I → ℝ) :
27     l (B s (R p)) = mass (T.branch s p) := by
28   have hs : B s (R p) = R (T.branch s p) :=
29     congrArg (fun F : (I → ℝ) →ₗ[ℝ] E => F p) (hB s)
30   rw [hs]
31   exact congrArg (fun f : (I → ℝ) →ₗ[ℝ] ℝ => f (T.branch s p)) hmass
32 
33 /-- The normalized state commutes with the observation summary. -/
34 theorem reduced_posterior (s : U × O) (p : I → ℝ) :
35     R (normalize mass (T.branch s p)) = normalize l (B s (R p)) := by
36   have hs : B s (R p) = R (T.branch s p) :=
37     congrArg (fun F : (I → ℝ) →ₗ[ℝ] E => F p) (hB s)
38   rw [normalize_transport R mass l hmass, hs]
39 
40 theorem reduced_word_readout (w : List (U × O)) (p : I → ℝ) :
41     l (wordAction B w (R p)) = mass (wordAction T.branch w p) := by
42   have hw := word_intertwining T.branch B R hB w
43   have hp := congrArg (fun F : (I → ℝ) →ₗ[ℝ] E => F p) hw
44   change wordAction B w (R p) = R (wordAction T.branch w p) at hp
45   rw [hp]
46   exact congrArg (fun f : (I → ℝ) →ₗ[ℝ] ℝ => f (wordAction T.branch w p)) hmass
47 
48 theorem realization_reads_all_words : ReadsAllWords T.branch R := by
49   intro w
50   exact ⟨l.comp (wordAction B w), fun p _ => reduced_word_readout T R B l hmass hB w p⟩
51 
52 theorem reduced_likelihood_prior (a : U) (z : E) (hz : z ∈ realizableBeliefs R) :
53     IsPrior (fun o => l (B (a,o) z)) := by
54   obtain ⟨p,hp,rfl⟩ := hz
55   simpa only [reduced_likelihood T R B l hmass hB] using T.likelihood_prior a p hp
56 
57 /-- Only positive-likelihood branches have a probabilistic posterior. -/
58 theorem reduced_posterior_realizable (s : U × O) (z : E)
59     (hz : z ∈ realizableBeliefs R) (hpos : 0 < l (B s z)) :
60     normalize l (B s z) ∈ realizableBeliefs R := by
61   obtain ⟨p,hp,rfl⟩ := hz
62   have htrue : 0 < mass (T.branch s p) := by
63     rwa [reduced_likelihood T R B l hmass hB] at hpos
64   exact ⟨normalize mass (T.branch s p), T.branch_posterior_prior s p hp htrue,
65     reduced_posterior T R B l hmass hB s p⟩
66 
67 theorem reduced_word_probability (w : List (U × O)) (z : E)
68     (hz : z ∈ realizableBeliefs R) :
69     0 ≤ l (wordAction B w z) ∧ l (wordAction B w z) ≤ 1 := by
70   obtain ⟨p,hp,rfl⟩ := hz
71   rw [reduced_word_readout T R B l hmass hB]
72   exact T.word_probability w p hp
73 
74 /-- Onto coordinates promote the mass identity to the whole coordinate space. -/
75 theorem reduced_mass_identity (hR : Function.Surjective R) (a : U) (z : E) :
76     ∑ o, l (B (a,o) z) = l z := by
77   obtain ⟨p,rfl⟩ := hR z
78   simp only [reduced_likelihood T R B l hmass hB]
79   rw [T.instrument_mass]
80   exact (congrArg (fun f : (I → ℝ) →ₗ[ℝ] ℝ => f p) hmass).symm
81 
82 end Semantics
83 
84 /-- A complete P26 realization is constructed from the supplied hidden instrument.
85 The result contains a literal first-coordinate mass row, unique transitions,
86 all-word equality and posterior closure on admissible branches. -/
87 theorem finite_instrument_closure [Nonempty I] (T : Instrument I U O) :
88     ∃ (r : ℕ) (hr : 0 < r)
89       (R : (I → ℝ) →ₗ[ℝ] (Fin r → ℝ))
90       (B : U × O → (Fin r → ℝ) →ₗ[ℝ] (Fin r → ℝ)),
91       let l : (Fin r → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj ⟨0,hr⟩
92       r = finrank ℝ (wordSpan T.branch mass) ∧
93       LinearIndependent ℝ (fun j => (LinearMap.proj j).comp R) ∧
94       Function.Surjective R ∧
95       LinearMap.range R.dualMap = wordSpan T.branch mass ∧
96       l.comp R = mass ∧
97       (∀ s, (B s).comp R = R.comp (T.branch s)) ∧
98       (∀ s D, D.comp R = R.comp (T.branch s) → D = B s) ∧
99       (∀ w p, l (wordAction B w (R p)) = mass (wordAction T.branch w p)) ∧
100       (∀ s z, z ∈ realizableBeliefs R → 0 < l (B s z) →
101         normalize l (B s z) ∈ realizableBeliefs R) := by
102   obtain ⟨r,hr,R,B,hd,hind,honto,hrow,hm,hc,hu⟩ := finite_instrument_coordinates T.branch
103   refine ⟨r,hr,R,B, ?_⟩
104   dsimp only
105   refine ⟨?_,hind,honto,?_,hm,hc,hu,?_,?_⟩
106   · rwa [instrumentCompletion_eq_wordSpan] at hd
107   · rwa [instrumentCompletion_eq_wordSpan] at hrow
108   · exact reduced_word_readout T R B _ hm hc
109   · exact reduced_posterior_realizable T R B _ hm hc
110 
111 end Komorebi.LSM.FiniteInstruments

Back to source controls