FPRD accessible-field sewing: working theorem draft

Status. Working proof, not yet repository evidence. No novelty claim. The fixed-cut cone theorem has passed an internal independent audit; its prior-art comparator is still running. Nothing here depends on the pending folding re-audit.

Contents

1. Why another sewing theorem is needed

For a finite-output target f:Σ∗→Bf:\Sigma^*\to B, write

Bi,N(u)=(f(uv))v∈Σ≤N,u∈Σi. B_{i,N}(u)=\bigl(f(uv)\bigr)_{v\in\Sigma^{\le N}}, \qquad u\in\Sigma^i .

The fixed-cut cone theorem answers an offline question: after one selected prefix has already been read, how many complete snapshots are needed if kk old-input tracks are supplied at positions chosen for that cut?

That theorem does not answer whether the supplied snapshots and positions can be produced by one online machine. There are three distinct levels:

  1. target compatibility: the cut tables describe one target;
  2. semantic quotient compatibility: named cut partitions form one horizon/grade grid over the target residuals;
  3. operational accessibility: one stationary local rule reaches the witnesses in that grid from one initial configuration.

The first two levels can hold while the third fails.

2. Pure semantic quotient sewing

Let

πi,N:Σi↠Ai,N \pi_{i,N}:\Sigma^i\twoheadrightarrow A_{i,N}

be a named finite partition. Say it is resolving when

ker⁡πi,N⊆ker⁡Bi,N.(R) \ker\pi_{i,N}\subseteq\ker B_{i,N}. \tag{R}

Then there is a unique surjection

hi,N:Ai,N↠Ri,N,hi,Nπi,N=Bi,N,(1) h_{i,N}:A_{i,N}\twoheadrightarrow R_{i,N}, \qquad h_{i,N}\pi_{i,N}=B_{i,N}, \tag{1}

where Ri,N=Bi,N(Σi)R_{i,N}=B_{i,N}(\Sigma^i) is the canonical M26 bounded residual cell.

Theorem A — named quotient-grid criterion

The resolving partitions assemble into a quotient grid over the M26 residual grid if and only if they satisfy:

ker⁡πi,N+1⊆ker⁡πi,N(H) \ker\pi_{i,N+1}\subseteq\ker\pi_{i,N} \tag{H}

and, for every a∈Σa\in\Sigma,

πi,N+1(u)=πi,N+1(u′)⟹πi+1,N(ua)=πi+1,N(u′a).(D) \pi_{i,N+1}(u)=\pi_{i,N+1}(u') \Longrightarrow \pi_{i+1,N}(ua)=\pi_{i+1,N}(u'a). \tag{D}

Under (H), there is a unique surjective horizon bond

bi,N:Ai,N+1↠Ai,N,bi,Nπi,N+1=πi,N.(2) b_{i,N}:A_{i,N+1}\twoheadrightarrow A_{i,N}, \qquad b_{i,N}\pi_{i,N+1}=\pi_{i,N}. \tag{2}

Under (D), there is a unique named prefix action

αi,N,a:Ai,N+1→Ai+1,N,αi,N,aπi,N+1(u)=πi+1,N(ua).(3) \alpha_{i,N,a}:A_{i,N+1}\to A_{i+1,N}, \qquad \alpha_{i,N,a}\pi_{i,N+1}(u)=\pi_{i+1,N}(ua). \tag{3}

All bond/action/cone squares commute.

Proof. A map out of the surjection π\pi is well-defined exactly when it is constant on ker⁡π\ker\pi. This proves the equivalences and uniqueness in (2) and (3). Surjectivity of πi,N+1\pi_{i,N+1} proves uniqueness of every commuting square: precomposing both routes with it sends uu to the same named lower-horizon or appended-prefix class. Equation (R) proves (1) by the same quotient argument. □\square

This is the strongest conclusion available from named partitions alone. It builds a semantic quotient grid, not a finite controller.

3. A doctrine-indexed accessible factorization

Pin a target-independent storage/observation doctrine D\mathcal D:

  • for each prefix uu, a set P(u)P(u) of legal layouts;
  • a finite observation alphabet OO and obs⁡u:P(u)→O\operatorname{obs}_u:P(u)\to O;
  • a finite action alphabet MM;
  • partial target-independent updates τu,a:P(u)×M⇀P(ua); \tau_{u,a}:P(u)\times M\rightharpoonup P(ua);
  • a declared set I⊆P(ε)I\subseteq P(\varepsilon) of initial layouts.

