pricing_discriminated
plain-language theorem explainer
Pairing (double-entry) pricing and linear surplus pricing disagree at the triple cover: J(3)/J(2) equals 8/3, not the linear ratio 2. Anyone testing seam-transfer census pricing against a single-column surplus law cites this numeric separation. The proof rewrites the left-hand side by the cover-cost identity and finishes by arithmetic.
Claim. With recognition cost $J(x)=(x+x^{-1})/2-1$, the cost ratio of the triple cover to the double cover is not the linear surplus ratio: $J(3)/J(2)\neq(3-1)/(2-1)$. Equivalently $8/3\neq 2$.
background
Recognition cost of a positive mismatch ratio $x$ is $J(x)=(x+x^{-1})/2-1$, the T5 unique cost. In this module the same $J$ is recovered as the character anomaly of a balanced $2\times 2$ seam transfer: if $\det W=1$ and $W$ has a real eigenvalue $x\neq 0$, reciprocity forces the other eigenvalue $x^{-1}$, and $\mathrm{Tr}(W)/2-1=J(x)$.
Panel Live Bet 2 asks whether pairing pricing can be told apart from linear single-column surplus pricing. At an $n$-fold retrace the linear law predicts cost ratio $(n-1)/(m-1)$ between covers $n$ and $m$; the pairing law (absolute surplus times relative surplus per post) predicts $J(n)/J(m)$. The triple-versus-double comparison is the first numeric discriminator.
proof idea
Short term proof. Rewrite the left-hand side with the cover-cost-ratio identity, which evaluates $J(3)/J(2)$ to the explicit rational $8/3$ coming from the triple-cover pairing (absolute surplus $2$ times relative surplus $2/3$). Then norm_num discharges $8/3\neq 2$. No case splits and no appeal to the balanced-transfer lemmas.
why it matters
Numeric falsifier record for panel Live Bet 2 inside SeamTransferCore (LEG-B Phase B). A measured or derived triple-retrace seam price of $2$ kills the trace carrier; $8/3$ confirms it. The two pricing hypotheses are therefore not observationally equivalent.
Feeds the module certificate that packages Phase B: conjugate forced from unit determinant, character anomaly equals $J$, census pricing reduced to seam-transfer structure, and the elliptic class ruled out as a mismatch carrier. Framework landmark: T5 $J$-uniqueness appears here as an empirical discriminator between census observables, not only as an algebraic identity on the forcing chain. Downstream holography and census arguments rely on this separation so linear surplus cannot masquerade as the double-entry law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.