Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Native Literal Moore Budgets

Abstract

Exact literal submission budgets on the entire actual stationary Moore fiber.

Full original fiber and four prices

Fix a finite prefix-free cut P and an arbitrary actual finite reference origin uo. Write C=canonicalRow(P,rho(uo)). OriginFiber(P,C) is the entire actual set of finite ordered alpha/beta origins u with canonicalRow(P,rho(u))=C. ImageValues(C) contains the acquired injective class values whose filling is an actual substitution image. The existing imageOriginEquiv is their bijection. The complete exterior, every reached occurrence, repeated-class partition, all different-class disequalities and every blocked-cut guard remain fixed. The whole target is target(C,theta)=canonicalRow(P,u), by native_full_root_feasibility. There is no source-size, depth or intrinsic-rank bound.

Occurrences(C,d) filters the original physical holeAddresses by holeLabel=d. Shortest(C,d) minimizes the pair (length(p),p) in lexicographic product order; price(C,d) is its length. The private shortest_spec applies the existing labels_witness and pinned Mathlib List.argmin and List.le_of_mem_argmin. Its first conclusion is occurrence membership; every occurrence p has length at least price(C,d), and equality of lengths implies shortest(C,d) is lexicographically at most p. Original numeric class names do not change. NativeWholeRowService.representative chooses the first lexicographic occurrence and is not assumed shortest.

For the existing Controller and Run, nativeCost(M,tr) sums length(M.addr(s)) over the exact running-state visit list tr. RootCost(T,tr) sums price(C,T.coord(s)) over that same kind of list. These are per-input sums before upper bounds. Repeated coordinates, repeated words, absence and empty words each cost one call; the empty word costs zero literal letters. An initial halt has empty trace and zero of both charges. No new controller, evaluator or candidate enumeration is introduced.

NativeLiteralFeasible extends the original NativeFeasible telescope with nativeCost at most ell on each original actual origin. The code is a function of actually acquired ImageValues and is the current initial state itself. RootLiteralFeasible extends RootFeasible with rootCost at most ell on every attained Chart. The remaining upper bounds are code-image cardinality at most r, cardinality of all installed running plus halting states at most K, and at most q calls. Unused states, equal-output halts and unused addresses count. Both encoder and table may be reselected.

Acquisition, genuine pre-cut export, complete access isolation, authenticated one-update continuity, lawful common entry and the stationary native port remain supplied paid premises. Literal cost prices only physically submitted words. Address construction and storage, table storage, whole-output representation, local work, elapsed time, acquisition, export, authentication, isolation, entry and service retain their separate costs. No mathematical theorem certifies those physical services.

The public supplier interfaces retain one original implementation and proof: NativeWholeRowService.labels_witness supplies occurrence nonemptiness; ActualObserverAbsorbingNormalization.skip_exact, skip_retained and skip_removed supply finite first exits; NativeSharedMooreSynthesis.referenceValues and referenceType supply truthful actual witnesses, and its evaluate_halt, evaluate_exact, evaluate_reindex, candidate_complete, bounded_mem and bounded_size supply exact evaluation and enumeration. All types in these public signatures are reachable through their original imports. Literal_candidate_sound is consumed by finite_literal_synthesis and the actual full-fiber candidate application; zero_call_literal is consumed by zero_budget_endpoint and its Reg family. Public visibility contributes no new mathematical content.

Static forced-successor contraction

The firstClass traversal is reused with its original hole identities and below-hole flag. Literal_geometry establishes two exhaustive implications. An exterior result inl(z) gives readout(a,evaluateRow(f,C))=z for every filling f, including arbitrary fillings not in the actual image. A hole result inr(d,below) gives an actual physical occurrence p of d and a suffix w with a=p++w, rowAt(p,C)=hole(d), and below exactly when w is nonempty. This includes visible ancestors, concrete leaves, blocked cones and absent extensions.

A running state survives exactly when its word enters a hole. Halts are always retained. For removed states the forced successor is M.next(s,z), where firstClass supplies the exterior reply z. ContractCode is a single finite static map on the entire installed carrier. It returns the first surviving running state or original halt along forced successors; when no exit exists it returns one fixed original halt z0. The public original skip_exact, skip_retained and skip_removed suppliers provide the finite first-exit facts. Their finite-orbit machinery identifies a nonexiting finite basin with eventual repetition. Every state of that basin has the same completion z0.

