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 Σ\Sigma, a target codomain BB, and a non-role resource budget ρ\rho. 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 ρ\rho-core of a uniformly described local storage doctrine consists of:

Pρ(u),Iρ⊆Pρ(ε),Oρ,Mρ,Wρ, P_\rho(u),\quad I_\rho\subseteq P_\rho(\varepsilon),\quad O_\rho,\quad M_\rho,\quad W_\rho,

where Pρ(u)P_\rho(u) is the set of legal storage/layout states after prefix uu, IρI_\rho is the allowed initializer set, OρO_\rho is the observation set, MρM_\rho is the set of local update instructions, and WρW_\rho is the set of local readout instructions. There are target-independent maps

obs⁡u:Pρ(u)→Oρ, \operatorname{obs}_u:P_\rho(u)\to O_\rho,

τu,a:Pρ(u)×Mρ⇀Pρ(ua), \tau_{u,a}:P_\rho(u)\times M_\rho\rightharpoonup P_\rho(ua),

and

ev⁡u:Pρ(u)×Wρ⇀B. \operatorname{ev}_u:P_\rho(u)\times W_\rho\rightharpoonup B.

The extra readout instruction is needed for weighted doctrines. For example, the storage state may contain an accumulated group value gg, while the readout instruction is a bounded final weight ww and ev⁡(g,w)=gw\operatorname{ev}(g,w)=gw. 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 ρ\rho, Oρ,Mρ,WρO_\rho,M_\rho,W_\rho, the initializer set, and every prefix fiber Pρ(u)P_\rho(u) 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 obs⁡u,τu,a\operatorname{obs}_u,\tau_{u,a}, or ev⁡u\operatorname{ev}_u.

An ss-role reachable-core presentation supplies finite tables

δ:[s]×Σ×Oρ→[s]×Mρ,ω:[s]×Oρ→Wρ \delta:[s]\times\Sigma\times O_\rho\to[s]\times M_\rho, \qquad \omega:[s]\times O_\rho\to W_\rho

on the local tuples that its run actually attains, together with an initial role and an initializer in IρI_\rho. Its run must be defined on every input under consideration.

2. The intrinsic certificate field

On the finite prefix tree Σ≤H\Sigma^{\le H}, an (s,ρ)(s,\rho)-accessible certificate is a labeling

q(u)∈[s],p(u)∈Pρ(u), q(u)\in[s],\qquad p(u)\in P_\rho(u),

μ(u,a)∈Mρ(∣u∣<H),ν(u)∈Wρ, \mu(u,a)\in M_\rho\quad(|u|<H),\qquad \nu(u)\in W_\rho,

