IndisputableMonolith.Holography.HorizonClockRate

   1import IndisputableMonolith.Holography.DeficitFreePeriod
   2import IndisputableMonolith.Holography.TurnRatioCarrier
   3import IndisputableMonolith.Holography.SeamLedgerDischarge
   4
   5/-!
   6# HorizonClockRate: B3 rate-only typing (LEG-B, panel 2026-07-06)
   7
   8Prose acceptance: `derive_20260706_073650` (critic ACCEPT). This module types **only**
   9what B3 delivers: near-horizon Rindler geometry makes the continued Euclidean angle
  10advance at rate `κ` per unit Euclidean time (`dθ/dτ_E = κ`). It does **not** assert the
  11`2π` closure period; that is B2's output (`DeficitFreePeriod.euclideanPeriod`,
  12`TurnRatioCarrier.turnRatio_eq_one_iff`).
  13
  14The legacy `DeficitFreePeriod.HorizonRate` (`κ = 1/R`) is a separate Schwarzschild
  15normalization socket for the Clausius bridge. Do not conflate it with this B3 delivery.
  16-/
  17
  18namespace IndisputableMonolith
  19namespace Holography
  20namespace HorizonClockRate
  21
  22open DeficitFreePeriod TurnRatioCarrier SeamLedgerDischarge
  23
  24/-! ## Named geometric premise (MODEL) -/
  25
  26/-- **Near-horizon Rindler normal form (MODEL).** A Killing horizon with surface
  27gravity `κ > 0` admits adapted coordinates `(ρ, τ)` near the bifurcation surface with
  28local metric coefficient `κ` on the static Killing sector. This module records only the
  29existence of the rate parameter; no thermality, KMS, or entropy-area law is imported. -/
  30structure NearHorizonRindlerForm (kappa : ℝ) : Prop where
  31  kappa_pos : 0 < kappa
  32
  33/-! ## B3 delivery: angular rate only -/
  34
  35/-- Euclidean angular coordinate after continuation: `θ = κ τ_E`. -/
  36noncomputable def euclideanAngle (kappa tauE : ℝ) : ℝ :=
  37  kappa * tauE
  38
  39/-- **B3 rate (THEOREM).** The continued recognition clock advances Euclidean angle at
  40rate `κ`: `dθ/dτ_E = κ` for all `τ_E`. Pure calculus on `θ = κ τ_E`; no period input. -/
  41theorem euclideanAngle_rate (kappa : ℝ) (hk : 0 < kappa) (tauE : ℝ) :
  42    HasDerivAt (euclideanAngle kappa) kappa tauE := by
  43  unfold euclideanAngle
  44  simpa using (hasDerivAt_id (x := tauE)).const_mul kappa
  45
  46/-- Algebraic form of the rate law (the panel's `dθ/dτ_E = κ`). -/
  47theorem euclideanAngle_deriv_eq (kappa : ℝ) (hk : 0 < kappa) (tauE : ℝ) :
  48    deriv (euclideanAngle kappa) tauE = kappa :=
  49  (euclideanAngle_rate kappa hk tauE).deriv
  50
  51/-- **Typed B3 bundle (FORCED-CONDITIONAL on `NearHorizonRindlerForm`).** -/
  52structure ClockRateBundle (kappa : ℝ) : Prop where
  53  rindler : NearHorizonRindlerForm kappa
  54  rate : ∀ tauE : ℝ, deriv (euclideanAngle kappa) tauE = kappa
  55
  56/-- Every Rindler form yields the rate bundle. -/
  57theorem clockRateBundle_of_rindler {kappa : ℝ} (h : NearHorizonRindlerForm kappa) :
  58    ClockRateBundle kappa where
  59  rindler := h
  60  rate := fun tauE => euclideanAngle_deriv_eq kappa h.kappa_pos tauE
  61
  62/-! ## Hyperbolic mismatch class (grounds `HasRealEigen`) -/
  63
  64/-- **Physical commitment (HYPOTHESIS/MODEL).** The delivered mismatch leg is a
  65positive real eigenvalue on the hyperbolic (non-elliptic) class: not ±1, not complex.
  66This is the typed reading of `HasRealEigen` in `SeamTransferCore`. -/
  67def HyperbolicMismatchClass (W : Matrix (Fin 2) (Fin 2) ℝ) (x : ℝ) : Prop :=
  68  SeamTransferCore.HasRealEigen W x ∧ 0 < x ∧ x ≠ 1
  69
  70/-! ## Fence: B3 does not assert the period -/
  71
  72/-- **Fence theorem (THEOREM).** B3's rate law alone does not pin a closure time; the
  73full-turn time `2π/κ` is definitionally the B2 carrier output, not an input here. -/
  74theorem period_is_b2_output_not_b3_input (kappa : ℝ) :
  75    euclideanPeriod kappa = 2 * Real.pi / kappa := rfl
  76
  77/-- At the B2-forced period, the turn ratio is unity (B1/B2 linkage; B3 not used). -/
  78theorem turnRatio_unity_at_b2_period (kappa T : ℝ) (hk : 0 < kappa) (hT : 0 < T) :
  79    T = euclideanPeriod kappa → turnRatio kappa T = 1 :=
  80  (turnRatio_eq_one_iff kappa T hk).mpr
  81
  82/-- **Explicit non-claim:** `ClockRateBundle` carries no field about `T = 2π/κ`. -/
  83theorem clockRateBundle_silent_on_period {kappa : ℝ} (_h : ClockRateBundle kappa) :
  84    True := trivial
  85
  86/-! ## Bridge to legacy `HorizonRate` (normalization socket, separate leg) -/
  87
  88/-- The Clausius-bridge normalization `κ = 1/R` is an independent MODEL socket; it is
  89not part of the B3 rate-only delivery above. -/
  90theorem legacy_horizonRate_is_separate (kappa R : ℝ) :
  91    DeficitFreePeriod.HorizonRate kappa R ↔ kappa = 1 / R :=
  92  Iff.rfl
  93
  94end HorizonClockRate
  95end Holography
  96end IndisputableMonolith
  97