KernelCostContent
plain-language theorem explainer
Packages the five single-ratio cost axioms the recognition kernel asserts: reciprocity, normalization, the Recognition Composition Law, unit log-curvature calibration, and continuity on positive reals. Anyone citing the kernel-to-J forcing step or the gravity reach-wall uses this bundle. It is a pure Prop structure, not a proved claim.
Claim. A function $F:\mathbb{R}\to\mathbb{R}$ has kernel cost content when: (i) $F(x)=F(x^{-1})$ for all $x>0$; (ii) $F(1)=0$; (iii) $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$ for all $x,y>0$; (iv) if $G(t)=F(e^t)$ then $G''(0)=1$; (v) $F$ is continuous on $(0,\infty)$.
background
This module asks how far the recognition kernel reaches into gravity's strain dynamics. The C2 bridge needs a residue: continuous strain motion that strictly lowers recognition cost off the least-cost state. The module separates what the kernel forces about cost from what it says about motion.
Kernel cost content is exactly the premise package consumed by the law that forces the cost to be $J$. Reciprocity means $F(x)=F(1/x)$ on positive ratios. Normalization is $F(1)=0$. The composition field is the Recognition Composition Law (RCL). Calibration is unit second derivative of $G(t)=F(e^t)$ at the origin (equivalently $\lim_{t\to 0} 2F(e^t)/t^2=1$). Continuity is on $(0,\infty)$.
Every field is a property of the cost of a single ratio. None quantifies over maps on the ledger, sequences of postings, or time evolution. The kernel fixes configuration cost; it does not prescribe how configurations move.
proof idea
No proof: this is a structure definition bundling five Prop fields on a cost $F:\mathbb{R}\to\mathbb{R}$. Inhabitants are built fieldwise (as in the companion theorem that $J$ satisfies all five). Downstream non-entailment arguments treat the whole package as a single hypothesis and exhibit a continuous strain map that preserves cost while never reaching the carrier.
why it matters
This is the named interface between the forcing chain's cost uniqueness and the gravity seven-gaps reach question. Downstream, $J$ is shown to inhabit the structure, so the kernel's cost content is realized. The reach-wall theorem then pairs that fact with the ledger's reciprocal involution $x\mapsto 1/x$ (strain $t\mapsto -t$): the map is continuous, preserves bare recognition cost, and never reaches the carrier from nonzero strain. The exact logical form is that kernel cost content does not imply every continuous strain map spends cost off the minimum.
In framework terms this sits at T5 ($J$-uniqueness via RCL plus the listed normalizations) and draws a hard line: the kernel fixes $J$, not the descent residue the C2 bridge adopts. That residue must be stated as a separate named postulate (the cost-spending substrate), not smuggled in as kernel content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.