bandGap_ratio
plain-language theorem explainer
The ratio of consecutive band-gap energies on the phi-ladder equals the golden ratio phi for any natural number rung k. Solid-state physicists working inside the Recognition Science framework cite this when confirming uniform self-similar scaling across the five semiconductor types. The proof is a direct term reduction that substitutes the power definition of bandGap and cancels via exponent arithmetic and ring simplification.
Claim. For every natural number $k$, the ratio of the band-gap energy at rung $k+1$ to the band-gap energy at rung $k$ equals the golden ratio $phi$.
background
The module constructs semiconductor band structure from configDim equal to 5, which yields exactly five canonical types: intrinsic, n-type doped, p-type doped, compensated, and degenerate. Band-gap energies are placed on the phi-ladder via the definition bandGap(k) := phi^k, imported from the upstream SolidStatePhysicsFromRS module. This supplies the scaling relation required by the certification structure in the same file.
proof idea
The term proof unfolds bandGap on both sides to obtain phi^{k+1} / phi^k. It adds a positivity hypothesis for phi^k, rewrites the division via div_eq_iff, applies the successor power rule, and closes with ring simplification.
why it matters
This theorem supplies the phi_ratio field inside the SemiconductorCert structure, which also records the count of five types and positivity of every band gap. It realizes the self-similar fixed-point property of phi inside the solid-state sector, consistent with the forced value of phi as the self-similar fixed point in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.