RotationP46.lean

1 import KomorebiLSM.RotationConeGeometry
2 
3 /-! The complete Proposition 46 statement for the actual rational process.
4 The finite-generator obstruction quantifies over every generator count,
5 including zero and redundant generating families. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.RotationP46
8 open scoped BigOperators
9 open RotationModel
10 open FiniteInstruments (wordAction)
11 
12 /-- The exact rational rotation process is probability-valid on its canonical
13 Lorentz cone, has predictive dimension three, and admits no finite normalized
14 positive-generator certificate. All objects are constructed in the imported
15 proof modules; no rank, orbit-density or cone-characterization hypothesis is
16 assumed by this endpoint. -/
17 theorem rational_rank_three_nonpolyhedral_model :
18     (∀ s, ∃ M : Matrix (Fin 3) (Fin 3) ℚ,
19       M.map (algebraMap ℚ ℝ) = matrix s) ∧
20     IsClosed cone ∧ Convex ℝ cone ∧ initial ∈ cone ∧ mass initial = 1 ∧
21     (∀ s z, z ∈ cone → operator s z ∈ cone) ∧
22     (∀ a z, ∑ o, mass (operator (a,o) z) = mass z) ∧
23     (∀ z, z ∈ cone → mass z = 1 →
24       Behavior.CausalLaw (fun w => mass (wordAction operator w z)) ∧
25       ∀ w, 0 ≤ mass (wordAction operator w z) ∧
26         mass (wordAction operator w z) ≤ 1) ∧
27     Behavior.CausalLaw process ∧
28     TestDomains.allTests operator mass = cone ∧
29     (∀ C : Set State, IsClosed C → Convex ℝ C →
30       (∀ a : ℝ, 0 ≤ a → ∀ z ∈ C, a • z ∈ C) → initial ∈ C →
31       (∀ z ∈ C, 0 ≤ mass z) →
32       (∀ s z, z ∈ C → operator s z ∈ C) → C = cone) ∧
33     (∀ n : ℕ, ¬ ∃ V : (Fin n → ℝ) →ₗ[ℝ] State,
34       mass.comp V = FiniteInstruments.mass ∧
35       initial ∈ PositiveLift.hull V ∧
36       ∀ s z, z ∈ PositiveLift.hull V → operator s z ∈ PositiveLift.hull V) ∧
37     realization.IsReachable ∧ realization.IsObservable ∧
38     Module.finrank ℝ (Behavior.space process) = 3 := by
39   refine ⟨matrix_is_rational, LorentzBaseNorm.model_cone_closed,
40     LorentzBaseNorm.model_cone_convex, initial_mem, initial_mass,
41     fun s z hz => operator_cone s hz, operator_mass, ?_, process_causal,
42     RotationConeGeometry.canonical_cone_eq, ?_, ?_, realization_reachable,
43     realization_observable, behavior_dimension_three⟩
44   · intro z hz hm
45     exact ⟨causal_of_normalized_cone z hz hm, normalized_word_probability z hz hm⟩
46   · intro C hc hv hs hi hm hb
47     exact RotationConeGeometry.invariant_probability_cone_unique hc hv hs hi hm hb
48   · intro n
49     rintro ⟨V, hn, hi, hb⟩
50     exact RotationConeGeometry.no_finite_normalized_generator_certificate V hn hi hb
51 
52 end Komorebi.LSM.RotationP46

Back to source controls