SymmUnit
plain-language theorem explainer
The SymmUnit class packages the two axioms that any candidate cost function F must obey: invariance under x to 1/x for positive arguments together with normalization at unity. Derivations of averaging bounds and Jensen sketches in the Cost module cite this class to guarantee that concrete realizations such as the gap function or J-cost inherit the required inversion symmetry. As a bare class definition it introduces the fields symmetric and unit0 with no proof obligations or further structure.
Claim. A function $F : ℝ → ℝ$ is called a symmetric unit when $F(x) = F(x^{-1})$ holds for every $x > 0$ and $F(1) = 0$.
background
The Cost module abstracts properties of functions that arise from the Recognition Composition Law and the J-uniqueness property. J-cost is the unique solution to the functional equation J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y) with J(1) = 0; the symmetry axiom follows immediately by substituting y = 1/x. The same class is declared in JcostCore and re-used here so that downstream structures can extend it uniformly. Concrete instances include the gap function F(Z) = log(1 + Z/φ)/log(φ) from AnchorPolicy and the generating functional F(z) = log(1 + z/φ) from Pipelines, both of which satisfy the axioms by direct substitution.
proof idea
This is a class definition with an empty proof body. It simply declares the two fields: the symmetry condition ∀ {x}, 0 < x → F x = F x⁻¹ and the normalization F 1 = 0. No tactics or lemmas are applied.
why it matters
SymmUnit is the base interface extended by AveragingBounds, AveragingDerivation, and JensenSketch, which add the comparison inequalities that relate F to J-cost on the exponential axis. These extensions close the loop from the Recognition Composition Law to the phi-ladder mass formula and the eight-tick octave. The symmetry axiom directly encodes the self-similarity under inversion forced at T5 of the UnifiedForcingChain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.