fix(frontier): count branching-program resources faithfully

Complexity/Computability/Circuit/Frontier/BranchingProgram.lean

@@ -138,8 +138,11 @@ def Unambiguous : Prop :=
 def edges (t : ℕ) : Set (M × (P.newly t → U) × M) :=
   {e | P.Edge t e.1 e.2.1 e.2.2}
 
-/-- The *size* of the program: its number of edges. -/
-noncomputable def size : ℕ :=
+/-- The *size* of a program with finitely many edges at each used step: its number of edges.
+The ambient state type need not be finite. -/
+-- Finiteness restricts the public domain; ncard itself does not require it.
+@[nolint unusedArguments]
+noncomputable def size [∀ t : Fin P.length, Finite (P.edges t.val)] : ℕ :=
   ∑ t ∈ Finset.range P.length, (P.edges t).ncard
 
 /-- A coordinate read at step `s < t` was read before layer `t`. -/
@@ -225,10 +228,11 @@ theorem mem_peers_sweep {t : ℕ} {x y : ι → U} :
 /-! ### The rectangle bound -/
 
 /-- At every layer, the inputs sharing the state of an accepted input have fewer than `K`
-distinct parts on one side of the cut. -/
+distinct parts on one side of the cut. Extended cardinality ensures that an infinite side is
+never counted as small. -/
 def SmallSides (K : ℕ) : Prop :=
   ∀ t ≤ P.length, ∀ x ∈ P.accepted,
-    (P.sweep.pastSide t x).ncard < K ∨ (P.sweep.futureSide t x).ncard < K
+    (P.sweep.pastSide t x).encard < K ∨ (P.sweep.futureSide t x).encard < K
 
 /-- A rectangle-free accepted set has small sides. -/
 private theorem smallSides_of_rectangleFree {K : ℕ} (hS : RectangleFree P.accepted K) :
@@ -242,8 +246,10 @@ theorem SmallSides.one_lt [Finite ι] [Finite U] {K : ℕ} (hS : P.SmallSides K)
     (hne : P.accepted.Nonempty) : 1 < K := by
   obtain ⟨x, hx⟩ := hne
   rcases hS 0 (Nat.zero_le _) x hx with h | h
-  · exact (P.sweep.one_le_ncard_pastSide hx 0).trans_lt h
-  · exact (P.sweep.one_le_ncard_futureSide hx 0).trans_lt h
+  · exact (P.sweep.one_le_ncard_pastSide hx 0).trans_lt
+      (encard_lt_coe_iff_finite_ncard_lt.mp h).2
+  · exact (P.sweep.one_le_ncard_futureSide hx 0).trans_lt
+      (encard_lt_coe_iff_finite_ncard_lt.mp h).2
 
 /-- A program that accepts some input and has a step has an edge. -/
 theorem one_le_size [Finite ι] [Finite U] [Finite M] (hL : 0 < P.length)
