Trajectory Code-Ledger Covariance

Abstract

Legal normalized trajectories have unique coordinates and code-ledger identity.

Theorem 1.1 (Legal trajectories have unique codes and binary identity).

$$\forall Rules\in \mathrm{Type}\left(\right),Ledger\in \mathrm{Type}\left(\right),events\in \mathrm{Nat}\left(\right)\to \mathrm{PrimeAxisTable}\left(\right),trajectory\in \mathrm{Nat}\left(\right)\to \mathrm{CodeLedgerState}\left(\mathrm{Prod}\left(Rules,Ledger\right)\right),coordinateStep\in \left(\forall t\in \mathrm{Nat}\left(\right),\mathrm{coordinate}\left(\mathrm{trajectory}\left(t+1\right)\right)=\mathrm{normalizedPrimeAxisAdd}\left(\mathrm{coordinate}\left(\mathrm{trajectory}\left(t\right)\right),\mathrm{events}\left(t\right)\right)\right),ruleStep\in \left(\forall t\in \mathrm{Nat}\left(\right),\mathrm{rule}\left(\mathrm{ledger}\left(\mathrm{trajectory}\left(t+1\right)\right)\right)=\mathrm{rule}\left(\mathrm{ledger}\left(\mathrm{trajectory}\left(t\right)\right)\right)\right),\left(\forall t\in \mathrm{Nat}\left(\right),\left(\forall p\in \mathrm{PrimeAxis}\left(\right),\mathrm{CanonicalRaw}\left(\mathrm{digits}\left(\mathrm{coordinate}\left(\mathrm{trajectory}\left(t+1\right)\right),p\right)\right)\wedge \mathrm{rawValue}\left(\mathrm{digits}\left(\mathrm{coordinate}\left(\mathrm{trajectory}\left(t+1\right)\right),p\right)\right)=\mathrm{rawValue}\left(\mathrm{digits}\left(\mathrm{coordinate}\left(\mathrm{trajectory}\left(t\right)\right),p\right)\right)+\mathrm{rawValue}\left(\mathrm{digits}\left(\mathrm{events}\left(t\right),p\right)\right)\right)\wedge \mathrm{decodePrimeAxisTable}\left(\mathrm{coordinate}\left(\mathrm{trajectory}\left(t+1\right)\right)\right)=\mathrm{decodePrimeAxisTable}\left(\mathrm{coordinate}\left(\mathrm{trajectory}\left(t\right)\right)\right)\cdot \mathrm{decodePrimeAxisTable}\left(\mathrm{events}\left(t\right)\right)\right)\wedge \left(\left(\forall t\in \mathrm{Nat}\left(\right),left\in \mathrm{PrimeAxisTable}\left(\right),right\in \mathrm{PrimeAxisTable}\left(\right),\left(\left(\forall p\in \mathrm{PrimeAxis}\left(\right),\mathrm{CanonicalRaw}\left(\mathrm{digits}\left(left,p\right)\right)\wedge \mathrm{rawValue}\left(\mathrm{digits}\left(left,p\right)\right)=\mathrm{rawValue}\left(\mathrm{digits}\left(\mathrm{coordinate}\left(\mathrm{trajectory}\left(t\right)\right),p\right)\right)+\mathrm{rawValue}\left(\mathrm{digits}\left(\mathrm{events}\left(t\right),p\right)\right)\right)\wedge \mathrm{decodePrimeAxisTable}\left(left\right)=\mathrm{decodePrimeAxisTable}\left(\mathrm{coordinate}\left(\mathrm{trajectory}\left(t\right)\right)\right)\cdot \mathrm{decodePrimeAxisTable}\left(\mathrm{events}\left(t\right)\right)\right)\Rightarrow \left(\left(\left(\forall p\in \mathrm{PrimeAxis}\left(\right),\mathrm{CanonicalRaw}\left(\mathrm{digits}\left(right,p\right)\right)\wedge \mathrm{rawValue}\left(\mathrm{digits}\left(right,p\right)\right)=\mathrm{rawValue}\left(\mathrm{digits}\left(\mathrm{coordinate}\left(\mathrm{trajectory}\left(t\right)\right),p\right)\right)+\mathrm{rawValue}\left(\mathrm{digits}\left(\mathrm{events}\left(t\right),p\right)\right)\right)\wedge \mathrm{decodePrimeAxisTable}\left(right\right)=\mathrm{decodePrimeAxisTable}\left(\mathrm{coordinate}\left(\mathrm{trajectory}\left(t\right)\right)\right)\cdot \mathrm{decodePrimeAxisTable}\left(\mathrm{events}\left(t\right)\right)\right)\Rightarrow left=right\right)\right)\wedge \left(\left(\forall i\in \mathrm{Nat}\left(\right),j\in \mathrm{Nat}\left(\right),\mathrm{rule}\left(\mathrm{ledger}\left(\mathrm{trajectory}\left(i\right)\right)\right)=\mathrm{rule}\left(\mathrm{ledger}\left(\mathrm{trajectory}\left(j\right)\right)\right)\right)\wedge \left(\left(\forall i\in \mathrm{Nat}\left(\right),j\in \mathrm{Nat}\left(\right),\mathrm{trajectory}\left(i\right)=\mathrm{trajectory}\left(j\right)\iff \left(\mathrm{canonicalCode}\left(\mathrm{trajectory}\left(i\right)\right)=\mathrm{canonicalCode}\left(\mathrm{trajectory}\left(j\right)\right)\wedge \mathrm{stateLedger}\left(\mathrm{ledger}\left(\mathrm{trajectory}\left(i\right)\right)\right)=\mathrm{stateLedger}\left(\mathrm{ledger}\left(\mathrm{trajectory}\left(j\right)\right)\right)\right)\right)\wedge \left(\left(\forall i\in \mathrm{Nat}\left(\right),j\in \mathrm{Nat}\left(\right),\mathrm{canonicalCode}\left(\mathrm{trajectory}\left(i\right)\right)\ne \mathrm{canonicalCode}\left(\mathrm{trajectory}\left(j\right)\right)\Rightarrow \mathrm{trajectory}\left(i\right)\ne \mathrm{trajectory}\left(j\right)\right)\wedge \left(\forall i\in \mathrm{Nat}\left(\right),j\in \mathrm{Nat}\left(\right),\mathrm{trajectory}\left(i\right)=\mathrm{trajectory}\left(j\right)\Rightarrow \mathrm{canonicalCode}\left(\mathrm{trajectory}\left(i\right)\right)=\mathrm{canonicalCode}\left(\mathrm{trajectory}\left(j\right)\right)\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Dynamics/TrajectoryCodeLedgerCovariance.legal_trajectory_code_ledger_covariance (✓ std3). ∎

Source. Repository-derived.

Commentary.

A legal event and every state coordinate use the existing finitely supported canonical prime-axis table. The trajectory advances by the existing rowwise normalizer. The theorem states both that its actual next coordinate satisfies the canonical axiswise sum and decoder law, and that any two coordinates satisfying those laws are equal. Thus stepwise uniqueness is not encoded by defining a witness to be the desired result.

The ledger carrier is a rule coordinate paired with the remaining ledger state. Adjacent preservation is iterated to prove that the rule is constant across the orbit. Applying the frozen code-ledger identity theorem then removes that fixed coordinate and yields the binary criterion. The two stated consequences, code change forcing state change and state equality forcing code equality, are exposed separately.

Pinned library searches found generic unique-existence, equivalence injectivity, and product extensionality, but no trajectory theorem on the repository’s prime-axis and ledger carriers. The proof instead composes the frozen unique-normalization and code-ledger declarations; it introduces no new carrier or normalization definition.

References

• Truth anchor: D5/S1/Dynamics/TrajectoryCodeLedgerCovariance.legal_trajectory_code_ledger_covariance
• Dependency: D5/S1/Digit/PrimeAxis/PrimeAxisNormalizationUnique
• Dependency: D5/S1/Dynamics/CodeLedgerIdentity