For kk labeled tracks, P(u)P(u) may be the kk-fold layout space. Birth-at-the-current-head, hold, recede, and other legal operations belong in MM. Random placement at an arbitrary old address does not appear unless the doctrine explicitly grants it.

A finite-role deterministic presentation has:

Q, q0, p0∈I,δ:Q×Σ×O→Q×M,ω:Q×O→B. Q,\ q_0,\ p_0\in I,\quad \delta:Q\times\Sigma\times O\to Q\times M,\quad \omega:Q\times O\to B.

It evolves from (qu,pu)(q_u,p_u) to (qua,pua)(q_{ua},p_{ua}) by δ\delta and τ\tau, and returns ω(qu,obs⁡u(pu))\omega(q_u,\operatorname{obs}_u(p_u)).

Definition — accessible resolving certificate

An ss-role certificate consists of

q:Σ∗→[s],p(u)∈P(u),μ(u,a)∈M, q:\Sigma^*\to[s],\qquad p(u)\in P(u), \qquad \mu(u,a)\in M,

with p(ε)∈Ip(\varepsilon)\in I, satisfying:

p(ua)=τu,a(p(u),μ(u,a));(A1) p(ua)=\tau_{u,a}(p(u),\mu(u,a)); \tag{A1}

(q(u),obs⁡u(p(u)))=(q(v),obs⁡v(p(v)))⟹f(u)=f(v);(A2) (q(u),\operatorname{obs}_u(p(u))) =(q(v),\operatorname{obs}_v(p(v))) \Longrightarrow f(u)=f(v); \tag{A2}

and, for every aa,

(q(u),obs⁡u(p(u)))=(q(v),obs⁡v(p(v)))⟹(q(ua),μ(u,a))=(q(va),μ(v,a)).(A3) (q(u),\operatorname{obs}_u(p(u))) =(q(v),\operatorname{obs}_v(p(v))) \Longrightarrow \bigl(q(ua),\mu(u,a)\bigr) =\bigl(q(va),\mu(v,a)\bigr). \tag{A3}

The important point is that these are conditions on target-indexed labels and storage witnesses. Transition and output tables are derived rather than inserted into the definition.

Theorem B — Myhill–Nerode-form representation

The target ff has a reachable deterministic D\mathcal D-presentation with at most ss finite roles if and only if it has an accessible resolving certificate with at most ss roles.

Proof.

From a presentation, use the actually reached roles, layouts, and chosen actions. Determinism gives (A1) and (A3); the single readout gives (A2).

Conversely, for every reachable local tuple (q,z,a)(q,z,a), define

δ(q,a,z)=(q(ua),μ(u,a)) \delta(q,a,z)=\bigl(q(ua),\mu(u,a)\bigr)

using any uu with (q(u),obs⁡u(p(u)))=(q,z)(q(u),\operatorname{obs}_u(p(u)))=(q,z). Condition (A3) makes this well-defined. Define

ω(q,z)=f(u) \omega(q,z)=f(u)

on reachable (q,z)(q,z); (A2) makes it well-defined. Fill unreachable entries arbitrarily. Starting from (q(ε),p(ε))(q(\varepsilon),p(\varepsilon)), induction on ∣u∣|u|, using (A1), shows that the compiled presentation reaches exactly (q(u),p(u))(q(u),p(u)), and then (A2) gives the correct output. □\square

For the zero-storage doctrine, observations and layouts are singletons. (A2) and (A3) reduce to a finite-index output-respecting right congruence. Thus Theorem B specializes exactly to Myhill–Nerode rather than merely resembling it.

This representation pattern is not presently claimed as new. Myhill–Nerode theorems for register automata and minimal-memory automata already combine finite control with nontrivial storage relations. The question for FPRD is whether the same accessible object also computes the finite-horizon Pareto frontier and interfaces cleanly with M26 and M33.

4. The missing root/branch law for cut advice

A cut-initialized protocol may separately supply configurations

(qu(v),pu(v)) \bigl(q^u(v),p^u(v)\bigr)

