Identify finite cuts of input-only domains

THEORY.md

@@ -314,8 +314,8 @@ extension are in [Examples](src/Examples/README.md).
 
 [IsDDS]: src/RandomSystems/System/Basic.lean#L81
 [automatonSystem_eq_of_bisim]: src/RandomSystems/System/Automaton.lean#L93
-[Domain]: src/RandomSystems/PDS/PDS.lean#L75
-[PDS]: src/RandomSystems/PDS/PDS.lean#L174
+[Domain]: src/RandomSystems/PDS/PDS.lean#L76
+[PDS]: src/RandomSystems/PDS/PDS.lean#L186
 [IsRandomSystem]: src/RandomSystems/Cumulative/Cumulative.lean#L43
 [RandomSystem]: src/RandomSystems/Cumulative/Cumulative.lean#L57
 [RandomSystem.RepliesAtQueriedInterface]: src/RandomSystems/Cumulative/Cumulative.lean#L74

src/RandomSystems/PDS/PDS.lean

@@ -23,6 +23,7 @@ the samples replying `ys` to `xs`. Source: [1, Definition 8, p. 13].
 ## Main results
 
 * `nextReply_apply`, `nextReply_weight_of_admitted`: the next-reply masses of a mixture
+* `Domain.cutDomain_ofInputs`: a finite input-only cut is an intersection with a length bound
 * `hasDomain_ofInputs_iff`: on an input domain `E`, having domain `E` is `dom(s) = E`
 * `HasDomain.length_le`, `HasDomain.finite`: complete transcripts and DDS replies respect the bound
 
@@ -112,6 +113,17 @@ def Domain.ofInputs (E : List A → Prop) (bound : ℕ) (hE : ∀ h, E h → h.l
     (hE : ∀ h, E h → h.length ≤ bound) (h : List (A × B)) (x : A) :
     (Domain.ofInputs E bound hE : Domain A B) h x = E (h.map Prod.fst ++ [x]) := rfl
 
+/-- Cutting an input-only domain intersects its input histories with the finite horizon. -/
+lemma Domain.cutDomain_ofInputs
+    -- `E` admits input histories; `n` is the maximum number of queried inputs.
+    (E : List A → Prop) (n : ℕ) :
+    cutDomain (B := B) (fun h x => E (h.map Prod.fst ++ [x])) n =
+      Domain.ofInputs (fun xs => E xs ∧ xs.length ≤ n) n (fun _ hx => hx.2) := by
+  unfold cutDomain Domain.ofInputs
+  congr 1
+  funext h x
+  simp only [List.length_append, List.length_map, List.length_singleton, Nat.add_one_le_iff]
+
 /-- `s` has domain `D`: it answers exactly the queries `D` admits along its own
 transcripts. For a domain of input histories this is `dom(s) = D`
 [1, Definitions 5 and 8, pp. 11, 13]. -/

src/RandomSystems/README.md

@@ -38,7 +38,9 @@ Successive cuts combine by the minimum horizon; an explicit `Finite q s` certifi
 The normalization predicate `IsRandomSystem D p` also accepts a query domain `D` with no
 global horizon. [Finite cuts](Cumulative/FiniteCuts.lean) place such a behavior in the existing
 bounded carrier: `IsRandomSystem.cut D p hp q` preserves masses through depth `q` and sets later
-masses to zero. `RandomSystem.limitMass` reconstructs a behavior from adjacent coherent cuts;
+masses to zero. `Domain.cutDomain_ofInputs` identifies an input-only cut with its input
+histories intersected with the length bound. `RandomSystem.limitMass` reconstructs a behavior from
+adjacent coherent cuts;
 `limitMass_cut` and `cut_limitMass` give the two round trips.
 
 [Converter total-query bounds](Converter/QueryBound.lean) use `InsideQueriesBounded α k`
@@ -244,10 +246,10 @@ of the program's inside queries:
 [IsBisim]: System/Automaton.lean#L74
 [automatonSystem_eq_of_bisim]: System/Automaton.lean#L93
 [DDE]: System/DDE.lean#L30
-[Domain]: PDS/PDS.lean#L75
-[Equivalent]: PDS/PDS.lean#L60
-[HasDomain]: PDS/PDS.lean#L118
-[PDS]: PDS/PDS.lean#L174
+[Domain]: PDS/PDS.lean#L76
+[Equivalent]: PDS/PDS.lean#L61
+[HasDomain]: PDS/PDS.lean#L130
+[PDS]: PDS/PDS.lean#L186
 [IsRandomSystem]: Cumulative/Cumulative.lean#L43
 [RandomSystem]: Cumulative/Cumulative.lean#L57
 [PDS.behavior]: Cumulative/Cumulative.lean#L220

src/Tests/DeterministicFiniteCuts.lean

@@ -47,6 +47,38 @@ example : IsDDS (cutSystem echo.1 1) := echo.2.cutSystem 1
 example : HasDomain (cutDomain echoDomain 1) (cutSystem echo.1 1) :=
   echo_hasDomain.cutSystem 1
 
+/-- The cut of the existing echo has an input-only domain with the additional length bound. -/
+lemma echo_cut_input_domain (n : ℕ) :
+    HasDomain (Domain.ofInputs (fun xs : List Bool =>
+      (xs ≠ [] ∧ xs.length ≤ 3) ∧ xs.length ≤ n) n (fun _ hx => hx.2))
+      (cutSystem echo.1 n) := by
+  have cut := echo_hasDomain.cutSystem n
+  change HasDomain (cutDomain (fun h x =>
+    (h.map Prod.fst ++ [x]) ≠ [] ∧ (h.map Prod.fst ++ [x]).length ≤ 3) n) _ at cut
+  rw [Domain.cutDomain_ofInputs (fun xs : List Bool => xs ≠ [] ∧ xs.length ≤ 3)] at cut
+  exact cut
+
+/-- The positive cut keeps the same evaluator with its certified two-input domain. -/
+example : HasDomain (Domain.ofInputs (fun xs : List Bool =>
+    (xs ≠ [] ∧ xs.length ≤ 3) ∧ xs.length ≤ 2) 2 (fun _ hx => hx.2))
+    (cutSystem echo.1 2) := echo_cut_input_domain 2
+
+/-- The zero cut also has its exact input-only certificate. -/
+example : HasDomain (Domain.ofInputs (fun xs : List Bool =>
+    (xs ≠ [] ∧ xs.length ≤ 3) ∧ xs.length ≤ 0) 0 (fun _ hx => hx.2))
+    (cutSystem echo.1 0) := echo_cut_input_domain 0
+
+/-- No first query is admitted by the zero-horizon input-only presentation. -/
+lemma zero_input_domain :
+    ¬ (Domain.ofInputs (B := Bool) (fun xs : List Bool =>
+      (xs ≠ [] ∧ xs.length ≤ 3) ∧ xs.length ≤ 0) 0 (fun _ hx => hx.2)) [] false := by
+  rw [← Domain.cutDomain_ofInputs]
+  exact fun h => Nat.not_lt_zero _ h.2
+
+#print axioms SystemAlgebra.Domain.cutDomain_ofInputs
+#print axioms echo_cut_input_domain
+#print axioms zero_input_domain
+
 #print axioms SystemAlgebra.cutSystem_cutSystem
 #print axioms SystemAlgebra.HasDomain.cutSystem
 #print axioms SystemAlgebra.HasDomain.finite