phiPowValueStr
plain-language theorem explainer
This definition computes integer powers of the golden ratio as fixed-decimal strings from a 16-digit rational approximation, inverting for negative exponents. Numerical verification routines in URC audit pipelines cite it to produce reproducible values for curvature and normalization checks. The implementation defines two recursive powering helpers, branches on the sign of the exponent, and delegates formatting to a rational decimal converter.
Claim. Let $r = 16180339887498948 / 10000000000000000$. For integer $k$ and digit count $d$, the map returns the decimal expansion of $r^k$ (or its reciprocal when $k < 0$) to exactly $d$ places after the decimal point.
background
The module supplies minimal pure numeric helpers for rational formatting. The definition hard-codes the rational $r$ for the golden ratio to control rounding in ratio comparisons on the phi-ladder. Upstream results include the power map on primordial spectra, which scales amplitude by wavenumber ratio, and the canonical arithmetic object that supplies a realization-independent Peano surface. The toNat conversion extracts iteration counts from logic naturals, while the continuum bridge identifies Laplacian actions with curvature defects.
proof idea
The definition introduces two recursive helpers for integer and natural powering. It branches on the sign of the input exponent: nonnegative cases raise numerator and denominator directly; negative cases invert by swapping and taking absolute value. The resulting rational is passed to the decimal formatter with the supplied digit count. No external lemmas are invoked; the body is a direct computational construction.
why it matters
The definition feeds the auditItems list that records proven status for eight-tick minimality, gap-45 timing, and Planck normalization. It supplies the reproducible strings required for phi-power evaluations inside the T7 octave and the alpha-inverse curvature pipeline. By remaining fully deterministic and computable it closes a numerical interface between the forcing chain and concrete constant checks without introducing external dependencies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.