reciprocity
plain-language theorem explainer
Reciprocity equates the J-cost of any recognition event to the J-cost of its reciprocal event. Ledger derivations in Recognition Science invoke it to obtain paired costs from J-symmetry. The term proof unfolds the cost and reciprocal definitions then invokes J_symmetric on the positive ratio.
Claim. Let $e$ be a recognition event with positive ratio $r$. Then $J(r) = J(r^{-1})$, where $J$ denotes the cost functional.
background
The LedgerForcing module establishes that J-symmetry forces double-entry ledger structure. A RecognitionEvent records source and target agents together with a positive ratio $r$. The event_cost of $e$ is $J(r)$. Upstream, J_symmetric asserts that $J(x) = J(x^{-1})$ for every $x > 0$.
proof idea
The term proof applies simp to unfold event_cost and reciprocal, then invokes J_symmetric on the positive ratio field of $e$.
why it matters
This supplies the second conjunct of ledger_forcing_principle, which chains J-symmetry to paired events, vanishing log-sum, and existence of balanced ledgers with zero total cost. It advances the forcing chain from J-uniqueness (T5) to double-entry structure required for conservation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Score entropy lets diffusion models rival GPT-2 on text
"the ratios pt(y)/pt(x) (which are collectively known as the concrete score) generalizing the typical score function"