for every base prefix uu. It can be perfectly lawful inside each continuation cone and still fail to be online.

The missing equation is

(qu(av),pu(av))=(qua(v),pua(v))(RB) \boxed{ \bigl(q^u(av),p^u(av)\bigr) = \bigl(q^{ua}(v),p^{ua}(v)\bigr) } \tag{RB}

for every u,a,vu,a,v. At v=εv=\varepsilon, the configuration freshly supplied at cut uaua must equal the successor actually reached from the cut at uu.

M26’s semantic diagonal equation equates target values and residuals. It does not imply (RB), which is an equality of presentation witnesses.

5. A genuine finite-horizon sewing theorem

Call D\mathcal D prefix-locally finite when O,M,IO,M,I are finite and each P(u)P(u) is finite. Fix ss. A depth-HH certificate is one joint certificate on the whole finite prefix tree Σ≤H\Sigma^{\le H}, correct at every prefix through depth HH, using one stationary transition/readout table and the normalized role palette [s][s]. The budget means “at most ss”: unused role names are allowed. Every labeled configuration must be reachable from the declared root by the legal updates.

Restriction from depth H+1H+1 to HH must remain inside the admitted stratum. More generally, the proof below needs every normalized parameter space to be finite (or compact), and legality and correctness to be closed local conditions.

Theorem C — locally finite causal sewing

For a prefix-locally-finite doctrine, the following are equivalent:

  1. ff has one exact D\mathcal D-presentation with at most ss roles;
  2. ff has one global accessible resolving certificate with at most ss roles;
  3. for every HH, f∣Σ≤Hf|_{\Sigma^{\le H}} has a depth-HH accessible resolving certificate with the same resource bound ss.

Proof. Theorem B gives 1⟺21\Longleftrightarrow2, and restriction gives 2⇒32\Rightarrow3.

For 3⇒23\Rightarrow2, make a rooted tree whose level-HH vertices are all depth-HH certificates, including their one stationary transition/readout table, and whose parent map is restriction to depth H−1H-1. Every level is nonempty. Each level is finite: its domain is a finite prefix tree, its role and edge labels range over finite sets, and every layout set P(u)P(u) is finite. Hence the tree is finitely branching. König’s lemma gives an infinite compatible branch. The union of that branch defines q,p,μq,p,\mu on all prefixes while preserving the stationary tables. Every local legality and correctness condition occurs in some finite level and therefore holds in the union. Induction from the root preserves accessibility. This is the required global certificate. □\square

If every finite certificate is the restriction of an admitted total presentation—for example because updates are totalized with a dead configuration—then in M33 notation, if

Ff(H)={s:a depth-H accessible certificate exists}, \mathcal F_f(H)= \{s:\text{a depth-}H\text{ accessible certificate exists}\},

then Theorem C gives

Ff(∞)=⋂HFf(H) \boxed{ \mathcal F_f(\infty)=\bigcap_H\mathcal F_f(H) }

for every fixed locally finite doctrine/resource stratum. This is the doctrine-specific reason the stratum is compact; it is not a new general compactness theorem.

Without that extension property, the finite certificate field is an outer relaxation F~f(H)\widetilde{\mathcal F}_f(H), not automatically M33’s feasible field. The theorem still identifies exact presentations with ⋂HF~f(H)\bigcap_H\widetilde{\mathcal F}_f(H); identifying the individual finite-horizon fibers requires total/nonblocking updates or a separate extension lemma.

6. Why local finiteness or closedness is load-bearing

Let a one-role presentation carry uncharged fuel t∈Nt\in\mathbb N, with observations ++ and 00. On aa, positive fuel decrements and zero stays zero; on bb, fuel resets to zero. The output accepts exactly in observation ++. Take the target a∗a^*: it accepts ana^n and rejects every word containing bb.

For horizon HH, initialization t=H+1t=H+1 is correct through HH: every all-aa word still has positive fuel, while the first bb forces observation zero permanently. No finite initialization is exact at all horizons, because at+1a^{t+1} is incorrectly rejected.

The certificate tree is infinitely branching at its root and has no infinite branch with one fixed admissible tt. In the one-point compactification its limit is t=∞t=\infty, but that point is outside the presentation doctrine.

