pith. machine review for the scientific record. sign in
theorem proved tactic proof

derived_constants_exist

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 158theorem derived_constants_exist : Nonempty DerivedConstants := by

proof body

Tactic-mode proof.

 159  constructor
 160  exact {
 161    phi := phi,
 162    E_coh := E_coh,
 163    tau_0 := 1,  -- placeholder
 164    c := 1,      -- placeholder
 165    hbar := E_coh,  -- hbar = E_coh * tau_0 = E_coh * 1
 166    G := 1,      -- placeholder
 167    alpha_inv := 137.036,  -- placeholder
 168    phi_golden := phi_sq,
 169    IR_gate := by ring,
 170    all_positive := ⟨phi_pos, E_coh_pos, by norm_num, by norm_num, E_coh_pos, by norm_num⟩
 171  }
 172
 173/-! ## Zero Parameters Claim -/
 174
 175/-- The zero-parameters claim: all constants derive from φ with no free parameters.
 176
 177This is the formal statement of the claim. The proof would require
 178completing the full derivation chain.
 179-/

depends on (28)

Lean names referenced from this declaration's body.