Accessible certificates and the full finite-horizon Pareto field
Status. Proof-grade working result. No novelty claim. This isolates the precise doctrine hypotheses under which accessible certificates compute the actual presentation-demand field, and the precise sense in which the fixed-cut resolving-cell frontier is only a dual projection of that field.
Contents
1. A resource-bounded local doctrine
Fix an input alphabet , a target codomain , and a non-role resource budget . The budget may include, for example,
- number of old-input tracks;
- a bound on transition and final weights;
- a bound on initializer magnitude;
- a finite sensor package; and
- any other local presentation parameter that is being charged.
The -core of a uniformly described local storage doctrine consists of:
where is the set of legal storage/layout states after prefix , is the allowed initializer set, is the observation set, is the set of local update instructions, and is the set of local readout instructions. There are target-independent maps
and
The extra readout instruction is needed for weighted doctrines. For example, the storage state may contain an accumulated group value , while the readout instruction is a bounded final weight and . Requiring equal target values whenever two finite roles agree would be wrong in that setting: the same role and final weight may legitimately produce different values from different accumulated register contents.
Assume for now that, for fixed , , the initializer set, and every prefix fiber are finite. Crucially, the observation and instruction alphabets are uniformly finite across all prefixes in the core, so a stationary controller table is a finite object. The prefix-indexed notation is typing convenience: the doctrine must have one uniform finite/effective description and may not encode the target or an arbitrary prefix oracle in , or .
An -role reachable-core presentation supplies finite tables
on the local tuples that its run actually attains, together with an initial role and an initializer in . Its run must be defined on every input under consideration.
2. The intrinsic certificate field
On the finite prefix tree , an -accessible certificate is a labeling
satisfying:
root and accessibility
correct local readout
one stationary readout table
one stationary transition table for every ,
All ingredients are target-side labels and doctrine-side legality relations; no automaton table is quantified in the definition.
Write
for the finite set of such certificates.
Theorem 1 — exact finite-horizon Pareto representation
For the reachable-core doctrine,
Consequently the complete finite-horizon reachable-core feasible field and its Pareto boundary are computed by the certificate field:
This simultaneously preserves roles, tracks, initializer bounds, and local parameter magnitude, because those resources are already pinned by and the chosen -core.
The certificate is an intrinsic finite constraint system once the target and doctrine are fixed, but it is generally noncanonical and is an unfolding of presentation consistency rather than a new minimal-memory quotient.
Proof
From a presentation, label every prefix by the role, storage state, update instruction, and readout instruction actually used on its run. Equations (C1)–(C4) follow from legality, correctness, and the fact that the presentation uses one deterministic pair of local tables.
Conversely, define from any attained node with , taking the value . Equation (C3) makes this well-defined. Define analogously from ; equation (C4) makes this well-defined. Start from the certificate’s root. Induction using (C1) shows that the compiled presentation reaches exactly , and (C2) proves correctness. No resource coordinate increases.
Total-presentation qualification
Equation (2) equals an M33 field of globally total presentations whenever every relevant certificate has budget-preserving core completion: its tables on attained local tuples extend to all declared local tuples without increasing . A doctrine-wide completion property is a convenient sufficient condition.
This condition is not formal decoration. Let
with , , and undefined. Give the sole readout instruction constant output . The constant-zero target has a one-role accessible certificate using storage state forever. But if a “total presentation” is required to induce a defined update from every legal storage state, no total table exists: the entry at observation has no legal action. Thus accessible certificates compute the reachable-core/partial field in complete generality; equality with a total field needs completion.
3. Fine-resource sewing and coarse-resource escape
Assume the -core is prefix-locally finite and restriction of a depth- certificate is an admitted depth- certificate.
Theorem 2 — exact sewing in every fixed fine stratum
If core completion holds, the same equivalence holds for exact total presentations.
Proof
Restriction proves the forward implication. For the reverse implication, make a rooted tree whose level- vertices are the depth- certificates and whose edges are restrictions. Each level is finite, because the prefix tree is finite and every label set in the fixed core is finite. There are vertices at arbitrarily great depth. König’s lemma gives an infinite compatible branch. Its union satisfies (C1)–(C4), because every instance of those local conditions occurs at a finite level. Theorem 1 compiles the union.
This yields a precise operational form of the M33 compact-core distinction for the pinned word-value observation tower and the resources actually represented in . If bounds raw local weights, this is a raw weight field. Identifying it with M33’s gauge-invariant canonical-height field additionally requires a pinned normal form, its access-tree data in the certificate, and a proof that compilation/completion preserves the normalized bound.
Suppose is a coarse budget, and is an omitted initializer/core-magnitude coordinate, so that . Then a coarse sewing defect is exactly the quantifier pattern
The first clause says every horizon can be fit after changing core. The second says every fixed compact core is eventually excluded. Thus the initializer/core magnitude is not bookkeeping: omitting it is precisely what permits the quantifier swap.
The fuel example realizes (4). A one-role machine has a natural-number fuel initializer; decrements positive fuel, resets it to zero, and the readout accepts iff fuel is positive. For the target , fuel works through horizon , but every fixed finite fuel fails on a longer all- word.
4. A dual cut obstruction with storage-volume charging
Now assume the doctrine has old-input tracks and obeys a cone-local Markov law. At grade , it maps its storage fibers into a finite target-independent set of prefix-independent complete non-role configuration types. Once a role and such a type are fixed, continuation behavior may depend only on future input and on old symbols reached through the declared length- track cones. It may not inspect the name or any uncharged content of the old prefix. This requirement covers observation, update, and readout.
Let be the types reachable in legal steps from a permitted initializer, and put
For a selected prefix family and continuation horizon , let be the resolving-cell/root-snapshot frontier of the fixed-cut cone theorem.
Theorem 3 — accessible cone obstruction
Every -accessible presentation correct through the selected cut and continuation horizon satisfies
Hence
is a presentation-independent lower bound on the role coordinate after the other resource coordinates have been fixed.
Proof
Map each to its finite role and complete non-role configuration type. There are at most such pairs. Prefixes in one fiber have equal role, register/storage type, and track layout. If two such prefixes also agree on the old symbols in the layout’s reach cones, the cone-local Markov law and determinism give identical continuation executions and hence identical future rows. Each fiber is consequently a resolving cell. These fibers form a cone factorization, so their number is at least .
The inequality can charge a weight/initializer coordinate explicitly. For example, suppose storage contains a register in a finitely generated group , initial register norm is at most , each transition multiplier has norm at most , and labeled old-input tracks have at most positions (including inactivity) at depth . Let every other mutable non-role mode contribute a factor . If
is the word-ball growth function, then
Therefore
For the spaced late-INDEX family, , so (7) becomes
This does not say that every group element in the ball is computationally useful; it is a generous information-capacity upper bound. Its value is as a dual obstruction: even after crediting the presentation for every possible register value and layout in its bounded core, the remaining residual demand must be carried by roles.
If the initializer factor already includes the register or auxiliary modes, the corresponding factors above are omitted rather than double counted.
Corollary 3a — polynomial-growth carriers force a genuine
state/track/bit-width tradeoff
Suppose, for constants ,
Then late INDEX obeys
In particular, for fixed , polynomially many roles, polynomially bounded local weights/initializers, and polynomial auxiliary-mode volume, the right side is , while the calibration family has . Such a presentation is impossible.
More quantitatively, if , is fixed, and the role and auxiliary-mode factors are polynomial in , equation (9) forces
Thus either the finite-role coordinate grows exponentially in the unresolved information, more tracks are supplied, or grows linearly in that information up to the displayed loss. Calling this physical bit-width requires a pinned succinct encoding, such as binary integer or Mal’cev coordinates. This conclusion uses growth volume only and does not infer an ability to decode every algebraically available value.
5. What is complete, and what provably is not
The fixed-cut resolving-cell number is complete for the pinned cut-initialized doctrine when the charged coordinate is the number of complete root snapshots and downstream strict-layered state is free. That is the fixed-cut representation theorem.
It is not complete for stationary online role demand, even if one retains for every exact cut and every horizon. Over a unary alphabet , the exact-grade prefix family is a singleton. Therefore
for every unary target , every , and every . Nevertheless the constant unary target has a one-state controller, while
has no finite-state controller. Thus no formula using only the complete collection of exact-cut values can characterize the online state field.
The missing information is genuinely multi-cut: one role name, one action table, and reachable storage witnesses must work across grades. The accessible certificate field supplies exactly that information.
Theorem 4 — complete finite dual obstruction
Under the hypotheses of Theorem 2, for every fixed fine budget , exactly one of the following holds:
- there is one exact global -presentation; or
- there is a finite prefix-closed tree on which the constraints (C1)–(C4) have no -labeling.
Proof
If the global presentation does not exist, Theorem 2 gives an with . Take , or any inclusion-minimal prefix-closed subinstance of its finite constraint system that remains unsatisfiable. Conversely, a global presentation restricts to a certificate on every such .
Theorem 4 is the complete dual; fixed-cut is a tractable scalar projection of it. A lower bound may therefore be organized in two stages:
- try a resolving-cell/cone obstruction such as (5);
- if every individual cut passes, exhibit a finite multi-cut obstruction to stationary role reuse or operational accessibility.
The square-language example proves that the second stage cannot in general be eliminated.
6. Resulting boundary for FPRD
Within a pinned core-local doctrine:
With prefix-local finiteness:
The fixed-cut resolving-cell frontier remains valuable, but in its correct role:
The new load-bearing distinctions are:
- reachable-core versus globally total presentations;
- fixed fine resources versus a coarse field that hides initializer/core escape;
- supplied cut configurations versus accessible cross-cut witnesses; and
- complete root snapshots versus reusable finite roles.