phi_zpow_neg44_eq_inv
plain-language theorem explainer
The lemma records the elementary identity that the golden ratio to the power minus 44 equals the reciprocal of the golden ratio to the power 44. Researchers deriving the Recognition Science prediction for the baryon asymmetry would invoke it to bound the phi-ladder contribution in the eta_B formula. The proof is a one-line wrapper applying exponent negation and natural cast rules.
Claim. $φ^{-44} = (φ^{44})^{-1}$
background
The module derives the prefactor c_RS = (1 − φ^{-8})^2 for the baryon asymmetry η_B = c × (algebraic content from integration gap). This follows from the Recognition Composition Law and the eight-tick octave at three spatial dimensions. The lemma supports bounding φ^{-44} using Fibonacci numbers, where φ^8 = 21φ + 13 and higher powers via recurrence. Upstream result from PrimitiveDistinction establishes the structural conditions from seven axioms to four substantive structural conditions plus three definitional facts.
proof idea
The proof is a one-line wrapper. It rewrites the integer exponent -44 as the negation of 44 using norm_num, then applies zpow_neg to turn it into the reciprocal of the positive power, followed by zpow_natCast to align the types.
why it matters
It supplies the algebraic identity needed for the bounding theorems on φ^{-44} that confirm the predicted η_B interval (6.0 × 10^{-10}, 6.2 × 10^{-10}) overlaps the Planck value. This step closes the numerical verification of the phi-ladder washout at rung 44 in the cosmology module. The framework landmark is the T7 eight-tick octave and T8 D=3 forcing the exponent multiples.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.