phiInv_pos
Positivity of the reciprocal of the golden ratio is recorded as a basic inequality supporting negative-rung quantities. Applications to decay rates, target ratios, and damping factors cite the result to place 1/φ strictly above zero before further bounds are derived. The proof is a one-line wrapper that unfolds the definition and invokes division positivity.
claimLet φ denote the golden ratio with φ > 0. Then 0 < 1/φ.
background
The CrossDomain.PhiInverseInvariants module treats 1/φ as the canonical attractor for negative-rung quantities including senolytic target ratios, Gini ceilings, amplitude decays, and mixing angles. The upstream definition introduces phiInv explicitly as the real number 1/phi. This positivity statement is required before the module can locate all such quantities inside the open unit interval, consistent with the structural claims that 1/φ < 1 and 1/φ = φ − 1.
proof idea
The proof is a one-line wrapper. It unfolds the definition of phiInv to obtain the division 1/phi, then applies the standard lemma that a positive numerator divided by a positive denominator remains positive, using the facts that 1 > 0 and phi > 0.
why it matters in Recognition Science
The result supplies the positivity field inside the PhiInverseInvariantsCert structure and is paired with the upper-bound lemma to prove all_phiInv_in_unit_interval. It anchors the cross-domain unification of 1/φ-governed phenomena and aligns with the self-similar fixed point phi forced in the Recognition Science chain. No open questions are resolved here; the declaration simply closes the positivity prerequisite.
scope and limits
- Does not compute a numerical approximation to 1/φ.
- Does not prove that 1/φ is the unique attractor.
- Does not extend the inequality beyond the real numbers.
- Does not address convergence speed toward the attractor.
Lean usage
all_phiInv_in_unit_interval := ⟨phiInv_pos, phiInv_lt_one⟩formal statement (Lean)
33theorem phiInv_pos : 0 < phiInv := by
proof body
Term-mode proof.
34 unfold phiInv
35 exact div_pos one_pos phi_pos
36