Pith. sign in
module module high

IndisputableMonolith.Gravity.RecordFluxBoostHeat

show as:
view Lean formalization →

Uniform attachment of exterior cut channels to one probe, so posted boost heat can be matched to the record-flux stress quadratic. The common pairing is an explicit geometric model input, not read off the cut record. Gravity workers on the posted-boost heat pathway cite this module. It packages the attachment hypothesis, heat-sum and contraction identities, a normalization assumption, and a small certificate.

claimA uniform probe attachment equips the exterior cut channels with one common covector pairing (a geometric model input). Under a posted-boost heat normalization assumption, the quadratic contraction of the cut-event stress equals a squared factor times the exterior step heat (sum of channel deltas). Zero covectors cannot realize nonzero posted heat.

background

Upstream, the record-flux stress module builds one probe-independent symmetric stress-like matrix from signed exterior cut-channel events and an explicit model covector assignment. Its quadratic contraction is already proved for every probe of that fixed matrix.

This module sits one layer up: it forces all cut channels to share a single probe attachment. The shared pairing is declared as model data; the cut record alone does not determine it. Exterior step heat is the sum of per-channel deltas, and the stress quadratic is related to that heat by a squared multiplicative factor once attachment and normalization are in place.

The local setting is conditional gravity bookkeeping: posted boost heat is matched to null-stress transport only after these geometric and normalization hypotheses are stated.

proof idea

Definition-and-lemma module, not a single theorem. It introduces a uniform probe attachment structure, then proves the exterior step heat (after cast) equals the sum of channel deltas. A contraction identity equates the quadratic form of the cut-event stress to a square times that heat. A named posted-boost heat normalization assumption is the bridge hypothesis. Matching of posted boost heat follows from attachment plus that assumption; a separate lemma shows zero covectors cannot produce nonzero posted heat. A small certificate bundles the package for downstream audit.

why it matters in Recognition Science

Feeds the RecordFluxBoostHeatAudit module, whose doc-comment states it is the axiom audit for conditional posted-record heat to null stress transport. Without uniform attachment and the heat-contraction identity, the audit has nothing concrete to discharge. In the gravity stack this is the bridge from probe-independent cut-event stress to the posted boost-heat side of the ledger. It does not itself close the full transport theorem; it supplies the geometric and algebraic ingredients the audit module checks.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (8)