Strict Anchored Boundary
Abstract
Strict supplied append and credit-limited deletion identify the anchored residual boundary of a finite relation.
Theorem 1.1 (Strict anchored specialization).
Proof. Machine-checked in Lean as D5/S3/ObserverMemory/StrictAnchoredBoundary.strict_anchored_specialization (✓ std3). ∎
Source. Repository-derived.
Commentary.
Fix an arbitrary finite nonempty alphabet A, a natural n, and a nonempty relation C of words of length n. At any admissible public type (k,d), a state is the unique decomposition u=vt with |v|=k-d and |t|=d. The carrier stores this decomposition of the actual controlled prefix, with a completion in the same C; it carries no immutable completed word. The root output is (|v|+|t|,|t|).
The common actions append a and delete a are strict Option transitions. Append requires k<n and an actual completion of vta. With an empty tail it replaces the anchor by va; with tail cw it replaces the anchor by vc and the tail by wa. Delete requires that the tail ends in the supplied a and removes it, leaving the anchor fixed. An empty tail or a mismatching supplied symbol has no edge. Successful labels are the supplied actions, and the public types are (k+1,d) and (k-1,d-1). There is no failure output or enabled-action sensor; deletion can expose a prefix with a different completion in C.
The boundary is (R(v),t), with R(v)={f: vf belongs to C}. The first theorem clause is the exact Option-map equation for public type and boundary. Its explicit boundaryStep gives append guard k<n and a nonempty derivative at ta, the two moving-anchor derivative updates, and the strict delete update (S,wa) to (S,w). These equations apply to every finite action interleaving, with undefined transitions retained as missing edges.
The converse is operational: reverse supplied deletions of z with |z|=|t| are legal exactly when z=t, and end at (v,empty). From there, appending a full-length f is legal exactly when vf belongs to C. These action words separate unequal tails or unequal anchor residuals on actual prefixes.
The image is the actual joint range, exactly pairs (S,t) with S an actual anchor residual at k-d, |t|=d, and a nonempty derivative of S at t. The image is in bijection with the dependent disjoint union of these tail fibers, so N is the sum over distinct actual S of |Pref_d(S)|. This is a joint image, with no independent product assumption.
Exact representations preserve strict domains and successor public types and representation values on actual states. An arbitrary family at public types can be represented in a common tagged carrier; only the image at the chosen type is counted. Equality of exact representation values implies equal legal languages by induction and hence equal boundaries. The realized-image factorization applies to this kernel inclusion. Commutation forces onto-ness and uniqueness, and the finite surjection cardinal theorem gives the lower bound N. The boundary’s strict transition equation attains this conditional state capacity.
All hypotheses and quantifiers include n=0, d=0, d=k, k=n, and singleton relations without special exclusions. The count describes internal labels at a supplied public type. Counting multiple public types requires their disjoint union. Binary encodings, when used, are the standard fixed-length finite-capacity encoding of N labels; the theorem assigns no cost to the relation description, transition table, computation, initialization, physical memory or past archive. An accessible extra source record must be part of the represented joint carrier.
In the displayed statement, mapTypeBoundary maps a successful state r to (publicType(r),boundary(C,r)) and preserves none. Subtype arguments denote their underlying states, and actual-image maps use the canonical range inclusions. card is finite cardinality; sum uses the indicated finite enumeration I. The factor equation is the pointwise form of equality between the two canonical range factorizations.