IndisputableMonolith.Foundation.MaximalForcing.RSHbarUniverse

   1import IndisputableMonolith.Foundation.MaximalForcing.RealityClosure
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Maximal Forcing: the RS-native action-quantum layer
   6
   7Sixth single-constant instantiation, reaching the quantum sector. The
   8RS-native action quantum, evaluated in the native gauge (`λ_rec = c = 1`,
   9`tick = τ₀`), is fixed to the parameter-free value `φ⁻⁵`.
  10
  11* The realization carrier is a candidate action-quantum value `h : ℝ`.
  12* The loose class `Lhbar0` is every candidate real.
  13* The gate class `LhbarRS` pins `h` to the RS-native value `hbar`.
  14* The claim under closure is "h = φ⁻⁵".
  15
  16Over `LhbarRS` the native value claim is forced, wrapping the proved
  17`Constants.hbar_eq_phi_inv_fifth`. Over `Lhbar0` it is independent: the RS value
  18satisfies it, `0` does not (`φ⁻⁵ > 0`). This is the native action-normalization
  19boundary, not a derivation of the SI value of Planck's constant.
  20
  21Together with `RSGravityUniverse` (`κ = 8φ⁵`) and `RSAlphaUniverse` (the α
  22window), this completes a trio of native/dimensionless φ-expression surfaces:
  23the native action normalization, the native gravitational coupling, and the
  24electromagnetic coupling window.
  25-/
  26
  27namespace IndisputableMonolith
  28namespace Foundation
  29namespace MaximalForcing
  30
  31open IndisputableMonolith.Constants (phi hbar hbar_eq_phi_inv_fifth hbar_pos)
  32
  33/-- Loosest action-quantum class `Lhbar0`: every candidate value. -/
  34def Lhbar0 : AdmissibilityClass ℝ where
  35  admissible := Set.univ
  36  label := "every candidate action-quantum value"
  37
  38/-- Gate-tightened action-quantum class `LhbarRS`: the candidate equals the
  39RS-native reduced Planck constant. -/
  40def LhbarRS : AdmissibilityClass ℝ where
  41  admissible := { h | h = hbar }
  42  label := "RS-native action quantum: h = ℏ"
  43
  44/-- `LhbarRS` is a tightening of `Lhbar0`. -/
  45def tighten_Lhbar0_LhbarRS : Tightening Lhbar0 LhbarRS where
  46  subset := by intro a _; trivial
  47  strict_witness := True
  48
  49/-- The forced claim of the action-quantum layer: `h = φ⁻⁵`. -/
  50def isHbarClaim : RealityClaim ℝ where
  51  label := "h = φ^(-5) (reduced Planck constant, parameter-free)"
  52  holds := fun h => h = phi ^ (-(5 : ℝ))
  53
  54/-- The action-quantum claim universe. -/
  55def hbarUniverse : ClaimUniverse where
  56  Realization := ℝ
  57  admissibility := LhbarRS
  58  claims := { isHbarClaim }
  59
  60/-- **Native action quantum as a forced invariant.** Over the RS-native gate, the
  61action quantum equals `φ⁻⁵`. Wraps `Constants.hbar_eq_phi_inv_fifth`.
  62This is not a claim that the SI value of `ℏ` is derived without a dimensional
  63anchor. -/
  64theorem forced_hbar : Forced LhbarRS.admissible isHbarClaim := by
  65  intro h hh
  66  have hh' : h = hbar := hh
  67  show h = phi ^ (-(5 : ℝ))
  68  rw [hh', hbar_eq_phi_inv_fifth]
  69
  70/-- The claim `isHbarClaim` is in the closure of the action-quantum universe. -/
  71theorem isHbarClaim_in_closure :
  72    InClosure Primitive.lawOfLogic hbarUniverse isHbarClaim := by
  73  show isHbarClaim ∈ hbarUniverse.claims
  74  exact Set.mem_singleton _
  75
  76/-- Forced-register entry for the reduced Planck constant. -/
  77def hbarForcedInvariant : ForcedInvariant Primitive.lawOfLogic hbarUniverse where
  78  claim := isHbarClaim
  79  in_closure := isHbarClaim_in_closure
  80  forced := forced_hbar
  81
  82/-- The action-quantum universe is fully classified. -/
  83theorem hbarUniverse_classifier :
  84    ∀ C : RealityClaim hbarUniverse.Realization,
  85      InClosure Primitive.lawOfLogic hbarUniverse C → ClaimClassification hbarUniverse C := by
  86  intro C hC
  87  have hCeq : C = isHbarClaim := Set.mem_singleton_iff.mp hC
  88  subst hCeq
  89  exact ClaimClassification.forced forced_hbar
  90
  91/-- A real `MaximalClosureCert` for the action-quantum universe. -/
  92def hbarUniverseCert : MaximalClosureCert Primitive.lawOfLogic hbarUniverse where
  93  classifies := hbarUniverse_classifier
  94
  95/-! ## The RS-native gate is the action-normalization boundary -/
  96
  97/-- The forced value is strictly positive: `φ⁻⁵ > 0`. -/
  98theorem hbar_value_pos : 0 < phi ^ (-(5 : ℝ)) := by
  99  rw [← hbar_eq_phi_inv_fifth]; exact hbar_pos
 100
 101/-- Over the loose class `Lhbar0`, the value claim is independent: the RS action
 102quantum satisfies it, and `0` does not. -/
 103theorem hbar_independent_over_Lhbar0 :
 104    Independent Lhbar0.admissible isHbarClaim := by
 105  refine ⟨hbar, 0, ?_, ?_, ?_, ?_⟩
 106  · trivial
 107  · trivial
 108  · show hbar = phi ^ (-(5 : ℝ)); exact hbar_eq_phi_inv_fifth
 109  · intro h
 110    have h0 : (0 : ℝ) = phi ^ (-(5 : ℝ)) := h
 111    have hp := hbar_value_pos
 112    linarith
 113
 114/-- **The RS-native tightening is explicit.** The value claim is independent over
 115`Lhbar0` but forced over `LhbarRS`; the tightening is the native
 116action-normalization assumption that later SI calibration maps into J·s. -/
 117theorem tightening_Lhbar0_LhbarRS_effective :
 118    Independent Lhbar0.admissible isHbarClaim ∧
 119    Forced LhbarRS.admissible isHbarClaim :=
 120  ⟨hbar_independent_over_Lhbar0, forced_hbar⟩
 121
 122end MaximalForcing
 123end Foundation
 124end IndisputableMonolith
 125