Encyclopedia Constants Constants Hbar Positive

ARTICLE 3 claims 2 theorems 1 model

Constants Hbar Positive

In Recognition Science, the fundamental quantum of action is defined as a product of two positive quantities, and a machine-checked theorem confirms it is greater than zero.

Verify this page

The positivity theorem

In physics, the Planck constant h relates a particle's energy to its frequency. Recognition Science (RS) defines its own fundamental action quantum, called hbar, as the product of two framework-native quantities: cLagLock, a coupling constant set to phi to the power minus five, and tau0, the fundamental time quantum set to one tick. The definition is a choice, not a derivation.

The theorem hbar_positive states that this defined hbar is greater than zero. The proof in the machine-checked library of formal theorems is immediate: it multiplies the lemma that cLagLock is positive with the lemma that tau0 is positive. Since phi is greater than one, phi to a negative power is positive, and tau0 is defined as one, so the product is positive.

The theorem also yields a numerical bound. A companion result, hbar_bounds, proves that hbar lies strictly between 0.088 and 0.093 in RS-native units. This is not a claim about the measured Planck constant in SI units; it is a statement about the framework's internal scale, where the unit of time is one tick.

In Recognition Science, the framework models this hbar as the fundamental action quantum, and the theorem establishes the basic consistency requirement that this quantum is a positive real number. It does not derive the value of the physical Planck constant, nor does it compare hbar to any measured quantity. The positivity theorem is a foundational sanity check on the framework's own definitions.

THEOREM hbar_positive · IndisputableMonolith/Constants.lean
hbar_positive · IndisputableMonolith/Constants.lean:362 
/-- **THEOREM C-004.2**: ℏ is positive (required for quantum dynamics). -/
theorem hbar_positive : hbar > 0 := hbar_pos
THEOREM hbar_bounds · IndisputableMonolith/Constants.lean
hbar_bounds · IndisputableMonolith/Constants.lean:396 
/-- **THEOREM C-004.5**: Bounds on ℏ from φ bounds.

    With φ ∈ (1.61, 1.62), we get ℏ ∈ (0.088, 0.093). -/
theorem hbar_bounds : (0.088 : ℝ) < hbar ∧ hbar < (0.093 : ℝ) := by
  rw [hbar_eq_phi_inv_fifth]
  have h1 : (1.61 : ℝ) < phi := phi_gt_onePointSixOne
  have h2 : phi < (1.62 : ℝ) := phi_lt_onePointSixTwo
  -- We want 0.088 < φ^(-5) < 0.093
  -- Since hbar = 1/φ^5, we need bounds on φ^5
  -- Lower bound: φ < 1.62, so φ^5 < 1.62^5, so 1/φ^5 > 1/1.62^5
  -- Upper bound: φ > 1.61, so φ^5 > 1.61^5, so 1/φ^5 < 1/1.61^5
  have h_phi5_lower : phi ^ (5 : ℝ) > (1.61 : ℝ) ^ (5 : ℝ) := by
    apply Real.rpow_lt_rpow
    · linarith
    · linarith
    · norm_num
  have h_phi5_upper : phi ^ (5 : ℝ) < (1.62 : ℝ) ^ (5 : ℝ) := by
    apply Real.rpow_lt_rpow
    · linarith
    · linarith
    · norm_num
  -- Convert to hbar = φ^(-5) bounds
  have hbar_lower : phi ^ (-(5 : ℝ)) > (0.088 : ℝ) := by
    have h_inv : phi ^ (-(5 : ℝ)) = 1 / (phi ^ (5 : ℝ)) := by
      rw [show (-(5 : ℝ)) = - (5 : ℝ) by norm_num]
      rw [Real.rpow_neg]
      · ring
      · exact le_of_lt phi_pos
    rw [h_inv]
    -- Since φ^5 < 1.62^5, we have 1/φ^5 > 1/1.62^5
    -- Compute 1.62^5 = 11.158... and 1/11.158 ≈ 0.0896 > 0.088
    have h_div : 1 / (phi ^ (5 : ℝ)) > 1 / ((1.62 : ℝ) ^ (5 : ℝ)) := by
      apply (one_div_lt_one_div (by positivity) (by positivity)).mpr
      linarith [h_phi5_upper]
    have h_numeric : 1 / ((1.62 : ℝ) ^ (5 : ℝ)) > (0.088 : ℝ) := by
      rw [show (5 : ℝ) = (5 : ℕ) by norm_num, Real.rpow_natCast]
      norm_num
    linarith
  have hbar_upper : phi ^ (-(5 : ℝ)) < (0.093 : ℝ) := by
    have h_inv : phi ^ (-(5 : ℝ)) = 1 / (phi ^ (5 : ℝ)) := by
      rw [show (-(5 : ℝ)) = - (5 : ℝ) by norm_num]
      rw [Real.rpow_neg]
      · ring
      · exact le_of_lt phi_pos
    rw [h_inv]
    -- Since φ^5 > 1.61^5, we have 1/φ^5 < 1/1.61^5
    -- Compute 1.61^5 = 10.817... and 1/10.817 ≈ 0.0924 < 0.093
    have h_div : 1 / (phi ^ (5 : ℝ)) < 1 / ((1.61 : ℝ) ^ (5 : ℝ)) := by
      apply (div_lt_div_iff₀ (by positivity) (by positivity)).mpr
      linarith [h_phi5_lower]
    have h_numeric : 1 / ((1.61 : ℝ) ^ (5 : ℝ)) < (0.093 : ℝ) := by
      rw [show (5 : ℝ) = (5 : ℕ) by norm_num, Real.rpow_natCast]
      norm_num
    linarith
  exact ⟨hbar_lower, hbar_upper⟩
