Original coordinates of a passing native image mode

Abstract

Exact epoch transport, canonical original rigidity and executable original prefixes.

An EpochInput I has n original natural parameters, k affine atomic indices, m state names, an optional equation at each name, a head power a(i), the original Presburger guard, and every original actual-image filter. A defined equation is rho to power a(i) of X(i) equal to its stored right side. Expressions contain arbitrary finite grounds, finite parameter atoms with fixed offsets, the explicit Omega token, decorated state occurrences and ordered pairs. A Potential s is a natural tuple satisfying a(i) at most s(i) and s(j) at most b+s(i)-a(i) at each occurrence rho to power b of X(j). These are the natural form of NIS.11 supplied by Theorem 3.3. No semantic identity or inverse is a field of the input.

imageValues(s,v)(i) is rho to power s(i) of v(i). transport(s,t,E) distributes a shift t through finite grounds, token offsets and pairs, replacing an occurrence rho to power b of X(j) by rho to power b+t-s(j) of Y(j). ShiftLegal checks every exponent before its use. commonShift(s) is the maximum of zero and all s(i), computed by a finite fold; it works for every reconstruction and additional filter and is independent of the requested depth and parameters.

Theorem 1.1 (The entire decorated solution relation is transported in both directions).

$$\forall n:Nat,(\forall k:Nat,(\forall m:Nat,(\forall I:\mathrm{EpochInput}\left(n,k,m\right),(\forall s:\mathrm{Fin}\left(m\right)\to Nat,((\mathrm{Potential}\left(I,s\right))⟹(\forall p:\mathrm{Fin}\left(n\right)\to Nat,(\forall w:\mathrm{Fin}\left(m\right)\to CompletionTree,(((\mathrm{Legal}\left(\mathrm{functionalInput}\left(I,s\right),p\right))\wedge ((\mathrm{SourceSatisfies}\left(\mathrm{functionalInput}\left(I,s\right),p,w\right))\wedge (\mathrm{SourcePasses}\left(\mathrm{functionalInput}\left(I,s\right),p,w\right))))⟺(\exists v:\mathrm{Fin}\left(m\right)\to CompletionTree,(((\mathrm{OriginalAdmissible}\left(I,p,v\right))\wedge (\mathrm{imageValues}\left(s,v\right)=w))\wedge (\forall u:\mathrm{Fin}\left(m\right)\to CompletionTree,(((\mathrm{OriginalAdmissible}\left(I,p,u\right))\wedge (\mathrm{imageValues}\left(s,u\right)=w))⟹(u=v)))))))))))))$$

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

Source. Repository-derived.

Commentary.

functionalInput applies the head shift s(i)-a(i) to each defined equation. It retains a state-image filter Y(i) in L at threshold s(i) for every name, including undefined states. An original filter C in L at threshold r becomes transport(s,t,C) in L at threshold r+t with t=commonShift(s). Every occurrence and repetition remains in the list. The affine indices and original legal domain are unchanged. OriginalAdmissible means the original legal domain, every decorated equation, and every original image filter, jointly.

Structural induction proves the literal evaluation identity for transport on every legal shift. Native injectivity recovers the original decorated equations from the shifted equations. The state-image filters provide every actual preimage, and injectivity makes their joint tuple unique. Applying injectivity once more proves both directions for every additional shifted filter. The result concerns entire completed assignments; arbitrary infinite and non-rational values are included.

Theorem 1.2 (Every original reconstruction has its actual common-shift image).

$$\forall k:Nat,(\forall m:Nat,(\forall s:\mathrm{Fin}\left(m\right)\to Nat,(\forall p:\mathrm{Fin}\left(k\right)\to Nat,(\forall v:\mathrm{Fin}\left(m\right)\to CompletionTree,(\forall E:\mathrm{Expression}\left(k,m\right),((\mathrm{evaluate}\left(p,\mathrm{imageValues}\left(s,v\right),\mathrm{transport}\left(s,\mathrm{commonShift}\left(s\right),E\right)\right)=\mathrm{rhoPower}\left(\mathrm{commonShift}\left(s\right),\mathrm{evaluate}\left(p,v,E\right)\right))\wedge (\mathrm{NativeImage}\left(\mathrm{commonShift}\left(s\right),\mathrm{evaluate}\left(p,\mathrm{imageValues}\left(s,v\right),\mathrm{transport}\left(s,\mathrm{commonShift}\left(s\right),E\right)\right)\right))))))))$$

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

