Pith. sign in
module module high

IndisputableMonolith.Mathematics.NumberTheoryFromRS

show as:
view Lean formalization →

The module derives number theoretic identities from the Recognition Science phi relation. Researchers connecting the RS forcing chain to Fibonacci sequences and counting functions would cite it. The module organizes a collection of identities and certificates built directly from the defining property φ² = φ + 1.

claim$\phi^2 = \phi + 1$

background

The module sits in the Mathematics domain. It imports Mathlib and IndisputableMonolith.Constants, where the fundamental RS time quantum is defined as τ₀ = 1 tick. The central object is the property φ² = φ + 1, the defining relation for the golden ratio phi that arises as the self-similar fixed point in the RS framework.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

This module supplies the number theory building blocks for the Recognition Science framework. It feeds downstream results such as NumberTheoryCert and rsi_count_five. It establishes the mathematical identities needed to derive counts and gaps from the phi ladder.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (8)