DerivedConstants
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not compute or verify numerical SI values for any constant.
- Does not prove the IR-gate or golden-ratio identities; they are recorded as hypotheses.
- Does not derive c, G or alpha_inv from phi; it only records them inside the record.
- Does not address the eight-tick octave or spatial dimension D=3.
formal statement (Lean)
144structure DerivedConstants where
145 phi : ℝ
146 E_coh : ℝ
147 tau_0 : ℝ
148 c : ℝ
149 hbar : ℝ
150 G : ℝ
151 alpha_inv : ℝ
152 -- Consistency conditions
153 phi_golden : phi ^ 2 = phi + 1
154 IR_gate : hbar = E_coh * tau_0
155 all_positive : 0 < phi ∧ 0 < E_coh ∧ 0 < tau_0 ∧ 0 < c ∧ 0 < hbar ∧ 0 < G
156
157/-- The derived constants exist (consistency). -/