IndisputableMonolith.Gravity.RecordFluxBoostHeat

   1import IndisputableMonolith.Gravity.RecordFluxStress
   2
   3/-!
   4# Posted-record heat to null stress flux
   5
   6This module isolates the exact algebraic bridge between the posted heat of a
   7fixed recognition cut and the null contraction of its event-stress matrix.
   8
   9If every active channel covector has the same pairing `q` with one probe `k`,
  10then the stress contraction is exactly `q²` times the posted record heat.
  11An explicit calibration law then gives the local boost-heat equation.
  12
  13Honesty tags:
  14
  15* THEOREM: the sum, contraction, calibration, and decoy algebra below.
  16* MODEL: the channel covectors, probe, uniform-pairing attachment, and physical
  17  heat calibration.
  18* OPEN: deriving those MODEL inputs from recognition geometry.
  19-/
  20
  21noncomputable section
  22
  23namespace IndisputableMonolith
  24namespace Gravity
  25namespace RecordFluxBoostHeat
  26
  27open ClausiusEinsteinBridge
  28open RecordFluxStress
  29open Holography.LocalRecognitionHorizonCut
  30
  31/--
  32Uniform attachment of the cut channels to one probe.  The common pairing is
  33an explicit geometric MODEL input; it is not inferred from the cut record.
  34-/
  35def UniformProbeAttachment
  36    {a s : ℕ}
  37    (p : ExteriorCutChannel a s → Fin 4 → ℝ)
  38    (k : Fin 4 → ℝ)
  39    (q : ℝ) : Prop :=
  40  ∀ ch, (∑ μ, p ch μ * k μ) = q
  41
  42/--
  43The real-valued posted heat is the sum of the real channel weights.
  44-/
  45theorem exteriorStepHeat_cast_eq_sum_channelDelta
  46    {a s b r : ℕ} {kappa : ℝ}
  47    {H : LocalHorizonContext a s b r kappa}
  48    (c c' : LocalCut H) :
  49    (exteriorStepHeat c c' : ℝ) =
  50      ∑ ch : ExteriorCutChannel a s, channelDelta c c' ch := by
  51  have h := exteriorStepHeat_eq_sum_channelDeltaZ c c'
  52  unfold channelDelta
  53  exact_mod_cast h
  54
  55/--
  56Uniform probe pairing converts the fixed event-stress contraction into the
  57posted cut heat times the common squared pairing.
  58-/
  59theorem quadContr_cutEventStress_eq_sq_mul_heat
  60    {a s b r : ℕ} {kappa : ℝ}
  61    {H : LocalHorizonContext a s b r kappa}
  62    (c c' : LocalCut H)
  63    (p : ExteriorCutChannel a s → Fin 4 → ℝ)
  64    (k : Fin 4 → ℝ)
  65    (q : ℝ)
  66    (hattach : UniformProbeAttachment p k q) :
  67    quadContr (cutEventStress c c' p) k =
  68      q ^ 2 * (exteriorStepHeat c c' : ℝ) := by
  69  rw [quadContr_cutEventStress]
  70  unfold UniformProbeAttachment at hattach
  71  simp_rw [hattach]
  72  rw [← Finset.sum_mul]
  73  rw [← exteriorStepHeat_cast_eq_sum_channelDelta c c']
  74  ring
  75
  76/--
  77Named MODEL normalization assumption required to convert bit-valued posted
  78heat into the local boost-energy normalization.  It supplies the whole
  79physical heat-scale conversion and is not derived from the record data.
  80-/
  81def PostedBoostHeatNormalizationAssumption
  82    (surfaceGravity boostMoment heatScale q : ℝ) : Prop :=
  83  heatScale = -surfaceGravity * boostMoment * q ^ 2
  84
  85/--
  86With uniform channel attachment and the explicit calibration, calibrated
  87posted heat equals minus surface gravity times boost moment times null stress
  88flux.  The theorem derives the equality from two separately named inputs.
  89-/
  90theorem matchesPostedBoostHeat_of_attachment
  91    {a s b r : ℕ} {kappa : ℝ}
  92    {H : LocalHorizonContext a s b r kappa}
  93    (c c' : LocalCut H)
  94    (p : ExteriorCutChannel a s → Fin 4 → ℝ)
  95    (k : Fin 4 → ℝ)
  96    (q surfaceGravity boostMoment heatScale : ℝ)
  97    (hattach : UniformProbeAttachment p k q)
  98    (hcal : PostedBoostHeatNormalizationAssumption
  99      surfaceGravity boostMoment heatScale q) :
 100    heatScale * (exteriorStepHeat c c' : ℝ) =
 101      -surfaceGravity * boostMoment *
 102        quadContr (cutEventStress c c' p) k := by
 103  rw [quadContr_cutEventStress_eq_sq_mul_heat c c' p k q hattach]
 104  unfold PostedBoostHeatNormalizationAssumption at hcal
 105  rw [hcal]
 106  ring
 107
 108/--
 109Load-bearing decoy: zero channel covectors produce zero stress flux, so they
 110cannot represent a nonzero calibrated posted heat.
 111-/
 112theorem zero_covectors_fail_nonzero_posted_heat
 113    {a s b r : ℕ} {kappa : ℝ}
 114    {H : LocalHorizonContext a s b r kappa}
 115    (c c' : LocalCut H)
 116    (k : Fin 4 → ℝ)
 117    (surfaceGravity boostMoment heatScale : ℝ)
 118    (hheat : heatScale * (exteriorStepHeat c c' : ℝ) ≠ 0) :
 119    ¬ heatScale * (exteriorStepHeat c c' : ℝ) =
 120      -surfaceGravity * boostMoment *
 121        quadContr
 122          (cutEventStress c c' (fun _ _ => (0 : ℝ))) k := by
 123  intro h
 124  rw [cutEventStress_zero_of_covector_zero] at h
 125  have hz :
 126      quadContr (0 : Matrix (Fin 4) (Fin 4) ℝ) k = 0 := by
 127    simp [quadContr]
 128  rw [hz, mul_zero] at h
 129  exact hheat h
 130
 131/-- Certificate for the conditional posted-heat transport. -/
 132structure RecordFluxBoostHeatCert : Prop where
 133  heat_is_channel_sum :
 134    ∀ {a s b r : ℕ} {kappa : ℝ}
 135      {H : LocalHorizonContext a s b r kappa}
 136      (c c' : LocalCut H),
 137      (exteriorStepHeat c c' : ℝ) =
 138        ∑ ch : ExteriorCutChannel a s, channelDelta c c' ch
 139  uniform_attachment_transports :
 140    ∀ {a s b r : ℕ} {kappa : ℝ}
 141      {H : LocalHorizonContext a s b r kappa}
 142      (c c' : LocalCut H)
 143      (p : ExteriorCutChannel a s → Fin 4 → ℝ)
 144      (k : Fin 4 → ℝ)
 145      (q surfaceGravity boostMoment heatScale : ℝ),
 146      UniformProbeAttachment p k q →
 147      PostedBoostHeatNormalizationAssumption
 148        surfaceGravity boostMoment heatScale q →
 149      heatScale * (exteriorStepHeat c c' : ℝ) =
 150        -surfaceGravity * boostMoment *
 151          quadContr (cutEventStress c c' p) k
 152
 153theorem recordFluxBoostHeatCert : RecordFluxBoostHeatCert where
 154  heat_is_channel_sum := exteriorStepHeat_cast_eq_sum_channelDelta
 155  uniform_attachment_transports :=
 156    matchesPostedBoostHeat_of_attachment
 157
 158end RecordFluxBoostHeat
 159end Gravity
 160end IndisputableMonolith
 161