module module high

`IndisputableMonolith.CrossDomain.PhiInverseInvariants`

The PhiInverseInvariants module supplies the canonical 1/φ together with its positivity, ordering, and power identities. Cross-domain researchers cite these when scaling quantities on the phi-ladder in biological or policy models. The module consists of a sequence of definitions and short algebraic lemmas built on the imported Constants.

claim$\phi^{-1}$ denotes the canonical inverse golden ratio, satisfying $\phi^{-1}>0$, $\phi^{-1}<1$, $\phi^{-1}<\phi$, $(\phi^{-1})^2=2-\phi$, and $(\phi^{-1})^3=2\phi-3$.

background

The module sits in the CrossDomain section and imports the RS time quantum $\tau_0=1$ tick from IndisputableMonolith.Constants. Its setting is the self-similar fixed point $\phi$ forced in T6 of the UnifiedForcingChain, with all quantities expressed in RS-native units where $c=1$.

It introduces the object phiInv as the canonical $1/\phi$ value and then defines derived cross-domain quantities (senolyticTargetRatio, giniCeiling, policyBalance, stemCellDecay, circadianDecay) that apply these invariants.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the $1/\phi$ invariants required by cross-domain scaling constructions that sit above the phi-ladder. It feeds the algebraic facts needed for later applications of the eight-tick octave and the mass formula yardstick.

scope and limits

Does not derive $\phi$ from the T0-T8 forcing chain.
Does not address the Recognition Composition Law.
Does not connect to the mass formula or Berry threshold.
Does not supply numerical values for $\alpha$ or $G$.

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