Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Finite original values of a passing mode

Abstract

Finite normal native inverses and symbolic values on an original Presburger partition.

Code is the finite free ordered binary tree with natural ranks at its leaves. expand replaces rank n by the native atom T(n) and preserves pairs. A normal code has no pair of primitive children with ranks n+1 and n, at any node. smart collapses exactly this pattern to rank n+2. encode recursively applies smart to the arbitrary finite Source input, including all mixed and repeated subtrees. It computes a normal code whose expansion is the original source.

Theorem 1.1 (Canonical encoding is normal and expands to the same source).

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/Constructor/NativeFiniteNormalInversion.encode_law (✓ std3). ∎

Source. Repository-derived.

Commentary.

The recursive smart constructor preserves normality and expansion. Induction over the entire finite source therefore retains its value, including every mixed and repeated subtree.

Theorem 1.2 (Rank translation expands to the actual native power).

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/Constructor/NativeFiniteNormalInversion.shift_expand (✓ std3). ∎

Source. Repository-derived.

Commentary.

Adding the same natural t to every primitive rank expands to t iterations of the native substitution. Primitive ranks use addition of iterates, and pairs use preservation of pairing. The equation holds for every finite code, including nonnormal codes.

Theorem 1.3 (Unique finite normal inversion on the actual image).

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/Constructor/NativeFiniteNormalInversion.finite_normal_inverse (✓ std3). ∎

Source. Repository-derived.

Commentary.

inverseCode visits every finite code leaf and applies rankInverse, propagating failure and preserving every pair. A successful result D is characterized exactly by shiftCode(t,D)=C, where shiftCode adds t to every leaf. Adding a common t preserves and reflects normality and its exceptional sibling relation. Expansion intertwines that rank shift with the actual native substitution.

For a normal primitive image, the existing actual atomic predecessor theorem supplies its natural inverse rank. For a normal pair image, the existing exact image grammar applies. A terminal alternative would force the normal pair to be primitive, a contradiction; the recursive alternative gives both child images. Induction constructs the successful inverse. Its expansion is the unique finite original. No inverse is applied outside an actual image.

Theorem 1.4 (Exact natural inverse indices, including every boundary).

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/Constructor/NativeFiniteNormalInversion.exact_natural_rank_inverse (✓ std3). ∎

Source. Repository-derived.

Commentary.

rankInverse(0,n) returns n. At a positive requested shift it rejects rank zero and cancels one successor from both inputs otherwise. Induction proves success with q exactly when q+t=n. A successful q exists exactly when t is at most n, and the natural equation has at most one q. This covers n=0, t=0, n=t and n<t without natural truncated subtraction.

Theorem 1.5 (A finite disjoint Presburger partition computes symbolic normal inverses).

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/Constructor/NativeFiniteNormalInversion.symbolic_presburger_inverse (✓ std3). ∎

Source. Repository-derived.

Commentary.

Template is a finite binary code with integer affine expressions at its primitive leaves. templateCode evaluates them at the same integer list xs and converts each to its natural rank. Nonnegative explicitly requires every input index to be nonnegative. normalPartition is a finite binary decision tree: normalize both children, then when both are primitive split on their rank equality a=b+1. The true branch collapses to b+2 and the false branch retains the pair. All other pairs remain. Each path guard is a conjunction of these Presburger equalities or their negations.

Partition.Leaf is a finite type of branch histories. It preserves distinct paths even when their outputs coincide. Exactly one path guard is true at each xs. Induction proves that its output is nonnegative, normal, and expands to the input value. Actual-image membership then supplies the successful finite inverse. inverseTemplate subtracts t in integer affine syntax, and the proof establishes nonnegativity of each resulting natural index. Its evaluated code is exactly the successful inverseCode result. The natural inverse relation is explicitly q+t=n; no natural clipped subtraction defines an inverse.

Theorem 1.6 (The symbolic original finite value is shared in every admissible solution).

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/Constructor/NativeFiniteNormalInversion.original_symbolic_finite_value (✓ std3). ∎

Source. Repository-derived.

Commentary.

I, s and mode are the actual EpochInput, valid potential tuple and computed passing mode from NativeOriginalReconstructionBridge. R contains arbitrary original reconstruction expressions. finiteImageExpressions is the executable symbolic finite pass on the actual normalized common-shift images. Its successful result f is independent of the original parameter tuple. finiteTemplate replaces each finite symbolic residual index by its owning original affine expression plus the fixed offset, retaining arbitrary grounds and mixed pairs. The last token has numerical rank zero and remains the explicit Omega slot in native evaluation; a successful finite symbolic pass never changes Omega into a new free rank.

For every original p at which originalImageGuard passes, the original guard and all affine nonnegativity conditions hold. finiteTemplate at that same p expands to finiteValue(f). The proved canonical reconstruction identity makes this finite image the actual rho to power commonShift(s) of the original coordinate. The displayed finite partition depends only on the stored finite syntax. At its unique active leaf, the guarded inverse template is a normal finite value equal to the canonical original reconstruction and to that reconstruction in every original admissible solution of the same projected normalized mode, at this same original p.

Together with original_classification_rigidity_prefix this supplies the canonical finite/infinite classification, symbolic finite rigidity, and terminating prefixes of Theorem 4.4 for the original reconstruction syntax. The finite Presburger partition handles symbolic inversion rather than enumerating p. Non-rational guarded completed values remain in scope for the infinite prefix clause. No assertion requires a canonically infinite value to stay infinite in another solution, and no physical inverse port, query cost or uniform runtime theorem is asserted.

References