UniformProbeAttachment
plain-language theorem explainer
Uniform probe attachment is the MODEL hypothesis that every exterior cut-channel covector pairs with one fixed probe to the same real value q. Horizon-flux and boost-heat arguments cite it to convert null stress contraction into posted record heat times q squared. The body is a pure Prop: a universal equality of pairings over channels, with no derived content.
Claim. For $a,s\in\mathbb{N}$, channel covectors $p$ on exterior cut channels $\mathrm{Fin}\,a\oplus\mathrm{Fin}\,s$ valued in $\mathbb{R}^4$, a probe $k\in\mathbb{R}^4$, and $q\in\mathbb{R}$, uniform attachment holds when $\sum_{\mu} p(\mathrm{ch})_{\mu}\,k_{\mu}=q$ for every channel $\mathrm{ch}$.
background
The module isolates the algebraic bridge from posted heat of a fixed recognition cut to the null contraction of its event-stress matrix. Exterior cut channels are the sum type of exterior-private bits and seam bits (ExteriorCutChannel a s := Fin a ⊕ Fin s). Each channel carries a real covector in four components; a single probe vector $k$ is paired against every such covector.
Posted heat is the real sum of channel weights on the cut. The module header states the target identity: if every active channel covector has the same pairing $q$ with one probe $k$, then the stress contraction equals $q^2$ times that posted heat. An explicit calibration law then yields the local boost-heat equation.
Honesty tags separate THEOREM algebra (sums, contractions, calibration) from MODEL inputs (covectors, probe, uniform pairing, physical heat scale). Deriving those MODEL inputs from recognition geometry remains OPEN.
proof idea
Definitional Prop, not a proved theorem. The body is the single quantified equality $\forall,\mathrm{ch},;\sum_\mu p(\mathrm{ch})\mu,k\mu=q$. No lemmas are applied; the declaration packages the uniform-pairing hypothesis for later use.
why it matters
This Prop is the named MODEL gate for the module's main transport theorems. quadContr_cutEventStress_eq_sq_mul_heat uses it to turn the fixed event-stress contraction into posted cut heat times the common squared pairing. matchesPostedBoostHeat_of_attachment then combines uniform attachment with an explicit calibration so that calibrated posted heat equals minus surface gravity times boost moment times null stress flux, "from two separately named inputs."
RecordFluxBoostHeatCert packages the conditional posted-heat transport and lists the channel-sum heat identity among its fields. In the broader Recognition gravity stack the declaration sits on the posted-record side of the flux bridge; it does not touch the T0–T8 forcing chain, RCL, or the phi-ladder mass formula. It marks the open gap flagged in the module doc: the common pairing is an explicit geometric MODEL input, not inferred from the cut record.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.