module module high

`IndisputableMonolith.CrossDomain.PhiInverseInvariants`

This module establishes the canonical value of 1/φ together with its positivity, bounds, and algebraic identities for use across Recognition Science domains. Cross-domain modelers working on decay rates, policy ratios, or biological scaling would cite these results when normalizing quantities to the golden-ratio inverse. The module is a collection of direct definitions and one-line algebraic verifications that follow immediately from the self-similar fixed-point equation for φ.

claimLet φ = (1 + √5)/2. The module defines φ⁻¹ ≔ 1/φ and proves φ⁻¹ > 0, φ⁻¹ < 1, φ⁻¹ < φ, φ⁻¹ = φ − 1, φ⁻² = 2 − φ, φ⁻³ = 2φ − 3, together with the auxiliary functions senolyticTargetRatio, giniCeiling, policyBalance, stemCellDecay, and circadianDecay that embed these invariants.

background

Recognition Science obtains φ as the unique positive fixed point of the self-similar map arising from the J-cost functional J(x) = (x + x⁻¹)/2 − 1. The upstream Constants module supplies the RS-native time quantum τ₀ = 1 tick, which sets the dimensional scale on which all subsequent φ-powers are expressed. The present module isolates the inverse φ⁻¹ and records the elementary relations that follow from φ² = φ + 1, making these relations available as reusable invariants for cross-domain constructions.

proof idea

This is a definition module, no proofs. Each declaration is either an abbreviation for 1/φ or a direct algebraic identity obtained by substituting the minimal polynomial of φ and simplifying.

why it matters in Recognition Science

The module supplies the concrete numerical and algebraic handle on φ⁻¹ that downstream cross-domain lemmas (senolyticTargetRatio, circadianDecay, etc.) require when they rescale quantities along the phi-ladder. It therefore closes the interface between the core forcing-chain results (T6) and the applied models that appear later in the CrossDomain hierarchy.

scope and limits

Does not derive the value of φ from the J-functional.
Does not prove uniqueness of the positive fixed point.
Does not connect φ⁻¹ to the mass-ladder or Berry threshold.
Does not supply numerical approximations beyond the exact algebraic forms.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (18)

def phiInv L31
theorem phiInv_pos L33
theorem phiInv_lt_one L37
theorem phiInv_lt_phi L41
theorem phiInv_eq_phi_minus_one L50
theorem phiInvSq_eq_two_minus_phi L60
theorem phiInvCubed_eq_two_phi_minus_three L69
def senolyticTargetRatio L80
def giniCeiling L83
def policyBalance L86
def stemCellDecay L89
def circadianDecay L92
def cabibboFactor L95
theorem all_phiInv_instances_equal L98
theorem all_phiInv_in_unit_interval L105
theorem cabibbo_in_unit L109
structure PhiInverseInvariantsCert L121
def phiInverseInvariantsCert L135