IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCJCost
Defines the J-cost bridge for two-step ratio orbits in the primitive recognition calculus: discrete orbit positions (two, half, onRatioOrbit) map into rationals and reals, landing on the T5 cost J. Uniqueness and kernel modules import it to evaluate native cost on PRC orbits. Structure is definitional scaffolding plus conversion and symmetry lemmas, not a single deep theorem.
claimOn two-step ratio orbits in the primitive recognition calculus, the module introduces orbit positions $2$ and $1/2$, the ratio-orbit embedding, and the real evaluation that recovers the T5 cost $J(x)=(x+x^{-1})/2-1$, together with reciprocal symmetry and normalization invariance of that cost.
background
Primitive recognition calculus works with discrete orbits before continuous physics is recovered. The sibling OrbitEuclidean layer supplies the Euclidean geometry of those orbits; this module specializes to the two-step (ratio) orbit and ties it to cost.
The classical T5 cost is $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$, forced by the Recognition Composition Law. FunctionalEquation supplies the helper lemmas used in the T5 uniqueness argument. Here the same $J$ is reached from PRC data: two/half as orbit positions, rational and real coercions, and onRatioOrbit as the carrier on which cost is evaluated.
Reciprocal symmetry ($J(x)=J(x^{-1})$) and normalization invariance are recorded so later uniqueness proofs can treat the orbit cost as the same functional object as the continuum $J$.
proof idea
Definition-and-coercion module rather than a single proof arc. It introduces two-step orbit positions and ratio-orbit maps, then provides toNat/toRat/toReal bridges so orbit data can be fed to the real-valued $J$-cost. Symmetry and invariance lemmas are short algebraic checks (reciprocal symmetry of $J$, invariance under normalization) that clear side conditions for importers. No deep tactic development lives here; the work is naming the objects and wiring them to Cost.FunctionalEquation and OrbitEuclidean.
why it matters in Recognition Science
Sits on the path from discrete PRC orbits to T5 $J$-uniqueness inside Recognition Science. Downstream, Kernel imports it as part of the PRC core; PRCNativeCostUniqueness uses the orbit-to-$J$ bridge to argue that the native PRC cost is the forced $J$; RationalField consumes the rational coercions when building the field structure on ratio data.
Without this layer, uniqueness would have to re-derive how two-step orbit positions evaluate to $J$ each time. It is the local dictionary between OrbitEuclidean geometry and the FunctionalEquation toolkit that underwrites T5 in the forcing chain.
scope and limits
- Does not prove T5 J-uniqueness; only exposes orbit-level cost maps used by that argument.
- Does not define the full PRC kernel or rational field; those are downstream modules.
- Does not treat continuous paths or higher-period orbits beyond the two-step ratio case.
- Does not derive physical constants or mass formulae; foundation cost wiring only.
used by (3)
depends on (2)
declarations in this module (21)
-
def
twoOrbit -
theorem
twoOrbit_toNat -
def
two -
theorem
two_toRat -
def
half -
theorem
half_toRat -
def
onRatioOrbit -
theorem
onRatioOrbit_toRat -
theorem
onRatioOrbit_toReal_jcost -
theorem
reciprocal_symmetric -
theorem
normalized_invariant -
def
div -
theorem
div_toRat -
def
rclLHS -
def
rclRHS -
theorem
canonical_rcl_surface -
structure
PRCNativeCostHypotheses -
def
PRCNativeCostUniquenessTarget -
theorem
bridge_to_existing_jcost_uniqueness -
structure
PRCJCostCertificate -
theorem
prc_jcost_certificate