C_xi_pos
plain-language theorem explainer
The positivity of the RS-derived morphology coupling coefficient C_ξ = 2 φ^{-4} follows by unfolding the definition and applying real-number positivity to the constant 2 and the negative power of φ. Galaxy rotation-curve modelers cite the result to guarantee the coupling term stays positive in spatial-profile fits. The proof is a direct term-mode reduction that invokes mul_pos after a single unfold and Real.rpow_pos_of_pos on the upstream phi_pos fact.
Claim. $0 < 2 φ^{-4}$, where φ is the golden-ratio fixed point of the Recognition forcing chain and the exponent -4 is fixed by the RS morphology formula.
background
The GravityParameters module classifies each galactic parameter by its RS status. C_ξ is listed under HAS RS BASIS with the explicit formula 2 φ^{-4} ≈ 0.292, to be compared with the fitted value 0.298 ± 0.015. The module sits atop the phi-ladder construction: φ emerges as the self-similar fixed point (T6) from the J-cost functional equation in PhiForcingDerived.of, while PrimitiveDistinction.from reduces the seven axioms to four structural conditions plus definitional facts. Upstream lemmas such as DAlembert.LedgerFactorization.of and SpectralEmergence.of supply the ledger and spectral scaffolding that justify placing the exponent -4 inside the morphology coefficient.
proof idea
The term proof first unfolds C_xi to expose the product 2 * phi^(-4). It then applies mul_pos to the manifestly positive constant 2 (via norm_num) and to the positive real power phi^(-4), the latter obtained directly from Real.rpow_pos_of_pos applied to the hypothesis phi_pos that φ > 0.
why it matters
The declaration closes the positivity check for the second entry in the module's seven-parameter table, confirming that the RS-basis formula 2 φ^{-4} remains positive and therefore usable in galactic gravity models. It sits downstream of the phi-forcing chain (T5 J-uniqueness through T6 phi fixed point) and is a sibling to the alpha_gravity and p_steepness positivity results. No downstream uses are recorded in the current graph, but the result removes a potential obstruction for any later theorem that invokes C_ξ inside a physical inequality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.