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 , write
The fixed-cut cone theorem answers an offline question: after one selected prefix has already been read, how many complete snapshots are needed if 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:
- target compatibility: the cut tables describe one target;
- semantic quotient compatibility: named cut partitions form one horizon/grade grid over the target residuals;
- 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
be a named finite partition. Say it is resolving when
Then there is a unique surjection
where 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:
and, for every ,
Under (H), there is a unique surjective horizon bond
Under (D), there is a unique named prefix action
All bond/action/cone squares commute.
Proof. A map out of the surjection is well-defined exactly when it is constant on . This proves the equivalences and uniqueness in (2) and (3). Surjectivity of proves uniqueness of every commuting square: precomposing both routes with it sends to the same named lower-horizon or appended-prefix class. Equation (R) proves (1) by the same quotient argument.
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 :
- for each prefix , a set of legal layouts;
- a finite observation alphabet and ;
- a finite action alphabet ;
- partial target-independent updates
- a declared set of initial layouts.
For labeled tracks, may be the -fold layout space. Birth-at-the-current-head, hold, recede, and other legal operations belong in . Random placement at an arbitrary old address does not appear unless the doctrine explicitly grants it.
A finite-role deterministic presentation has:
It evolves from to by and , and returns .
Definition — accessible resolving certificate
An -role certificate consists of
with , satisfying:
and, for every ,
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 has a reachable deterministic -presentation with at most finite roles if and only if it has an accessible resolving certificate with at most 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 , define
using any with . Condition (A3) makes this well-defined. Define
on reachable ; (A2) makes it well-defined. Fill unreachable entries arbitrarily. Starting from , induction on , using (A1), shows that the compiled presentation reaches exactly , and then (A2) gives the correct output.
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
for every base prefix . It can be perfectly lawful inside each continuation cone and still fail to be online.
The missing equation is
for every . At , the configuration freshly supplied at cut must equal the successor actually reached from the cut at .
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 prefix-locally finite when are finite and each is finite. Fix . A depth- certificate is one joint certificate on the whole finite prefix tree , correct at every prefix through depth , using one stationary transition/readout table and the normalized role palette . The budget means “at most ”: unused role names are allowed. Every labeled configuration must be reachable from the declared root by the legal updates.
Restriction from depth to 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:
- has one exact -presentation with at most roles;
- has one global accessible resolving certificate with at most roles;
- for every , has a depth- accessible resolving certificate with the same resource bound .
Proof. Theorem B gives , and restriction gives .
For , make a rooted tree whose level- vertices are all depth- certificates, including their one stationary transition/readout table, and whose parent map is restriction to depth . 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 is finite. Hence the tree is finitely branching. König’s lemma gives an infinite compatible branch. The union of that branch defines 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.
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
then Theorem C gives
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 , not automatically M33’s feasible field. The theorem still identifies exact presentations with ; 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 , with observations and . On , positive fuel decrements and zero stays zero; on , fuel resets to zero. The output accepts exactly in observation . Take the target : it accepts and rejects every word containing .
For horizon , initialization is correct through : every all- word still has positive fuel, while the first forces observation zero permanently. No finite initialization is exact at all horizons, because is incorrectly rejected.
The certificate tree is infinitely branching at its root and has no infinite branch with one fixed admissible . In the one-point compactification its limit is , 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
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:
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
accepted exactly when . If a track is supplied at the final old at the delimiter, a fixed post-cut rule can recede and detect equality. But the required supplied address grows with , 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:
If there are at most non-position roles and at most possible positions per track, then
Late INDEX makes this projection exact at the cut:
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:
The two failure modes are now explicit:
- semantic nonuniformity across grades (square length);
- 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.