pith. machine review for the scientific record. sign in
theorem proved tactic proof high

rs_params_positive

show as:
view Lean formalization →

Both the ILG exponent defined as (1 minus one over phi) over two and the lag constant defined as phi to the minus five are strictly positive. Modelers of the GR limit in Recognition Science cite the result when establishing that the parameters remain perturbative. The tactic proof splits the conjunction, unfolds each definition, invokes positivity and one-less-than-phi for the golden ratio, then closes with linarith and the positivity of real powers.

claimLet $phi$ be the golden ratio. Define $alpha = (1 - phi^{-1})/2$ and $C_{lag} = phi^{-5}$. Then $0 < alpha$ and $0 < C_{lag}$.

background

The module proves concrete bounds on ILG parameters that Recognition Science derives from its geometry and coherence scale. Alpha equals (1 minus one over phi) divided by two; C_lag equals phi to the minus five. These expressions appear directly in the module documentation as the objects whose smallness must be shown rather than assumed. Upstream lemmas supply phi greater than one and phi positive, both taken from the Constants module and the PhiSupport layer.

proof idea

Constructor splits the conjunction into separate goals. The first goal unfolds the alpha definition, obtains phi_pos and one_lt_phi, shows one over phi is less than one via div_lt_one, then applies linarith. The second goal unfolds the C_lag definition and applies Real.rpow_pos_of_pos to phi_pos.

why it matters in Recognition Science

The result is invoked by the two downstream theorems that bound the product of the parameters below 0.1 and below 0.02. It supplies the positivity half of the perturbative regime required by the module's source derivation. The step sits inside the Recognition Science parameter chain that begins from the golden-ratio fixed point and feeds the GR-limit analysis.

scope and limits

Lean usage

have hα_pos := rs_params_positive.1

formal statement (Lean)

  32theorem rs_params_positive :
  33  0 < alpha_from_phi ∧ 0 < cLag_from_phi := by

proof body

Tactic-mode proof.

  34  constructor
  35  · unfold alpha_from_phi
  36    have hφ_pos : 0 < Constants.phi := Constants.phi_pos
  37    have hφ_gt_one : 1 < Constants.phi := Constants.one_lt_phi
  38    have : 0 < 1 - 1 / Constants.phi := by
  39      have : 1 / Constants.phi < 1 := (div_lt_one hφ_pos).mpr hφ_gt_one
  40      linarith
  41    linarith
  42  · unfold cLag_from_phi
  43    exact Real.rpow_pos_of_pos Constants.phi_pos _
  44
  45/-- PROVEN: α < 1 (straightforward from φ > 1). -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (7)

Lean names referenced from this declaration's body.