Pith. sign in
module module moderate

IndisputableMonolith.Physics.MagnonFromPhiLadder

show as:
view Lean formalization →

Defines magnon dispersion data on the Recognition Science phi-ladder: a domain cost, its nonnegativity, a positive canonical energy threshold, and an inhabited magnon-dispersion certificate. Condensed-matter or RS phenomenology workers cite the certificate when matching spin-wave spectra to ladder rungs. The module is mostly definitions plus short positivity and equality lemmas over Cost and Constants.

claimThe module supplies a domain cost $C$, proves $C \ge 0$ and an evaluation identity, fixes a canonical threshold $T > 0$, and packages a magnon dispersion certificate asserting that magnon energies are organized on the $\varphi$-ladder relative to $T$.

background

Recognition Science places particle and quasiparticle scales on a discrete $\varphi$-ladder (golden ratio fixed by the J-cost self-similarity). Masses and related energies take the schematic form yardstick $\cdot \varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$. The Cost import supplies the underlying J-cost infrastructure; Constants supplies RS-native units (including the tick $\tau_0$).

Magnons are collective spin-wave modes. This physics module treats their dispersion as ladder data rather than a free continuum fit: a domain cost measures mismatch to the ladder, and a canonical threshold sets the positive energy scale against which rungs are counted.

Sibling declarations name that cost, its pointwise evaluation and nonnegativity, the threshold and its positivity, and a certificate type MagnonDispCert with an inhabited instance.

proof idea

Definition-heavy module, not a single deep theorem. Domain cost and canonical threshold are introduced as defs; nonnegativity and positivity are short lemmas over the Cost layer and arithmetic of $\varphi$. The certificate is a structure bundling the dispersion claim; inhabitation is a constructive witness that the fields can be filled from the ladder data. No long tactic scripts; equality and sign facts discharge the supporting lemmas.

why it matters in Recognition Science

Gives RS a concrete condensed-matter landing: magnon spectra as phi-ladder objects rather than purely phenomenological fits. Ties spin-wave energy scales to the same $\varphi$ forced at T6 and to the Cost/J framework used elsewhere in the monolith. Downstream use is not yet wired in the graph (no used_by edges), so the module stands as a physics-side certificate surface for later spectrum or materials comparisons. It does not itself close the forcing chain T0–T8; it consumes Constants and Cost to state a quasiparticle claim in RS-native units.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)