pith. sign in
module module moderate

IndisputableMonolith.Physics.MagnetismFromRS

show as:
view Lean formalization →

The module Physics.MagnetismFromRS supplies definitions that model magnetic phenomena inside the Recognition Science framework using the J-cost. It introduces zero-field cases (J=0), applied fields, phenomenon counts, and certification objects. Physicists deriving electromagnetism from the RS forcing chain would cite these objects. The module contains only definitions and no proofs.

claimDefinitions of MagneticPhenomenon, magneticPhenomenonCount, zero_field (satisfying $J=0$), applied_field, MagnetismCert, and magnetismCert.

background

The module imports IndisputableMonolith.Cost, whose J-cost is the central recognition measure satisfying $J(x)=(x+x^{-1})/2-1$. In the Recognition Science setting, magnetism is treated as a recognition phenomenon whose zero-field limit is the case J=0. The sibling declarations therefore introduce the basic vocabulary for magnetic behavior on the phi-ladder.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module establishes the interface for magnetism within Recognition Science and supplies the objects that later physics derivations would invoke. It directly encodes the zero-field condition J=0 that follows from T5 J-uniqueness. No downstream theorems are listed yet.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)