rcl_identity
plain-language theorem explainer
The Recognition Composition Law equates the J-cost of a product and quotient to an expression involving the product and sum of individual J-costs for nonzero reals. Foundation paper F1 researchers cite it to establish geometric-mean minimization and simultaneous versus sequential descent in log-domain geometry. The proof is a direct algebraic reduction: unfold the Jcost definition, clear denominators with field_simp, and verify the polynomial identity by ring.
Claim. For all nonzero real numbers $x$ and $y$, $J(xy) + J(x/y) = 2 J(x) J(y) + 2 J(x) + 2 J(y)$, where $J(z) := ½(z + z^{-1}) - 1$.
background
The module defines the canonical reciprocal cost $J(x) = ½(x + x^{-1}) - 1$ in the log-domain geometry of foundation paper F1. This identity is the Recognition Composition Law (RCL) listed as F1.5.1. It extends core J-cost identities from JcostCore and supports results on geometric-mean optimality and log-domain descent. The local setting is the foundation paper F1, which derives physics from this functional equation and cites the law for applications in NS, P vs NP, Yang-Mills, and RH.
proof idea
The proof introduces auxiliary facts that the product and quotient are nonzero, then unfolds the definition of Jcost. It applies field_simp to clear the denominators under the given nonzeroness hypotheses, and concludes with the ring tactic to verify the resulting polynomial equality.
why it matters
This theorem is the core Recognition Composition Law (RCL) in the F1 foundation paper, directly supporting geometric-mean minimization of total bond cost and the distinction between simultaneous and sequential descent. It aligns with the Recognition Science framework's use of the RCL to derive the phi-ladder and eight-tick octave structure. No open questions are touched here as the identity is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.