SymmUnit
plain-language theorem explainer
SymmUnit encodes reciprocity symmetry under inversion for positive arguments together with normalization at unity for a real function F. Cost analysts in Recognition Science cite it when establishing averaging bounds or Jensen sketches that compare candidate functions to the explicit Jcost. The declaration is a direct class definition introducing the two axioms with no further obligations.
Claim. A function $F:ℝ→ℝ$ satisfies the symmetric-unit axioms if $F(x)=F(x^{-1})$ for every $x>0$ and $F(1)=0$.
background
In the Cost.JcostCore module the Jcost function is constructed from the Recognition Composition Law J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y). The explicit form J(x)=(x+x^{-1})/2-1 (equivalently cosh(log x)-1) automatically obeys reciprocity and vanishes at 1. Upstream results supply concrete realizations of F, including the gap generator log(1+z/φ) from Pipelines and the alias gap(Z) from AnchorPolicy, both of which are shown to meet the same two axioms.
proof idea
This is the definition of the class SymmUnit; it directly records the symmetric and unit0 fields. No lemmas or tactics are invoked; the class serves as the interface that downstream declarations such as AveragingBounds and JensenSketch extend.
why it matters
SymmUnit is the base class extended by AveragingBounds, AveragingDerivation and JensenSketch, which in turn feed the theorems even_on_log_of_symm and F_eq_J_on_pos_alt. It supplies the symmetry axiom required by the T5 J-uniqueness step of the forcing chain and by the eight-tick octave structure. The declaration closes the interface that lets cost models be compared to Jcost without committing to a specific formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.