Preserve attachment observations under sufficient inside cuts

REUSE.md

@@ -40,6 +40,7 @@ are in `SystemAlgebra`. The probability operations below are in `Probability.Dis
 | Retained state with fresh transitions | `TypedSystem.ofProbAutomaton` in [ProbAutomaton] |
 | Retained key as an automaton | `TypedSystem.ofProbAutomaton_eq_keyed` in [KeyedAutomaton] |
 | Program attachment | `TypedConverter.ofProgram_smul_ofProbAutomaton` in [ProgramAttachment] |
+| Sufficient inside horizon | `replies_apply_cutSystem_iff` in [inside cuts] |
 | Independent joint law | `prodProbDist` in [Distribution] |
 | Selected independent coordinates | `ProbDist.map_pi_comp` in [Kernel] |
 | Independent finite family of draws | `ProbDist.pi` in [Distribution] |
@@ -62,6 +63,7 @@ are in `SystemAlgebra`. The probability operations below are in `Probability.Dis
 
 [UnlimitedSource]: src/RandomSystems/System/Source.lean
 [SourceCuts]: src/RandomSystems/Typed/SourceCuts.lean
+[inside cuts]: src/RandomSystems/Converter/InsideCuts.lean
 [converter cuts]: src/RandomSystems/Converter/FiniteCuts.lean
 [query bounds]: src/RandomSystems/Converter/QueryBound.lean
 [parallel cuts]: src/RandomSystems/Cumulative/Parallel.lean

src/RandomSystems.lean

@@ -33,6 +33,7 @@ public import RandomSystems.Converter.ResourceCanon
 public import RandomSystems.Converter.SerialAccounting
 public import RandomSystems.Converter.QueryBound
 public import RandomSystems.Converter.FiniteCuts
+public import RandomSystems.Converter.InsideCuts
 public import RandomSystems.Converter.QueryRouting
 public import RandomSystems.Cumulative.ConnectionObservation
 public import RandomSystems.Cumulative.Cumulative

src/RandomSystems/Converter/InsideCuts.lean

