kernelUpObs
plain-language theorem explainer
Defines the kernel observation on a posting-rated world: the carrier-enlarging up-step weight from size one to size two equals one. Anyone citing D13 (rate-sensitive carrier dynamics) or the D12/D13 contrast uses this predicate as the discriminating observation. The body is a one-line abbreviation of the birth branch of the carrier step weight at (1,2).
Claim. For a posting-rated world $w$ (bare posting dynamics plus an attached birth-death rate law), the kernel observation holds when the carrier-enlarging step weight from size $1$ to size $2$ equals $1$, i.e. the birth rate at size one is one.
background
Gap-2 Room B is a necessary-reasons census for insertion asymmetry: recognition structure is asked to force the asymmetric carrier-enlarging rate law (one creation opportunity per tick, one deletion choice per existing label), or a counting-equivalent law $\mu(n+1)=(n+1)\lambda n$ that is not baked from a weight. The target is a search directive, never a proof premise.
A posting-rated world packages bare posting dynamics with an attached birth-death rate law. Reachability in such a world is exactly bare posting reachability and cannot inspect the rates. By contrast, the carrier step weight is the birth-death kernel on carrier sizes: from size $m$ the world steps up to $m+1$ with its birth rate and down to $m-1$ with its per-label death rate, so the kernel is a genuine function of the attached rates.
D12 established that bare posting is blind to the rate law (no posting-respecting selector separates counting rates from the equal-per-slot decoy). D13 asks for a rate-sensitive observation that factors through the carrier-enlarging kernel instead.
proof idea
Pure definition: the predicate on a rated world $w$ is exactly the equality of the carrier step weight at source size $1$ and target size $2$ with the constant $1$. Unfolding the step weight, that is the birth-rate branch $w.\mathrm{rates}.\mathrm{birth},1 = 1$. No tactics or lemmas are involved.
why it matters
This is the concrete observation that closes D13 as sharpened. Downstream, D13_sharpened_holds exhibits it as a predicate that factors through the carrier-enlarging kernel, holds of the counting rates sizeBlindBirthPerLabelDeath, and fails of the equal-per-slot decoy. D13_theorem packages the same triple into the rate-sensitivity interface, with factorization provenance rather than a vacuous True. The contrast theorem kernel_sees_what_posting_cannot pairs D12's wall (posting cannot select) with this observation's success on the same two worlds.
In the census, D10 gives existence of the counting rates and D11 builds the insertion kernel from them; D12 scopes selection away from bare posting; this definition supplies the kernel-side discriminator that D13 needs. Ledger provenance of the kernel schedule itself is deferred to D14. Framework-wise it sits in the gravity seven-gaps chain on carrier insertion asymmetry, not in the T0-T8 forcing spine.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.