pith. sign in
module module high

IndisputableMonolith.Materials.PhiLadderPhononResonance

show as:
view Lean formalization →

This module defines phonon resonance frequencies on the Recognition Science phi-ladder for materials modeling. It sets the frequency at rung k to scale as the base frequency times phi to the power k. High-Tc superconductivity researchers cite these definitions when optimizing hydride systems such as H3S. The module supplies basic rung lemmas on monotonicity and adjacent ratios as supporting structure.

claimThe phonon resonance frequency at rung $k$ satisfies $ω_p(k) = ω_0 φ^k$, where $φ$ is the self-similar fixed point and $ω_0$ is the base frequency in RS-native units.

background

Recognition Science places material resonances on the phi-ladder, a discrete scaling structure derived from the J-cost functional and the eight-tick octave. The module imports the fundamental time quantum τ₀ = 1 tick from Constants and cost machinery from Cost to anchor frequencies. It introduces phonon_rung as the mapping from integer rung index to resonance properties, together with lemmas establishing that the rung function is strictly increasing and that adjacent ratios equal φ.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the phonon resonance definitions that feed the hydride superconductor optimization in HydrideSCOptimization. It supports the single-parameter φ-rung search for high-Tc materials such as H3S, LaH10 and YH6 under RS_PAT_010, deepening Plan v5 Track E6. Downstream work uses these rungs to locate optimal lattice parameters in 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)