Pith. sign in
module module high

IndisputableMonolith.Materials.PhiLadderPhononResonance

show as:
view Lean formalization →

This module defines the phonon resonance frequency on the Recognition Science phi-ladder as ω_p(k) = ω_0 φ^k. Materials researchers modeling high-Tc hydrides cite it for discrete rung selection in optimization landscapes. The module supplies supporting definitions and elementary properties of the rung map with no complex derivations.

claimThe phonon resonance frequency at rung \(k\) is given by \(\omega_p(k) = \omega_0 \cdot \phi^k\).

background

The module imports Constants, where the fundamental RS time quantum satisfies τ₀ = 1 tick, and Cost. It operates inside the phi-ladder construction already present in the Recognition framework, where discrete rungs are indexed by integers and scaled by successive factors of the self-similar fixed point φ.

Sibling declarations introduce phonon_rung as the integer index, together with lemmas establishing that the map is positive, strictly increasing, and satisfies a constant ratio between adjacent rungs. These objects sit in the Materials domain and prepare the ground for resonance calculations that later feed superconductor models.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the phonon resonance model that is deepened in HydrideSCOptimization for the single-parameter φ-rung search in high-Tc hydrides (H₃S, LaH₁₀, YH₆). It fills Track E6 of Plan v5 and supplies the resonance frequency that the downstream module uses to optimize the hydrogen-dominant landscape.

scope and limits

used by (1)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (10)