Constants

/-- 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

/-- **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⟩

/-- RS-native gravitational coupling projection through the recognition/Planck
    bridge: \(G = \lambda_{\text{rec}}^2 c^3 / (\pi \hbar)\).

    This is not a prediction of the SI value of Newton's constant.  SI conversion
    requires the dimensional bridge in `Foundation/SIBridgeClosure.lean`. -/
noncomputable def G : ℝ := (lambda_rec^2) * (c^3) / (Real.pi * hbar)

/-- Fundamental recognition wavelength λ_rec.
    In the 8-tick cycle, λ_rec = ℓ₀ (in RS-native units).

## ATTACKER BREADCRUMB (read this before declaring λ_rec a calibration)

`λ_rec = ℓ₀ = 1` looks like a unit choice on the surface. It is a
**derived** quantity, not a calibration. The chain:

1. The bit cost `J_bit = 1` (normalized recognition event cost).
2. The curvature cost `J_curv(λ) = 2λ²` from the Q₃ Gauss-Bonnet
   normalization (8 vertices × angular deficit π/2 each = 4π = 2π·χ(S²)).
3. The balance condition `J_bit = J_curv` forces a unique positive
   `λ_0 = 1/√2` in dimensionless RS-native units.
4. The discrete lattice convention `ℓ₀ = 1` (one voxel = one causal step)
   absorbs the `√2`, giving `λ_rec = ℓ₀ = 1`.

Every step is proved in `IndisputableMonolith/Constants/LambdaRecDerivation.lean`:
see `balance_at_lambda_0`, `balance_unique_positive_root`,
`balance_determines_lambda`, `total_curvature_gauss_bonnet`,
`G_derivation_chain_complete`. Zero sorry, zero RS-internal axioms.

`G := λ_rec² · c³ / (π · ℏ)` follows by substitution and gives
`G = φ⁵/π` in RS-native units (zero free parameters at this level).

## Where the SI bridge actually sits (NOT here)

If you are looking for the place the framework calibrates against
SI/CODATA, it is NOT λ_rec. The SI bridge lives in:
* `Constants/RSNativeUnits.lean` `ExternalCalibration` structure
  (seconds_per_tick, meters_per_voxel, joules_per_coh, with c-consistency).
* `Foundation/DimensionalBridgeStructural.lean` (the explicit "principal
  open frontier" tag with the named residual).
The dimensional bridge is one open frontier, not a hidden cluster of
calibrations spread across the constants. -/
noncomputable def lambda_rec : ℝ := ell0

/-- Light-cone identity: ℓ₀ = c · τ₀ (in RS-native units). -/
lemma c_ell0_tau0 : c * tau0 = ell0 := by
  simp [c, tau0, ell0, tick]

/-- The fundamental time unit τ₀ (duration of one tick) in RS-native units. -/
@[simp] noncomputable def tau0 : ℝ := tick

/-- The speed of light c in RS-native units (voxel/tick). -/
@[simp] noncomputable def c : ℝ := 1

/-- The fundamental length unit ℓ₀ in RS-native units (voxel). -/
@[simp] noncomputable def ell0 : ℝ := 1

/-- **THEOREM C-004.2**: ℏ is positive (required for quantum dynamics). -/
theorem hbar_positive : hbar > 0 := hbar_pos

/-- **THEOREM C-004.3**: ℏ < 1 (the action quantum is small compared to natural units).

    Proof: φ > 1 ⟹ φ⁵ > 1 ⟹ φ⁻⁵ < 1. -/
theorem hbar_lt_one : hbar < 1 := by
  rw [hbar_eq_phi_inv_fifth]
  have h1 : phi ^ (5 : ℝ) > 1 := by
    have hphi : phi > 1 := one_lt_phi
    have hexp : (5 : ℝ) > 0 := by norm_num
    have h1_lt : (1 : ℝ) < phi ^ (5 : ℝ) := by
      rw [← Real.one_rpow (5 : ℝ)]
      apply Real.rpow_lt_rpow
      · norm_num
      · linarith
      · norm_num
    linarith
  have h2 : 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 [h2]
  have h3 : phi ^ (5 : ℝ) > 0 := by positivity
  apply (div_lt_iff₀ h3).mpr
  linarith