Gravity Record Flux Boost Heat Posted Boost Heat Normalization Assumption

The calibration bridge

In the Recognition Science framework, a ledger is a discrete record of events, and the framework's library is a machine-checked collection of formal theorems built from that starting point. One module in that library, RecordFluxBoostHeat, studies a fixed cut in that record and asks how the heat posted to that cut relates to a quantity called null stress flux, a measure of energy flow along a lightlike direction. The central theorem in the module proves that when every active channel in the cut pairs with a single probe in the same way, the stress contraction equals the square of that common pairing times the posted heat.

The declaration PostedBoostHeatNormalizationAssumption is not a theorem but a definitional choice. It states that a heat scale equals minus surface gravity times boost moment times the square of the common pairing. This is the physical calibration: it converts the bit-valued posted heat into a continuous energy scale. The framework is explicit that this assumption supplies the whole physical heat-scale conversion and is not derived from the record data. It is a MODEL input, a deliberate choice about how to attach the discrete ledger to continuous physics.

With that assumption in place, a second theorem derives the local boost-heat equation: calibrated posted heat equals minus surface gravity times boost moment times null stress flux. The equality follows from two separately named inputs, the uniform attachment and the calibration assumption. A companion theorem shows the boundary of the construction: if all channel covectors are zero, the stress flux vanishes, so zero channels cannot represent a nonzero calibrated posted heat. That decoy result keeps the construction honest about what the algebra can and cannot carry.

What the declaration does not claim is just as important. It does not derive the uniform attachment from the cut record; the common pairing is an explicit geometric MODEL input. It does not derive the physical heat calibration from recognition geometry; that derivation remains OPEN. The theorems prove the algebra that follows once those MODEL inputs are granted, not the inputs themselves. The framework's own honesty tags make this division explicit: the sum, contraction, calibration, and decoy algebra are THEOREM, while the channel covectors, probe, uniform-pairing attachment, and physical heat calibration are MODEL.

/--
Named MODEL normalization assumption required to convert bit-valued posted
heat into the local boost-energy normalization.  It supplies the whole
physical heat-scale conversion and is not derived from the record data.
-/
def PostedBoostHeatNormalizationAssumption
    (surfaceGravity boostMoment heatScale q : ℝ) : Prop :=
  heatScale = -surfaceGravity * boostMoment * q ^ 2

/--
With uniform channel attachment and the explicit calibration, calibrated
posted heat equals minus surface gravity times boost moment times null stress
flux.  The theorem derives the equality from two separately named inputs.
-/
theorem matchesPostedBoostHeat_of_attachment
    {a s b r : ℕ} {kappa : ℝ}
    {H : LocalHorizonContext a s b r kappa}
    (c c' : LocalCut H)
    (p : ExteriorCutChannel a s → Fin 4 → ℝ)
    (k : Fin 4 → ℝ)
    (q surfaceGravity boostMoment heatScale : ℝ)
    (hattach : UniformProbeAttachment p k q)
    (hcal : PostedBoostHeatNormalizationAssumption
      surfaceGravity boostMoment heatScale q) :
    heatScale * (exteriorStepHeat c c' : ℝ) =
      -surfaceGravity * boostMoment *
        quadContr (cutEventStress c c' p) k := by
  rw [quadContr_cutEventStress_eq_sq_mul_heat c c' p k q hattach]
  unfold PostedBoostHeatNormalizationAssumption at hcal
  rw [hcal]
  ring

/--
Load-bearing decoy: zero channel covectors produce zero stress flux, so they
cannot represent a nonzero calibrated posted heat.
-/
theorem zero_covectors_fail_nonzero_posted_heat
    {a s b r : ℕ} {kappa : ℝ}
    {H : LocalHorizonContext a s b r kappa}
    (c c' : LocalCut H)
    (k : Fin 4 → ℝ)
    (surfaceGravity boostMoment heatScale : ℝ)
    (hheat : heatScale * (exteriorStepHeat c c' : ℝ) ≠ 0) :
    ¬ heatScale * (exteriorStepHeat c c' : ℝ) =
      -surfaceGravity * boostMoment *
        quadContr
          (cutEventStress c c' (fun _ _ => (0 : ℝ))) k := by
  intro h
  rw [cutEventStress_zero_of_covector_zero] at h
  have hz :
      quadContr (0 : Matrix (Fin 4) (Fin 4) ℝ) k = 0 := by
    simp [quadContr]
  rw [hz, mul_zero] at h
  exact hheat h

/--
Uniform attachment of the cut channels to one probe.  The common pairing is
an explicit geometric MODEL input; it is not inferred from the cut record.
-/
def UniformProbeAttachment
    {a s : ℕ}
    (p : ExteriorCutChannel a s → Fin 4 → ℝ)
    (k : Fin 4 → ℝ)
    (q : ℝ) : Prop :=
  ∀ ch, (∑ μ, p ch μ * k μ) = q

What this page does not claim

The physical heat calibration is derived from recognition geometry; deriving it remains OPEN. The uniform attachment of channels to a probe follows from the cut record; it is an explicit MODEL input. The declaration proves anything about the existence of the surface gravity or boost moment values it references.

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/Gravity/RecordFluxBoostHeat.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: