costCompose_zero_left
The cost composition operation satisfies 0 ★ a = 2a for every real a. Researchers deriving algebraic properties of the J-cost structure in Recognition Science cite this identity when proving the ★-magma has no identity element. The proof is a direct unfolding of the binary operation definition followed by ring normalization.
claimFor all real numbers $a$, $0 ★ a = 2a$, where the operation is defined by $a ★ b := 2ab + 2a + 2b$.
background
In the CostAlgebra module the binary operation ★ is introduced by the definition costCompose(a, b) := 2ab + 2a + 2b. This formula is induced by the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y), which encodes how J-costs combine under multiplication of ratios. The upstream declaration costCompose supplies the explicit algebraic expression and the infix notation used throughout the module.
proof idea
The proof is a one-line wrapper that unfolds the definition of costCompose and applies ring_nf to simplify the resulting polynomial expression.
why it matters in Recognition Science
This identity is invoked in the downstream theorem costCompose_no_identity to establish that the nonnegative ★-magma possesses no identity element. It supplies a basic algebraic fact required for the cost algebra that sits inside the Recognition framework and ultimately feeds the forcing chain from the RCL through the phi-ladder to the derivation of three spatial dimensions.
scope and limits
- Does not establish the symmetric right-zero identity a ★ 0 = 2a.
- Does not assume or enforce nonnegativity of a.
- Does not connect directly to the definition of the J function.
- Does not address associativity or commutativity of ★.
formal statement (Lean)
136theorem costCompose_zero_left (a : ℝ) : (0 : ℝ) ★ a = 2 * a := by
proof body
Term-mode proof.
137 unfold costCompose
138 ring_nf
139