DerivedConstants
plain-language theorem explainer
DerivedConstants collects the real numbers phi, E_coh, tau_0, c, hbar, G and alpha_inv into one record together with the golden-ratio equation for phi, the IR-gate identity for hbar, and strict positivity of every entry. A researcher tracing the zero-parameter derivation of all physical constants from a single self-similar fixed point would cite this record to assert a consistent bundle exists. The declaration is a pure structure whose fields already embed the three consistency conditions.
Claim. A record of real numbers $phi$, $E_{coh}$, $tau_0$, $c$, $hbar$, $G$, $alpha^{-1}$ satisfying $phi^2 = phi + 1$, $hbar = E_{coh} tau_0$, and $0 < phi$, $0 < E_{coh}$, $0 < tau_0$, $0 < c$, $0 < hbar$, $0 < G$.
background
The RRF foundation module states that all physical constants derive from phi via the chain phi to E_coh to tau_0 to c to hbar to G to alpha inverse. E_coh is defined as phi to the power negative five in RS-native units. The module lists the IR gate identity hbar equals E_coh times tau_0 and the Planck gate that fixes G in terms of lambda_rec, c, hbar and pi.
proof idea
This is a structure definition with an empty proof body. The three consistency conditions are written directly as fields of the structure type; no tactics or lemmas are applied.
why it matters
The structure supplies the concrete object required by the downstream theorem derived_constants_exist, which proves the record is nonempty, and by ZeroParametersClaim, which asserts that every constant is a function of phi alone. It therefore closes the formal statement of the derivation chain listed in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.