pith. sign in
module module high

IndisputableMonolith.Physics.RecognitionCompositionLawCert

show as:
view Lean formalization →

This module certifies the Recognition Composition Law under the normalization condition J(1) = 0. Researchers deriving the J-cost functional equation or the phi-ladder mass formula would cite it to anchor the RCL axioms. The module imports Cost definitions and structures the certification via sibling lemmas on normalization, symmetry, and positivity.

claimThe Recognition Composition Law holds with normalization $J(1) = 0$, where $J(x) = (x + x^{-1})/2 - 1$ satisfies $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$.

background

The Cost module supplies the J-cost function and its basic properties. Recognition Science derives physics from the single functional equation known as the Recognition Composition Law (RCL). This module certifies the RCL in the Physics namespace, beginning with the normalization statement J(1) = 0 that follows directly from the closed-form expression for J.

proof idea

This is a definition module, no proofs. It organizes certification lemmas (rcl_normalised, rcl_symmetric, rcl_positive, jcost_uniqueness_axioms, RCLCert, rclCert) that establish the normalized RCL from the imported Cost axioms.

why it matters in Recognition Science

The module supplies the normalized RCL that underpins the forcing chain (T0-T8) and the derivation of constants such as hbar = phi^{-5} and the alpha band. It feeds the J-uniqueness step (T5) and the self-similar fixed point (T6) used in downstream mass and dimension derivations.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)