Matching Full-Fiber Controllers
Abstract
Six fixed common controllers attain the prescribed export, invocation and total-state counts on the entire actual repeated-partner inverse fiber.
The source domain is the entire infinite NativeSixSourceCones.Fiber. The acquired finite class values are recovered using the exact existing NativeClassRootImage chart. Their six root types give the acquired profile; no query obtains this profile after the access cut. NativeFullRootFeasibility.actual_type supplies precisely its admissibility, and native_full_root_feasibility supplies the whole predecessor-row target. NativeFiniteRootMinimax.finite_root_minimax supplies the executable target equality. The existing admissibleCode_spec is used directly to check the finite admissibility predicate.
The six positions are a,b1,b2,c,b3,b4. Their canonical class ordinals are 0,1,3,4,5,7. The acquired label is j exactly when right class bj has alpha root, and zero otherwise. A finite check of all admissible six-root assignments proves that its old occurrence mask and complete target are exactly holeList(j) and predecessor(j). This check includes arbitrary internal branches: the native chart and target bridge prove that root types suffice for this row. It is not a test of six example sources.
Every installed table has fixed literal addresses and fixed transitions for alpha, beta, branch and absent. All five halts output the complete canonical predecessor rows directly. In the ten-state table a partner state queries LLL; beta leads to the b1,b2 chain, branch leads to the b3,b4 chain, and alpha or absent leads to the zero halt. A right test takes alpha to its named positive halt. Its other replies take the prescribed next state or zero halt. The nine-state table checks b1,b2,b3,b4 sequentially. The eight-state table starts at b1 for labels 0,1,2 and at b3 for labels 3,4; it uses only b1,b2,b3. The seven-state table starts at the zero halt, b1 or b3 for blocks {0},{1,2},{3,4}. The six-state table starts at the corresponding halt for labels 0,1,2, and at b3 for {3,4}. The five-state table starts directly at its output halt.
The original FTC8.2 application uses the separate literal T8 table: Reads D1,D2,D3 have literals LLR, LRR,RLR; D1 sends alpha to H1, beta or absent to H0 and branch to D2; D2 sends alpha to H2 and every other reply to H0; D3 sends alpha to H3, branch to H4 and beta or absent to H0. The five halts H0 through H4 store the complete rows R0 through R4, with original entries e0=D1 and e1=D3 and call bound L=2. This literal T8 is distinct from the public eight-state controller above, whose running-state value is eight.
For every origin in the full Fiber whose substitution has the canonical row, the acquired label selects D1 for Pi1, Pi2 and all seven zero profiles and selects D3 for Pi3 and Pi4. The existing install_correct theorem, with the exact original finite-correctness premise, therefore supplies the entire canonical predecessor row from the selected original entry in at most two native calls on the same stationary source. The quantifier is the whole infinite origin fiber; the eleven profile paths explain the finite table but do not narrow the source domain.
The forced-attainment application quantifies an arbitrary legal finite preparer: every numbered Read or Halt remains available, including unused or duplicate literals, shared states, all four successors, cycles and early halts; its only mutable memory is the current state and its numerical binary cap may be zero. Universal selected-serving success supplies termination within that preparer’s own cap and correctness only for the bit it emits, with no BOTH premise and no requirement on the unselected entry. On the actual Pi1 source, entry one returns the different row R4, so correctness forces bit zero; on the actual Pi3 source, entry zero returns the different row R0, so correctness forces bit one. The existing run_terminal uniqueness result and the predecessor-row disequalities provide the two within-cap witnesses.
The correspondence is entirely to existing carriers: GenealogicalFiberTransport.Source and substitution, NativeSixSourceCones.Fiber and canonicalRow P, the NativeSerialMachine Record/native interpretation, and the original install_correct and run_terminal declarations. These kernel-checked applications establish the native mathematical correspondence and two-call/own-cap consequences. Authentication, acquisition permission, export and isolation, storage, pricing and elapsed physical time remain separately supplied operational conditions.
Theorem 1.1 (Six Exact Attainments).
Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/NativeRepeatedPartnerControllers.matching_controllers (✓ std3). ∎
Source. Repository-derived.
Commentary.
ConstantEntry maps every acquired label to running state zero. Attains asserts exact realized entry range cardinality, correctness and an invocation upper bound on every actual origin, an actual origin attaining that bound, and reachability on actual origins of every running and halting state. The respective finite running types are Fin 5, Fin 4, Fin 3, Fin 2, Fin 1 and Fin 0; every halt type is Fin 5. Hence the exact (capacity,calls,running,halts,total) tuples are (1,3,5,5,10), (1,4,4,5,9), (2,2,3,5,8), (3,1,2,5,7), (4,1,1,5,6), (5,0,0,5,5).
The exported value is the whole entry state. Its realized range is proved equal to a finite set with the stated exact cardinality, so inclusion gives the recoverable complete-entry normalization. The encoder and controller are chosen together from the acquired data. These statements assume genuine acquisition, same-version authentication, lawful export and the access cut; they provide no fixed-arbitrary-encoder guarantee and no physical storage, time, table or address-production equivalence.
All target-zero profiles are included: beta may occur at a, at c, at any bj, or nowhere, while branches can have arbitrary finite internal structure. A partner read is used as a group discriminator only where its actual reply and admissibility justify that transition. The all-fiber proof does not assume that partner queries are target-only group tests. Shared finite states and early halting entries are explicit in the exported-block controllers. The six simultaneous actual origins establish exact range, worst-case and reachability claims; universal correctness comes from the separate actual-profile bridge.