pith. machine review for the scientific record. sign in
def definition def or abbrev high

coeff

show as:
view Lean formalization →

The coeff definition supplies the general term of the alternating gap-series expansion in Recognition Science, indexed via successor to start at n+1. Ethics normal-form constructions cite it when aggregating coefficients over filtered move lists to populate primitive tables. The implementation is a direct algebraic expression that divides the signed unit by both the shifted index and the corresponding power of phi.

claimFor each natural number $n$, define $c(n) = (-1)^{n+1} / ((n+1) φ^{n+1})$, where $φ$ denotes the golden ratio. This supplies the $n$th coefficient (1-indexed) in the formal power series for the gap logarithm evaluated at argument $z/φ$.

background

The Pipelines module treats the golden ratio $φ$ as a fixed concrete real number. The gap-series coefficient is the general term appearing in the expansion of $log(1 + z/φ)$, kept purely algebraic here. Upstream, the gap itself is defined as the product of closure and Fibonacci factors whose main theorem asserts equality to 45; the successor operation from ArithmeticFromLogic supplies the index shift that makes the series 1-indexed by design.

proof idea

One-line wrapper that applies successor to obtain $k = n+1$, then directly assembles the closed-form term $(-1)^k / (k · φ^k)$. No lemmas are invoked beyond the built-in real arithmetic and exponentiation on naturals.

why it matters in Recognition Science

This definition is referenced by aggCoeff and its auxiliary lemmas in Ethics.Virtues.NormalForm to compute summed coefficients for each (pair, primitive) entry when constructing NormalForm objects from move lists. It supplies the algebraic backbone for the gap series before any convergence or identification with $log(1 + 1/φ)$ is proved in a companion module. The construction sits downstream of the phi-forcing and gap=45 results and upstream of the normal-form well-formedness theorems.

scope and limits

formal statement (Lean)

  16noncomputable def coeff (n : ℕ) : ℝ :=

proof body

Definition body.

  17  let k := n.succ
  18  ((-1 : ℝ) ^ k) / (k : ℝ) / (phi ^ k)
  19
  20/-- Finite partial sum (0..n-1) of the gap coefficients (evaluated at z=1).
  21This stays purely algebraic here; convergence and identification with
  22`log(1 + 1/φ)` can be proved in a companion module that imports analysis. -/

used by (21)

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

depends on (13)

Lean names referenced from this declaration's body.