Pith. sign in
module module moderate

IndisputableMonolith.Gravity.SevenGaps.Gap2LabelInsertionDynamics

show as:
view Lean formalization →

Defines size-indexed birth and death rates for a one-kind label carrier, together with detailed-balance and equal-per-slot rate laws. Gap-2 workers cite it when checking whether constant weights and per-slot symmetry can produce insertion stationarity. The module packages rate structures, balance identities, and three short lemmas (D01–D03) that separate ordinary detailed balance from the asymmetric insertion law.

claimFor a one-kind label carrier of size $n$, let $\mathrm{birth}(n)$ be the total forward rate $n\to n+1$ and $\mathrm{death}(n)$ the total backward rate $n\to n-1$. Detailed balance relates these rates to a weight; equal-per-slot rates assign the same per-label contribution at each size. Constant weight plus equal-per-slot rates satisfy ordinary detailed balance, yet fail the Gap-2 insertion-stationarity condition.

background

Gap 2 in the Seven Gaps gravity program asks whether recognition-ledger structure forces the gluing law (inverse-factorial labeled weight) and the gauge-counting principle, or else yields a scoped no-go. The upstream module on gluing-law stationarity frames insertion stationarity and the bare-posting wall as the exact goal.

This module supplies the kinetic language for that question: size-indexed birth and death rates on a single label kind. Birth at $n$ is the total rate of enlarging the carrier; death at $n$ is the total rate of shrinking it (evaluated when the current size is one larger). Detailed balance is the equilibrium relation between those rates and a weight on sizes. Equal-per-slot rates mean every occupied label contributes the same infinitesimal rate, independent of which slot is chosen.

The sibling definitions also record a small reason table and status tags used by the necessary-reasons censuses that import this file.

proof idea

Definition-heavy module with a short lemma spine. BirthDeathRates and DetailedBalance fix the rate and balance interfaces. D01 relates the balance ratio to a scaled death rate. equalPerSlotRates and constantWeight are pure rate/weight shapes; constantWeight_detailedBalance_equalPerSlot and D02 show that constant weight with equal-per-slot rates closes ordinary detailed balance. D03 is the negative companion: the same equal-per-slot package does not imply insertion stationarity. No deep tactic proof; the content is interface plus elementary algebraic checks.

why it matters in Recognition Science

Feeds two Gap-2 necessary-reasons censuses. GaugeCountingInevitableReasons assumes the measure target (gauge-counting principle / $\nu=1/|\mathrm{Aut}|$) and lists every fact that would make it unavoidable; rate-balance structure from this module is part of that census. InsertionAsymmetryInevitableReasons takes as target the asymmetric carrier-enlarging law (size-blind birth per label death, or $\mu(n+1)=(n+1)\lambda n$ not baked from weight) and again uses these birth/death and balance facts as candidate reasons.

In the broader RS gravity stack, Gap 2 sits between ledger posting structure and the combinatorial weight that should match gauge volumes. Showing that symmetric equal-per-slot kinetics give detailed balance yet miss insertion stationarity sharpens why an asymmetric insertion law, if forced, is not a free modeling choice.

scope and limits

used by (2)

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 (30)