assumedTargetStatus
plain-language theorem explainer
Status tag for the Gap-2 label-insertion census: the corrected target (carrier-enlarging birth/death dynamics forcing InsertionStationarity and hence the gauge-counting principle) is recorded as open on the rate-asymmetry question. Anyone auditing the seven-gap gravity ledger cites this string when checking which necessary reasons remain unresolved. It is a one-line string constant, not a proved claim.
Claim. The assumed-target status for the Gap-2 label-insertion dynamics census is the literal tag $\mathrm{OPEN\_RATE\_ASYMMETRY}$: the physical rate asymmetry (size-blind birth versus per-label death) that would force insertion stationarity is not yet derived from recognition structure.
background
Gap-2 in the gravity seven-gaps program asks for an explicit carrier-enlarging label-insertion and removal dynamics that forces InsertionStationarity (equivalently the gluing law), and thereby inverse factorials and the gauge-counting principle, without smuggling in $\mu$, Aut, unit fugacity, or stationarity under another name.
The module runs a necessary-reasons census: each candidate reason is marked THEOREM, OPEN, MODEL, or REFUTED. Honesty notes already prove that detailed balance equates weight ratios to rate ratios; equal per-slot insert/delete rates force constant weight and therefore fail InsertionStationarity; size-blind birth with per-label death forces stationarity once unit and atom are fixed. What remains open is deriving, from recognition structure, that birth is size-blind (one creation opportunity per tick) while death is per existing label, or an equivalent asymmetry yielding $\mu_{n+1}=(n+1)\lambda_n$ without writing the stationary law into the rates by hand.
An upstream sibling status in the gauge-counting inevitable-reasons module tags a different assumed target as REFUTED_AS_STATED and redirects to the uninhabited CorrectedMeasurePremise.
proof idea
No proof. The declaration is a definitional string constant equal to "OPEN_RATE_ASYMMETRY". It records census metadata for the module's reason table and composite certificate; there is no tactic or term argument.
why it matters
The tag feeds the composite certificate labelInsertionDynamics_certified, which packages the nine-row reason table, the proved detailed-balance and equal-per-slot failures, and the positive size-blind-birth / per-label-death forcing of InsertionStationarity, while leaving the measure-derived benchmark unmoved until later D07/D08 closures.
In the Recognition gravity ledger this is the honesty marker for Gap-2: theorems already rule out equirating slots and decoy rate laws, but the physical origin of the birth/death asymmetry is still open. Cambrian target research can grind lemmas once the dynamics is typed; it cannot invent that missing asymmetry. The flag therefore prevents overclaiming that richer ledger structure alone forces the gauge-counting principle, and keeps the census aligned with the binding Gap-2 gluing-law / insertion-stationarity session prompt.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.