primeEulerEvent_target
plain-language theorem explainer
The target index of the recognition event constructed from a prime Euler factor with positive exponent σ is exactly the prime p. Number theorists building arithmetic-to-ledger embeddings cite this when confirming that prime data is preserved as the event index in the forcing ledger. The proof is a direct reflexivity reduction from the event constructor definition.
Claim. For any positive real number $σ$ and any prime $p$, if $E(σ,p)$ is the recognition event whose ratio equals $p^{-σ}$, then the target of $E$ equals $p$.
background
The Concrete Euler Ledger module constructs the first explicit arithmetic-to-ledger bridge in Recognition Science. For positive real exponent σ and finite prime support, it produces a LedgerForcing.Ledger whose recognition events have ratios given by the Euler terms $p^{-σ}$ together with their reciprocals. The prime Euler event itself is the basic object: source 0, target the prime p, ratio $p^{-σ}$, with positivity of the ratio guaranteed by the hypothesis on σ.
proof idea
The proof is a one-line wrapper that applies reflexivity to the target field in the constructor of the prime Euler event.
why it matters
This result anchors the index preservation step in the arithmetic ledger construction, ensuring each prime contributes an event whose target recovers the original prime. It supports the finite Euler ledger objects that deliver double-entry balance, zero net flow, and positive J-costs, forming the concrete bridge object described in the module before any full RSPhysicalThesis claim. The declaration sits inside the forcing chain after the basic RecognitionEvent and LedgerForcing structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.