polarisation_symmetric
plain-language theorem explainer
Symmetry of the J-cost under inversion is recorded for positive reals. Opinion-network modelers invoke it to equate costs at opposing polarisation extremes. The result is obtained by direct appeal to the Jcost_symm lemma from the Cost module.
Claim. For every positive real number $r$, the cost function satisfies $J(r) = J(r^{-1})$.
background
The Sociology.PolarisationFromSigmaCascade module examines opinion networks under sigma conservation and predicts two equilibria: consensus at $J ≈ 0$ and maximal divergence at $J(φ)$ with $J(φ) ∈ (0.11, 0.13)$. The module documentation states that algorithmic curation can push the system across the $J(φ)$ band and that $J$ is symmetric so both extremes carry equal cost. This theorem rests on the Jcost_symm lemma, which states that for $x > 0$, Jcost $x$ = Jcost $x^{-1}$, proved by unfolding the definition and applying field simplification followed by ring.
proof idea
One-line wrapper that applies the Jcost_symm lemma from IndisputableMonolith.Cost, passing the positivity hypothesis hr.
why it matters
It supplies the symmetric field inside the PolarisationCert structure that certifies the two-equilibria prediction. The symmetry aligns with T5 J-uniqueness in the forcing chain, where $J(x) = (x + x^{-1})/2 - 1$, and ensures the phi-ladder treats $r$ and $r^{-1}$ identically. The module notes that this closes the argument that curation drives the system across the $J(φ)$ band without favoring one extreme.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.