Thus an arbitrary integer cut placement or initializer may escape even when role and track counts stay fixed. The repair is one of:

  • restrict to a prefix-locally-finite admissible layout family;
  • charge/bound the initializer magnitude as another resource;
  • use a compact normalized presentation core with a closed admissible locus.

This is exactly the M33 compact-core/escape distinction in operational form.

7. Two independent failures of weaker claims

7.1 Semantic compatibility without cross-grade finite control

For

L□={an:n is a square}, L_\square=\{a^n:n\text{ is a square}\},

every exact typed cut has one row. Every literal diagonal law commutes, and every per-grade zero-track partition has one cell. Nevertheless the unary output sequence is not ultimately periodic, so no finite controller exists. M26 detects the omitted structure:

qL□(N)≥N+2. q_{L_\square}(N)\ge N+2.

The problem is not horizon restriction inside a grade; it is the absence of one bounded cross-grade role/readout/action system.

7.2 Lawful post-cut motion without a reachable initializer

In the absolute-address no-birth/no-right doctrine, consider well-formed words

⊢an#at \vdash a^n\#a^t

accepted exactly when t=nt=n. If a track is supplied at the final old aa at the delimiter, a fixed post-cut rule can recede and detect equality. But the required supplied address grows with nn, while an online no-right/no-birth track cannot reach it from a fixed initial address.

The post-cut controller is uniform; the initializer is not accessible. Equation (RB) is exactly what fails.

8. Relation to the fixed-cut cone frontier

Every online certificate induces, at every cut, a complete-snapshot partition. The fixed-cut cone theorem therefore supplies a necessary projection:

χk(m,n)≤#{reachable complete snapshots after length m}. \chi_k(m,n) \le \#\{\text{reachable complete snapshots after length }m\}.

If there are at most ss non-position roles and at most LmL_m possible positions per track, then

χk(m,n)≤sLmk.(4) \chi_k(m,n)\le sL_m^k. \tag{4}

Late INDEX makes this projection exact at the cut:

χk=2max⁡(2r−k,0). \chi_k=2^{\max(2^r-k,0)}.

The fixed-cut theorem is therefore a dual obstruction for the accessible frontier. It is not itself the accessible frontier.

The underlying motion doctrine is standard up to reversing the address convention: it is a one-way multi-head automaton, or a leading head with trailing heads. The counting mechanism is also standard configuration counting. What the late-INDEX example isolates is a regime distinction. Systematic and bit-probe data structures choose probe addresses from the query, which produces multiplicative redundancy–probe tradeoffs. Here the query is future input, so initial placement is necessarily query-oblivious; motion may remain adaptive after the query begins. On the deliberately spaced family this forced timing yields the exact additive boundary above. That is an instantiation and a diagnostic contrast, not currently a novelty claim or a universal conservation law.

9. What this says about admitting incompletely specified folding

M33 admission and operational sewing are different thresholds.

  • A folding doctrine may be admitted to the demand-field layer with a set of finite presentations, a well-defined possibly set-valued semantic map, and pinned resources. Deterministic internal crease-selection actions are not required merely to define that field.
  • Theorems B and C make a stronger conclusion. They require a local observation/action doctrine, because “reachable from the preceding cut” is meaningless until legal one-step evolution is specified.

So an incompletely specified origami model can enter FPRD now. It cannot inherit a causal sewing or track-factorization theorem until the missing operational structure is supplied or the theorem is reformulated relationally.

10. Current assessment

The substantive advance is not that compatible diagrams commute. It is the separation and exact reconnection of:

target rows⟵named semantic quotient grid⟵accessible causal lift⟷finite presentation. \text{target rows} \longleftarrow \text{named semantic quotient grid} \longleftarrow \text{accessible causal lift} \longleftrightarrow \text{finite presentation}.

The two failure modes are now explicit:

  1. semantic nonuniformity across grades (square length);
  2. presentation witnesses that are legal after a cut but unreachable before it (supplied-track advice).

The next comparator question is whether Theorem B is already a standard Myhill–Nerode theorem for automata with storage. The FPRD-specific candidate delta, if any, is the integration with the fixed-cut cone Pareto frontier, M26 quotient grid, and M33 compact-core escape field.