MODEL hbar · IndisputableMonolith/Constants.lean
hbar · IndisputableMonolith/Constants.lean:305 
/-- Native action quantum in RS-native units: `hbar = E_coh · tau0 = φ⁻⁵ · 1`.

## ATTACKER BREADCRUMB (read before declaring ℏ = φ⁻⁵ "true by definition")

The lemma `hbar_eq_phi_inv_fifth` below closes by `unfold; simp`. That is
intentional: this file *defines* the RS-native action unit. Two separate
questions then arise, and they have different answers; do not collapse them.

* Is the EXPONENT `5` forced, or a free choice? Forced, modulo one modeling
  step. The coherence energy carries one factor of `φ⁻¹` per configuration
  degree of freedom of a recognition event, and a recognition event has
  `D + 2` such degrees: `D` spatial (lattice, T8), `1` temporal (tick advance,
  T2), `1` balance (ledger neutrality `J(x)=J(x⁻¹)`, T3). With `D = 3` forced
  by T8 this gives `configDim = 5`, hence `E_coh = φ^(-(D+2)) = φ⁻⁵`. This is
  boundary item B-22, proved in `Foundation/GapDerivation.lean`
  (`configDim_at_D3`, `E_coh_gap_eq`, `Gap45Cert.ecoh`). The link back to THIS
  constant is machine-checked there:
  `GapDerivation.Constants_E_coh_eq_configDim` and
  `GapDerivation.hbar_exponent_eq_configDim` prove
  `E_coh = hbar = φ^(-(configDim D))`. The forced content is the count
  `D + 2`; the only modeling input is the `φ⁻¹`-per-dof rule. So the honest tag
  for the exponent is derived-modulo-one-modeling-step, NOT pure unit choice.
* Is the SI VALUE of `ℏ` (in J·s) predicted? No. A pure-number theory cannot
  output an absolute dimensionful SI constant without a dimensional anchor:
  see `Constants/NativeDimensionalBoundary.no_nontrivial_dimensionless_monomial`.

So "true by definition" is correct only at the level of native units (one tick
= the time unit ⟹ the native action quantum is `φ⁻⁵` as a pure number). The
substantive, non-definitional content is that the exponent equals the forced
configuration dimension `D + 2 = 5`.

## What the SI calibration looks like

Mapping `hbar_RS = φ⁻⁵` to SI units requires a dimensional anchor.  The
conversion is uniquely determined once the anchor is supplied
(`Foundation/SIBridgeClosure.lean`, `Verification/FirstPrinciplesToSI.lean`,
`Measurement/RSNative/Calibration/SingleAnchor.lean`); the boundary theorem
explaining why an anchor is required lives in
`Constants/NativeDimensionalBoundary.lean`. -/
noncomputable def hbar : ℝ := cLagLock * tau0

What this page does not claim

This theorem does not derive the value of the physical Planck constant in SI units. This theorem does not compare hbar to any measured quantity. This theorem does not assign a physical interpretation to the framework's internal scale.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Constants.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND