SatisfiesCompositionLaw
plain-language theorem explainer
The definition encodes the Recognition Composition Law for a function F from reals to reals. It requires the equality F(xy) + F(x/y) = 2 F(x) F(y) + 2 F(x) + 2 F(y) to hold for all positive x and y. T5 uniqueness proofs in the forcing chain rely on this predicate as the core assumption. The declaration is a direct predicate definition with no computational content.
Claim. A function $F : (0,∞) → ℝ$ satisfies the composition law if $F(xy) + F(x/y) = 2 F(x) F(y) + 2 F(x) + 2 F(y)$ for all $x, y > 0$.
background
This module supplies functional equation helpers for the T5 cost uniqueness proof. The composition law is the Recognition Composition Law (RCL) that any cost function must obey. Upstream results include the reparametrization G(F, t) = F(exp t) that converts the law into an additive form, and the reciprocal automorphism from CostAlgebra that ensures symmetry. The local setting is lemmas supporting the derivation of J as the unique cost satisfying the axioms.
proof idea
This is a direct definition of the predicate. It consists of a universal quantification over positive reals with the stated equality. No lemmas or tactics are applied beyond the definition itself.
why it matters
This definition supplies the composition hypothesis to cost_algebra_unique and cost_algebra_unique_aczel, which conclude that the cost equals J. It is the central equation for T5 J-uniqueness in the forcing chain. The law also appears in PrimitiveCostHypotheses and drives derivations such as composition_law_forces_reciprocity. It aligns with the RCL landmark that forces the self-similar fixed point phi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 2 of 2)
-
Golden-ratio exponent fixes a gravity kernel, then meets 147 galaxies
"Definition A1 (RCL): J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y) for all x,y>0"
-
One golden-ratio curve organizes four periodic-table trends at once
"The model's input cost function J is the unique solution on R_>0 of the functional equation J(xy) + J(x/y) = 2 J(x) J(y) + 2 J(x) + 2 J(y), under the regularity conditions of continuity, normalization J(1)=0, stationarity J'(1)=0, and positive curvature J''(1)>0 ... The unique solution is J(x) = ½(x + x⁻¹) − 1 = cosh(ln x) − 1."