Source. Repository-derived.

Commentary.

For every finite native expression E and every original assignment v, the distributed expression is exactly rho to power commonShift(s) of the original evaluation. Its actual-image membership is proved by that original evaluation as witness. This includes zero states, zero shift, mixed pairs, repeated names, arbitrary grounds and the explicit Omega. The expression identity and image membership are conclusions of the syntax induction, rather than assumptions about a reconstruction context.

Theorem 1.3 (The finite guarded evaluator denotes the actual original image).

$$\forall n:Nat,(\forall k:Nat,(\forall m:Nat,(\forall r:Nat,(\forall I:\mathrm{EpochInput}\left(n,k,m\right),(\forall s:\mathrm{Fin}\left(m\right)\to Nat,(\forall valid:\mathrm{Potential}\left(I,s\right),(\forall mode:\mathrm{EffectiveMode}\left(\mathrm{functionalInput}\left(I,s\right)\right),(\forall R:\mathrm{Fin}\left(r\right)\to \mathrm{Expression}\left(k,m\right),(\forall p:\mathrm{Fin}\left(n\right)\to Nat,(\forall passing:\mathrm{holds}\left(\mathrm{originalImageGuard}\left(\mathrm{functionalInput}\left(I,s\right),mode\right),\mathrm{environment}\left(p\right)\right),(\forall i:\mathrm{Fin}\left(r\right),(\mathrm{value}\left(\mathrm{tokenKind}\left(k\right),\mathrm{tokenRank}\left(\mathrm{ranks}\left(\mathrm{base}\left(I\right),p\right)\right),\mathrm{canonicalSolution}\left(\mathrm{canonicalSystem}\left(I,s,mode\right),\mathrm{tokenKind}\left(k\right),\mathrm{tokenRank}\left(\mathrm{ranks}\left(\mathrm{base}\left(I\right),p\right)\right)\right),\mathrm{reconstructionImages}\left(I,s,R,i\right)\right)=\mathrm{rhoPower}\left(\mathrm{commonShift}\left(s\right),\mathrm{evaluate}\left(\mathrm{ranks}\left(\mathrm{base}\left(I\right),p\right),\mathrm{canonicalOriginal}\left(I,s,valid,mode,p,passing\right),R\left(i\right)\right)\right)))))))))))))$$

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

Source. Repository-derived.

Commentary.

presentation is the existing executable root-link normalization of functionalInput, retaining both reconstruction and projection maps. reconstructionImages substitutes its retained reconstruction into the distributed common-shift expression. canonicalSystem fixes each exceptional finite normalized free atom by a ground equation and leaves live free names undefined. Its existing leaf-limit canonicalSolution therefore assigns Omega to live names. Guarded uniqueness identifies this solution with the saturation canonical extension.

Passing is the actual computed originalImageGuard of functionalInput at the same original parameter tuple. The existing exact image-guard theorem supplies legality and every retained filter. The epoch correspondence then supplies canonicalOriginal as the unique original preimage of effectiveCanonical. The displayed equality connects the symbolic finite-forcing and finite prefix APIs to this actual original reconstruction. No rational presentation is required.

Theorem 1.4 (Decidable canonical finiteness, same-parameter rigidity and effective original prefixes).

