K
plain-language theorem explainer
K is defined as the positive square root of the golden ratio phi. Workers on RS constants, causality reachability, or defect distances cite this when scaling ballP steps or bounding quasi-triangle failures. The declaration is a direct noncomputable assignment that inherits phi from sibling definitions in the same module.
Claim. Let $K = ϕ^{1/2}$, where $ϕ$ is the golden ratio fixed point.
background
The Constants module opens with the statement that the fundamental RS time quantum is τ₀ = 1 tick. K supplies a dimensionless bridge ratio built from phi, the self-similar fixed point obtained in the forcing chain. The single upstream dependency is the curvature functional K(λ) = λ²/λ_rec² − 1 from LambdaRecDerivation, retained for compatibility but distinct from the present constant.
proof idea
The declaration is a direct noncomputable definition that evaluates phi to the power 1/2.
why it matters
K is referenced by forty downstream declarations, among them defectDist_no_global_quasi_triangle (Proposition 2.6) in CostAlgebra and the family of ballP, inBall, and reach_mem_ballP lemmas in Causality.BallP. It therefore supplies the scaling factor required for reachability predicates and for the global non-existence of a uniform quasi-triangle constant. The definition closes the link between the T6 phi fixed point and concrete applications such as photobiomodulation energy bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.