golden_rule
plain-language theorem explainer
The symmetry J(r) = J(1/r) for positive recognition ratios r formalizes the golden rule inside the Recognition Science ethical framework. RS philosophers cite it to equate reciprocity with invariance of the J-cost under inversion. The proof is a one-line wrapper that applies the Jcost_symm lemma from the Cost module.
Claim. For every real number $r > 0$, the J-cost satisfies $J(r) = J(r^{-1})$.
background
J-cost is the recognition cost induced by a multiplicative recognizer, given by derivedCost on the comparator. In the EthicsFromJCost module the framework asserts that an action is ethical precisely when it does not raise J on the agent's ledger and avoids asymmetric costs on others. The module states: 'the golden rule is equivalent to the symmetry of J: J(r) = J(1/r)'. Upstream, the lemma Jcost_symm asserts Jcost x = Jcost x^{-1} for x > 0 and is proved by rewriting to the squared form followed by field_simp and ring.
proof idea
This is a one-line wrapper that directly invokes the Jcost_symm lemma from the Cost module, supplying the positivity hypothesis hr.
why it matters
The theorem supplies the golden_rule field inside the EthicsCert structure, which also records that five ethical frameworks exist and that Jcost 1 = 0. It realizes the module claim that the golden rule follows from J-symmetry, linking the philosophy tier to the foundational cost definitions and the multiplicative recognizer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.