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

F

show as:
view Lean formalization →

The generating functional F(z) equals the natural logarithm of one plus z over the golden ratio. Researchers deriving mass gaps or anchor residues in Recognition Science cite this expression as the base generator. The definition is a direct assignment with no additional lemmas or reductions required.

claimDefine the function $F: ℝ → ℝ$ by $F(z) = log(1 + z/φ)$, where $φ$ denotes the golden ratio.

background

The Pipelines module fixes the golden ratio as a concrete real number. Upstream gap definitions in RSBridge.Anchor and Masses.AnchorPolicy express the residue at the anchor scale as log(1 + Z/φ) / log(φ) for integer Z, representing the integrated mass anomalous dimension for fermion species. The ContinuumBridge.as structure equates a weighted Laplacian sum over simplices to a scaled sum of defects.

proof idea

Direct definition that assigns the built-in real logarithm of one plus the argument scaled by the golden ratio.

why it matters in Recognition Science

This supplies the core generator appearing in downstream results such as SatisfiesRCL in CostAlgebra, which encodes the Recognition Composition Law, and in anchor policies for mass derivations. The form aligns with the phi-ladder scaling in the framework, where masses follow yardstick times phi to the power of rung minus eight plus gap(Z).

scope and limits

formal statement (Lean)

  27noncomputable def F (z : ℝ) : ℝ := Real.log (1 + z / phi)

proof body

Definition body.

  28
  29/-- The master gap value as the generator at z=1. -/

used by (40)

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

… and 10 more

depends on (8)

Lean names referenced from this declaration's body.