phi
plain-language theorem explainer
The golden ratio is supplied as the positive real solving x squared minus x minus one equals zero. Researchers modeling self-similar scaling and phi-ladders in Recognition Science cite this constant for rung assignments and mass formulas. The declaration is a direct algebraic assignment using the square root of five.
Claim. $phi = (1 + sqrt(5))/2$
background
The VoxelWalks module introduces discrete path constructions scaled by the golden ratio. Phi is the self-similar fixed point obtained from the J-uniqueness condition in the forcing chain. The definition supplies the numerical value used in subsequent ladder and sigma constructions within the same module.
proof idea
Direct definition that evaluates the closed-form expression for the positive root of the quadratic x^2 - x - 1 = 0.
why it matters
This definition realizes the T6 self-similar fixed point in the T0-T8 forcing chain. It anchors the phi-ladder appearing in mass formulas and the eight-tick octave. Downstream siblings such as sigmaCore and A2 rely on this constant for scaling relations in voxel walks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.