Side-determinacy: myopia and unbounded circumambience

Locality predicates on string functions for the function-level subregular hierarchy. The kernel OutputDependsOn f i K says output coordinate i of f is fixed by the input positions in K. Two notions are instances:

• Myopia (the "no look-ahead" condition): a side's influence on the output is bounded.
• Unbounded circumambience: some target depends on input arbitrarily far on both sides at once.

Main definitions

• OutputDependsOn — output coord i determined by input positions in K.
• UnboundedDependence f s — for every distance d, some output flips under a perturbation strictly beyond d on side s.
• IsMyopicTowards f s — the negation: dependence on side s is bounded.
• IsUnboundedCircumambient — co-located form: for every d, ONE base word with a target that flips under both a far-left and a far-right perturbation.

Implementation notes

The predicates are distance-based (∀ d, ∃ word + target), not fixed-index. A fixed target index has only finitely many positions to its left, so a fixed-index "unbounded left dependence" is unsatisfiable; the unbounded distance must be witnessed by ever-longer words. The co-located IsUnboundedCircumambient keeps both perturbations on a single shared base, so any computing automaton hits one context where neither side alone fixes the output.

Circumambience is not the weak-determinism boundary: a map can be IsUnboundedCircumambient yet weakly deterministic (a two-sided union spread is perturbed at one output by either side, but neither side alone reverts it). The not-weakly-deterministic classification is driven by the strictly stronger RequiresBothSides (in Bimachine.lean), where perturbing either far side reverts the target to the identity.

def Subregular.OutputDependsOn {α : Type u_1} {β : Type u_2} (f : List α → List β) (i : ℕ) (K : Set ℕ) : Prop

Output coordinate i of f is determined by the input positions in K: equal-length inputs agreeing on K agree at output i. Monotone in K.

Equations

• Subregular.OutputDependsOn f i K = ∀ (u v : List α), u.length = v.length → (∀ (k : ℕ), k ∈ K → u[k]? = v[k]?) → (f u)[i]? = (f v)[i]?

