phiInverseInvariantsCert
plain-language theorem explainer
The definition assembles a certificate structure for the inverse golden ratio 1/φ that bundles positivity, strict upper bounds below 1 and below φ, the identity 1/φ = φ - 1, the relations 1/φ² = 2 - φ and 1/φ³ = 2φ - 3, equality of five cross-domain instances, and the Cabibbo factor lying in (0, 1/φ). A Recognition Science modeler would cite it to invoke the complete set of 1/φ properties in one reference. Construction proceeds by direct field assignment from the supporting lemmas in the same module.
Claim. Let φ be the golden ratio. The certificate asserts 0 < φ^{-1}, φ^{-1} < 1, φ^{-1} < φ, φ^{-1} = φ - 1, 1/φ² = 2 - φ, 1/φ³ = 2φ - 3, that the senolytic target ratio equals the Gini ceiling which equals the policy balance which equals the stem cell decay which equals the circadian decay, and that the Cabibbo factor c satisfies 0 < c < φ^{-1}.
background
The module CrossDomain.PhiInverseInvariants establishes 1/φ as the attractor for negative-rung quantities including decay rates and optimal fractions. Key definitions include phiInv := 1/φ, with phiInv_pos proving 0 < phiInv, phiInv_lt_one proving phiInv < 1, and phiInv_lt_phi proving phiInv < φ. The Fibonacci identity phiInv_eq_phi_minus_one states phiInv = φ - 1, while phiInvSq_eq_two_minus_phi and phiInvCubed_eq_two_phi_minus_three give the squared and cubed relations. The theorem all_phiInv_instances_equal shows the five quantities senolyticTargetRatio, giniCeiling, policyBalance, stemCellDecay, and circadianDecay are identical. The cabibbo_in_unit theorem places the Cabibbo factor below phiInv. These results rest on the golden ratio properties phi_sq_eq and phi_cubed_eq imported from Constants.
proof idea
The definition is a one-line structure instantiation of PhiInverseInvariantsCert that maps each field directly to the corresponding lemma: phiInv_pos to phiInv_pos, phiInv_lt_one to phiInv_lt_one, phiInv_lt_phi to phiInv_lt_phi, fib_identity to phiInv_eq_phi_minus_one, inv_sq_identity to phiInvSq_eq_two_minus_phi, inv_cubed_identity to phiInvCubed_eq_two_phi_minus_three, five_instances_equal to all_phiInv_instances_equal, and cabibbo_smaller to cabibbo_in_unit.
why it matters
This certificate packages the cross-domain convergence on 1/φ, fulfilling the module's structural claim that 1/φ serves as the canonical attractor for decay rates, dampings, and target ratios. It draws on the framework's phi-ladder and negative-rung quantities, providing a compact reference that aligns with the eight-tick octave and D=3 implications through invariant preservation. No parent theorems are listed in the used-by graph, leaving its integration into larger forcing chains as an open extension point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.