The exitAdapter only instantiates the existing finite first-exit proof. Its predicate labels and empty decoder are proof data, never an installed state, cache, field, service or query. No cached-observer normalization theorem is applied to a native run. Only the exact finite first-exit primitives are reused, under their own finite carrier assumptions.

A terminating Run on any filled row cannot start in or reach a nonexiting forced basin: induction on that exact Run gives a finite first exit. This also applies when the exported initial state is removed. Different inputs may still use opposite edges of a shared cycle; the argument excludes only a forced constant cycle on one required input.

Contract installs the surviving subtype of the original running carrier together with every original halt. Surviving addresses and all halt outputs are unchanged; next(s,z) is ContractCode(M.next(s,z)). It does not clone histories or add a state. The export is actually replaced before entry by ContractCode composed with the original acquired code. This changes the exported code itself and retains no copy of the old code. An initial forced chain ending at a halt initializes that halt directly; no post-entry silent step, phase or extra field is introduced.

Contract_run proves the exact filtered original successful Run, ending at the identical original halt. Its first conjunct is the live transfer input. The separate run_exit basin-exclusion proof supplies its second conjunct, which the main transfer projects away; basin exclusion remains an independently required source conclusion. SurvivingTrace deletes exactly the removed running visits and retains their order. Each next edge jumps across the intervening forced segment. Thus calls and submitted words are precisely the surviving calls and words of the same original input. Filtered_resources bounds both its length and its sum by the corresponding original quantities. The code image is an image of the old code image, and the surviving carrier is a subtype, so neither cardinality increases. The arbitrary nonexiting-basin completion is used on no required path.

Joint bounds from one truthful padded origin

For nonempty classes, apply paid_native_recode to the contracted table. Its installedWordBound takes the maximum over every installed surviving address, including unused states. Existing simultaneous actual-image padding selects values(theta) and origins(theta) preserving the complete exterior, injectivity, all repetitions, exact root type and complete target. Branch-valued classes are deeper than that finite menu bound. This is a bound on the chosen table, not a restriction on the original fiber.

At each surviving state write its word as p++w at its first entered hole, with class d. Reuse classReply: an empty suffix forwards the root reply; a proper suffix maps alpha and beta to absent and branch to branch on padded inputs. The unreachable absent root argument may be filled arbitrarily. The root table uses the same surviving states and original halts, with next(s,classReply(z)); the coloring selects the contracted truthful export on the one padded actual origin for theta.

The existing paid_native_recode equality holds for every fuel and entry and retains the halt and entire state list. The root path therefore equals the contracted native path on this same selected actual origin. For each visit, price(d) is at most length(p), which is at most length(p++w). Paid_price_le sums these inequalities on that common path. Its physical-prefix premise is the new literal_geometry law; after expansion of the same-delivery helpers this is content, while the subsequent minimum and sum algebra reuse existing suppliers. Its call bound and literal bound both compare to that same original native input after filtering. No independently optimized origins or marginal maxima are combined. Shared states, convergence and different-input union cycles require no history expansion.

Shortest installation on every original origin

InstallShortest changes only the physical address at a root state to shortest(C,coord(s)); carriers, four transitions and fixed complete outputs remain the original root fields. Shortest_read applies rowAt_evaluate to the actual hole occurrence. Actual_address_geometry then identifies the reply with the class root for every filling, and hence every original actual origin, including arbitrarily shallow or deep branch values. The native and root evaluator results, visits and halt agree on that source, and nativeCost equals rootCost term by term.

The producer inspects its acquired class terms, computes their root types and really exports exportCode(c,v) before the cut. Install_full_fiber supplies exact equality between this actual code range and the attained coloring range, using full chart attainability; no separate color register or discarded source value remains accessible. The whole target identity includes the inverse exterior, canonical restricted partition, all disequalities and every predecessor guard. The sufficient construction is not restricted to padded witnesses.

If there are no classes, the existing shared_moore_feasibility empty branch supplies the one complete target and one halt. A root table cannot have any running state because its coordinate would inhabit the empty class type; every trace is empty and both costs vanish. The resources r=K=1 and q=ell=0 satisfy all stated upper budgets. The transfer preserves upper resources; it asserts neither fixed arbitrary encoder performance nor equality with the original uncontracted native trace.

