PostedBoostHeatNormalizationAssumption
plain-language theorem explainer
Named model assumption equating heat scale to minus surface gravity times boost moment times pairing squared. It converts bit-valued posted heat into the local boost-energy normalization and is not derived from record data. Downstream boost-heat matching theorems take it as an explicit input. The body is a pure propositional equality, not a proved identity.
Claim. The posted boost-heat normalization assumption on surface gravity $\kappa$, boost moment $B$, heat scale $h$, and channel-probe pairing $q$ is the equality $h = -\kappa\, B\, q^{2}$.
background
The module isolates the algebraic bridge from posted heat on a fixed recognition cut to the null contraction of its event-stress matrix. When every active channel covector pairs with one probe $k$ by the same value $q$, the stress contraction equals $q^{2}$ times posted record heat; an explicit calibration then yields the local boost-heat equation.
Honesty tags split THEOREM content (sum, contraction, calibration algebra) from MODEL inputs (channel covectors, probe, uniform pairing, physical heat calibration). Deriving those MODEL inputs from recognition geometry remains OPEN.
This declaration is the named MODEL normalization that turns bit-valued posted heat into the local boost-energy scale. It is not extracted from the record data itself.
proof idea
Definitional Prop: the body is the single equality heatScale = -surfaceGravity * boostMoment * q ^ 2. No tactics, no lemmas, no derivation. Callers discharge or assume it as a hypothesis.
why it matters
Supplies the physical heat-scale conversion used by matchesPostedBoostHeat_of_attachment, which states that with uniform channel attachment and this calibration, calibrated posted heat equals minus surface gravity times boost moment times null stress flux, derived from two separately named inputs. Also appears in the certificate structure RecordFluxBoostHeatCert for conditional posted-heat transport.
In the Recognition gravity stack this is the MODEL hinge between discrete posted heat and continuum boost energy on a local horizon. It does not close the OPEN task of deriving the calibration from recognition geometry; it only names the conversion so the THEOREM layer can stay clean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.