@@ -277,7 +283,10 @@ theorem ncard_accepted_le_of_smallSides [Finite ι] [Finite U] [Finite M] (hL :
   have hK1 := hS.one_lt hne
   by_cases hK : K ≤ P.accepted.ncard
   · calc P.accepted.ncard ≤ (K - 1) * (K - 1) * P.sweep.transitionCount :=
-          P.sweep.ncard_le_mul_transitionCount hK1 hK hS
+          P.sweep.ncard_le_mul_transitionCount hK1 hK fun t ht x hx =>
+            (hS t ht x hx).imp
+              (fun h => (encard_lt_coe_iff_finite_ncard_lt.mp h).2)
+              (fun h => (encard_lt_coe_iff_finite_ncard_lt.mp h).2)
       _ ≤ (K - 1) ^ 2 * P.size := by
           rw [sq]
           exact Nat.mul_le_mul_left _ P.transitionCount_sweep_le_size
@@ -414,8 +423,9 @@ theorem abs_signedCount_accepted_le [Finite ι] [Finite U] [Finite M] (hP : P.Un
     · push Not at hthick
       have hsmall : P.SmallSides K := fun t ht x hx => by
         by_cases hA : K ≤ (P.sweep.pastSide t x).ncard
-        · exact Or.inr (hthick t ht x hx hA)
-        · exact Or.inl (not_le.mp hA)
+        · exact Or.inr (encard_lt_coe_iff_finite_ncard_lt.mpr
+            ⟨toFinite _, hthick t ht x hx hA⟩)
+        · exact Or.inl (encard_lt_coe_iff_finite_ncard_lt.mpr ⟨toFinite _, not_le.mp hA⟩)
       have hcount : (P.accepted.ncard : ℝ) ≤ ((K - 1) ^ 2 * P.size : ℕ) := by
         exact_mod_cast P.ncard_accepted_le_of_smallSides hL hsmall
       linarith [abs_signedCount_le S P.accepted,

Complexity/Computability/Circuit/Frontier/Sweep.lean

@@ -143,8 +143,8 @@ def futureSide (t : ℕ) (x : ι → U) : Set (↥(P.revealed t)ᶜ → U) :=
 /-- The rectangular hull of the peers of `x` lies inside `S`, so in a rectangle-free set one of
 its sides is small. -/
 theorem pastSide_lt_or_futureSide_lt {K : ℕ} (hS : RectangleFree S K) (t : ℕ) (x : ι → U) :
-    (P.pastSide t x).ncard < K ∨ (P.futureSide t x).ncard < K := by
-  refine hS.ncard_lt_or _ _ _ fun z ⟨⟨y, ⟨hy, hyx⟩, hzy⟩, ⟨y', ⟨hy', hy'x⟩, hzy'⟩⟩ => ?_
+    (P.pastSide t x).encard < K ∨ (P.futureSide t x).encard < K := by
+  refine hS _ _ _ fun z ⟨⟨y, ⟨hy, hyx⟩, hzy⟩, ⟨y', ⟨hy', hy'x⟩, hzy'⟩⟩ => ?_
   exact P.splice t y hy y' hy' (hyx.trans hy'x.symm) z
     (domRestrict_eq_domRestrict_iff.mp hzy).symm (domRestrict_eq_domRestrict_iff.mp hzy').symm
 
@@ -262,7 +262,9 @@ theorem ncard_le [Finite ι] [Finite U] {K : ℕ} (hS : RectangleFree S K) (hK :
   rcases S.eq_empty_or_nonempty with rfl | hne
   · simp
   simpa only [sq] using P.ncard_le_mul_transitionCount (hS.one_lt hne) hK
-    fun t _ x _ => P.pastSide_lt_or_futureSide_lt hS t x
+    fun t _ x _ => (P.pastSide_lt_or_futureSide_lt hS t x).imp
+      (fun h => (encard_lt_coe_iff_finite_ncard_lt.mp h).2)
+      (fun h => (encard_lt_coe_iff_finite_ncard_lt.mp h).2)
 
 end Sweep
 

ComplexityTests/FrontierBranchingProgramCard.lean

@@ -0,0 +1,220 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+import Complexity.Computability.Circuit.Frontier.BranchingProgram
+
+/-! Regressions for the infinite-cardinality examples reported in #1717. -/
+
+open Cslib.Circuits.Frontier Set
+
+namespace ComplexityTests.FrontierBranchingProgramCard
+
+/-- One step reads the only coordinate; the edge condition ignores its label. -/
+private def oneStep (U M : Type) (s : M) (edge : M → M → Prop) : ReadOnceNBP Unit U M where
+  length := 1
+  revealed t := if t = 0 then ∅ else univ
+  revealed_zero := by simp
+  revealed_length := by simp
+  revealed_mono := by
+    intro a b hab
+    by_cases ha : a = 0
+    · simp [ha]
+    · have hb : b ≠ 0 := by omega
+      simp [ha, hb]
+  start := s
+  accept := s
+  Edge _ m _ m' := edge m m'
+
+private theorem oneStep_accepted (U M : Type) (s : M) (edge : M → M → Prop)
+    (h : edge s s) : (oneStep U M s edge).accepted = univ := by
+  ext x
+  constructor
+  · intro _
+    trivial
+  · intro _
+    exact ⟨fun _ => s, rfl, rfl, fun _ _ => h⟩
+
+-- Only layers 0 and 1 count when comparing accepting paths.
+private theorem oneStep_unambiguous (U M : Type) (s : M) (edge : M → M → Prop) :
+    (oneStep U M s edge).Unambiguous := by
+  intro x γ δ hγ hδ t ht
+  have h : t = 0 ∨ t = 1 := by
+    change t ≤ 1 at ht
+    omega
+  rcases h with rfl | rfl
+  · exact hγ.start.trans hδ.start.symm
+  · exact hγ.accept.trans hδ.accept.symm
+
+private def allEdges : ReadOnceNBP Unit Bool ℕ :=
+  oneStep Bool ℕ 0 fun _ _ => True
+
+example : allEdges.accepted = univ := oneStep_accepted _ _ _ _ trivial
+
+example : allEdges.Unambiguous := oneStep_unambiguous _ _ _ _
+
+private theorem allEdges_infinite : (allEdges.edges 0).Infinite := by
+  have h : allEdges.edges 0 = univ := by ext e; rfl
+  rw [h]
+  exact infinite_univ
+
+-- The underlying natural set cardinality is zero, but the public size API is unavailable.
+example : (allEdges.edges 0).ncard = 0 := allEdges_infinite.ncard
+
+example : True := by
+  fail_if_success have : ℕ := allEdges.size
+  trivial
+
+/-- Two useful self-loop edges, with states still in the infinite ambient type ℕ. -/
+private def twoLoops : ReadOnceNBP Unit Bool ℕ :=
+  oneStep Bool ℕ 0 fun m m' => m = 0 ∧ m' = 0
+
+private def loopCoordinate : twoLoops.newly 0 :=
+  ⟨(), by simp [ReadOnceNBP.newly, twoLoops, oneStep]⟩
+
+private def loopEdge (b : Bool) : ℕ × (twoLoops.newly 0 → Bool) × ℕ :=
+  (0, fun _ => b, 0)
+
+private theorem loopEdge_injective : Function.Injective loopEdge := by
+  intro a b h
+  exact congrArg (fun e => e.2.1 loopCoordinate) h
+
+private theorem twoLoops_edges : twoLoops.edges 0 = range loopEdge := by
+  ext ⟨m, a, m'⟩
+  change (m = 0 ∧ m' = 0) ↔ ∃ b, loopEdge b = (m, a, m')
+  constructor
+  · rintro ⟨rfl, rfl⟩
+    refine ⟨a loopCoordinate, Prod.ext rfl (Prod.ext ?_ rfl)⟩
+    funext i
+    exact congrArg a (Subsingleton.elim loopCoordinate i)
+  · rintro ⟨b, h⟩
+    exact ⟨(congrArg Prod.fst h).symm, (congrArg (fun e => e.2.2) h).symm⟩
+
+private instance twoLoops_finite (t : Fin twoLoops.length) : Finite (twoLoops.edges t.val) := by
+  have ht : t.val = 0 := by
+    have := t.isLt
+    change t.val < 1 at this
+    omega
+  have h : (twoLoops.edges t.val).Finite := by
+    rw [ht, twoLoops_edges]
+    exact finite_range loopEdge
+  exact h.to_subtype
+
+example : twoLoops.accepted = univ := oneStep_accepted _ _ _ _ ⟨rfl, rfl⟩
+
+example : twoLoops.Unambiguous := oneStep_unambiguous _ _ _ _
+
+example : twoLoops.size = 2 := by
+  rw [ReadOnceNBP.size]
+  change ∑ t ∈ Finset.range 1, (twoLoops.edges t).ncard = 2
+  rw [Finset.sum_range_one, twoLoops_edges, ncard_range_of_injective loopEdge_injective]
+  simp [Nat.card_eq_fintype_card]
+
+-- Adding every edge contains both useful loops, but cannot supply a finite size of zero.
+example (t : ℕ) (m m' : ℕ) (a : twoLoops.newly t → Bool) :
+    twoLoops.Edge t m a m' → allEdges.Edge t m a m' := fun _ => trivial
+
+/-- Infinite alphabet, one state, and every input accepted. -/
+private def natInputs : ReadOnceNBP Unit ℕ Unit :=
+  oneStep ℕ Unit () fun _ _ => True
+
+private theorem natInputs_accepted : natInputs.accepted = univ :=
+  oneStep_accepted _ _ _ _ trivial
+
+example : natInputs.Unambiguous := oneStep_unambiguous _ _ _ _
+
+private theorem natInputs_peers (t : ℕ) (x : Unit → ℕ) : natInputs.sweep.peers t x = univ := by
+  ext y
+  rw [ReadOnceNBP.mem_peers_sweep, natInputs_accepted]
+  simp
+
+private theorem natInputs_future_infinite (x : Unit → ℕ) :
+    (natInputs.sweep.futureSide 0 x).Infinite := by
+  let i₀ : ↥(natInputs.revealed 0)ᶜ := ⟨(), by simp [natInputs, oneStep]⟩
+  refine infinite_of_injective_forall_mem
+    (f := fun n : ℕ => fun _ : ↥(natInputs.revealed 0)ᶜ => n) ?_ ?_
+  · intro m n h
+    exact congrFun h i₀
+  · intro n
+    exact ⟨fun _ => n, by rw [natInputs_peers]; trivial, rfl⟩
+
+private theorem natInputs_past_infinite (x : Unit → ℕ) :
+    (natInputs.sweep.pastSide 1 x).Infinite := by
+  let i₁ : natInputs.revealed 1 := ⟨(), by simp [natInputs, oneStep]⟩
+  refine infinite_of_injective_forall_mem
+    (f := fun n : ℕ => fun _ : natInputs.revealed 1 => n) ?_ ?_
+  · intro m n h
+    exact congrFun h i₁
+  · intro n
+    exact ⟨fun _ => n, by rw [natInputs_peers]; trivial, rfl⟩
+
+private theorem natInputs_past_zero (x : Unit → ℕ) :
+    natInputs.sweep.pastSide 0 x = {fun _ => 0} := by
+  ext a
+  constructor
+  · intro _
+    refine mem_singleton_iff.mpr (funext fun i => ?_)
+    exact False.elim (by simpa [ReadOnceNBP.sweep, natInputs, oneStep] using i.property)
+  · intro ha
+    obtain rfl := mem_singleton_iff.mp ha
+    exact ⟨fun _ => 0, by rw [natInputs_peers]; trivial, rfl⟩
+
+private theorem natInputs_future_one (x : Unit → ℕ) :
+    natInputs.sweep.futureSide 1 x = {fun _ => 0} := by
+  ext a
+  constructor
+  · intro _
+    refine mem_singleton_iff.mpr (funext fun i => ?_)
+    exact False.elim (by simpa [ReadOnceNBP.sweep, natInputs, oneStep] using i.property)
+  · intro ha
+    obtain rfl := mem_singleton_iff.mp ha
+    exact ⟨fun _ => 0, by rw [natInputs_peers]; trivial, rfl⟩
+
+example : (natInputs.sweep.futureSide 0 (fun _ => 0)).encard = ⊤ :=
+  encard_eq_top_iff.mpr (natInputs_future_infinite _)
+
+example : (natInputs.sweep.pastSide 1 (fun _ => 0)).encard = ⊤ :=
+  encard_eq_top_iff.mpr (natInputs_past_infinite _)
+
+-- This is the erroneous old natural-cardinality condition, reconstructed explicitly.
+example : ∀ t ≤ natInputs.length, ∀ x ∈ natInputs.accepted,
+    (natInputs.sweep.pastSide t x).ncard < 1 ∨
+      (natInputs.sweep.futureSide t x).ncard < 1 := by
+  intro t ht x _
+  have h : t = 0 ∨ t = 1 := by
+    change t ≤ 1 at ht
+    omega
+  rcases h with rfl | rfl
+  · right
+    rw [(natInputs_future_infinite x).ncard]
+    decide
+  · left
+    rw [(natInputs_past_infinite x).ncard]
+    decide
+
+example : ¬natInputs.SmallSides 1 := by
+  intro h
+  have hx : (fun _ => 0) ∈ natInputs.accepted := by rw [natInputs_accepted]; trivial
+  rcases h 0 (Nat.zero_le _) _ hx with hpast | hfuture
+  · rw [natInputs_past_zero, encard_singleton] at hpast
+    norm_num at hpast
+  · rw [encard_eq_top_iff.mpr (natInputs_future_infinite _)] at hfuture
+    exact (not_lt_of_ge le_top) hfuture
+
+-- One singleton side suffices at each boundary; the other side may remain infinite.
+example : natInputs.SmallSides 2 := by
+  intro t ht x _
+  have h : t = 0 ∨ t = 1 := by
+    change t ≤ 1 at ht
+    omega
+  rcases h with rfl | rfl
+  · left
+    rw [natInputs_past_zero, encard_singleton]
+    norm_num
+  · right
+    rw [natInputs_future_one, encard_singleton]
+    norm_num
+
+end ComplexityTests.FrontierBranchingProgramCard