Finite shared-table consumer

SynthesizeLiteral searches precisely NativeSharedMooreSynthesis.boundedCandidates(C,K). LiteralCheck first applies the original check for actual code-image size, bounded termination and whole output. For every attained theta it evaluates that same candidate path and checks rootCost at most ell. A running state after q calls fails even at price zero; early or initial halts succeed. Repeated queries are charged again. There is no global acyclicity requirement and no new enumeration or evaluator.

Weighted_carrier_complete reuses candidate_complete and evaluate_reindex through their public original declarations. It reindexes both arbitrary finite carriers by Fintype.equivFin and retains all installed states. Coordinate prices commute with the inverse running-state equivalence, so mapping the exact trace preserves its literal sum. Whole outputs outside outputList are replaced by one attained target only at unused halts; a reached halt already has its correct attained output. Every actual run, code range bound, state count, call count and literal sum survives. The existing unweighted existential alone is not used as a literal certificate.

Literal_candidate_sound installs the actual accepted candidate, its shortest physical words and its acquired export on the entire original fiber. Finite_literal_synthesis consumes literal_moore_feasibility in the converse: contract and recode a native witness, put that root witness into the same bounded finite universe, and use the additional literal check. Thus a positive finite answer gives an acquired encoder and one stationary shared table under the supplied services. No arbitrary program extraction or physical-resource certification follows.

Zero calls, zero letters and edge cuts

Write m=targetCount(C), the cardinality of the entire attained predecessor-output image, equal to the actual full-fiber output image by target factorization and chart attainability. The existing complete_output_lower and zero_call_endpoint own the complete-output halt lower bound and exact zero-call criterion. The zero-call part directly applies that supplier: at q=0 the evaluator starts at a halt, so its trace and literal sum are zero. Conversely the same m complete-output halts with m actual initial codes suffice with both costs zero.

If the root is outside P, every shortest occurrence belongs to P by canonicalRow_reached and therefore has positive length. Zero literal sum then forces the root trace empty. Evaluate_exact gives the same halt at fuel zero, reducing to the existing zero-call endpoint. If the root belongs to P, prefix freedom forces P to be the singleton root; its canonical row is hole zero and its whole predecessor target count is one. The one-halt construction works at both zero budgets. Empty cuts and entirely blocked cuts have no reached classes and constant target; all blocked guards remain in the complete installed output. Zero_budget_endpoint states the iff for q=0 or ell=0 with the other upper budget arbitrary.

The entire right-hole fiber

Take P={R}, current row C=pair(beta,hole zero). Its current trees are exactly pair(beta,x). For a leaf origin only beta works, with image pair(beta,alpha). For a paired origin pair(s,z), equality of its left image with beta and the existing substitution inverse force s=alpha; every finite z works. Equivalently the entire origin fiber is beta together with pair(alpha,z) for all finite z, without a selected-source or size restriction. NativeCutFibers.recover_fill and legal_values_row give the two full-row directions; the injectivity component of SourceTransportCentralizer.source_transport_centralizer identifies the left predecessor. Pair_image and no_alpha retain the original actual image grammar.

The whole predecessor at beta is Y0=concrete beta, with R blocked at that concrete root and empty reached partition. At pair(alpha,z) it is Y1=pair(alpha,hole zero), with singleton reached partition {R}. Their guards and partitions are not replaced by two bare output labels. The current right value is alpha at beta and rho(z) at every paired origin. Taking z=alpha gives beta and z=beta gives branch, so all three class-root types are attained. No paired origin has alpha at the current right root, by no_alpha. The shortest occurrence is R and its price is one.

RightHoleInput is the first real literal checker input. It has one running state querying the sole class, two whole-output halts Y0,Y1 and one constant initial code. Alpha selects Y0; beta and branch select Y1; the absent edge uses an existing halt. LiteralCheck at r=1,q=1,ell=1 accepts, with exactly three installed states. Literal_candidate_sound applies that certificate on every original origin. The mathematical table is installed with the physical word R, so each actual path makes one call and pays one letter.

For any K,q, r=1 and ell=0 are impossible on this same entire fiber. Every actually invoked native word would have to be empty; its reply is branch on every current tree. The common initial state and deterministic stationary transition then force the same terminating path and halt at beta and pair(alpha,alpha), whose whole predecessor rows differ. Equivalently the compiled zero_budget_endpoint gives m=2, contradicting r=1. This uses the entire-fiber contract and imposes no state or call bound beyond the given finite K,q.