theorem Subregular.OutputDependsOn.mono {α : Type u_1} {β : Type u_2} {f : List α → List β} {i : ℕ} {K K' : Set ℕ} (hKK' : K ⊆ K') (h : OutputDependsOn f i K) : OutputDependsOn f i K'

def Subregular.AgreeFrom {α : Type u_1} (u v : List α) (j : ℕ) : Prop

u and v agree at every index ≥ j.

Equations

• Subregular.AgreeFrom u v j = ∀ (k : ℕ), j ≤ k → u[k]? = v[k]?

def Subregular.AgreeUpto {α : Type u_1} (u v : List α) (j : ℕ) : Prop

u and v agree at every index ≤ j.

Equations

• Subregular.AgreeUpto u v j = ∀ (k : ℕ), k ≤ j → u[k]? = v[k]?

theorem Subregular.take_eq_of_agree {α : Type u_1} {u v : List α} {i : ℕ} (h : ∀ (k : ℕ), k < i → u[k]? = v[k]?) : List.take i u = List.take i v

Prefixes agreeing below i have equal i-truncations.

theorem Subregular.drop_eq_of_agree {α : Type u_1} {u v : List α} {i : ℕ} (h : ∀ (k : ℕ), i ≤ k → u[k]? = v[k]?) : List.drop i u = List.drop i v

Lists agreeing from i upward have equal i-suffixes.

theorem Subregular.AgreeUpto.take_eq {α : Type u_1} {u v : List α} {j : ℕ} (h : AgreeUpto u v j) {i : ℕ} (hij : i ≤ j + 1) : List.take i u = List.take i v

Agreement up to j transports truncations: h.take_eq for h : AgreeUpto u v j.

theorem Subregular.AgreeFrom.drop_eq {α : Type u_1} {u v : List α} {j : ℕ} (h : AgreeFrom u v j) {i : ℕ} (hij : j ≤ i) : List.drop i u = List.drop i v

Agreement from j transports suffixes: h.drop_eq for h : AgreeFrom u v j.

def Subregular.UnboundedDependence {α : Type u_1} {β : Type u_2} (f : List α → List β) : Direction → Prop

Unbounded dependence on side s: for every distance d, some target output position flips under a perturbation strictly beyond d on side s (the perturbed input agrees on the near window + the whole opposite side).

Equations

• One or more equations did not get rendered due to their size.

def Subregular.IsMyopicTowards {α : Type u_1} {β : Type u_2} (f : List α → List β) (s : Direction) : Prop

Myopia towards s: dependence on side s is bounded.

Equations

• Subregular.IsMyopicTowards f s = ¬Subregular.UnboundedDependence f s

def Subregular.IsFarPerturbation {α : Type u_1} (base u : List α) (i d : ℕ) (s : Direction) : Prop

An equal-length variant of base differing only beyond the d-margin of target i on side s — the far perturbation of the two-sided diagnostics.

Equations

• Subregular.IsFarPerturbation base u i d Subregular.Direction.left = (u.length = base.length ∧ Subregular.AgreeFrom base u (i - d))
• Subregular.IsFarPerturbation base u i d Subregular.Direction.right = (u.length = base.length ∧ Subregular.AgreeUpto base u (i + d))

def Subregular.IsUnboundedCircumambient {α : Type u_1} {β : Type u_2} (f : List α → List β) : Prop

Unbounded circumambience, co-located: for every d, one base word with a target i whose output flips under a far perturbation on either side. Co-location keeps both flips on a single base (one automaton context).

Equations

• One or more equations did not get rendered due to their size.

theorem Subregular.IsUnboundedCircumambient.left {α : Type u_1} {β : Type u_2} {f : List α → List β} (h : IsUnboundedCircumambient f) : UnboundedDependence f Direction.left

Co-located circumambience yields unbounded dependence on the left.

theorem Subregular.IsUnboundedCircumambient.right {α : Type u_1} {β : Type u_2} {f : List α → List β} (h : IsUnboundedCircumambient f) : UnboundedDependence f Direction.right

…and on the right.

theorem Subregular.IsUnboundedCircumambient.not_myopic {α : Type u_1} {β : Type u_2} {f : List α → List β} (h : IsUnboundedCircumambient f) (s : Direction) : ¬IsMyopicTowards f s

Circumambient ⟹ not myopic (either side): a real consequence, since circumambience exhibits unbounded dependence on each side.

@[simp]

theorem Subregular.not_isMyopicTowards_iff {α : Type u_1} {β : Type u_2} {f : List α → List β} {s : Direction} : ¬IsMyopicTowards f s ↔ UnboundedDependence f s

f is non-myopic towards s exactly when it has unbounded dependence there (IsMyopicTowards is by definition the negation of UnboundedDependence).

theorem Subregular.IsMyopicTowards.right_of_prefixDetermined {α : Type u_1} {β : Type u_2} {f : List α → List β} (h : ∀ (i : ℕ), OutputDependsOn f i {k : ℕ | k < i}) : IsMyopicTowards f Direction.right

Prefix-determined ⟹ right-myopic. A map each of whose output coordinates is fixed by the input's strict prefix ({k | k < i}) has no rightward look-ahead, so it is myopic towards the right. (The canonical left-to-right scan has this shape.)

def Subregular.LeftDetermined {α : Type u_1} {β : Type u_2} (f : List α → List β) (i : ℕ) : Prop

Output coordinate i is fixed by the prefix {k | k ≤ i} (the right side is irrelevant) — the footprint shape of a left-to-right transducer.

Equations

• Subregular.LeftDetermined f i = Subregular.OutputDependsOn f i {k : ℕ | k ≤ i}

theorem Subregular.IsMyopicTowards.right_of_leftDetermined {α : Type u_1} {β : Type u_2} {f : List α → List β} (h : ∀ (i : ℕ), LeftDetermined f i) : IsMyopicTowards f Direction.right

Left-determined everywhere ⟹ right-myopic. If every output coordinate is fixed by its prefix {k | k ≤ i}, the map has no rightward look-ahead.