$$\forall n:Nat,(\forall k:Nat,(\forall m:Nat,(\forall r:Nat,(\forall I:\mathrm{EpochInput}\left(n,k,m\right),(\forall s:\mathrm{Fin}\left(m\right)\to Nat,(\forall valid:\mathrm{Potential}\left(I,s\right),(\forall mode:\mathrm{EffectiveMode}\left(\mathrm{functionalInput}\left(I,s\right)\right),(\forall R:\mathrm{Fin}\left(r\right)\to \mathrm{Expression}\left(k,m\right),(\forall p:\mathrm{Fin}\left(n\right)\to Nat,(\forall passing:\mathrm{holds}\left(\mathrm{originalImageGuard}\left(\mathrm{functionalInput}\left(I,s\right),mode\right),\mathrm{environment}\left(p\right)\right),((\mathrm{OriginalAdmissible}\left(I,p,\mathrm{canonicalOriginal}\left(I,s,valid,mode,p,passing\right)\right))\wedge (\forall i:\mathrm{Fin}\left(r\right),(((\mathrm{IsFinite}\left(\mathrm{evaluate}\left(\mathrm{ranks}\left(\mathrm{base}\left(I\right),p\right),\mathrm{canonicalOriginal}\left(I,s,valid,mode,p,passing\right),R\left(i\right)\right)\right))⟺(i\in \mathrm{finiteReconstructions}\left(I,s,mode,R\right)))\wedge (((i\in \mathrm{finiteReconstructions}\left(I,s,mode,R\right))⟹(\exists g:Source,((\mathrm{evaluate}\left(\mathrm{ranks}\left(\mathrm{base}\left(I\right),p\right),\mathrm{canonicalOriginal}\left(I,s,valid,mode,p,passing\right),R\left(i\right)\right)=\mathrm{embed}\left(g\right))\wedge (\forall v:\mathrm{Fin}\left(m\right)\to CompletionTree,((\mathrm{OriginalAdmissible}\left(I,p,v\right))⟹((\mathrm{EffectiveInMode}\left(\mathrm{functionalInput}\left(I,s\right),mode,p,\mathrm{imageValues}\left(s,v\right)\right))⟹(\mathrm{evaluate}\left(\mathrm{ranks}\left(\mathrm{base}\left(I\right),p\right),v,R\left(i\right)\right)=\mathrm{embed}\left(g\right))))))))\wedge (\forall h:Nat,(\mathrm{originalPrefixProgram}\left(I,s,mode,p,R,h,i\right)=\mathrm{cutoff}\left(h+1,\mathrm{evaluate}\left(\mathrm{ranks}\left(\mathrm{base}\left(I\right),p\right),\mathrm{canonicalOriginal}\left(I,s,valid,mode,p,passing\right),R\left(i\right)\right)\right)))))))))))))))))$$

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

Source. Repository-derived.

Commentary.

finiteReconstructions is the existing finite symbolic pass, applied to canonicalSystem and reconstructionImages. It is executable and independent of p. Native powers preserve and reflect finiteness, so membership decides exactly the finiteness of each canonical original reconstruction. For each finite member the theorem produces one finite Source g equal to that reconstruction and to the reconstruction in every original admissible solution whose shifted assignment belongs to the same projected normalized mode. All such solutions use the same original p.

Only exceptional finite free values are fixed in canonicalSystem. Every original alternative in that mode satisfies these equations; live free states remain unrestricted. Existing symbolic_finite_forcing therefore fixes the common-shift image, and injectivity fixes its original value. This clause does not say that an alternative value of a canonically infinite coordinate is infinite. Symbolic finite inversion with an original-parameter Presburger partition is supplied by NativeFiniteNormalInversion.original_symbolic_finite_value.

originalPrefixProgram runs the existing finite guarded image prefix program at inclusive depth H(t)+h and decodes its result at output cutoff h+1. Pattern d observes addresses of length strictly less than d; hence the image cutoff is H(t)+h+1=H(t)+(h+1). The existing decoder proves equality with the original cutoff for every supplied h and p, including h=0 and t=0. This constructs prefixes offline and asserts no physical inverse port, query cost or uniform runtime bound.

References

• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/Constructor/NativeOriginalReconstructionBridge.canonical_reconstruction_image
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/Constructor/NativeOriginalReconstructionBridge.epoch_solution_correspondence
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/Constructor/NativeOriginalReconstructionBridge.original_classification_rigidity_prefix
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/Constructor/NativeOriginalReconstructionBridge.reconstruction_transport
• Dependency: D5/S3/Arith/FibonacciAtomic/Observer/Constructor/NativeEffectiveImageGuard
• Dependency: D5/S3/Arith/FibonacciAtomic/Observer/Constructor/NativeOriginalCoordinatePrefix