@@ -0,0 +1,81 @@
+module
+
+public import RandomSystems.Converter.QueryBound
+public import RandomSystems.PDS.FiniteCuts
+
+/-!
+# Attachment through a sufficient inside horizon
+
+`IsDDCFrom.replies_apply_cutSystem_iff` preserves completed outside replies through horizon
+`q` when the resource is cut at the total inside-query bound `k q`.
+`IsDDCFrom.cutSystem_trim_apply_cutSystem` packages this agreement as equality of canonical
+outside cuts. The completed attachment history supplies the resource prefixes used by the
+converter.
+-/
+
+@[expose] public section
+
+namespace SystemAlgebra
+
+-- Outside ports `O` expose `U`/`V`; inside ports `J` expose `X`/`Y`.
+variable {O J : Type} {U V : O → Type} {X Y : J → Type}
+-- `E` and `F` admit inside and outside input histories, respectively.
+variable {E : List (Σ j, X j) → Prop} {F : List (Σ o, U o) → Prop}
+variable {b : ℕ} {α : InsideOutsideSystem O J U V X Y} {R : InterfaceSystem J X Y}
+
+/-- An inside cut at the total-query bound preserves every completed outside transcript. -/
+lemma IsDDCFrom.replies_apply_cutSystem_iff
+    (ha : IsDDCFrom E F b α)
+    -- `hk` counts all inside queries; `mono` permits increasing the outside horizon.
+    {k : ℕ → ℕ} (hk : InsideQueriesBounded α k) (mono : Monotone k)
+    -- `hR` preserves reply ports, and `hRE` specifies the resource's exact input domain.
+    (hR : RepliesAtQueriedInterface R) (hRE : ∀ xs, (R xs).Dom ↔ E xs)
+    {q : ℕ} {xs : List (Σ o, U o)} {ys : List (Σ o, V o)} (hq : xs.length ≤ q) :
+    Replies (apply α (cutSystem R (k q))) xs ys ↔ Replies (apply α R) xs ys := by
+  constructor
+  · intro hr
+    rw [apply_eq] at hr ⊢
+    exact hr.interconnect_mono (pair_mono (fun _ _ hy => hy)
+      (fun xs y hy => (filterDom_mem_iff _ R xs y).mp hy |>.2))
+  · intro hr
+    obtain ⟨H, hi, T, hT, replies, hQ, _⟩ := ha.attach_idle hR hRE xs ys hr
+    -- The converter's outside inputs are exactly the observed input history.
+    have outside : outsideInputs (T.map Prod.fst) = xs := by
+      rw [← hT]
+      exact hi.outsideInputs_resource
+    -- Its retained resource history is bounded by the same completed transcript.
+    have length : (restrict (some ()) H).length ≤ k q := by
+      rw [hQ]
+      exact (hk T replies).trans (by rw [outside]; exact mono hq)
+    have same : ∀ p, p <+: restrict (some ()) H → R p = cutSystem R (k q) p := by
+      intro p hp
+      exact (cutSystem_apply_of_length_le R _ p (hp.length_le.trans length)).symm
+    have prefixes := hi.interconnect_eq_on_prefixes (pair_eq_on_prefixes_right α same)
+    rw [apply_eq] at hr ⊢
+    exact (replies_congr_of_prefix prefixes ys).mp hr
+
+/-- Canonical outside cuts agree when the inside horizon covers every possible query. -/
+lemma IsDDCFrom.cutSystem_trim_apply_cutSystem
+    (ha : IsDDCFrom E F b α) {k : ℕ → ℕ}
+    (hk : InsideQueriesBounded α k) (mono : Monotone k)
+    (hR : RepliesAtQueriedInterface R) (hRE : ∀ xs, (R xs).Dom ↔ E xs) (q : ℕ) :
+    cutSystem (trim (apply α (cutSystem R (k q)))) q =
+      cutSystem (trim (apply α R)) q := by
+  have canonical (S : InterfaceSystem J X Y) : IsDDS (trim (apply α S)) :=
+    SilentAtEmpty.isDDS_trim (by
+      simp only [SilentAtEmpty, apply_eq, interconnect_nil, Part.not_none_dom, not_false_eq_true])
+  apply IsDDS.eq_of_replies_iff ((canonical _).cutSystem q) ((canonical _).cutSystem q)
+  intro xs ys
+  by_cases hq : xs.length ≤ q
+  · rw [replies_cutSystem_iff _ q hq, replies_cutSystem_iff _ q hq,
+      replies_trim_iff, replies_trim_iff]
+    exact ha.replies_apply_cutSystem_iff hk mono hR hRE hq
+  · have hn : xs ≠ [] := by intro he; subst xs; exact hq (Nat.zero_le q)
+    have absent (s : System (Σ o, U o) (Σ o, V o)) : ¬ Replies (cutSystem s q) xs ys := by
+      intro hr
+      have hd := hr.dom hn
+      rw [cutSystem_apply_of_bound_lt s q xs (Nat.lt_of_not_ge hq)] at hd
+      exact hd
+    exact iff_of_false (absent _) (absent _)
+
+end SystemAlgebra

src/RandomSystems/Converter/ResourceAttachment.lean

@@ -31,7 +31,6 @@ Definition 3.9 (printed p. 62).
 
 namespace SystemAlgebra
 
-open Classical
 
 variable {O M J : Type} {U V : O → Type} {Xm Ym : M → Type} {X Y : J → Type}
 
@@ -55,7 +54,8 @@ def allOutsideOutput :
   | ⟨⟨⟨some (), j⟩, h⟩, _⟩ => False.elim (h ⟨j, rfl⟩)
 
 /-- The system obtained by attaching all the converter's inside interfaces. -/
-noncomputable def apply (α : InsideOutsideSystem O J U V X Y) (R : InterfaceSystem J X Y) : InterfaceSystem O U V :=
+noncomputable def apply (α : InsideOutsideSystem O J U V X Y) (R : InterfaceSystem J X Y) :
+    InterfaceSystem O U V :=
   relabel (attachAlong id α R) allOutsideInput allOutsideOutput
 
 lemma apply_eq (α : InsideOutsideSystem O J U V X Y) (R : InterfaceSystem J X Y) :