satisfying:

  1. root and accessibility p(ε)∈Iρ,p(ua)=τu,a(p(u),μ(u,a));(C1) p(\varepsilon)\in I_\rho,\qquad p(ua)=\tau_{u,a}(p(u),\mu(u,a)); \tag{C1}

  2. correct local readout ev⁡u(p(u),ν(u))=f(u);(C2) \operatorname{ev}_u(p(u),\nu(u))=f(u); \tag{C2}

  3. one stationary readout table (q(u),obs⁡up(u))=(q(v),obs⁡vp(v))⟹ν(u)=ν(v);(C3) (q(u),\operatorname{obs}_u p(u)) =(q(v),\operatorname{obs}_v p(v)) \Longrightarrow \nu(u)=\nu(v); \tag{C3}

  4. one stationary transition table for every a∈Σa\in\Sigma, (q(u),obs⁡up(u))=(q(v),obs⁡vp(v))⟹(q(ua),μ(u,a))=(q(va),μ(v,a)).(C4) (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{C4}

All ingredients are target-side labels and doctrine-side legality relations; no automaton table is quantified in the definition.

Write

Certf(H;s,ρ) \mathsf{Cert}_f(H;s,\rho)

for the finite set of such certificates.

Theorem 1 — exact finite-horizon Pareto representation

For the reachable-core doctrine,

f∣Σ≤H has an (s,ρ)-presentation  ⟺  Certf(H;s,ρ)≠∅.(1) \boxed{ f|_{\Sigma^{\le H}}\text{ has an }(s,\rho)\text{-presentation} \iff \mathsf{Cert}_f(H;s,\rho)\ne\varnothing . } \tag{1}

Consequently the complete finite-horizon reachable-core feasible field and its Pareto boundary are computed by the certificate field:

Ffcore(H)={(s,ρ):Certf(H;s,ρ)≠∅}.(2) \boxed{ \mathcal F_f^{\rm core}(H) = \{(s,\rho):\mathsf{Cert}_f(H;s,\rho)\ne\varnothing\}. } \tag{2}

This simultaneously preserves roles, tracks, initializer bounds, and local parameter magnitude, because those resources are already pinned by [s][s] and the chosen ρ\rho-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 ω(q,z)\omega(q,z) from any attained node uu with (q(u),obs⁡p(u))=(q,z)(q(u),\operatorname{obs}p(u))=(q,z), taking the value ν(u)\nu(u). Equation (C3) makes this well-defined. Define δ(q,a,z)\delta(q,a,z) analogously from (q(ua),μ(u,a))(q(ua),\mu(u,a)); equation (C4) makes this well-defined. Start from the certificate’s root. Induction using (C1) shows that the compiled presentation reaches exactly (q(u),p(u))(q(u),p(u)), and (C2) proves correctness. No resource coordinate increases. □\square

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 (s,ρ)(s,\rho). A doctrine-wide completion property is a convenient sufficient condition.

This condition is not formal decoration. Let

P(u)={0,1},I={0},O={0,1},M={m}, P(u)=\{0,1\},\quad I=\{0\},\quad O=\{0,1\},\quad M=\{m\},

with obs⁡(p)=p\operatorname{obs}(p)=p, τ(0,m)=0\tau(0,m)=0, and τ(1,m)\tau(1,m) undefined. Give the sole readout instruction constant output 00. The constant-zero target has a one-role accessible certificate using storage state 00 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 11 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 ρ\rho-core is prefix-locally finite and restriction of a depth-H+1H+1 certificate is an admitted depth-HH certificate.

Theorem 2 — exact sewing in every fixed fine stratum

Certf(∞;s,ρ)≠∅  ⟺  ∀H Certf(H;s,ρ)≠∅.(3) \boxed{ \mathsf{Cert}_f(\infty;s,\rho)\ne\varnothing \iff \forall H\ \mathsf{Cert}_f(H;s,\rho)\ne\varnothing . } \tag{3}

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-HH vertices are the depth-HH 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. □\square

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 ρ\rho. If ρ\rho 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 rr is a coarse budget, and b∈Nb\in\mathbb N is an omitted initializer/core-magnitude coordinate, so that ρ=(r,b)\rho=(r,b). Then a coarse sewing defect is exactly the quantifier pattern

[∀H ∃b Certf(H;s,r,b)≠∅]∧[∀b ∃H Certf(H;s,r,b)=∅].(4) \boxed{ \bigl[\forall H\ \exists b\ \mathsf{Cert}_f(H;s,r,b)\ne\varnothing\bigr] \quad\land\quad \bigl[\forall b\ \exists H\ \mathsf{Cert}_f(H;s,r,b)=\varnothing\bigr]. } \tag{4}

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; aa decrements positive fuel, bb resets it to zero, and the readout accepts iff fuel is positive. For the target a∗a^*, fuel H+1H+1 works through horizon HH, but every fixed finite fuel fails on a longer all-aa word.

4. A dual cut obstruction with storage-volume charging

Now assume the doctrine has kk old-input tracks and obeys a cone-local Markov law. At grade mm, it maps its storage fibers into a finite target-independent set Cρ(m)C_\rho(m) 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-nn track cones. It may not inspect the name or any uncharged content of the old prefix. This requirement covers observation, update, and readout.

Let ReachType⁡ρ(m)⊆Cρ(m)\operatorname{ReachType}_\rho(m)\subseteq C_\rho(m) be the types reachable in mm legal steps from a permitted initializer, and put

Vρ(m)=∣ReachType⁡ρ(m)∣. V_\rho(m)=|\operatorname{ReachType}_\rho(m)|.

For a selected prefix family U⊆ΣmU\subseteq\Sigma^m and continuation horizon nn, let χk(f;U,n)\chi_k(f;U,n) be the resolving-cell/root-snapshot frontier of the fixed-cut cone theorem.

Theorem 3 — accessible cone obstruction

Every (s,ρ)(s,\rho)-accessible presentation correct through the selected cut and continuation horizon satisfies

χk(f;U,n)≤s Vρ(m).(5) \boxed{ \chi_k(f;U,n)\le s\,V_\rho(m). } \tag{5}

Hence

s≥⌈χk(f;U,n)Vρ(m)⌉(6) \boxed{ s\ge \left\lceil\frac{\chi_k(f;U,n)}{V_\rho(m)}\right\rceil } \tag{6}

is a presentation-independent lower bound on the role coordinate after the other resource coordinates have been fixed.

Proof

Map each u∈Uu\in U to its finite role and complete non-role configuration type. There are at most sVρ(m)sV_\rho(m) 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 χk\chi_k. □\square

The inequality can charge a weight/initializer coordinate explicitly. For example, suppose storage contains a register in a finitely generated group GG, initial register norm is at most bb, each transition multiplier has norm at most bb, and kk labeled old-input tracks have at most m+1m+1 positions (including inactivity) at depth mm. Let every other mutable non-role mode contribute a factor Cρaux(m)C_\rho^{\rm aux}(m). If

γG(R)=∣{g∈G:∣g∣≤R}∣ \gamma_G(R)=|\{g\in G:|g|\le R\}|

is the word-ball growth function, then

Vk,b(m)≤Cρaux(m) ∣Ib∣ γG((m+1)b)(m+1)k. V_{k,b}(m) \le C_\rho^{\rm aux}(m)\, |I_b|\,\gamma_G((m+1)b)(m+1)^k.

Therefore

log⁡2s+log⁡2∣Ib∣+log⁡2Cρaux(m)+log⁡2γG((m+1)b)+klog⁡2(m+1)≥log⁡2χk.(7) \boxed{ \log_2 s+\log_2|I_b|+ \log_2 C_\rho^{\rm aux}(m)+ \log_2\gamma_G((m+1)b)+k\log_2(m+1) \ge \log_2\chi_k. } \tag{7}

For the spaced late-INDEX family, log⁡2χk=d−k\log_2\chi_k=d-k, so (7) becomes

log⁡2s+log⁡2∣Ib∣+log⁡2Cρaux(m)+log⁡2γG((m+1)b)+klog⁡2(m+1)+k≥d.(8) \boxed{ \log_2 s+\log_2|I_b|+ \log_2 C_\rho^{\rm aux}(m)+ \log_2\gamma_G((m+1)b)+k\log_2(m+1)+k \ge d. } \tag{8}

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 C,D,C0,D0C,D,C_0,D_0,

γG(R)≤C(1+R)D,∣Ib∣≤C0(1+b)D0. \gamma_G(R)\le C(1+R)^D, \qquad |I_b|\le C_0(1+b)^{D_0}.

Then late INDEX obeys

d≤log⁡2s+k+klog⁡2(m+1)+Dlog⁡2(1+(m+1)b)+D0log⁡2(1+b)+log⁡2Cρaux(m)+O(1).(9) \boxed{ \begin{aligned} d\le {}& \log_2s+k+k\log_2(m+1)\\ &+D\log_2(1+(m+1)b) +D_0\log_2(1+b)\\ &+\log_2 C_\rho^{\rm aux}(m)+O(1). \end{aligned} } \tag{9}

In particular, for fixed kk, polynomially many roles, polynomially bounded local weights/initializers, and polynomial auxiliary-mode volume, the right side is O(log⁡m)O(\log m), while the calibration family has d=Θ(m/log⁡m)d=\Theta(m/\log m). Such a presentation is impossible.

More quantitatively, if D+D0>0D+D_0>0, kk is fixed, and the role and auxiliary-mode factors are polynomial in mm, equation (9) forces

log⁡2(1+b)=Ω ⁣(dD+D0)−O(log⁡m).(10) \log_2(1+b)=\Omega\!\left(\frac{d}{D+D_0}\right)-O(\log m). \tag{10}

Thus either the finite-role coordinate grows exponentially in the unresolved information, more tracks are supplied, or log⁡(1+b)\log(1+b) grows linearly in that information up to the displayed O(log⁡m)O(\log m) 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 χk\chi_k 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 χk(f;m,n)\chi_k(f;m,n) for every exact cut and every horizon. Over a unary alphabet Σ={a}\Sigma=\{a\}, the exact-grade prefix family Σm\Sigma^m is a singleton. Therefore

χk(f;m,n)=1 \chi_k(f;m,n)=1

for every unary target ff, every m,nm,n, and every kk. Nevertheless the constant unary target has a one-state controller, while

L□={at2:t≥0} L_\square=\{a^{t^2}:t\ge0\}

has no finite-state controller. Thus no formula using only the complete collection of exact-cut χk\chi_k 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 (s,ρ)(s,\rho), exactly one of the following holds:

  1. there is one exact global (s,ρ)(s,\rho)-presentation; or
  2. there is a finite prefix-closed tree T⊆Σ∗T\subseteq\Sigma^* on which the constraints (C1)–(C4) have no (s,ρ)(s,\rho)-labeling.

Proof

If the global presentation does not exist, Theorem 2 gives an HH with Certf(H;s,ρ)=∅\mathsf{Cert}_f(H;s,\rho)=\varnothing. Take T=Σ≤HT=\Sigma^{\le H}, 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 TT. □\square

Theorem 4 is the complete dual; fixed-cut χk\chi_k is a tractable scalar projection of it. A lower bound may therefore be organized in two stages:

  1. try a resolving-cell/cone obstruction such as (5);
  2. 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:

finite-horizon presentation Pareto field=accessible-certificate Pareto field. \boxed{ \text{finite-horizon presentation Pareto field} = \text{accessible-certificate Pareto field}. }

With prefix-local finiteness:

global failure at a fixed fine budget  ⟺  one finite accessible-certificate obstruction exists. \boxed{ \text{global failure at a fixed fine budget} \iff \text{one finite accessible-certificate obstruction exists}. }

The fixed-cut resolving-cell frontier remains valuable, but in its correct role:

resolving cells are a useful dual projection, not the full field. \boxed{ \text{resolving cells are a useful dual projection, not the full field}. }

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.