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

c_pos

show as:
view Lean formalization →

c_rs > 0 follows from the algebraic identity c_rs = 1 in RS-native units. Researchers deriving constants from the recognition composition law cite it to anchor positivity of c, ℏ, and G. The tactic proof rewrites via c_rs_eq_one then applies norm_num to verify the inequality.

claim$c_{RS} > 0$, where $c_{RS}$ is the ratio of fundamental length to the eight-tick period derived from the recognition composition law.

background

The ConstantDerivations module derives physical constants from the RS foundation rather than postulating them. Speed of light emerges as ℓ₀/τ₀ with τ₀ the eight-tick octave; upstream forcing chain yields J-uniqueness, φ as fixed point, and c_rs = 1 in native units. Module documentation states these constants are ratios algebraic in φ, not free parameters.

proof idea

One-line wrapper that rewrites the goal using c_rs_eq_one to obtain 1 > 0, then invokes norm_num to discharge the numerical inequality.

why it matters in Recognition Science

Supplies the c_pos hypothesis required by the Physical structure in Bridge.DataCore and by G_pos, kappa_einstein_pos in Constants. It closes the derivation step from the T0-T8 forcing chain to explicit constants c = 1, ℏ = φ^{-5}, G = φ^5 / π. Supports the claim that no free parameters enter at this level.

scope and limits

formal statement (Lean)

 110theorem c_pos : c_rs > 0 := by rw [c_rs_eq_one]; norm_num

proof body

Tactic-mode proof.

 111
 112/-! ## Planck's Constant: ℏ = E_coh · τ₀ -/
 113
 114/-- **Planck's reduced constant** in RS-native units.
 115
 116    ℏ is the product of coherence energy and fundamental time.
 117    This sets the scale of the IR gate (minimum action for coherent state).
 118
 119    In RS-native units: ℏ = φ^(-5) · 1 = φ^(-5). -/
 120noncomputable def ℏ_rs : ℝ := E_coh * τ₀
 121
 122/-- ℏ = φ^(-5) in RS-native units. -/
 123theorem ℏ_rs_eq : ℏ_rs = φ_val^(-5 : ℤ) := by
 124  unfold ℏ_rs E_coh τ₀
 125  ring
 126
 127/-- ℏ > 0. -/
 128theorem ℏ_pos : ℏ_rs > 0 := by
 129  rw [ℏ_rs_eq]
 130  exact zpow_pos phi_pos (-5)
 131
 132/-- ℏ is algebraic in φ. -/
 133theorem ℏ_algebraic_in_φ : ∃ n : ℤ, ℏ_rs = φ_val^n := ⟨-5, ℏ_rs_eq⟩
 134
 135/-! ## Gravitational Constant: G -/
 136
 137/-- **Gravitational constant** in RS-native units.
 138
 139    G emerges as the curvature extremum in recognition geometry.
 140    The derivation involves the holographic bound and ledger capacity.
 141
 142    G ~ ℓ₀³/(τ₀² · M₀) where M₀ is the fundamental mass.
 143
 144    In RS-native units with natural mass scale M₀ = 1/φ^5:
 145    G = ℓ₀³ · φ^5 / τ₀² = 1 · φ^5 / 1 = φ^5. -/

used by (22)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (23)

Lean names referenced from this declaration's body.