LocalHorizonContext
plain-language theorem explainer
A shared parameter pack that binds a one-sided horizon-cut model, a posted horizon-record dimension, and a near-horizon Rindler rate (kappa > 0) into one local context. Downstream exterior-record heat, channel stress, and boost-heat transport theorems quantify over this pack. It is pure data: three fields, no thermality or curvature axioms.
Claim. A local horizon context for natural parameters $a,s,b,r$ and real surface-gravity scale $\kappa$ consists of a horizon-record dimension $N\in\mathbb{N}$, a one-sided cut model $\mathrm{HorizonSumsPerSide}(a,s,b,r,N)$, and a near-horizon Rindler-form model at rate $\kappa$. No thermality, curvature, or Einstein-equation premise is part of the data.
background
The module packages three audited legs on one shared context. LEG-A is the one-sided cut model HorizonSumsPerSide, which forces the horizon record to double-post the seam. Posted-record heat is then the exterior projection of a closed cut configuration, with discrete books balance and unit-temperature Clausius proved as theorems about that record. LEG-B is the near-horizon rate model NearHorizonRindlerForm, presently only the positivity constraint $\kappa>0$, with the least positive deficit-free period proved separately.
A LocalCut is a globally closed one-sided cut living inside such a context: cut data are relative to the context, while rate and one-sided premises sit on the context itself. Interior-private and rest-of-universe data are invisible in the exterior record. The module deliberately excludes stress tensors, Ricci curvature, focusing laws, Unruh claims, and Einstein equations.
Carrier dimensions $a,s,b,r$ size the exterior cut channels and record bookkeeping; $\kappa$ is the Rindler acceleration scale used later when calibrated posted heat is matched to surface-gravity times boost moment times null flux.
proof idea
No proof: this is a structure declaration. It packages three fields (horizon-record dimension, one-sided-cut witness, near-horizon Rindler witness) under parameters $(a,s,b,r,\kappa)$. Downstream theorems quantify over an instance $H$ and over closed cuts $c,c':\mathrm{LocalCut},H$.
why it matters
This context is the ambient type for the exterior-record heat and stress pipeline. Parent results in RecordFluxBoostHeat and RecordFluxStress all take {H : LocalHorizonContext a s b r kappa}: exterior step heat equals the sum of channel deltas; uniform channel attachment plus calibration yields posted heat equal to minus surface gravity times boost moment times null stress flux; quadratic probe pairing converts event-stress contraction into posted heat times squared pairing; zero covectors cannot represent nonzero calibrated heat. The certificate RecordFluxBoostHeatCert is stated uniformly over such contexts.
In the Recognition holography layer this is the seam between the one-sided cut model and the near-horizon rate model, without smuggling thermality. It supports discrete Clausius / books-balance statements about exterior records while remaining silent on curvature match and Einstein equations. Framework landmarks touched only indirectly: eight-tick / Clifford grading sits upstream of the broader ledger story, not inside this pack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.