derived_constants_exist
plain-language theorem explainer
Existence of a DerivedConstants structure collecting constants derived from φ is asserted by direct construction. Researchers on parameter-free constant derivations in the RRF framework would cite it for consistency. The proof builds the structure instance explicitly, invoking positivity lemmas for φ and E_coh together with ring to confirm the IR gate identity.
Claim. There exists a structure with components φ, E_coh, τ₀, c, ℏ, G, α⁻¹ satisfying φ² = φ + 1, all components positive, and the IR gate ℏ = E_coh · τ₀.
background
The RRF foundation module states that all physical constants derive from φ via gate identities in the chain φ → E_coh → τ₀ → c → ℏ → G → α⁻¹. DerivedConstants is the structure holding these values plus the golden-ratio property φ² = φ + 1 and positivity conditions. The module notes that constants are derived rather than assumed, with SI values from calibration. Upstream lemmas supply E_coh_pos (0 < E_coh) and the definition G = λ_rec² c³ / (π ℏ).
proof idea
Constructor tactic opens the Nonempty goal; exact then supplies a concrete DerivedConstants record. Fields are populated from phi and E_coh in scope, norm_num discharges positivity, and ring verifies the IR gate identity. The construction relies on E_coh_pos and phi_pos from the Constants module.
why it matters
The result supports the zero-parameters claim that constants derive from φ without free parameters, as stated in the module. It supplies the consistency step for the derivation chain and aligns with Recognition Science landmarks including the RCL identity and the eight-tick octave. Full numerical closure of the chain remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.