PRCDoubledTraceHypotheses
plain-language theorem explainer
Five axioms a doubled-trace map T on ratio orbits must obey to come from a native PRC cost: reciprocal symmetry, normalization invariance, the d'Alembert (RCL) identity, unit calibration T(1)≃2, and matching the native doubled cost at 2. Uniqueness and coherent-root arguments cite this bundle as the working hypothesis package. It is a Prop structure, not a proved statement.
Claim. A map $T$ from ratio orbits to ratio orbits satisfies the doubled-trace hypotheses when: (i) $T(q)$ is cross-equivalent to $T(q^{-1})$ for every $q$; (ii) $T(q)$ is cross-equivalent to $T$ of the normalized ratio of $q$; (iii) $T$ obeys the native d'Alembert identity $\mathrm{crossEq}\bigl(T(xy)+T(x/y),\,T(x)\,T(y)\bigr)$ for nonzero $x,y$; (iv) $T(1)$ is cross-equivalent to $2$; (v) $T(2)$ matches the native doubled-cost evaluation at $2$.
background
In the Primitive Recognition Calculus, ratios live as RatioOrbit displays: a signed-orbit numerator over a nonzero distinction-nat denominator. Equality of displays is not raw identity but crossEq, the internal cross-multiplication relation (K4.10): two orbits match when scaled numerators balance as signed orbits. Reciprocals and normalization act on these displays before any real embedding.
A native cost $F$ is lifted to a doubled trace $T_F=2(F+1)$. Under that change of variable the Recognition Composition Law becomes the native d'Alembert equation on $T$: the sum of traces at $xy$ and $x/y$ is cross-equivalent to the product of the traces. The module packages exactly the axioms needed so that such a $T$ behaves like the doubled trace of a native PRC cost.
Upstream, reciprocal is the orbit-level inverse (and the ledger reciprocal event), and normalization is the canonical reduction of a ratio orbit. Those enter the first two fields of the structure.
proof idea
No proof: this is a structure ... : Prop bundling five fields. Each field is a named hypothesis on a map $T:\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$. The d'Alembert field is the sibling predicate that restates RCL after $T_F=2(F+1)$. Downstream theorems inhabit the structure by refine { reciprocal := ?_, ... } and discharge each field from native-cost hypotheses.
why it matters
This is the working hypothesis interface for the doubled-trace uniqueness track in PRC native-cost uniqueness. The first consumer proves that every native cost $F$ induces a doubled trace satisfying the bundle. Coherent-root and zero-calibrated root targets quantify over maps obeying these hypotheses and ask for a multiplicative ratio character whose trace realizes $T$. Cross-equivalence respect theorems also take the bundle as input and conclude that $T$ respects crossEq once normalization is canonical.
Framework-wise the d'Alembert field is the RCL (Recognition Composition Law) in doubled-trace coordinates, the same functional equation that forces J-uniqueness (T5) in the forcing chain. Unit and two-point calibrations pin the affine gauge so the character lift can recover the native cost, not merely an unnormalized solution of RCL. Open blockers downstream are the coherent-root and linear-root targets that still sit above this interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.