@@ -271,7 +271,8 @@ lemma apply_forwardAll {R : InterfaceSystem J X Y} (hR : SilentAtEmpty R) :
   · rintro ⟨j, y⟩; exact Or.inr ⟨_, rfl, rfl⟩
 
 /-- Identity on a partial responding DDS, with its domain unchanged. -/
-lemma trim_apply_id {R : InterfaceSystem J X Y} (hR : IsDDS R) (hresp : RepliesAtQueriedInterface R) :
+lemma trim_apply_id {R : InterfaceSystem J X Y} (hR : IsDDS R)
+    (hresp : RepliesAtQueriedInterface R) :
     trim (apply (idConverter J X Y) R) = R := by
   apply IsDDS.eq_of_replies_iff
     (SilentAtEmpty.isDDS_trim (s := apply (idConverter J X Y) R)
@@ -282,7 +283,8 @@ lemma trim_apply_id {R : InterfaceSystem J X Y} (hR : IsDDS R) (hresp : RepliesA
   · intro hr
     rw [apply_eq] at hr
     have ht := hr.interconnect_mono (pair_mono (fun _ _ h => canon_mem h) (fun _ _ h => h))
-    change Replies (interconnect (pair (forwardAll J X Y) R) resourceRoute resourceInput) xs ys at ht
+    change Replies (interconnect (pair (forwardAll J X Y) R)
+      resourceRoute resourceInput) xs ys at ht
     rwa [← apply_eq, apply_forwardAll hR.1] at ht
   · exact replies_apply_id hresp
 
@@ -342,6 +344,19 @@ lemma pair_eq_on_prefixes_left {A B C D : Type} {s t : System A B} (R : System C
     rw [pair_left, pair_left, he _ hp]
   · simp only [List.concat_eq_append, pair_right]
 
+/-- The right component is read only at prefixes of its own retained history. -/
+lemma pair_eq_on_prefixes_right {A B C D : Type} (α : System A B) {R S : System C D}
+    {H : List (Two A C)} (he : ∀ p, p <+: restrict (some ()) H → R p = S p) :
+    ∀ G, G <+: H → pair α R G = pair α S G := by
+  intro G hG
+  rcases List.eq_nil_or_concat G with rfl | ⟨G, ⟨_ | ⟨⟨⟩⟩, x⟩, rfl⟩
+  · rfl
+  · simp only [List.concat_eq_append, pair_left]
+  · simp only [List.concat_eq_append] at hG ⊢
+    have hp := restrict_prefix (some ()) hG
+    simp only [restrict_some_snoc_right] at hp
+    rw [pair_right, pair_right, he _ hp]
+
 /-- Domain preservation depends only on finite converter behavior. This is
 the closure principle used when lifting to fresh converters. -/
 lemma IsResponsiveDDC.mapsDomain_of_replies {E : List (Σ j, X j) → Prop}

src/RandomSystems/README.md

@@ -48,6 +48,8 @@ preservation is supplied separately by `IsDDCFrom.mapsDomain`.
 [Finite converter cuts](Converter/FiniteCuts.lean) intersect the original outside domain with
 the observation horizon and the inside domain with its total-query allowance.
 `IsDDCFrom.filterDom_of_insideQueriesBounded` supplies this exact certificate.
+[Inside cuts](Converter/InsideCuts.lean) preserve completed attachment replies through `q`
+when the resource is cut at `k q`; the canonical outside cuts are equal.
 
 [Independent parallel behaviors](Cumulative/Parallel.lean) multiply the masses of their
 projected transcripts. `parallelMass_isRandomSystem` retains matching query/reply tags and

src/Tests.lean

@@ -64,6 +64,7 @@ public import Tests.SamplingAlgebra
 public import Tests.SerialAccounting
 public import Tests.ConverterQueryBound
 public import Tests.ConverterFiniteCuts
+public import Tests.AttachmentInsideCuts
 public import Tests.SharedRouting
 public import Tests.Substitution.Axioms
 public import Tests.Substitution.Calculation

src/Tests/AttachmentInsideCuts.lean

@@ -0,0 +1,64 @@
+module
+
+public import RandomSystems.Converter.InsideCuts
+public import Tests.DirectCalls
+
+/-! A sufficient inside cut preserves forwarding and two-query calls, including horizon zero. -/
+
+@[expose] public section
+
+namespace SystemAlgebra.Tests.AttachmentInsideCuts
+
+open DirectCalls
+
+/-- The existing function evaluator echoes Boolean queries through horizon `n`. -/
+noncomputable abbrev echo (n : ℕ) :=
+  DDS.ofFunction (boolInterface n).domain (boolInterface n).nonempty_prefix id
+
+/-- A single Unit port makes every reply stay at the queried interface. -/
+lemma echo_ports (n : ℕ) : RepliesAtQueriedInterface (echo n).1 := by
+  intro h x y hr
+  exact Subsingleton.elim _ _
+
+/-- Forwarding through one query agrees after cutting a three-query resource at one. -/
+lemma forwarding_one :
+    let E := (boolInterface 3).domain
+    let α := (DDC.filter (Y := fun _ : Unit => Bool) (fun h => h = [] ∨ E h)
+      (prefix_or_nil (boolInterface 3).nonempty_prefix.2)).1
+    cutSystem (trim (apply α (cutSystem (echo 3).1 1))) 1 =
+      cutSystem (trim (apply α (echo 3).1)) 1 := by
+  have ha := isDDCFrom_filter (Y := fun _ : Unit => Bool) (boolInterface 3).nonempty_prefix
+  exact ha.cutSystem_trim_apply_cutSystem
+    (insideQueriesBounded_id.of_le
+      (fun xs y hy => (filterDom_mem_iff _ _ xs y).mp hy |>.2)) monotone_id
+    (echo_ports 3) (DDS.ofFunction_dom _ _ _) 1
+
+/-- The interior cut genuinely removes the evaluator's second reply. -/
+lemma cut_removes_second :
+    cutSystem (echo 3).1 1 [⟨(), false⟩, ⟨(), true⟩] = Part.none ∧
+      (echo 3).1 [⟨(), false⟩, ⟨(), true⟩] = Part.some ⟨(), true⟩ := by
+  constructor
+  · exact cutSystem_apply_of_bound_lt _ _ _ (Nat.lt_succ_self 1)
+  · change (echo 3).1 ([⟨(), false⟩] ++ [⟨(), true⟩]) = Part.some ⟨(), true⟩
+    rw [DDS.ofFunction_snoc, ite_eq_left ⟨List.cons_ne_nil _ _, Nat.le_succ 2⟩]
+    rfl
+
+/-- The existing toggle call has the same canonical outside cut at every horizon, including zero. -/
+lemma toggle_cut (q : ℕ) :
+    let α := callConverter (V := fun _ => Bool) (Y := fun _ => Bool) toggleCall
+      (boolInterface 1).domain
+    cutSystem (trim (apply α (cutSystem (echo 2).1 2))) q =
+      cutSystem (trim (apply α (echo 2).1)) q :=
+  toggleCall_isDDCFrom.cutSystem_trim_apply_cutSystem
+    (toggleCall_isDDCFrom.insideQueriesBounded_of_domain (fun _ hx => hx.2))
+    monotone_const (echo_ports 2) (DDS.ofFunction_dom _ _ _) q
+
+example := toggle_cut 0
+
+#print axioms SystemAlgebra.pair_eq_on_prefixes_right
+#print axioms SystemAlgebra.IsDDCFrom.replies_apply_cutSystem_iff
+#print axioms SystemAlgebra.IsDDCFrom.cutSystem_trim_apply_cutSystem
+#print axioms forwarding_one
+#print axioms toggle_cut
+
+end SystemAlgebra.Tests.AttachmentInsideCuts