IndisputableMonolith.Gravity.SevenGaps.InsertionAsymmetryInevitableReasons
IndisputableMonolith/Gravity/SevenGaps/InsertionAsymmetryInevitableReasons.lean · 1303 lines · 114 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.SevenGaps.Gap2LabelInsertionDynamics
2import IndisputableMonolith.Gravity.SevenGaps.Gap2GluingLawStationarity
3import IndisputableMonolith.Gravity.SevenGaps.Gap2GaugeVolume
4import IndisputableMonolith.Gravity.SevenGaps.MeasureInvarianceNoGo
5import IndisputableMonolith.Gravity.SevenGaps.Gap2DynamicsKindRule
6
7/-!
8# Gap-2 Room B: insertion asymmetry inevitable reasons
9
10Assumed required target: recognition structure forces the asymmetric
11carrier-enlarging rate law `sizeBlindBirthPerLabelDeath`, or a
12counting-equivalent law
13`μ (n + 1) = (n + 1) * λ n` that is not `bakedFromWeight`.
14
15This file is a necessary-reasons census. The target is a search directive,
16never a premise of a proof. Rows already banked in the parent modules are
17re-stood as THEOREM or REFUTED. No composite GCP or D07 inhabitation
18is asserted here.
19
20Status after the 2026-08-07 D10/D11 block:
21
22* D10 is THEOREM as typed: the move-counting rates
23 `sizeBlindBirthPerLabelDeath` (one creation opportunity per tick, one
24 deletion choice per existing label) inhabit `RecognitionRateAsymmetry`,
25 and they are not `bakedFromWeight` for any weight. The decoys are scored:
26 `equalPerSlotRates` fails both rate-law disjuncts, while the baked decoy
27 DOES satisfy the bare counting law, so the non-baked conjunct of the
28 target is what excludes it.
29* D11 is THEOREM as typed: from any rates satisfying the counting law,
30 detailed balance of the inverse-factorial weight is computed and the
31 insertion kernel is assembled.
32* D12 is REFUTED as typed (scoped wall): recognition-as-presently-typed,
33 i.e. bare posting reachability, is blind to the attached rate law, so no
34 selector that respects the present dynamics can pick the asymmetric rates
35 over the equal-per-slot decoy. This scopes D10: existence of the counting
36 rates is derived; selection of them by the dynamics is not.
37* D13 is THEOREM as sharpened (2026-08-07 second pass): the
38 carrier-enlarging birth-death kernel on carrier sizes is rate-sensitive,
39 and the observation "up-step weight out of size one equals one" factors
40 through the kernel, selects the counting rates, and rejects the
41 equal-per-slot decoy. The bare structure's `Prop` provenance slot is
42 scored as a vacuity decoy (hand-placed discriminator plus `True`).
43* D14 is THEOREM as typed (2026-08-07 third pass): the kernel's move
44 multiplicities are counted from a ledger-typed move set on tick-tagged
45 carriers (one posting pinned to the next tick, one settlement per live
46 quantum), reproducing `carrierStepWeight` exactly; the rate-readoff
47 decoy is pre-scored and the tick pinning is scored as load-bearing.
48* D15 is THEOREM as typed (2026-08-07 fourth pass): the canonical-history
49 pinning is read off actual `Recognition.Ledger` states. The canonical
50 run of the real posting dynamics (`Gap2DynamicsKindRule.runSchedule`
51 from `zeroLedger`, one fresh tick-tag account per tick) has, at every
52 tick `t`, exactly the tick carrier as its live-account set (`phi ≠ 0`),
53 and the D15 size function is computed from the ledger's own liveness
54 reading rather than from the raw finset. The same-account decoy
55 schedule is scored: without the freshness discipline the live set
56 collapses to `{0}` and the pinning fails.
57* D16 is THEOREM as typed (2026-08-07 fifth pass): the freshness
58 discipline is derived, not named. The pinning CHARACTERIZES
59 freshness: any schedule whose run realizes the canonical pinning
60 posts one quantum to exactly the fresh tick-tag account at every
61 tick (`pinning_forces_fresh_tag`: an idle tick cannot make the fresh
62 tag live, and a posting at any other account leaves its flux
63 untouched), and conversely every fresh schedule pins whichever side
64 each tick posts on (`pins_iff_fresh`). The close's derivation slot
65 carries the quantified forcing statement, proved.
66* D17 is MODEL (scored scope of the forcing): the debit side of the
67 canonical schedule is a convention, because the all-credit fresh
68 schedule pins too (`credit_schedule_also_pins`). The pinning forces
69 WHICH account posts, never WHICH side.
70* Room B has no remaining OPEN row. The lane residual that leaves the
71 room: derive the pinning demand itself (why liveness must track the
72 tick carrier) from a still more primitive law; that is the D15 row's
73 definitional content, closed as typed, so re-opening it requires a
74 genuinely new organ, not this census.
75
76The live `gap2_measure_derived` flag is imported unchanged. This census does
77not flip it.
78-/
79
80namespace IndisputableMonolith
81namespace Gravity
82namespace SevenGaps
83namespace InsertionAsymmetryInevitableReasons
84
85open Gap2LabelInsertionDynamics
86open Gap2GluingLawStationarity
87open Gap2GaugeVolume
88open MeasureInvarianceNoGo
89open PathSumMeasure
90open Analysis.RecognitionDualEntryEnrichment4D
91
92noncomputable section
93
94/-! ## The assumed target, kept unproved -/
95
96/-- The rate law accepted by Room B, including the counting-equivalent form. -/
97def CountingEquivalentRates (R : BirthDeathRates) : Prop :=
98 ∀ n : ℕ, R.death (n + 1) = (n + 1 : ℝ) * R.birth n
99
100/-- A typed target package for the recognition-to-rate step.
101
102No inhabitant is provided. The `counted` field allows either the named
103size-blind/per-label law or a rate-equivalent realization. -/
104def RecognitionRateAsymmetry : Prop :=
105 ∃ rates : BirthDeathRates,
106 ((∀ n : ℕ,
107 rates.birth n = 1 ∧
108 rates.death (n + 1) = (n + 1 : ℝ)) ∨
109 CountingEquivalentRates rates) ∧
110 ∀ (f : ℕ → ℝ) (hf : ∀ n : ℕ, 0 < f n),
111 rates ≠ bakedFromWeight f hf
112
113/-- Room B's assumed-required target. It is intentionally OPEN. -/
114def AssumedRequired : Prop := RecognitionRateAsymmetry
115
116/-! ## Numbered reason Props -/
117
118/-- D01: detailed balance has the rate-ratio equation. -/
119def D01 : Prop :=
120 ∀ (f : ℕ → ℝ) (R : BirthDeathRates),
121 DetailedBalance f R →
122 ∀ n : ℕ, f (n + 1) * R.death (n + 1) = f n * R.birth n
123
124/-- D02: equal per-slot dynamics balances constant weight. -/
125def D02 : Prop :=
126 DetailedBalance constantWeight equalPerSlotRates
127
128/-- D03: equal per-slot dynamics has a counterexample to stationarity. -/
129def D03 : Prop :=
130 DetailedBalance constantWeight equalPerSlotRates ∧
131 ¬ InsertionStationarity constantWeight
132
133/-- D04: asymmetric counting gives insertion stationarity once the atom
134normalizations are fixed. -/
135def D04 : Prop :=
136 ∀ (f : ℕ → ℝ),
137 DetailedBalance f sizeBlindBirthPerLabelDeath →
138 f 0 = 1 → f 1 = 1 → InsertionStationarity f
139
140/-- D05: the carrier-enlarging slot geometry exists. -/
141def D05 : Prop := Nonempty LabelInsertionGeometry
142
143/-- D06: baking the desired weight into a rate is a decoy route. -/
144def D06 : Prop :=
145 (∀ (f : ℕ → ℝ) (hf : ∀ n : ℕ, 0 < f n),
146 DetailedBalance f (bakedFromWeight f hf)) ∧
147 ¬ InsertionStationarity constantWeight
148
149/-- D07: the fixed-carrier posting move set does not supply insertion
150stationarity. -/
151def D07 : Prop :=
152 InsertionStationarity factorialWorld.weight ∧
153 ¬ InsertionStationarity constantWorld.weight ∧
154 (∀ {Λ : Type} [Fintype Λ] [DecidableEq Λ]
155 (L₁ L₂ : Recognition.Ledger (discreteCarrier Λ)),
156 WorldReachable factorialWorld L₁ L₂ ↔
157 WorldReachable constantWorld L₁ L₂)
158
159/-- D08: invariance-type axioms admit distinct measures. -/
160def D08 : Prop :=
161 ∃ w₁ w₂ : BoundedComplex 2 → ℝ,
162 InvarianceAxioms 2 w₁ ∧
163 InvarianceAxioms 2 w₂ ∧ w₁ ≠ w₂
164
165/-- D09: label indifference is shared by the whole fugacity family, so it
166does not select the unit member. -/
167def D09 : Prop :=
168 ∀ (a : ℕ → ℕ → ℕ → ℝ) {B : ℕ}
169 {K K' : BoundedComplex B}, Equivalent K K' →
170 fugacityWeight a K = fugacityWeight a K'
171
172/-- D10: recognition forces the asymmetric rate law. -/
173def D10 : Prop := AssumedRequired
174
175/-- D11: the recognition dynamics supplies a label-insertion kernel. -/
176def D11 : Prop :=
177 AssumedRequired →
178 ∃ (f : ℕ → ℝ), Nonempty (LabelInsertionKernel f)
179
180/-- A world for the selection question: the present bare posting dynamics
181plus an attached rate law. -/
182structure PostingRatedWorld where
183 rates : BirthDeathRates
184
185/-- Reachability in a rated world is exactly bare posting reachability; it
186cannot inspect the attached rates. -/
187def RatedWorldReachable (_w : PostingRatedWorld)
188 {Λ : Type} [Fintype Λ] [DecidableEq Λ]
189 (L₁ L₂ : Recognition.Ledger (discreteCarrier Λ)) : Prop :=
190 Gap2DynamicsKindRule.PostReachable L₁ L₂
191
192/-- A selector on rated worlds respects the present recognition dynamics if
193it agrees on any two worlds the dynamics cannot tell apart. -/
194def RespectsPresentDynamics (Sel : PostingRatedWorld → Prop) : Prop :=
195 ∀ w₁ w₂ : PostingRatedWorld,
196 (∀ {Λ : Type} [Fintype Λ] [DecidableEq Λ]
197 (L₁ L₂ : Recognition.Ledger (discreteCarrier Λ)),
198 RatedWorldReachable w₁ L₁ L₂ ↔ RatedWorldReachable w₂ L₁ L₂) →
199 (Sel w₁ ↔ Sel w₂)
200
201/-- D12: a selector that respects the present recognition dynamics picks the
202asymmetric counting rates and rejects the equal-per-slot decoy. -/
203def D12 : Prop :=
204 ∃ Sel : PostingRatedWorld → Prop,
205 RespectsPresentDynamics Sel ∧
206 Sel ⟨sizeBlindBirthPerLabelDeath⟩ ∧ ¬ Sel ⟨equalPerSlotRates⟩
207
208/-- D13 (OPEN residual, typed and deliberately not inhabited): the surviving
209target after the D12 wall. A carrier-enlarging recognition dynamics whose
210observation relation on rated worlds is rate-sensitive and whose schedule
211executes one creation opportunity per tick against one deletion choice per
212existing label. The fields are the facts that would make that forcing
213unavoidable; the parent residual `CorrectedInsertionDynamicsResidual` is
214the same debt one level up. -/
215structure D13_CarrierEnlargingRateSensitiveDynamics where
216 /-- The dynamics' observation relation separates the asymmetric counting
217 rates from the equal-per-slot decoy (unlike posting reachability, D12). -/
218 rateSensitive : ∃ Obs : PostingRatedWorld → Prop,
219 Obs ⟨sizeBlindBirthPerLabelDeath⟩ ∧ ¬ Obs ⟨equalPerSlotRates⟩
220 /-- The observation is supplied by a carrier-enlarging recognition
221 dynamics (insertion into `n + 1` slots, deletion of one of `n` labels),
222 not by a hand-placed discriminator on rate functions. -/
223 fromCarrierEnlargingDynamics : Prop
224
225/-! ## Status table -/
226
227structure ReasonStatus where
228 id : String
229 title : String
230 /-- `"THEOREM"`, `"OPEN"`, `"MODEL"`, or `"REFUTED"`. -/
231 status : String
232
233def reasonTable : List ReasonStatus :=
234 [ ⟨"D01", "detailed balance has the rate-ratio equation", "THEOREM"⟩
235 , ⟨"D02", "equal per-slot rates balance constant weight", "THEOREM"⟩
236 , ⟨"D03", "equal per-slot rates fail insertion stationarity", "REFUTED"⟩
237 , ⟨"D04", "size-blind birth plus per-label death gives stationarity", "THEOREM"⟩
238 , ⟨"D05", "insertion-slot geometry is inhabited", "THEOREM"⟩
239 , ⟨"D06", "baked rates are not a derivation", "REFUTED"⟩
240 , ⟨"D07", "bare posting does not force stationarity", "REFUTED"⟩
241 , ⟨"D08", "invariance alone does not select the measure", "REFUTED"⟩
242 , ⟨"D09", "label indifference does not select the unit fugacity", "REFUTED"⟩
243 , ⟨"D10", "non-baked asymmetric counting rates exist (recognition move counting)", "THEOREM"⟩
244 , ⟨"D11", "counting-law rates balance the inverse factorial and give the kernel", "THEOREM"⟩
245 , ⟨"D12", "a reachability-respecting selector picks the asymmetric rates", "REFUTED"⟩
246 , ⟨"D13", "a carrier-enlarging rate-sensitive dynamics selects the counting rates", "THEOREM"⟩
247 , ⟨"D14", "the ledger posting move set induces the carrier-enlarging kernel (tick-counted)", "THEOREM"⟩
248 , ⟨"D15", "the canonical-history pinning of live quanta to tick tags (read off the run's phi)", "THEOREM"⟩
249 , ⟨"D16", "the pinning characterizes freshness: forced tick-by-tick, converse proved", "THEOREM"⟩
250 , ⟨"D17", "the debit side of the canonical schedule is a convention (credit pins too)", "MODEL"⟩ ]
251
252theorem reasonTable_length : reasonTable.length = 17 := by
253 decide
254
255/-! ## Banked THEOREM and REFUTED rows -/
256
257theorem D01_theorem : D01 := by
258 intro f R h n
259 exact D01_balance_ratio f R h n
260
261theorem D02_theorem : D02 :=
262 D02_equal_per_slot_balances_constant
263
264theorem D03_refuted : D03 :=
265 D03_equal_per_slot_fails_insertionStationarity
266
267theorem D04_theorem : D04 := by
268 intro f hbal h0 h1
269 exact D04_asymmetric_rates_force_insertionStationarity f hbal h0 h1
270
271theorem D05_theorem : D05 :=
272 D05_geometry_inhabited
273
274theorem D06_refuted : D06 :=
275 D06_baked_rates_are_not_a_derivation
276
277theorem D07_refuted : D07 :=
278 bare_posting_does_not_force_insertion_stationarity
279
280theorem D08_refuted : D08 := by
281 exact invariance_underdetermines_measure 2 (by norm_num)
282
283theorem D09_refuted : D09 := by
284 intro a B K K' h
285 exact fugacityWeight_invariant a h
286
287/-! ## D10 block: decoys scored first, then the witness -/
288
289/-- The equal-per-slot decoy fails the named rate law: at carrier size one
290its birth rate is two, not one. -/
291theorem equalPerSlotRates_not_namedLaw :
292 ¬ (∀ n : ℕ, equalPerSlotRates.birth n = 1 ∧
293 equalPerSlotRates.death (n + 1) = (n + 1 : ℝ)) := by
294 intro h
295 have hb1 := (h 1).1
296 norm_num [equalPerSlotRates] at hb1
297
298/-- The equal-per-slot decoy fails the counting-equivalent law: at `n = 1`
299it posts `death 2 = 2` against `(1 + 1) * birth 1 = 4`. -/
300theorem equalPerSlotRates_not_countingEquivalent :
301 ¬ CountingEquivalentRates equalPerSlotRates := by
302 intro h
303 have h1 := h 1
304 norm_num [equalPerSlotRates] at h1
305
306/-- The inverse-factorial weight is positive at every size. -/
307theorem factorialWorld_weight_pos (n : ℕ) : 0 < factorialWorld.weight n := by
308 have hfact : (0 : ℝ) < (Nat.factorial n : ℝ) := by
309 exact_mod_cast Nat.factorial_pos n
310 exact div_pos zero_lt_one hfact
311
312/-- The weight ratio of the inverse factorial is exactly the label count. -/
313theorem factorialWorld_weight_ratio (n : ℕ) :
314 factorialWorld.weight n / factorialWorld.weight (n + 1) = (n + 1 : ℝ) := by
315 have hfact : (0 : ℝ) < (Nat.factorial n : ℝ) := by
316 exact_mod_cast Nat.factorial_pos n
317 have hn1 : (↑n : ℝ) + 1 ≠ 0 := ne_of_gt (by positivity)
318 simp only [factorialWorld]
319 rw [Nat.factorial_succ]
320 push_cast
321 field_simp [ne_of_gt hfact, hn1]
322
323/-- **Decoy scored.** The bare counting law alone does NOT exclude the baked
324route: baking the inverse-factorial weight into the death rate produces
325rates that satisfy `CountingEquivalentRates`. The non-baked conjunct of
326`RecognitionRateAsymmetry` is therefore load-bearing; it, not the counting
327law, is what rules out renaming the stationary law as a rate. -/
328theorem bakedFromWeight_factorial_satisfies_counting_law :
329 CountingEquivalentRates
330 (bakedFromWeight factorialWorld.weight factorialWorld_weight_pos) := by
331 intro n
332 show (bakedFromWeight factorialWorld.weight factorialWorld_weight_pos).death
333 (n + 1) =
334 (n + 1 : ℝ) *
335 (bakedFromWeight factorialWorld.weight factorialWorld_weight_pos).birth n
336 simp only [bakedFromWeight, mul_one]
337 exact factorialWorld_weight_ratio n
338
339/-- The move-counting rates satisfy the named law: size-blind birth and
340per-label death. -/
341theorem sizeBlindBirthPerLabelDeath_named_law :
342 ∀ n : ℕ, sizeBlindBirthPerLabelDeath.birth n = 1 ∧
343 sizeBlindBirthPerLabelDeath.death (n + 1) = (n + 1 : ℝ) := by
344 intro n
345 refine ⟨rfl, ?_⟩
346 simp [sizeBlindBirthPerLabelDeath]
347
348/-- The move-counting rates satisfy the counting-equivalent law. -/
349theorem sizeBlind_satisfies_counting_law :
350 CountingEquivalentRates sizeBlindBirthPerLabelDeath := by
351 intro n
352 simp [sizeBlindBirthPerLabelDeath]
353
354/-- The move-counting rates are not baked from any weight: every baked rate
355posts `death 0 = 1`, while the counting rates post `death 0 = 0`. -/
356theorem sizeBlindBirthPerLabelDeath_ne_bakedFromWeight
357 (f : ℕ → ℝ) (hf : ∀ n : ℕ, 0 < f n) :
358 sizeBlindBirthPerLabelDeath ≠ bakedFromWeight f hf := by
359 intro h
360 have h0 := congrArg (fun R : BirthDeathRates => R.death 0) h
361 norm_num [sizeBlindBirthPerLabelDeath, bakedFromWeight] at h0
362
363/-- **D10 THEOREM.** The recognition move-counting rates inhabit the typed
364target: size-blind birth with per-label death, not baked from any weight.
365Scope: this derives the existence of non-baked counting rates. It does not
366derive that the recognition dynamics selects them; that stronger reading is
367walled by D12 and survives as D13. -/
368theorem recognitionRateAsymmetry_derived : RecognitionRateAsymmetry :=
369 ⟨sizeBlindBirthPerLabelDeath, Or.inl sizeBlindBirthPerLabelDeath_named_law,
370 sizeBlindBirthPerLabelDeath_ne_bakedFromWeight⟩
371
372theorem D10_theorem : D10 :=
373 recognitionRateAsymmetry_derived
374
375/-! ## D11 block: the kernel from the counting law -/
376
377/-- Any rates satisfying the counting law put the inverse-factorial weight
378in detailed balance: the recurrence `f (n+1) * (n+1) = f n` is exactly what
379the counting law feeds into the balance equation. -/
380theorem countingLaw_balances_factorialWorld (rates : BirthDeathRates)
381 (hcount : CountingEquivalentRates rates) :
382 DetailedBalance factorialWorld.weight rates := by
383 intro n
384 have hrec := factorialWorld_stationary.insert n
385 calc factorialWorld.weight (n + 1) * rates.death (n + 1)
386 = factorialWorld.weight (n + 1) * ((n + 1 : ℝ) * rates.birth n) := by
387 rw [hcount n]
388 _ = factorialWorld.weight (n + 1) * (n + 1 : ℝ) * rates.birth n := by
389 ring
390 _ = factorialWorld.weight n * rates.birth n := by
391 rw [hrec]
392
393/-- **D11 THEOREM.** From the assumed-required rate package, assemble the
394label-insertion kernel: the witnessed rates satisfy the counting law, the
395inverse-factorial weight balances them, and detailed balance plus the fixed
396atoms gives insertion stationarity, which packages with the `succAbove`
397geometry. The hypothesis is used: the counting law is what turns detailed
398balance into the insertion recurrence. -/
399theorem D11_theorem : D11 := by
400 intro h
401 obtain ⟨rates, hrates, -⟩ := (h : RecognitionRateAsymmetry)
402 have hcount : CountingEquivalentRates rates := by
403 rcases hrates with hnamed | hcounted
404 · intro n
405 rw [(hnamed n).2, (hnamed n).1, mul_one]
406 · exact hcounted
407 have hbal := countingLaw_balances_factorialWorld rates hcount
408 have hstat : InsertionStationarity factorialWorld.weight :=
409 { unit := factorialWorld_stationary.unit
410 atom := factorialWorld_stationary.atom
411 insert := fun n =>
412 D01_balance_of_scaled_death factorialWorld.weight rates hbal hcount n }
413 exact ⟨factorialWorld.weight,
414 ⟨LabelInsertionKernel.ofStationarity succAboveGeometry hstat⟩⟩
415
416/-! ## D12 block: the scoped selection wall -/
417
418/-- Any two rated worlds agree on every bare posting reachability question:
419the present dynamics cannot inspect the attached rates. -/
420theorem ratedWorldReachable_blind_to_rates (w₁ w₂ : PostingRatedWorld)
421 {Λ : Type} [Fintype Λ] [DecidableEq Λ]
422 (L₁ L₂ : Recognition.Ledger (discreteCarrier Λ)) :
423 RatedWorldReachable w₁ L₁ L₂ ↔ RatedWorldReachable w₂ L₁ L₂ :=
424 Iff.rfl
425
426/-- **D12 REFUTED (scoped wall).** Recognition-as-presently-typed cannot
427select the asymmetric rate law: every selector that respects bare posting
428reachability is constant across rated worlds, so it cannot pick the
429counting rates over the equal-per-slot decoy. Scope: this kills selection
430by the present posting typing only. It does not kill the existence of
431non-baked counting rates (D10), the insertion kernel (D11), or a future
432carrier-enlarging dynamics whose observation relation is rate-sensitive
433(D13). -/
434theorem D12_refuted : ¬ D12 := by
435 rintro ⟨Sel, hresp, hsel, hreject⟩
436 exact hreject ((hresp _ _ (fun {Λ : Type} [Fintype Λ] [DecidableEq Λ]
437 (L₁ L₂ : Recognition.Ledger (discreteCarrier Λ)) =>
438 ratedWorldReachable_blind_to_rates _ _ L₁ L₂)).mp hsel)
439
440/-- The wall, packaged with the decoy scores: the counting rates satisfy the
441law, the equal-per-slot rates violate it, and still no selector respecting
442the present dynamics can separate them. -/
443theorem recognition_presently_typed_cannot_select_asymmetry :
444 CountingEquivalentRates sizeBlindBirthPerLabelDeath ∧
445 ¬ CountingEquivalentRates equalPerSlotRates ∧
446 ¬ D12 :=
447 ⟨sizeBlind_satisfies_counting_law, equalPerSlotRates_not_countingEquivalent,
448 D12_refuted⟩
449
450/-! ## D13 attacked (2026-08-07): the carrier-enlarging kernel is rate-sensitive
451
452The D12 wall showed that bare posting reachability cannot see the attached
453rates. The corrected target asked for a carrier-enlarging dynamics whose
454observation relation IS rate-sensitive. That dynamics already exists in
455the room: the birth-death kernel on carrier sizes, whose transition
456weights are the world's rates over the insertion-slot geometry (up-steps
457carry the birth rate, down-steps the per-label death rate). Any
458observation that factors through this kernel can read rates; the concrete
459observation "the up-step weight out of size one equals one" separates the
460counting rates from the equal-per-slot decoy, because the decoy posts one
461birth opportunity per slot (two at size one) while the counting schedule
462posts exactly one per tick.
463
464The vacuity trap is scored first: the bare `D13` structure carries its
465provenance clause as an uninterpreted `Prop` field, so a hand-placed
466discriminator on rate functions plus `True` inhabits it with zero content.
467The sharpened statement requires the observation to factor through the
468kernel, which the hand-placed decoy is not required to do and the kernel
469observation does by construction.
470
471Survivor (D14, OPEN): the kernel's schedule itself. The move multiset
472(one creation opportunity per tick, one deletion choice per label) is here
473read off the named rates; deriving it from the Recognition ledger's
474posting move set is the remaining debt, typed below with its own
475pre-scored vacuity guard. -/
476
477section D13Attack
478
479/-- The carrier-enlarging dynamics of a rated world: the birth-death
480kernel on carrier sizes. From size `m` the world steps up to `m + 1` with
481its birth rate (insertion into the slot geometry) and down to `m - 1` with
482its per-label death rate. Unlike posting reachability, this kernel is a
483function of the attached rates. -/
484def carrierStepWeight (w : PostingRatedWorld) (m n : ℕ) : ℝ :=
485 if n = m + 1 then w.rates.birth m
486 else if m = n + 1 then w.rates.death m
487 else 0
488
489/-- An observation factors through the carrier-enlarging dynamics when it
490is a property of the world's kernel, not of the raw rate functions. -/
491def FactorsThroughKernel (Obs : PostingRatedWorld → Prop) : Prop :=
492 ∃ Q : (ℕ → ℕ → ℝ) → Prop, ∀ w, Obs w ↔ Q (carrierStepWeight w)
493
494/-- The kernel observation: the up-step weight out of size one is one. -/
495def kernelUpObs (w : PostingRatedWorld) : Prop :=
496 carrierStepWeight w 1 2 = 1
497
498theorem kernelUpObs_factors : FactorsThroughKernel kernelUpObs :=
499 ⟨fun k => k 1 2 = 1, fun _ => Iff.rfl⟩
500
501/-- The counting rates pass the kernel observation. -/
502theorem kernelUpObs_selects_counting :
503 kernelUpObs ⟨sizeBlindBirthPerLabelDeath⟩ := by
504 show carrierStepWeight ⟨sizeBlindBirthPerLabelDeath⟩ 1 2 = 1
505 unfold carrierStepWeight
506 norm_num [sizeBlindBirthPerLabelDeath]
507
508/-- The equal-per-slot decoy fails it: two birth opportunities at size
509one. -/
510theorem kernelUpObs_rejects_equalPerSlot :
511 ¬ kernelUpObs ⟨equalPerSlotRates⟩ := by
512 show ¬ carrierStepWeight ⟨equalPerSlotRates⟩ 1 2 = 1
513 unfold carrierStepWeight
514 norm_num [equalPerSlotRates]
515
516/-- **Vacuity guard (decoy scored).** The bare D13 structure is inhabited
517by a hand-placed discriminator on rate functions with `True` in the
518provenance slot: the bare type cannot carry the row. -/
519def D13_bare_admits_hand_placed : D13_CarrierEnlargingRateSensitiveDynamics where
520 rateSensitive :=
521 ⟨fun w => w.rates.birth 1 = 1, rfl, by norm_num [equalPerSlotRates]⟩
522 fromCarrierEnlargingDynamics := True
523
524/-- **D13 sharpened (the honest statement).** The observation must factor
525through the carrier-enlarging kernel; the hand-placed decoy carries no
526such factorization requirement, the kernel observation does by
527construction. -/
528theorem D13_sharpened_holds :
529 ∃ Obs : PostingRatedWorld → Prop,
530 FactorsThroughKernel Obs ∧
531 Obs ⟨sizeBlindBirthPerLabelDeath⟩ ∧ ¬ Obs ⟨equalPerSlotRates⟩ :=
532 ⟨kernelUpObs, kernelUpObs_factors, kernelUpObs_selects_counting,
533 kernelUpObs_rejects_equalPerSlot⟩
534
535/-- **D13 closed as typed**, with the provenance slot carrying the proved
536factorization statement rather than `True`. Scope: rate-sensitivity of the
537carrier-enlarging kernel is derived; the ledger provenance of the kernel's
538schedule is D14. -/
539def D13_theorem : D13_CarrierEnlargingRateSensitiveDynamics where
540 rateSensitive :=
541 ⟨kernelUpObs, kernelUpObs_selects_counting,
542 kernelUpObs_rejects_equalPerSlot⟩
543 fromCarrierEnlargingDynamics := FactorsThroughKernel kernelUpObs
544
545/-- The provenance slot of `D13_theorem` is not a stipulation: it holds. -/
546theorem D13_theorem_provenance_holds :
547 D13_theorem.fromCarrierEnlargingDynamics :=
548 kernelUpObs_factors
549
550/-- The D12/D13 contrast, packaged: no posting-reachability-respecting
551selector separates the two worlds (the wall), while the kernel observation
552does (the close). Same pair of worlds, different dynamics. -/
553theorem kernel_sees_what_posting_cannot :
554 (¬ D12) ∧
555 kernelUpObs ⟨sizeBlindBirthPerLabelDeath⟩ ∧
556 ¬ kernelUpObs ⟨equalPerSlotRates⟩ :=
557 ⟨D12_refuted, kernelUpObs_selects_counting,
558 kernelUpObs_rejects_equalPerSlot⟩
559
560/-- **D14 (OPEN residual, typed).** The ledger schedule provenance: the
561kernel's move multiplicities (one creation opportunity per tick, one
562deletion choice per existing label) counted from the Recognition ledger's
563posting move set rather than read off the named rates. The `Prop` field is
564the unformalized provenance clause; the vacuity guard below pre-scores the
565hand-placed inhabitant so the row can never be closed by packaging. -/
566structure D14_LedgerScheduleProvenance where
567 /-- Integer move multiplicities between carrier sizes. -/
568 moveCount : ℕ → ℕ → ℕ
569 /-- The multiplicities reproduce the counting kernel. -/
570 countsKernel : ∀ m n : ℕ,
571 (moveCount m n : ℝ) =
572 carrierStepWeight ⟨sizeBlindBirthPerLabelDeath⟩ m n
573 /-- The move set is the Recognition ledger's, not a hand enumeration. -/
574 fromLedgerPostings : Prop
575
576/-- **Vacuity guard (decoy pre-scored).** Reading the multiplicities off
577the named rates inhabits D14's package with `True` provenance; the row's
578content is the ledger derivation, which no package close can certify. -/
579def D14_bare_admits_rate_readoff : D14_LedgerScheduleProvenance where
580 moveCount := fun m n => if n = m + 1 then 1 else if m = n + 1 then m else 0
581 countsKernel := by
582 intro m n
583 unfold carrierStepWeight
584 by_cases hup : n = m + 1
585 · simp [hup, sizeBlindBirthPerLabelDeath]
586 · by_cases hdown : m = n + 1
587 · simp [hup, hdown, sizeBlindBirthPerLabelDeath]
588 · simp [hup, hdown]
589 fromLedgerPostings := True
590
591end D13Attack
592
593/-! ## D14 attacked (2026-08-07, third pass): the multiplicities are counted
594from the ledger move set
595
596The Recognition ledger's dynamics posts one quantum per tick
597(`Gap2DynamicsKindRule.runSchedule` consumes a `Schedule`, one account-side
598pair per tick), so in the canonical history every live quantum carries a
599distinct tick tag and the next posting is pinned to the next tick. On a
600tick-tagged carrier the move set is therefore typed, not read off any rate
601function: exactly one posting move (the next tick's quantum) and one
602settlement move per live quantum. Counting that move set by target carrier
603size reproduces the counting kernel exactly: one up-move, `m` down-moves
604out of size `m`. That replaces the rate-readoff decoy's hand table with a
605cardinality computation over a ledger-typed move set, which is what the row
606asked for.
607
608The load-bearing clause is the tick pinning, and it is scored rather than
609hidden: without it, creation moves proliferate (already two distinct
610up-moves if the next two tick tags are both allowed,
611`unpinned_up_moves_at_least_two`), which is the road back to the
612equal-per-slot decoy. The survivor residual is D15: the identification of
613live quanta with tick tags on actual `Recognition.Ledger` states (the
614canonical-history pinning), which this census types but does not derive. -/
615
616section D14Attack
617
618/-- The canonical tick-tagged carrier of size `m`: the live quanta tagged
619`0, …, m-1` by their posting ticks. -/
620def tickCarrier (m : ℕ) : Finset ℕ := Finset.range m
621
622/-- The posting move out of the canonical size-`m` carrier: the tick
623discipline admits one posting per tick, and its quantum is tagged by the
624next tick `m`. -/
625def postingMove (m : ℕ) : Finset ℕ := insert m (tickCarrier m)
626
627/-- The settlement moves: one per live quantum; settling quantum `t`
628erases its tag. -/
629def settlementMoves (m : ℕ) : Finset (Finset ℕ) :=
630 (tickCarrier m).image (tickCarrier m).erase
631
632/-- The full ledger move set out of the canonical size-`m` carrier. -/
633def ledgerMoves (m : ℕ) : Finset (Finset ℕ) :=
634 insert (postingMove m) (settlementMoves m)
635
636/-- The ledger-counted transition multiplicity: the number of ledger moves
637out of the canonical size-`m` carrier landing on a size-`n` carrier. -/
638def ledgerMoveCount (m n : ℕ) : ℕ :=
639 ((ledgerMoves m).filter (fun T => T.card = n)).card
640
641theorem postingMove_card (m : ℕ) : (postingMove m).card = m + 1 := by
642 unfold postingMove tickCarrier
643 rw [Finset.card_insert_of_notMem (by simp), Finset.card_range]
644
645theorem settlementMove_card {m : ℕ} {T : Finset ℕ}
646 (hT : T ∈ settlementMoves m) : T.card = m - 1 := by
647 obtain ⟨t, ht, rfl⟩ := Finset.mem_image.mp hT
648 rw [Finset.card_erase_of_mem ht]
649 simp [tickCarrier]
650
651theorem settlementMoves_card (m : ℕ) : (settlementMoves m).card = m := by
652 unfold settlementMoves tickCarrier
653 rw [Finset.card_image_of_injOn (Finset.erase_injOn _), Finset.card_range]
654
655/-- **One up-move.** Exactly one ledger move enlarges the carrier: the
656tick-pinned posting. -/
657theorem ledgerMoveCount_up (m : ℕ) : ledgerMoveCount m (m + 1) = 1 := by
658 unfold ledgerMoveCount ledgerMoves
659 rw [Finset.filter_insert, if_pos (postingMove_card m)]
660 have hempty : (settlementMoves m).filter (fun T => T.card = m + 1) = ∅ := by
661 rw [Finset.filter_eq_empty_iff]
662 intro T hT
663 rw [settlementMove_card hT]
664 omega
665 rw [hempty]
666 simp
667
668/-- **`m + 1` down-moves out of size `m + 1`.** One settlement per live
669quantum, and distinct quanta give distinct results. -/
670theorem ledgerMoveCount_down (m : ℕ) : ledgerMoveCount (m + 1) m = m + 1 := by
671 unfold ledgerMoveCount ledgerMoves
672 have hpost : ¬ (postingMove (m + 1)).card = m := by
673 rw [postingMove_card]
674 omega
675 rw [Finset.filter_insert, if_neg hpost]
676 have hall : (settlementMoves (m + 1)).filter (fun T => T.card = m) =
677 settlementMoves (m + 1) := by
678 rw [Finset.filter_eq_self]
679 intro T hT
680 rw [settlementMove_card hT]
681 omega
682 rw [hall, settlementMoves_card]
683
684/-- No other transition is reachable by one ledger move. -/
685theorem ledgerMoveCount_off (m n : ℕ) (h1 : n ≠ m + 1) (h2 : m ≠ n + 1) :
686 ledgerMoveCount m n = 0 := by
687 unfold ledgerMoveCount ledgerMoves
688 have hpost : ¬ (postingMove m).card = n := by
689 rw [postingMove_card]
690 omega
691 rw [Finset.filter_insert, if_neg hpost]
692 rw [Finset.card_eq_zero, Finset.filter_eq_empty_iff]
693 intro T hT
694 obtain ⟨t, ht, rfl⟩ := Finset.mem_image.mp hT
695 have htm : t < m := Finset.mem_range.mp ht
696 rw [Finset.card_erase_of_mem ht]
697 simp only [tickCarrier, Finset.card_range]
698 omega
699
700/-- **The counted kernel is the counting kernel.** The ledger-counted
701multiplicities reproduce `carrierStepWeight` at the counting rates
702exactly. -/
703theorem ledgerMoveCount_eq_kernel (m n : ℕ) :
704 (ledgerMoveCount m n : ℝ) =
705 carrierStepWeight ⟨sizeBlindBirthPerLabelDeath⟩ m n := by
706 unfold carrierStepWeight
707 by_cases hup : n = m + 1
708 · subst hup
709 rw [ledgerMoveCount_up]
710 simp [sizeBlindBirthPerLabelDeath]
711 · by_cases hdown : m = n + 1
712 · subst hdown
713 rw [ledgerMoveCount_down]
714 simp only [if_neg hup, if_pos rfl, sizeBlindBirthPerLabelDeath]
715 push_cast
716 ring
717 · rw [ledgerMoveCount_off m n hup hdown]
718 simp [hup, hdown]
719
720/-- **D14 closed as typed**, with the provenance slot carrying the counting
721statement itself: the multiplicities are the cardinalities of the
722size-partitioned ledger move set, not a hand table. Scope: the tick-tagged
723carrier is the canonical history's state; deriving that pinning on actual
724`Recognition.Ledger` states is D15. -/
725def D14_theorem : D14_LedgerScheduleProvenance where
726 moveCount := ledgerMoveCount
727 countsKernel := ledgerMoveCount_eq_kernel
728 fromLedgerPostings :=
729 ∀ m n : ℕ, ledgerMoveCount m n =
730 ((ledgerMoves m).filter (fun T => T.card = n)).card
731
732/-- The provenance slot of `D14_theorem` holds definitionally: the counts
733ARE the move-set cardinalities. -/
734theorem D14_theorem_provenance_holds : D14_theorem.fromLedgerPostings :=
735 fun _ _ => rfl
736
737/-- **The tick pinning is load-bearing (decoy scored).** Without it the
738creation moves proliferate: allowing just the next two tick tags already
739gives two distinct up-moves, the road back to per-slot birth counting. -/
740theorem unpinned_up_moves_at_least_two (m : ℕ) :
741 insert m (tickCarrier m) ≠ insert (m + 1) (tickCarrier m) := by
742 intro h
743 have hmem : m ∈ insert (m + 1) (tickCarrier m) := by
744 rw [← h]
745 exact Finset.mem_insert_self m _
746 rcases Finset.mem_insert.mp hmem with h1 | h2
747 · omega
748 · exact absurd (Finset.mem_range.mp h2) (lt_irrefl m)
749
750/-- **D15 (OPEN residual, typed).** The canonical-history pinning: live
751quanta of an actual `Recognition.Ledger` state identified with tick tags,
752so that the tick-carrier move count is the ledger's own. The `Prop` field
753is the unformalized pinning clause; the vacuity guard below pre-scores the
754hand identification so the row cannot close by packaging. -/
755structure D15_CanonicalHistoryPinning where
756 /-- A size function on tick carriers agreeing with cardinality. -/
757 size : Finset ℕ → ℕ
758 agrees : ∀ S : Finset ℕ, size S = S.card
759 /-- The identification of live ledger quanta with tick tags is the
760 canonical history's, not a hand choice. -/
761 fromCanonicalHistory : Prop
762
763/-- **Vacuity guard (decoy pre-scored).** The hand identification inhabits
764D15's package with `True` provenance. -/
765def D15_bare_admits_hand_pinning : D15_CanonicalHistoryPinning where
766 size := Finset.card
767 agrees := fun _ => rfl
768 fromCanonicalHistory := True
769
770end D14Attack
771
772/-! ## D15 attacked (2026-08-07, fourth pass): the pinning is read off the
773ledger's own run
774
775The canonical history is the run of the actual posting dynamics
776(`Gap2DynamicsKindRule.runSchedule`, whose step is the real
777`Recognition.Ledger` posting increment) from the zero ledger, under the
778schedule that posts tick `t`'s quantum to the fresh tick-tag account `t`.
779On the tick-tag carrier `discreteCarrier ℕ` the run's state after `t`
780ticks is exactly the indicator ledger of the tick carrier, and an account
781is live (`phi ≠ 0`) exactly when its tag is a posted tick
782(`canonicalRun_live_iff`). The D15 size function is then computed from
783the ledger state's own liveness reading, not from the raw finset, and the
784provenance slot carries the proved pinning statement.
785
786The load-bearing freshness discipline is scored rather than hidden: the
787same-account decoy schedule (every tick posts to account `0`) yields a
788run whose live set collapses to `{0}`, so the pinning fails at tick 2
789(`sameAccount_fails_pinning`). Deriving the freshness discipline itself
790from ledger law, rather than naming it as the canonical history's
791defining property, is the survivor residual D16, typed below with its
792named-schedule decoy pre-scored. -/
793
794section D15Attack
795
796open Gap2DynamicsKindRule
797
798/-- The canonical tick schedule: at tick `t`, post one quantum to the
799fresh tick-tag account `t` (debit side). -/
800def tickSchedule : Schedule ℕ :=
801 fun t => some (t, LedgerPostingAdjacency.Side.debit)
802
803/-- The canonical history: the run of the actual posting dynamics from
804the zero ledger under the canonical tick schedule. -/
805def canonicalRun (t : ℕ) : Recognition.Ledger (discreteCarrier ℕ) :=
806 runSchedule zeroLedger tickSchedule t
807
808/-- The indicator ledger of a tick carrier: one posted quantum per tag. -/
809def carrierLedger (S : Finset ℕ) :
810 Recognition.Ledger (discreteCarrier ℕ) where
811 debit := fun u => if u ∈ S then 1 else 0
812 credit := fun _ => 0
813
814theorem canonicalRun_succ (t : ℕ) :
815 canonicalRun (t + 1) =
816 postAt (canonicalRun t) t LedgerPostingAdjacency.Side.debit := by
817 simp [canonicalRun, runSchedule, tickSchedule]
818
819theorem canonicalRun_debit (t u : ℕ) :
820 (canonicalRun t).debit u = if u ∈ tickCarrier t then 1 else 0 := by
821 induction t with
822 | zero =>
823 simp [canonicalRun, runSchedule, zeroLedger, tickCarrier]
824 | succ t ih =>
825 rw [canonicalRun_succ]
826 show (if u = t then (canonicalRun t).debit u + 1
827 else (canonicalRun t).debit u) = _
828 by_cases h : u = t
829 · subst h
830 rw [if_pos rfl, ih,
831 if_neg (by simp [tickCarrier]),
832 if_pos (by simp [tickCarrier])]
833 norm_num
834 · rw [if_neg h, ih]
835 have hmem : u ∈ tickCarrier (t + 1) ↔ u ∈ tickCarrier t := by
836 unfold tickCarrier
837 simp only [Finset.mem_range]
838 omega
839 by_cases hu : u ∈ tickCarrier t
840 · rw [if_pos hu, if_pos (hmem.mpr hu)]
841 · rw [if_neg hu, if_neg (fun hc => hu (hmem.mp hc))]
842
843theorem canonicalRun_credit (t u : ℕ) : (canonicalRun t).credit u = 0 := by
844 induction t with
845 | zero =>
846 simp [canonicalRun, runSchedule, zeroLedger]
847 | succ t ih =>
848 rw [canonicalRun_succ]
849 exact ih
850
851private theorem tickLedger_ext
852 {L₁ L₂ : Recognition.Ledger (discreteCarrier ℕ)}
853 (hd : ∀ u, L₁.debit u = L₂.debit u)
854 (hc : ∀ u, L₁.credit u = L₂.credit u) : L₁ = L₂ := by
855 cases L₁
856 cases L₂
857 simp only [Recognition.Ledger.mk.injEq]
858 exact ⟨funext hd, funext hc⟩
859
860/-- **The canonical run's states ARE the tick-carrier ledgers.** -/
861theorem canonicalRun_eq_carrierLedger (t : ℕ) :
862 canonicalRun t = carrierLedger (tickCarrier t) := by
863 apply tickLedger_ext
864 · intro u
865 rw [canonicalRun_debit]
866 rfl
867 · intro u
868 rw [canonicalRun_credit]
869 rfl
870
871theorem canonicalRun_phi (t u : ℕ) :
872 Recognition.phi (canonicalRun t) u =
873 if u ∈ tickCarrier t then 1 else 0 := by
874 unfold Recognition.phi
875 rw [canonicalRun_debit, canonicalRun_credit]
876 by_cases h : u ∈ tickCarrier t <;> simp [h]
877
878/-- **The pinning read off the ledger.** An account of the canonical run
879is live exactly when its tag is a posted tick. -/
880theorem canonicalRun_live_iff (t u : ℕ) :
881 Recognition.phi (canonicalRun t) u ≠ 0 ↔ u ∈ tickCarrier t := by
882 rw [canonicalRun_phi]
883 by_cases h : u ∈ tickCarrier t
884 · simp [h]
885 · simp [h]
886
887theorem carrierLedger_phi (S : Finset ℕ) (u : ℕ) :
888 Recognition.phi (carrierLedger S) u = if u ∈ S then 1 else 0 := by
889 by_cases h : u ∈ S <;> simp [Recognition.phi, carrierLedger, h]
890
891/-- Ledger-computed size: count the tags that the ledger state itself
892marks live. -/
893def ledgerLiveSize (S : Finset ℕ) : ℕ :=
894 (S.filter (fun u => Recognition.phi (carrierLedger S) u ≠ 0)).card
895
896theorem ledgerLiveSize_agrees (S : Finset ℕ) : ledgerLiveSize S = S.card := by
897 unfold ledgerLiveSize
898 have hfilter :
899 S.filter (fun u => Recognition.phi (carrierLedger S) u ≠ 0) = S := by
900 apply Finset.filter_eq_self.mpr
901 intro u hu
902 rw [carrierLedger_phi, if_pos hu]
903 norm_num
904 rw [hfilter]
905
906/-- The provenance statement: the canonical run's states are the
907tick-carrier ledgers, and liveness is tick-tag membership. -/
908def CanonicalPinning : Prop :=
909 (∀ t : ℕ, canonicalRun t = carrierLedger (tickCarrier t)) ∧
910 ∀ t u : ℕ,
911 Recognition.phi (canonicalRun t) u ≠ 0 ↔ u ∈ tickCarrier t
912
913theorem canonicalPinning_holds : CanonicalPinning :=
914 ⟨canonicalRun_eq_carrierLedger, canonicalRun_live_iff⟩
915
916/-- **D15 closed as typed**: the size function is computed from the ledger
917state's own liveness reading, and the provenance slot carries the proved
918canonical pinning rather than `True`. Scope: the freshness discipline of
919the canonical schedule is named, not derived (D16). -/
920def D15_theorem : D15_CanonicalHistoryPinning where
921 size := ledgerLiveSize
922 agrees := ledgerLiveSize_agrees
923 fromCanonicalHistory := CanonicalPinning
924
925theorem D15_theorem_provenance_holds : D15_theorem.fromCanonicalHistory :=
926 canonicalPinning_holds
927
928/-- **Freshness scored (decoy).** The same-account schedule posts every
929tick to account `0`. -/
930def sameAccountSchedule : Schedule ℕ :=
931 fun _ => some (0, LedgerPostingAdjacency.Side.debit)
932
933/-- Without the fresh-tag discipline the pinning fails: at tick 2 the
934same-account run holds tag 1 dead while the tick carrier holds it live. -/
935theorem sameAccount_fails_pinning :
936 ¬ ∀ t u : ℕ,
937 Recognition.phi (runSchedule zeroLedger sameAccountSchedule t) u ≠ 0 ↔
938 u ∈ tickCarrier t := by
939 intro hall
940 have hcomp :
941 Recognition.phi (runSchedule zeroLedger sameAccountSchedule 2) 1 = 0 := by
942 simp [runSchedule, sameAccountSchedule, postAt, zeroLedger,
943 Recognition.phi]
944 exact (hall 2 1).mpr (by simp [tickCarrier]) hcomp
945
946/-- **D16 (OPEN residual, typed).** The fresh-tag schedule discipline: a
947schedule whose run realizes the canonical pinning, derived from ledger law
948rather than named. The `Prop` field is the unformalized derivation
949clause; the vacuity guard below pre-scores the named-schedule inhabitant
950so the row cannot close by packaging. -/
951structure D16_FreshTagDiscipline where
952 sched : Schedule ℕ
953 pins : ∀ t u : ℕ,
954 Recognition.phi (runSchedule zeroLedger sched t) u ≠ 0 ↔
955 u ∈ tickCarrier t
956 /-- The schedule's freshness is forced by ledger law, not stipulated. -/
957 fromLedgerLaw : Prop
958
959/-- **Vacuity guard (decoy pre-scored).** Naming the canonical schedule
960inhabits D16's package with `True` provenance; the row's content is the
961derivation of freshness, which no package close can certify. -/
962def D16_bare_admits_named_schedule : D16_FreshTagDiscipline where
963 sched := tickSchedule
964 pins := canonicalRun_live_iff
965 fromLedgerLaw := True
966
967/-! ### D16 attacked (2026-08-07, fifth pass): the pinning characterizes
968freshness
969
970The freshness discipline is not a stipulation on top of the canonical
971pinning: it is FORCED by it. An idle tick cannot make the fresh tag live,
972and a posting at any other account leaves the fresh tag's flux untouched,
973so any schedule whose run realizes the pinning posts to exactly the fresh
974tick-tag account at every tick (`pinning_forces_fresh_tag`). Conversely
975every fresh schedule pins, whichever side each tick posts on
976(`freshSchedule_pins`), giving the full characterization `pins_iff_fresh`.
977What the forcing does NOT cover, scored: the debit side of the canonical
978schedule is a convention, because the all-credit fresh schedule pins too
979(`credit_schedule_also_pins`); the side convention is recorded as MODEL
980(D17). -/
981
982/-- Posting at one account leaves every other account's flux unchanged. -/
983theorem postAt_phi_ne (L : Recognition.Ledger (discreteCarrier ℕ)) (k : ℕ)
984 (s : LedgerPostingAdjacency.Side) (u : ℕ) (hu : u ≠ k) :
985 Recognition.phi (postAt L k s) u = Recognition.phi L u := by
986 cases s <;> simp [postAt, Recognition.phi, hu]
987
988/-- **Freshness forced, tick by tick.** Any schedule whose run realizes
989the canonical pinning posts, at every tick, one quantum to exactly the
990fresh tick-tag account. -/
991theorem pinning_forces_fresh_tag (sched : Schedule ℕ)
992 (hpins : ∀ t u : ℕ,
993 Recognition.phi (runSchedule zeroLedger sched t) u ≠ 0 ↔
994 u ∈ tickCarrier t) (t : ℕ) :
995 ∃ s, sched t = some (t, s) := by
996 have hlive : Recognition.phi (runSchedule zeroLedger sched (t + 1)) t ≠ 0 :=
997 (hpins (t + 1) t).mpr (by simp [tickCarrier])
998 have hdead : Recognition.phi (runSchedule zeroLedger sched t) t = 0 := by
999 by_contra h
1000 have hmem := (hpins t t).mp h
1001 simp [tickCarrier] at hmem
1002 cases hsched : sched t with
1003 | none =>
1004 have hstep : runSchedule zeroLedger sched (t + 1) =
1005 runSchedule zeroLedger sched t := by
1006 simp [runSchedule, hsched]
1007 rw [hstep] at hlive
1008 exact absurd hdead hlive
1009 | some p =>
1010 obtain ⟨a, s⟩ := p
1011 by_cases ha : a = t
1012 · exact ⟨s, by rw [ha]⟩
1013 · have hstep : runSchedule zeroLedger sched (t + 1) =
1014 postAt (runSchedule zeroLedger sched t) a s := by
1015 simp [runSchedule, hsched]
1016 rw [hstep, postAt_phi_ne _ _ _ _ (fun h => ha h.symm)] at hlive
1017 exact absurd hdead hlive
1018
1019/-- Column readout of a fresh run: an account's debit column holds one
1020quantum exactly when its tag has been posted on the debit side, and
1021likewise for credit. -/
1022theorem freshRun_columns (side : ℕ → LedgerPostingAdjacency.Side) (t u : ℕ) :
1023 (runSchedule zeroLedger (fun n => some (n, side n)) t).debit u =
1024 (if u ∈ tickCarrier t ∧ side u = LedgerPostingAdjacency.Side.debit
1025 then 1 else 0) ∧
1026 (runSchedule zeroLedger (fun n => some (n, side n)) t).credit u =
1027 (if u ∈ tickCarrier t ∧ side u = LedgerPostingAdjacency.Side.credit
1028 then 1 else 0) := by
1029 induction t with
1030 | zero =>
1031 constructor <;> simp [runSchedule, zeroLedger, tickCarrier]
1032 | succ t ih =>
1033 obtain ⟨ihd, ihc⟩ := ih
1034 have hstep : runSchedule zeroLedger (fun n => some (n, side n)) (t + 1) =
1035 postAt (runSchedule zeroLedger (fun n => some (n, side n)) t) t
1036 (side t) := by
1037 simp [runSchedule]
1038 have hmem : ∀ v : ℕ,
1039 v ∈ tickCarrier (t + 1) ↔ v ∈ tickCarrier t ∨ v = t := by
1040 intro v
1041 simp only [tickCarrier, Finset.mem_range]
1042 omega
1043 have hdead_t : t ∉ tickCarrier t := by simp [tickCarrier]
1044 rw [hstep]
1045 cases hs : side t with
1046 | debit =>
1047 constructor
1048 · show (if u = t then
1049 (runSchedule zeroLedger (fun n => some (n, side n)) t).debit u + 1
1050 else
1051 (runSchedule zeroLedger (fun n => some (n, side n)) t).debit u) = _
1052 by_cases hu : u = t
1053 · subst hu
1054 rw [if_pos rfl, ihd, if_neg (fun h => hdead_t h.1),
1055 if_pos ⟨(hmem u).mpr (Or.inr rfl), hs⟩, zero_add]
1056 · rw [if_neg hu, ihd]
1057 refine if_congr ?_ rfl rfl
1058 constructor
1059 · rintro ⟨hm, hside⟩
1060 exact ⟨(hmem u).mpr (Or.inl hm), hside⟩
1061 · rintro ⟨hm, hside⟩
1062 exact ⟨((hmem u).mp hm).resolve_right hu, hside⟩
1063 · show (runSchedule zeroLedger (fun n => some (n, side n)) t).credit u = _
1064 rw [ihc]
1065 refine if_congr ?_ rfl rfl
1066 constructor
1067 · rintro ⟨hm, hside⟩
1068 exact ⟨(hmem u).mpr (Or.inl hm), hside⟩
1069 · rintro ⟨hm, hside⟩
1070 rcases (hmem u).mp hm with h | h
1071 · exact ⟨h, hside⟩
1072 · rw [h] at hside
1073 exact absurd (hside.symm.trans hs)
1074 (fun hcon => LedgerPostingAdjacency.Side.noConfusion hcon)
1075 | credit =>
1076 constructor
1077 · show (runSchedule zeroLedger (fun n => some (n, side n)) t).debit u = _
1078 rw [ihd]
1079 refine if_congr ?_ rfl rfl
1080 constructor
1081 · rintro ⟨hm, hside⟩
1082 exact ⟨(hmem u).mpr (Or.inl hm), hside⟩
1083 · rintro ⟨hm, hside⟩
1084 rcases (hmem u).mp hm with h | h
1085 · exact ⟨h, hside⟩
1086 · rw [h] at hside
1087 exact absurd (hside.symm.trans hs)
1088 (fun hcon => LedgerPostingAdjacency.Side.noConfusion hcon)
1089 · show (if u = t then
1090 (runSchedule zeroLedger (fun n => some (n, side n)) t).credit u + 1
1091 else
1092 (runSchedule zeroLedger (fun n => some (n, side n)) t).credit u) = _
1093 by_cases hu : u = t
1094 · subst hu
1095 rw [if_pos rfl, ihc, if_neg (fun h => hdead_t h.1),
1096 if_pos ⟨(hmem u).mpr (Or.inr rfl), hs⟩, zero_add]
1097 · rw [if_neg hu, ihc]
1098 refine if_congr ?_ rfl rfl
1099 constructor
1100 · rintro ⟨hm, hside⟩
1101 exact ⟨(hmem u).mpr (Or.inl hm), hside⟩
1102 · rintro ⟨hm, hside⟩
1103 exact ⟨((hmem u).mp hm).resolve_right hu, hside⟩
1104
1105/-- **Every fresh schedule pins**, whichever side each tick posts on. -/
1106theorem freshSchedule_pins (side : ℕ → LedgerPostingAdjacency.Side) :
1107 ∀ t u : ℕ,
1108 Recognition.phi
1109 (runSchedule zeroLedger (fun n => some (n, side n)) t) u ≠ 0 ↔
1110 u ∈ tickCarrier t := by
1111 intro t u
1112 obtain ⟨hd, hc⟩ := freshRun_columns side t u
1113 show (runSchedule zeroLedger (fun n => some (n, side n)) t).debit u -
1114 (runSchedule zeroLedger (fun n => some (n, side n)) t).credit u ≠ 0 ↔ _
1115 rw [hd, hc]
1116 by_cases hu : u ∈ tickCarrier t
1117 · cases hs : side u <;> simp [hu, hs]
1118 · simp [hu]
1119
1120/-- **D16 closed as typed: the pinning characterizes freshness.** A
1121schedule realizes the canonical pinning exactly when it posts one quantum
1122to the fresh tick-tag account at every tick, with only the side free.
1123Freshness is ledger law, not a stipulation. -/
1124theorem pins_iff_fresh (sched : Schedule ℕ) :
1125 (∀ t u : ℕ,
1126 Recognition.phi (runSchedule zeroLedger sched t) u ≠ 0 ↔
1127 u ∈ tickCarrier t) ↔
1128 ∃ side : ℕ → LedgerPostingAdjacency.Side,
1129 sched = fun t => some (t, side t) := by
1130 constructor
1131 · intro hpins
1132 refine ⟨fun t => (pinning_forces_fresh_tag sched hpins t).choose, ?_⟩
1133 funext t
1134 exact (pinning_forces_fresh_tag sched hpins t).choose_spec
1135 · rintro ⟨side, rfl⟩
1136 exact freshSchedule_pins side
1137
1138/-- The derivation clause carried by the D16 close: freshness is forced
1139by the pinning for EVERY schedule, quantified, not named. -/
1140def FreshnessForcedByLedgerLaw : Prop :=
1141 ∀ sched : Schedule ℕ,
1142 (∀ t u : ℕ,
1143 Recognition.phi (runSchedule zeroLedger sched t) u ≠ 0 ↔
1144 u ∈ tickCarrier t) →
1145 ∀ t : ℕ, ∃ s, sched t = some (t, s)
1146
1147theorem freshnessForced_holds : FreshnessForcedByLedgerLaw :=
1148 pinning_forces_fresh_tag
1149
1150/-- **D16 closed.** The package's derivation slot carries the quantified
1151forcing statement, proved, rather than `True` or a naming. -/
1152def D16_theorem : D16_FreshTagDiscipline where
1153 sched := tickSchedule
1154 pins := canonicalRun_live_iff
1155 fromLedgerLaw := FreshnessForcedByLedgerLaw
1156
1157theorem D16_theorem_fromLedgerLaw_holds : D16_theorem.fromLedgerLaw :=
1158 freshnessForced_holds
1159
1160/-- **Scope of the forcing, scored (D17, MODEL).** The pinning does not
1161force the debit side: the all-credit fresh schedule pins too. The debit
1162convention of the canonical schedule is a MODEL choice, not ledger law. -/
1163theorem credit_schedule_also_pins :
1164 ∀ t u : ℕ,
1165 Recognition.phi (runSchedule zeroLedger
1166 (fun n => some (n, LedgerPostingAdjacency.Side.credit)) t) u ≠ 0 ↔
1167 u ∈ tickCarrier t :=
1168 freshSchedule_pins fun _ => LedgerPostingAdjacency.Side.credit
1169
1170end D15Attack
1171
1172/-! ## Corrected floor plan and next block -/
1173
1174structure CorrectedFloorPlan where
1175 failedReason : String
1176 measurement : String
1177 correctedTarget : String
1178 doesNotKill : String
1179
1180/-- Stub floor plan. A failed row narrows the target; it does not reverse it. -/
1181def correctedFloorPlans : List CorrectedFloorPlan :=
1182 [ ⟨"D03",
1183 "equal per-slot rates balance constant weight, which fails insertion stationarity",
1184 "count one birth opportunity and one death opportunity per existing label",
1185 "the existence of insertion slots or the asymmetric target"⟩
1186 , ⟨"D06",
1187 "bakedFromWeight makes detailed balance algebraic",
1188 "derive rates from recognition move counting, without the stationary weight",
1189 "the abstract detailed-balance identity"⟩
1190 , ⟨"D07",
1191 "bare posting preserves the carrier and has the wrong move degree",
1192 "add a carrier-enlarging recognition dynamics",
1193 "the label-insertion geometry"⟩
1194 , ⟨"D08",
1195 "invariance axioms admit distinct candidate measures",
1196 "use a substrate fact stronger than invariance",
1197 "the existing gauge-counting theorem once its premise is supplied"⟩
1198 , ⟨"D09",
1199 "size fugacities are relabeling-invariant",
1200 "derive a selector stronger than label indifference",
1201 "the invariance calculation itself"⟩
1202 , ⟨"D12",
1203 "every selector respecting bare posting reachability is constant across rated worlds",
1204 "select the counting rates from a carrier-enlarging recognition dynamics whose observation relation is rate-sensitive",
1205 "the existence of non-baked counting rates (D10), the insertion kernel (D11), or the insertion-slot geometry"⟩ ]
1206
1207theorem correctedFloorPlans_length : correctedFloorPlans.length = 6 := by
1208 decide
1209
1210/-- Room B has no remaining OPEN row after the D16 close: the pinning
1211characterizes freshness, and the side convention is MODEL (D17). -/
1212def nextAttackBlock : List String := []
1213
1214theorem nextAttackBlock_length : nextAttackBlock.length = 0 := by
1215 decide
1216
1217/-! ## Immutable status -/
1218
1219theorem gap2_measure_derived_unmoved :
1220 FullTheoryLedger.fullTheoryBenchmarks.gap2_measure_derived = true :=
1221 Gap2GluingLawStationarity.gap2_measure_derived_unmoved
1222
1223/-! ## Composite certificate -/
1224
1225/-- Packages the D10/D11 closures, the scored decoys, the D12 wall, the
1226D13 close, the D14 ledger-counted schedule, the D15 canonical pinning
1227read off the ledger's own run, and the D16 freshness forcing. Does not
1228move the measure flag. -/
1229theorem insertionAsymmetryReasons_certified :
1230 reasonTable.length = 17 ∧
1231 RecognitionRateAsymmetry ∧
1232 D11 ∧
1233 CountingEquivalentRates
1234 (bakedFromWeight factorialWorld.weight factorialWorld_weight_pos) ∧
1235 CountingEquivalentRates sizeBlindBirthPerLabelDeath ∧
1236 ¬ CountingEquivalentRates equalPerSlotRates ∧
1237 ¬ D12 ∧
1238 (∃ Obs : PostingRatedWorld → Prop,
1239 FactorsThroughKernel Obs ∧
1240 Obs ⟨sizeBlindBirthPerLabelDeath⟩ ∧ ¬ Obs ⟨equalPerSlotRates⟩) ∧
1241 (∀ m n : ℕ, (ledgerMoveCount m n : ℝ) =
1242 carrierStepWeight ⟨sizeBlindBirthPerLabelDeath⟩ m n) ∧
1243 CanonicalPinning ∧
1244 FreshnessForcedByLedgerLaw ∧
1245 correctedFloorPlans.length = 6 ∧
1246 nextAttackBlock.length = 0 ∧
1247 FullTheoryLedger.fullTheoryBenchmarks.gap2_measure_derived = true :=
1248 ⟨reasonTable_length, recognitionRateAsymmetry_derived, D11_theorem,
1249 bakedFromWeight_factorial_satisfies_counting_law,
1250 sizeBlind_satisfies_counting_law, equalPerSlotRates_not_countingEquivalent,
1251 D12_refuted, D13_sharpened_holds, ledgerMoveCount_eq_kernel,
1252 canonicalPinning_holds, freshnessForced_holds, correctedFloorPlans_length,
1253 nextAttackBlock_length, gap2_measure_derived_unmoved⟩
1254
1255#print axioms D01_theorem
1256#print axioms D02_theorem
1257#print axioms D03_refuted
1258#print axioms D04_theorem
1259#print axioms D05_theorem
1260#print axioms D06_refuted
1261#print axioms D07_refuted
1262#print axioms D08_refuted
1263#print axioms D09_refuted
1264#print axioms recognitionRateAsymmetry_derived
1265#print axioms D10_theorem
1266#print axioms D11_theorem
1267#print axioms countingLaw_balances_factorialWorld
1268#print axioms bakedFromWeight_factorial_satisfies_counting_law
1269#print axioms sizeBlindBirthPerLabelDeath_ne_bakedFromWeight
1270#print axioms equalPerSlotRates_not_countingEquivalent
1271#print axioms D12_refuted
1272#print axioms recognition_presently_typed_cannot_select_asymmetry
1273#print axioms kernelUpObs_selects_counting
1274#print axioms kernelUpObs_rejects_equalPerSlot
1275#print axioms D13_sharpened_holds
1276#print axioms D13_theorem_provenance_holds
1277#print axioms kernel_sees_what_posting_cannot
1278#print axioms ledgerMoveCount_up
1279#print axioms ledgerMoveCount_down
1280#print axioms ledgerMoveCount_eq_kernel
1281#print axioms D14_theorem_provenance_holds
1282#print axioms unpinned_up_moves_at_least_two
1283#print axioms canonicalRun_eq_carrierLedger
1284#print axioms canonicalRun_live_iff
1285#print axioms ledgerLiveSize_agrees
1286#print axioms canonicalPinning_holds
1287#print axioms D15_theorem_provenance_holds
1288#print axioms sameAccount_fails_pinning
1289#print axioms pinning_forces_fresh_tag
1290#print axioms freshSchedule_pins
1291#print axioms pins_iff_fresh
1292#print axioms freshnessForced_holds
1293#print axioms D16_theorem_fromLedgerLaw_holds
1294#print axioms credit_schedule_also_pins
1295#print axioms insertionAsymmetryReasons_certified
1296#print axioms gap2_measure_derived_unmoved
1297
1298end
1299end InsertionAsymmetryInevitableReasons
1300end SevenGaps
1301end Gravity
1302end IndisputableMonolith
1303