EmptyThenRight has two running states, querying the empty word and R respectively, plus the same two original whole-output halts. The initial empty query always goes to the R state; every actual run has two calls and sum 0+1=1, and every installed state is reached on some actual input. It uses budgets (1,4,2,1). In the original paidTable the first exterior-constant query is actually paid at the only root coordinate and ignored; the second asks that coordinate again. The unchanged two-state visit list therefore costs 1+1=2. ContractCode removes exactly the initial empty-word state and exports the surviving R-state code before entry. The retained three-state run costs one. This is the strict failure of unchanged-path literal domination; the four-upper-budget correspondence still holds.

Suppliers, attribution and limits

The attained chart is Proposition 10.2; the entire predecessor factorization is Theorem 10.4; simultaneous actual-image padding is Proposition 10.5. Their original suppliers are Retained Literal Root Depth Theorem 2.2 and Transport–Memory Completion RA.2207. Definitions 12.1–12.2 own the stationary state-only table and acquired code normalization. Theorem 12.3 supplies the hole-entering response map and its paid constant case; Proposition 13.5 identifies that case’s literal boundary. Serial Joint Resource Frontier Lemma 3.4 owns the shortest physical-occurrence convention without class renaming.

Native Signed Feasibility Proposition 7.4 and Theorem 8.1 and Atomic Block Conjugacy sections 6.2–6.4 already treat same-source literal charges, cleanup or weighted protocol trees in their own contracts; none supplies this installed-state bound. No cached-reply execution or history expansion preserves K here. The cached observer is only a proof adapter for the finite first-exit primitives, whose distinct cache, fee and entry assumptions are not imported as native operational premises.

Mehryar Mohri, Weighted Automata Algorithms, section 6.1, Theorem 4 and algorithm, author PDF pages 21–22 (https://cs.nyu.edu/~mohri/pub/hwa.pdf), assumes complete semirings and computable closures and keeps state set Q. Randal E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers C-35(8), pages 677–691, DOI 10.1109/TC.1986.1676819, Definition 5 and section 4.2, author PDF pages 5,10–11 (https://www.cs.cmu.edu/~bryant/pubdir/ieeetc86.pdf), treats ordered acyclic Boolean graphs. These inspected planning sources are structural precedents, not premises about paid native calls, acquired exports, forced-cycle basins or full-fiber four-budget feasibility. Mathlib epsilon-NFA acceptance equality likewise supplies none of those source/export/state/literal obligations.

This is a source-specific composition of mature finite-graph methods with actual one-image and shortest-occurrence suppliers, consumed by the per-attained-input literal checker on the existing shared universe. No exhaustive absence or global novelty claim is made. Encoder/controller reselection and upper budgets are essential. Prescribed encoder performance, exact original graphs or call counts, unchanged original native traces, arbitrary extraction and physical certification remain outside the claim. No extra update or observation service is supplied.

Theorem 1.1 (Exact four upper budgets).

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/FiniteMenu/NativeLiteralMoore.literal_moore_feasibility (✓ std3). ∎

Source. Repository-derived.

Commentary.

The iff is on the original complete actual fiber. The necessity construction deletes exterior-constant states, composes the actual pre-cut export with one static map, and then uses the existing truthful common-path padded recoding. Sufficiency installs shortest actual words on every original origin. All four inequalities are simultaneous.

Theorem 1.2 (Finite shared-table criterion).

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/FiniteMenu/NativeLiteralMoore.finite_literal_synthesis (✓ std3). ∎

Source. Repository-derived.

Commentary.

The executable boolean is the literal check on the existing boundedCandidates universe. The proof transports actual running-state lists and their prices under arbitrary finite carrier renaming and retains complete unused-output normalization. The passing candidate itself has full-fiber soundness.

Theorem 1.3 (Both zero-budget iff endpoints).

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/FiniteMenu/NativeLiteralMoore.zero_budget_endpoint (✓ std3). ∎

Source. Repository-derived.

Commentary.

For either zero upper budget, feasibility is exactly targetCount at most both the export and total-state budgets. The other upper budget is arbitrary. Prefix freedom handles a root cut; positive physical prices handle every nonroot cut, including empty or blocked supports.

References