cLagLock
plain-language theorem explainer
The definition assigns the locked lag constant the value phi to the negative fifth power in RS-native units. Researchers deriving coherence energies, reduced Planck constants, or Einstein kappa from Recognition Science would cite this when matching scales to the phi fixed point. The assignment is a direct power expression with no lemmas or reductions applied.
Claim. The canonical locked lag constant is given by $C_{lock} = phi^{-5}$ in the real numbers, where $phi$ denotes the golden ratio fixed point of the J-cost function.
background
The Constants module works in RS-native units where the fundamental time quantum satisfies tau0 = 1 tick. The golden ratio phi is the unique real number greater than one that arises as the self-similar fixed point under the J-uniqueness relation J(x) = (x + x^{-1})/2 - 1. Sibling declarations establish phi_pos, phi_gt_onePointFive, and phi_irrational to support exponentiation and ordering.
proof idea
This is a direct noncomputable definition that sets the real value to phi raised to the power of negative five. No tactics, lemmas, or reductions are invoked; the expression is the body of the def.
why it matters
The constant supplies the coherence energy scale E_coh and enters the definition of hbar = cLagLock * tau0, which is then used in kappa_einstein_eq and the Planck gate identity. It realizes the Phase 2 claim that E_coh equals phi^{-5} and aligns with the T5 J-uniqueness and T7 eight-tick octave landmarks. Downstream results such as hbar_eq_phi_inv_fifth and planck_gate_identity depend on it to close the constant matching.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.