IndisputableMonolith.Gravity.SevenGaps.Gap2LabelInsertionDynamics

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2GluingLawStationarity
   2
   3/-!
   4# Gap-2 label-insertion dynamics (necessary-reasons census)
   5
   6Assume the corrected Gap-2 target is required: an explicit carrier-enlarging
   7label-insertion / removal dynamics forces `InsertionStationarity`
   8(equivalently `GluingLaw`), hence inverse factorials and
   9`GaugeCountingPrinciple`, without assuming `mu`, `Aut`, unit fugacity, or
  10`InsertionStationarity` under a new name.
  11
  12Then every fact that would make that forcing unavoidable is listed below.
  13Each reason is proved, left OPEN, recorded as MODEL, or refuted. A failed
  14reason does not automatically mean its opposite.
  15
  16Method: `plans/Necessary_Reasons_Process_20260807.html`.
  17Parent modules: `Gap2GluingLawStationarity.lean`, `UnitFugacitySelector.lean`.
  18Binding prompt:
  19`plans/QG_Gap2_GluingLaw_Insertion_Stationarity_Session_Prompt_20260807.txt`.
  20
  21Honesty:
  22
  23* THEOREM: birth-death detailed balance equates the weight ratio to the rate
  24  ratio; equal per-slot insert and delete rates force a constant weight and
  25  therefore fail InsertionStationarity; size-blind birth with per-label death
  26  (counting-derived rates) forces InsertionStationarity once unit/atom are
  27  fixed; the geometry half is already inhabited; decoy rate laws that bake in
  28  the answer fail the derivation gate.
  29* REFUTED as a selector: equirating the `n+1` insertion slots with the `n+1`
  30  deletion choices at equal unit rate per choice; bare fixed-carrier posting
  31  (parent); renaming InsertionStationarity as a “rate.”
  32* OPEN: derive, from recognition structure, that birth is size-blind (one
  33  creation opportunity per tick) while death is per existing label — or an
  34  equivalent asymmetric counting that yields `μ_{n+1} = (n+1) λ_n` without
  35  writing the stationary law into the rates by hand.
  36* Cambrian Target Research can grind lemmas once this dynamics is typed; it
  37  cannot invent the missing physical rate asymmetry. No Target Research job
  38  is required to bank the census below.
  39* `gap2_measure_derived` is not moved.
  40-/
  41
  42namespace IndisputableMonolith
  43namespace Gravity
  44namespace SevenGaps
  45namespace Gap2LabelInsertionDynamics
  46
  47open Gap2GluingLawStationarity Gap2GaugeVolume
  48open MeasureSubstrateBlocker FullTheoryLedger
  49
  50noncomputable section
  51
  52/-! ## Reason census
  53
  54D01 detailed balance equates weight ratio to rate ratio
  55D02 equal per-slot insert/delete rates force constant weight
  56D03 equal per-slot rates fail InsertionStationarity (decoy)
  57D04 size-blind birth + per-label death forces InsertionStationarity
  58D05 geometry of n+1 slots is inhabited (parent)
  59D06 baking 1/(n+1) or factorials into a “rate” is not a derivation
  60D07 recognition forces size-blind birth / per-label death asymmetry
  61D08 LabelInsertionKernel inhabited from recognition dynamics
  62D09 GaugeCountingPrinciple derived (flag may move only then)
  63-/
  64
  65structure ReasonStatus where
  66  id : String
  67  title : String
  68  /-- `"THEOREM"`, `"OPEN"`, `"MODEL"`, or `"REFUTED"`. -/
  69  status : String
  70
  71def reasonTable : List ReasonStatus :=
  72  [ ⟨"D01", "detailed balance equates weight ratio to rate ratio", "THEOREM"⟩
  73  , ⟨"D02", "equal per-slot insert/delete rates force constant weight", "THEOREM"⟩
  74  , ⟨"D03", "equal per-slot rates fail InsertionStationarity", "REFUTED"⟩
  75  , ⟨"D04", "size-blind birth + per-label death forces InsertionStationarity", "THEOREM"⟩
  76  , ⟨"D05", "n+1 slot geometry inhabited", "THEOREM"⟩
  77  , ⟨"D06", "baking 1/(n+1) into a rate is not a derivation", "REFUTED"⟩
  78  , ⟨"D07", "recognition forces birth/death rate asymmetry", "OPEN"⟩
  79  , ⟨"D08", "LabelInsertionKernel from recognition dynamics", "OPEN"⟩
  80  , ⟨"D09", "GaugeCountingPrinciple derived from insertion dynamics", "OPEN"⟩ ]
  81
  82theorem reasonTable_length : reasonTable.length = 9 := by
  83  decide
  84
  85/-! ## Birth-death rates on carrier size -/
  86
  87/-- Size-indexed birth and death rates for a one-kind label carrier.
  88`birth n` is the total forward rate `n → n+1`.
  89`death n` is the total backward rate `n → n-1` (used at `n = m+1`). -/
  90structure BirthDeathRates where
  91  birth : ℕ → ℝ
  92  death : ℕ → ℝ
  93  birth_pos : ∀ n, 0 < birth n
  94  death_pos : ∀ n, 0 < death (n + 1)
  95
  96/-- Detailed balance for a size weight under birth-death rates. -/
  97def DetailedBalance (f : ℕ → ℝ) (R : BirthDeathRates) : Prop :=
  98  ∀ n : ℕ, f (n + 1) * R.death (n + 1) = f n * R.birth n
  99
 100/-- **D01.** Under detailed balance and positivity, the weight ratio equals the
 101rate ratio. -/
 102theorem D01_balance_ratio (f : ℕ → ℝ) (R : BirthDeathRates)
 103    (h : DetailedBalance f R) (n : ℕ) :
 104    f (n + 1) * R.death (n + 1) = f n * R.birth n :=
 105  h n
 106
 107/-- **D01 companion.** Solving for the recurrence form used by insertion
 108stationarity: if death is `(n+1)` times birth, balance is exactly
 109`f(n+1)·(n+1) = f n` after cancelling a common positive birth rate. -/
 110theorem D01_balance_of_scaled_death (f : ℕ → ℝ) (R : BirthDeathRates)
 111    (h : DetailedBalance f R)
 112    (hμ : ∀ n, R.death (n + 1) = (n + 1 : ℝ) * R.birth n) (n : ℕ) :
 113    f (n + 1) * (n + 1 : ℝ) = f n := by
 114  have hb := R.birth_pos n
 115  have hbal := h n
 116  have hμn := hμ n
 117  -- f(n+1) * ((n+1)*birth n) = f n * birth n
 118  have : f (n + 1) * ((n + 1 : ℝ) * R.birth n) = f n * R.birth n := by
 119    simpa [hμn] using hbal
 120  have hne : (R.birth n : ℝ) ≠ 0 := ne_of_gt hb
 121  -- cancel birth n
 122  have h' : f (n + 1) * (n + 1 : ℝ) * R.birth n = f n * R.birth n := by
 123    simpa [mul_assoc] using this
 124  exact mul_right_cancel₀ hne h'
 125
 126/-! ## Equal per-slot rates (symmetric counting) -/
 127
 128/-- The smallest symmetric dynamics: each of the `n+1` insertion slots fires at
 129unit rate, and each of the `n+1` labels may be deleted at unit rate. Total
 130birth and death are both `n+1`. -/
 131def equalPerSlotRates : BirthDeathRates where
 132  birth := fun n => (n + 1 : ℝ)
 133  death := fun n => (n : ℝ)
 134  birth_pos := fun n => by exact_mod_cast Nat.succ_pos n
 135  death_pos := fun n => by
 136    have : (0 : ℝ) < (n + 1 : ℝ) := by exact_mod_cast Nat.succ_pos n
 137    simpa using this
 138
 139/-- Constant unit weight. -/
 140def constantWeight : ℕ → ℝ := fun _ => 1
 141
 142theorem constantWeight_detailedBalance_equalPerSlot :
 143    DetailedBalance constantWeight equalPerSlotRates := by
 144  intro n
 145  simp [constantWeight, equalPerSlotRates]
 146
 147/-- **D02.** Equal per-slot rates put constant weight in detailed balance. -/
 148theorem D02_equal_per_slot_balances_constant :
 149    DetailedBalance constantWeight equalPerSlotRates :=
 150  constantWeight_detailedBalance_equalPerSlot
 151
 152/-- **D03 REFUTED as a selector of InsertionStationarity.** The symmetric
 153slot/label counting dynamics balances the constant weight, which fails
 154insertion stationarity at `n = 1`. So “count insertion slots and deletion
 155choices the same way” does not force the gluing law. -/
 156theorem D03_equal_per_slot_fails_insertionStationarity :
 157    DetailedBalance constantWeight equalPerSlotRates ∧
 158      ¬ InsertionStationarity constantWeight := by
 159  refine ⟨D02_equal_per_slot_balances_constant, ?_⟩
 160  intro h
 161  have hs := h.insert 1
 162  norm_num [constantWeight] at hs
 163
 164/-! ## Asymmetric counting: size-blind birth, per-label death -/
 165
 166/-- Birth is size-blind (total forward rate `1`). Death is per existing label
 167(total backward rate `n` at size `n`). Both factors come from move counting:
 168one creation opportunity, `n` removable labels. The factor `n+1` never appears
 169as a hand-written stationary coefficient. -/
 170def sizeBlindBirthPerLabelDeath : BirthDeathRates where
 171  birth := fun _ => (1 : ℝ)
 172  death := fun n => (n : ℝ)
 173  birth_pos := fun _ => by norm_num
 174  death_pos := fun n => by exact_mod_cast Nat.succ_pos n
 175
 176/-- **D04.** Under size-blind birth and per-label death, detailed balance plus
 177unit/atom is exactly `InsertionStationarity`. -/
 178theorem D04_asymmetric_rates_force_insertionStationarity (f : ℕ → ℝ)
 179    (hbal : DetailedBalance f sizeBlindBirthPerLabelDeath)
 180    (h0 : f 0 = 1) (h1 : f 1 = 1) :
 181    InsertionStationarity f where
 182  unit := h0
 183  atom := h1
 184  insert := by
 185    intro n
 186    -- death (n+1) = n+1, birth n = 1
 187    have hμ : ∀ k, sizeBlindBirthPerLabelDeath.death (k + 1)
 188        = (k + 1 : ℝ) * sizeBlindBirthPerLabelDeath.birth k := by
 189      intro k
 190      simp [sizeBlindBirthPerLabelDeath]
 191    simpa using D01_balance_of_scaled_death f sizeBlindBirthPerLabelDeath hbal hμ n
 192
 193/-- Inverse-factorial weight satisfies the asymmetric-rate detailed balance. -/
 194theorem D04_factorial_is_stationary :
 195    DetailedBalance factorialWorld.weight sizeBlindBirthPerLabelDeath ∧
 196      InsertionStationarity factorialWorld.weight := by
 197  refine ⟨?_, factorialWorld_stationary⟩
 198  intro n
 199  -- (1/(n+1)!) * (n+1) = 1/n!
 200  simp only [factorialWorld, sizeBlindBirthPerLabelDeath, mul_one]
 201  have hpos : (0 : ℝ) < (Nat.factorial n : ℝ) := by exact_mod_cast Nat.factorial_pos n
 202  have hcast : ((n + 1 : ℕ) : ℝ) = (n : ℝ) + 1 := by push_cast; ring
 203  rw [Nat.factorial_succ, hcast]
 204  push_cast
 205  field_simp
 206
 207/-! ## Decoy: baking the answer into the rates -/
 208
 209/-- A “rate” manufactured from a desired weight so that detailed balance holds
 210by algebra. This is the prompt’s decoy: it contains the stationary law, not a
 211physical counting. -/
 212def bakedFromWeight (f : ℕ → ℝ) (hf : ∀ n, 0 < f n) : BirthDeathRates where
 213  birth := fun _ => (1 : ℝ)
 214  death := fun n =>
 215    match n with
 216    | 0 => 1
 217    | n + 1 => f n / f (n + 1)
 218  birth_pos := fun _ => by norm_num
 219  death_pos := fun n => by
 220    have hnum := hf n
 221    have hden := hf (n + 1)
 222    exact div_pos hnum hden
 223
 224theorem bakedFromWeight_balances (f : ℕ → ℝ) (hf : ∀ n, 0 < f n) :
 225    DetailedBalance f (bakedFromWeight f hf) := by
 226  intro n
 227  have hden := ne_of_gt (hf (n + 1))
 228  simp only [bakedFromWeight]
 229  field_simp [hden]
 230
 231/-- **D06 REFUTED as a derivation.** For the constant decoy weight, the baked
 232rates balance it, yet InsertionStationarity fails. More generally, baking
 233`f n / f(n+1)` into death is renaming the stationary law as a rate. -/
 234theorem D06_baked_rates_are_not_a_derivation :
 235    (∀ f hf, DetailedBalance f (bakedFromWeight f hf)) ∧
 236      ¬ InsertionStationarity constantWeight := by
 237  refine ⟨fun f hf => bakedFromWeight_balances f hf, ?_⟩
 238  intro h
 239  have hs := h.insert 1
 240  norm_num [constantWeight] at hs
 241
 242/-! ## Geometry re-stand and residual -/
 243
 244/-- **D05.** Parent theorem: slot geometry is inhabited. -/
 245theorem D05_geometry_inhabited : Nonempty LabelInsertionGeometry :=
 246  succAboveGeometry_inhabited
 247
 248structure CorrectedFloorPlan where
 249  failedReason : String
 250  measurement : String
 251  correctedTarget : String
 252  doesNotKill : String
 253
 254def correctedFloorPlans : List CorrectedFloorPlan :=
 255  [ ⟨"D03",
 256      "equalPerSlotRates balances constantWeight; constantWeight fails InsertionStationarity.insert at n=1",
 257      "force an asymmetric counting: size-blind birth vs per-label death (or equivalent μ=(n+1)λ from move counts, not from the stationary formula)",
 258      "that n+1 insertion slots exist, or that deletion choices can be counted"⟩
 259  , ⟨"D06",
 260      "bakedFromWeight sets death(n+1)=f n/f(n+1) so balance is algebra",
 261      "rates must come from move counting or recognition schedule, never from the desired weight",
 262      "the abstract birth-death detailed-balance identity itself"⟩ ]
 263
 264theorem correctedFloorPlans_length : correctedFloorPlans.length = 2 := by
 265  decide
 266
 267/-- Surviving residual after this census: derive the asymmetric rate law
 268`sizeBlindBirthPerLabelDeath` (or any counting-equivalent) from recognition
 269structure / the posting schedule nature executes. -/
 270structure CorrectedInsertionDynamicsResidual where
 271  /-- Named recognition prior that forces size-blind birth and per-label death. -/
 272  namedRateAsymmetry : Prop
 273  /-- That prior is not equal per-slot insert/delete counting. -/
 274  notEqualPerSlot : Prop
 275  /-- That prior does not bake the stationary ratio into the rates. -/
 276  notBakedFromWeight : Prop
 277  /-- From the prior, InsertionStationarity holds of the physical size weight. -/
 278  forcesInsertionStationarity : Prop
 279
 280def assumedTargetStatus : String := "OPEN_RATE_ASYMMETRY"
 281
 282def firstAttackBlock : List String :=
 283  ["D07", "D04", "D03", "D06", "D08"]
 284
 285theorem firstAttackBlock_length : firstAttackBlock.length = 5 := by
 286  decide
 287
 288/-- Package: asymmetric counting rates + unit/atom + geometry close the kernel
 289and therefore GCP. This is a conditional closure, not a derivation of the rates. -/
 290noncomputable def D04_asymmetric_rates_give_kernel (f : ℕ → ℝ)
 291    (hbal : DetailedBalance f sizeBlindBirthPerLabelDeath)
 292    (h0 : f 0 = 1) (h1 : f 1 = 1) :
 293    LabelInsertionKernel f :=
 294  LabelInsertionKernel.ofStationarity succAboveGeometry
 295    (D04_asymmetric_rates_force_insertionStationarity f hbal h0 h1)
 296
 297theorem D04_asymmetric_rates_give_gcp (B : ℕ) (f : ℕ → ℝ)
 298    (hbal : DetailedBalance f sizeBlindBirthPerLabelDeath)
 299    (h0 : f 0 = 1) (h1 : f 1 = 1) :
 300    GaugeCountingPrinciple
 301      (classMass (B := B) (fun K => f K.nV * f K.nE * f K.nT)) :=
 302  labelInsertionKernel_gives_gaugeCounting B
 303    (D04_asymmetric_rates_give_kernel f hbal h0 h1)
 304
 305/-- Measure flag remains unmoved until D07/D08 close. -/
 306theorem gap2_measure_derived_unmoved :
 307    fullTheoryBenchmarks.gap2_measure_derived = true :=
 308  Gap2GluingLawStationarity.gap2_measure_derived_unmoved
 309
 310/-! ## Composite certificate -/
 311
 312theorem labelInsertionDynamics_certified :
 313    reasonTable.length = 9 ∧
 314      DetailedBalance constantWeight equalPerSlotRates ∧
 315      ¬ InsertionStationarity constantWeight ∧
 316      (DetailedBalance factorialWorld.weight sizeBlindBirthPerLabelDeath ∧
 317        InsertionStationarity factorialWorld.weight) ∧
 318      Nonempty LabelInsertionGeometry ∧
 319      correctedFloorPlans.length = 2 ∧
 320      firstAttackBlock.length = 5 ∧
 321      assumedTargetStatus = "OPEN_RATE_ASYMMETRY" ∧
 322      fullTheoryBenchmarks.gap2_measure_derived = true := by
 323  refine ⟨reasonTable_length, D02_equal_per_slot_balances_constant,
 324    D03_equal_per_slot_fails_insertionStationarity.2, D04_factorial_is_stationary,
 325    D05_geometry_inhabited, correctedFloorPlans_length, firstAttackBlock_length,
 326    rfl, gap2_measure_derived_unmoved⟩
 327
 328#print axioms D01_balance_of_scaled_death
 329#print axioms D02_equal_per_slot_balances_constant
 330#print axioms D03_equal_per_slot_fails_insertionStationarity
 331#print axioms D04_asymmetric_rates_force_insertionStationarity
 332#print axioms D04_factorial_is_stationary
 333#print axioms D04_asymmetric_rates_give_gcp
 334#print axioms D06_baked_rates_are_not_a_derivation
 335#print axioms labelInsertionDynamics_certified
 336
 337end
 338
 339end Gap2LabelInsertionDynamics
 340end SevenGaps
 341end Gravity
 342end IndisputableMonolith
 343