pith. sign in
module module high

IndisputableMonolith.Physics.SemiconductorPhysicsFromRS

show as:
view Lean formalization →

The SemiconductorPhysicsFromRS module derives semiconductor relations from Recognition Science by linking carrier multiplicity to spatial dimensionality. It centers on the equality of two carrier types with D minus one. Condensed-matter researchers applying RS to device physics would cite the module for its dimensional reduction step. The module organizes definitions and equalities around the carrier-types relation drawn from the upstream Constants import.

claimIn the Recognition Science model the number of carrier types satisfies $n = D - 1$, where $D$ denotes the number of spatial dimensions.

background

Recognition Science obtains D = 3 from the forcing chain T0-T8. The imported Constants module supplies the base time quantum τ₀ = 1 tick. The present module introduces SemiconductorDevice together with carrierTypes and crystalSymmetries to express semiconductor behavior in RS-native units, with the central relation carrierTypes = D - 1.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the semiconductor layer that connects the RS forcing chain (T8: D = 3) to device models. It feeds the sibling SemiconductorPhysicsCert. The relation 2 carrier types = D - 1 follows directly from the eight-tick octave and the spatial-dimension derivation.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (8)