IndisputableMonolith.Gravity.SevenGaps.GaugeCountingInevitableReasons
IndisputableMonolith/Gravity/SevenGaps/GaugeCountingInevitableReasons.lean · 710 lines · 78 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.SevenGaps.MeasureSubstrateBlocker
2import IndisputableMonolith.Gravity.SevenGaps.MeasureInvarianceNoGo
3import IndisputableMonolith.Gravity.SevenGaps.Gap2PostingLayerFloor
4import IndisputableMonolith.Gravity.SevenGaps.Gap2GaugeVolume
5import IndisputableMonolith.Gravity.SevenGaps.Gap2LabelInsertionDynamics
6import IndisputableMonolith.Gravity.SevenGaps.Gap2GluingLawStationarity
7import IndisputableMonolith.Gravity.SevenGaps.Gap2FugacityPostingGluing
8import IndisputableMonolith.Gravity.SevenGaps.Gap2SizeBlindnessReach
9import IndisputableMonolith.Gravity.SevenGaps.Gap2LedgerSiteBlindness
10import IndisputableMonolith.Gravity.Analysis.RecognitionDualEntryEnrichment4D
11
12/-!
13# Gauge-counting inevitable reasons (necessary-reasons census)
14
15Assume the Gap-2 measure target is required: richer RecognitionLedger /
16posting-layer structure forces
17`MeasureSubstrateBlocker.GaugeCountingPrinciple` for the physical class
18mass (equivalently `ν = 1/|Aut|`). Then every fact that would make that
19unavoidable is listed below. Each reason is proved, left OPEN, recorded
20as MODEL, or refuted. A failed reason does not automatically mean its
21opposite: it forces a corrected floor plan.
22
23Method: `plans/Necessary_Reasons_Process_20260807.html`.
24Exemplar shape: `OneCarrierInevitableReasons.lean`.
25Binding prompt:
26`plans/QG_Gap2_GaugeCounting_Necessary_Reasons_Session_Prompt_20260807.txt`.
27
28Honesty:
29
30* THEOREM: invariance underdetermines the measure; GCP ↔ gaugeOrbitMass;
31 gaugeOrbitMass satisfies GCP; uniform class mass fails GCP; pinned
32 carrier collapses to complex counting; uniqueness wall for invariant
33 enrichments; equivariant costs contribute no factor; label-asymmetric
34 letter costs exist; orbit-stabilizer accounting; mere label-indifference
35 does not select Gibbs.
36* THEOREM (R18 block): the fugacity–action rebooking gauge
37 `(a, S) ↦ (t·a, S + log t)` preserves the Boltzmann product pointwise;
38 every satisfiable rebooking-invariant prior admits a non-unit-fugacity
39 representative, so none can select `a ≡ 1`; every product-visible prior
40 (one that sees only the physical weight) is rebooking-invariant.
41* REFUTED as a derivation of GCP from richer structure: invariant
42 enrichment, equivariant posting cost, bare-posting gluing, unit fugacity
43 from posting+gluing, size-blindness from cluster decomposition,
44 disjoint-union factorization, ledger-cost readout, vertex-site symmetry
45 count, and “label indifference” as a selecting principle.
46* REFUTED (scoped, R18): no prior that sees only the physical Boltzmann
47 product forces the Gibbs numerator `a ≡ 1`. The literal
48 `AssumedRequired` Prop is vacuously inhabitable (`R18_vacuity_guard`
49 scores that decoy); the honest discharge is the wall, not the
50 inhabitant.
51* OPEN residual: an action-first prior. The only selectors outside the
52 wall pin the action independently of the measure: derive the ledger
53 action (the posting schedule nature executes) first, then the fugacity
54 booking is a convention and GCP for the counting measure is R03. Child
55 census rows U12 (derive `GluingLaw`) and U13 (justified asymmetry) in
56 `UnitFugacitySelector.lean` are the typed sub-lanes.
57* No inhabitation of “ledger forces GCP” is claimed. The corrected target
58 is typed below.
59-/
60
61namespace IndisputableMonolith
62namespace Gravity
63namespace SevenGaps
64namespace GaugeCountingInevitableReasons
65
66open PathSumMeasure ExactShellGaugePreflight
67open MeasureSubstrateBlocker MeasureInvarianceNoGo
68open Gap2PostingLayerFloor Gap2GaugeVolume Gap2PostingCostDerivation
69open GaugeHistoryMeasure
70open Gap2LabelInsertionDynamics Gap2GluingLawStationarity
71open Gap2FugacityPostingGluing Gap2SizeBlindnessReach Gap2GluingDerivation
72open Gap2LedgerSiteBlindness
73open IndisputableMonolith.Gravity.RecognitionLedger
74open Analysis.RecognitionDualEntryEnrichment4D
75
76noncomputable section
77
78/-! ## Reason census
79
80R01 invariance axioms underdetermine the path-sum measure
81R02 GaugeCountingPrinciple ↔ ν = gaugeOrbitMass
82R03 gaugeOrbitMass satisfies GaugeCountingPrinciple
83R04 uniform class mass fails GaugeCountingPrinciple
84R05 pinned CanonicalHistory count equals complex count
85R06 state-factored weights collapse on the pinned carrier
86R07 among invariant labeled weights, GCP forces Gibbs (uniqueness wall)
87R08 equivariant posting costs contribute no measure factor
88R09 label-asymmetric letter costs exist
89R10 mere label-indifference does not select Gibbs
90R11 orbit-stabilizer accounting is theorem (label count = orbit × |Aut|)
91R12 bare fixed-carrier posting moves do not derive the gluing factor
92R13 posting structure plus gluing does not force unit fugacity
93R14 cluster decomposition does not derive size-blindness as stated
94R15 disjoint-union multiplicativity does not force the class weight
95R16 recognition ledger cost values do not read out the class measure
96R17 Fin-2 vertex-site symmetry count cannot supply Aut-sensitive mass
97R18 Gibbs numerator a ≡ 1 is forced by a prior principle / schedule
98-/
99
100/-- Status table for the reason census. -/
101structure ReasonStatus where
102 id : String
103 title : String
104 /-- `"THEOREM"`, `"OPEN"`, `"MODEL"`, or `"REFUTED"`. -/
105 status : String
106
107def reasonTable : List ReasonStatus :=
108 [ ⟨"R01", "invariance axioms underdetermine the measure", "THEOREM"⟩
109 , ⟨"R02", "GCP iff ν equals gaugeOrbitMass", "THEOREM"⟩
110 , ⟨"R03", "gaugeOrbitMass satisfies GCP", "THEOREM"⟩
111 , ⟨"R04", "uniform class mass fails GCP", "THEOREM"⟩
112 , ⟨"R05", "pinned history count equals complex count", "THEOREM"⟩
113 , ⟨"R06", "pinned state-factored weights are complex functions", "THEOREM"⟩
114 , ⟨"R07", "invariant enrichment unique Gibbs / cannot derive GCP", "REFUTED"⟩
115 , ⟨"R08", "equivariant cost contributes no measure factor", "REFUTED"⟩
116 , ⟨"R09", "label-asymmetric letter costs exist", "THEOREM"⟩
117 , ⟨"R10", "mere label-indifference does not select Gibbs", "REFUTED"⟩
118 , ⟨"R11", "orbit-stabilizer accounting is theorem", "THEOREM"⟩
119 , ⟨"R12", "bare posting does not derive gluing", "REFUTED"⟩
120 , ⟨"R13", "posting+gluing does not force unit fugacity", "REFUTED"⟩
121 , ⟨"R14", "cluster decomposition does not give size-blindness", "REFUTED"⟩
122 , ⟨"R15", "disjoint-union factorization does not force class weight", "REFUTED"⟩
123 , ⟨"R16", "ledger cost values do not read class measure", "REFUTED"⟩
124 , ⟨"R17", "Fin-2 site-symmetry count is Aut-blind", "REFUTED"⟩
125 , ⟨"R18", "no rebooking-invariant (incl. product-visible) prior forces a≡1", "REFUTED"⟩ ]
126
127theorem reasonTable_length : reasonTable.length = 18 := by
128 decide
129
130/-! ## Already THEOREM reasons (imported and re-stood) -/
131
132/-- **R01.** Invariance alone underdetermines the path-sum measure. -/
133theorem R01_invariance_underdetermines (B : ℕ) (hB : 2 ≤ B) :
134 ∃ w₁ w₂ : BoundedComplex B → ℝ,
135 InvarianceAxioms B w₁ ∧ InvarianceAxioms B w₂ ∧ w₁ ≠ w₂ :=
136 invariance_underdetermines_measure B hB
137
138/-- **R02.** Normalized gauge counting selects exactly the counting mass. -/
139theorem R02_gcp_iff_gaugeOrbitMass {B : ℕ} (ν : TriangulationClass B → ℝ) :
140 GaugeCountingPrinciple ν ↔ ν = gaugeOrbitMass :=
141 gaugeCountingPrinciple_iff_eq_gaugeOrbitMass ν
142
143/-- **R03.** The counting-defined mass satisfies GCP. -/
144theorem R03_gaugeOrbitMass_satisfies {B : ℕ} :
145 GaugeCountingPrinciple (gaugeOrbitMass : TriangulationClass B → ℝ) :=
146 gaugeOrbitMass_satisfies
147
148/-- **R04.** The quotient-uniform decoy fails GCP. -/
149theorem R04_uniform_fails (B : ℕ) (hB : 2 ≤ B) :
150 ¬ GaugeCountingPrinciple
151 (uniformClassMass : TriangulationClass B → ℝ) :=
152 uniformClassMass_not_gaugeCounting B hB
153
154/-- **R05.** On the pinned carrier, counting is complex counting. -/
155theorem R05_pinned_count_is_complex (B : ℕ) :
156 Nat.card (CanonicalHistory B) = Nat.card (BoundedComplex B) :=
157 canonical_count_eq_complex_count B
158
159/-- **R06.** State-factored weights collapse on the pinned carrier. -/
160theorem R06_pinned_weights_are_complex {B : ℕ}
161 (F : ∀ (K : BoundedComplex B), DualEntryStrainState (PostingAlphabet K) → ℝ) :
162 ∃ g : BoundedComplex B → ℝ, ∀ CH : CanonicalHistory B,
163 F CH.underlying CH.H.state = g CH.underlying :=
164 state_factored_weight_is_complex_function F
165
166/-- **R09.** Label-asymmetric letter costs exist. -/
167theorem R09_label_asymmetric_exists : ∃ c : LetterCost, ¬ Equivariant c :=
168 label_asymmetric_structure_exists
169
170/-- **R11.** Orbit-stabilizer accounting is theorem, not premise. -/
171theorem R11_orbit_stabilizer {B : ℕ} (K : BoundedComplex B) :
172 gaugeOrbitCard K * Nat.card (Aut K)
173 = K.nV.factorial * (K.nE.factorial * K.nT.factorial) :=
174 irreducible_input_is_orbit_stabilizer K
175
176/-! ## REFUTED derivation routes (richer structure → GCP) -/
177
178/-- **R07 REFUTED as a derivation.** Among relabeling-invariant labeled
179weights, GCP holds of the class mass iff the weight is Gibbs pointwise.
180Asking for GCP among invariant enrichments leaves no degree of freedom:
181the principle and the Gibbs premise are the same assumption stated twice. -/
182theorem R07_invariant_enrichment_unique_gibbs (B : ℕ) (w : BoundedComplex B → ℝ)
183 (hinv : ∀ K K', Equivalent K K' → w K = w K') :
184 GaugeCountingPrinciple (classMass w) ↔
185 ∀ K : BoundedComplex B, w K = gibbsWeight K :=
186 invariant_enrichment_unique_gibbs B w hinv
187
188/-- **R08 REFUTED as a derivation.** Equivariant letter costs post `mu`
189exactly when their Boltzmann numerator is identically one. -/
190theorem R08_equivariant_cost_no_factor {c : LetterCost} (hc : Equivariant c)
191 (B : ℕ) :
192 (∀ K : BoundedComplex B,
193 classMass (postedWeight c B) (Quotient.mk (relabelSetoid B) K) = mu K)
194 ↔ ∀ K : BoundedComplex B, Real.exp (-(historyCost c B K)) = 1 :=
195 equivariant_cost_contributes_no_factor hc B
196
197/-- **R10 REFUTED as a selecting principle.** For any function `a` of the
198three index sizes, the fugacity weight is relabeling-invariant, so an
199entire family is label-indifferent. Indifference alone cannot select the
200Gibbs weight `a ≡ 1`. Banked kill:
201`N-route-gap2-premise-is-label-indifference`. -/
202theorem R10_indifference_family_underdetermines {B : ℕ}
203 (a : ℕ → ℕ → ℕ → ℝ) {K K' : BoundedComplex B}
204 (h : Equivalent K K') :
205 fugacityWeight a K = fugacityWeight a K' :=
206 fugacityWeight_invariant a h
207
208/-- **R10 companion.** GCP for a fugacity weight holds exactly when the
209fugacity is one on occupied sectors: the undischarged selector is unit
210cross-sector fugacity, not indifference. -/
211theorem R10_gcp_iff_unit_fugacity {B : ℕ} (a : ℕ → ℕ → ℕ → ℝ) :
212 GaugeCountingPrinciple (classMass (fugacityWeight a : BoundedComplex B → ℝ)) ↔
213 ∀ K : BoundedComplex B, a K.nV K.nE K.nT = 1 :=
214 gaugeCounting_iff_fugacity_one a
215
216/-! ## Corrected floor plan (no automatic opposite) -/
217
218/-- A failed reason does not license its opposite by default. -/
219structure CorrectedFloorPlan where
220 failedReason : String
221 measurement : String
222 correctedTarget : String
223 doesNotKill : String
224
225/-- Banked corrected floor plans from failed reasons. -/
226def correctedFloorPlans : List CorrectedFloorPlan :=
227 [ ⟨"R07",
228 "among invariant labeled weights, GCP ↔ weight = gibbsWeight pointwise",
229 "derive the Gibbs weight (or a≡1) from a prior principle, not from invariant enrichment of the complex",
230 "orbit-stabilizer accounting, GCP↔1/|Aut|, or the counting mass itself"⟩
231 , ⟨"R08",
232 "equivariant costs post mu iff Boltzmann numerator is identically 1",
233 "any cost-layer derivation must either force numerator 1 by a new premise or leave the equivariant class",
234 "non-equivariant / label-asymmetric letter costs (R09 inhabited)"⟩
235 , ⟨"R10",
236 "every a(sizes)/(nV!nE!nT!) is label-indifferent, so indifference admits a family",
237 "force the Gibbs numerator a≡1 among that family (or an equivalent selecting law)",
238 "the statement that GCP equals label-density / 1/|Aut| once Gibbs is chosen"⟩
239 , ⟨"assumed target",
240 "posting_layer_floor: pinned carrier + uniqueness wall exclude richer invariant derivation of GCP",
241 "CorrectedMeasurePremise: force Gibbs numerator a≡1 from a named prior stronger than indifference, or from justified label-asymmetric structure, or from the posting schedule nature executes",
242 "GCP as a typed obligation, gaugeOrbitMass_satisfies, or mu = 1/|Aut| once Gibbs is selected"⟩
243 , ⟨"R18",
244 "every satisfiable rebooking-invariant prior admits a doubled-fugacity representative (t=2 gauge step at the two-point complex), and every product-visible prior is rebooking-invariant",
245 "action-first: derive the ledger action independently of the measure, then the fugacity booking is a convention and GCP holds of the counting measure by R03",
246 "the child-census lanes U12 (derive GluingLaw) and U13 (justified asymmetry), or any prior that pins the action rather than the measure"⟩ ]
247
248theorem correctedFloorPlans_length : correctedFloorPlans.length = 5 := by
249 decide
250
251/-- **Corrected measure premise (typed, not inhabited).** The surviving
252obligation after the reason audit: select the Gibbs numerator `a ≡ 1`
253among the indifference family, by a named principle stronger than
254relabeling indifference. -/
255structure CorrectedMeasurePremise where
256 /-- Named prior that forces the Boltzmann numerator to be identically one
257 (equivalently selects gibbsWeight among size-dependent indifference
258 weights). -/
259 selectsGibbsNumerator : Prop
260 /-- That prior is not mere relabeling invariance / label indifference. -/
261 strongerThanIndifference : Prop
262 /-- From the prior, GaugeCountingPrinciple holds of the physical class mass. -/
263 forcesGCP : Prop
264
265/-- Room C's assumed-required target.
266
267The proposition records the surviving obligation: some ledger fact stronger
268than label indifference must select the Gibbs numerator and force
269`GaugeCountingPrinciple`. It is a target package, not an inhabitant. -/
270def AssumedRequired : Prop :=
271 ∃ p : CorrectedMeasurePremise,
272 p.selectsGibbsNumerator ∧
273 p.strongerThanIndifference ∧ p.forcesGCP
274
275/-- The assumed target “richer ledger structure forces GCP” is not claimed.
276The corrected obligation is the uninhabited `CorrectedMeasurePremise`. -/
277def assumedTargetStatus : String := "REFUTED_AS_STATED"
278
279/-! ## Numbered reason Props -/
280
281def R01 : Prop :=
282 ∀ (B : ℕ), 2 ≤ B →
283 ∃ w₁ w₂ : BoundedComplex B → ℝ,
284 InvarianceAxioms B w₁ ∧ InvarianceAxioms B w₂ ∧ w₁ ≠ w₂
285
286def R02 : Prop :=
287 ∀ {B : ℕ} (ν : TriangulationClass B → ℝ),
288 GaugeCountingPrinciple ν ↔ ν = gaugeOrbitMass
289
290def R03 : Prop :=
291 ∀ (B : ℕ),
292 GaugeCountingPrinciple (gaugeOrbitMass : TriangulationClass B → ℝ)
293
294def R04 : Prop :=
295 ∀ (B : ℕ), 2 ≤ B →
296 ¬ GaugeCountingPrinciple
297 (uniformClassMass : TriangulationClass B → ℝ)
298
299def R05 : Prop :=
300 ∀ (B : ℕ),
301 Nat.card (CanonicalHistory B) = Nat.card (BoundedComplex B)
302
303def R06 : Prop :=
304 ∀ {B : ℕ}
305 (F : ∀ (K : BoundedComplex B),
306 DualEntryStrainState (PostingAlphabet K) → ℝ),
307 ∃ g : BoundedComplex B → ℝ,
308 ∀ CH : CanonicalHistory B,
309 F CH.underlying CH.H.state = g CH.underlying
310
311def R07 : Prop :=
312 ∀ (B : ℕ) (w : BoundedComplex B → ℝ),
313 (∀ K K', Equivalent K K' → w K = w K') →
314 (GaugeCountingPrinciple (classMass w) ↔
315 ∀ K : BoundedComplex B, w K = gibbsWeight K)
316
317def R08 : Prop :=
318 ∀ {c : LetterCost}, Equivariant c → ∀ (B : ℕ),
319 (∀ K : BoundedComplex B,
320 classMass (postedWeight c B) (Quotient.mk (relabelSetoid B) K) = mu K)
321 ↔ ∀ K : BoundedComplex B, Real.exp (-(historyCost c B K)) = 1
322
323def R09 : Prop := ∃ c : LetterCost, ¬ Equivariant c
324
325def R10 : Prop :=
326 ∀ {B : ℕ} (a : ℕ → ℕ → ℕ → ℝ)
327 {K K' : BoundedComplex B}, Equivalent K K' →
328 fugacityWeight a K = fugacityWeight a K'
329
330def R11 : Prop :=
331 ∀ {B : ℕ} (K : BoundedComplex B),
332 gaugeOrbitCard K * Nat.card (Aut K)
333 = K.nV.factorial * (K.nE.factorial * K.nT.factorial)
334
335/-- R12 is the imported bare-posting-to-gluing no-go. -/
336def R12 : Prop :=
337 InsertionStationarity factorialWorld.weight ∧
338 ¬ InsertionStationarity constantWorld.weight ∧
339 (∀ {Λ : Type} [Fintype Λ] [DecidableEq Λ]
340 (L₁ L₂ : Recognition.Ledger (discreteCarrier Λ)),
341 WorldReachable factorialWorld L₁ L₂ ↔
342 WorldReachable constantWorld L₁ L₂)
343
344def R13 : Prop :=
345 ∀ {u v w : ℝ}, 0 < u → 0 < v → 0 < w →
346 ¬ (u = 1 ∧ v = 1 ∧ w = 1) →
347 ∃ (c : LetterCost) (f : ℕ → ℕ → ℕ → ℝ),
348 KindOnly c ∧ Equivariant c ∧ SizeBlind (postedWeight c)
349 ∧ (∀ (B' : ℕ) (K : BoundedComplex B'),
350 postedWeight c B' K = sizeWeight f K)
351 ∧ CarrierShuffle f
352 ∧ ¬ UnitFugacity f
353
354def R14 : Prop :=
355 ∀ {lam : ℝ}, 0 < lam → lam ≠ 1 →
356 SatisfiesTheOtherHypotheses (statWeight properStat lam)
357 ∧ ¬ SizeBlind (statWeight properStat lam)
358 ∧ classMass (statWeight properStat lam 2)
359 (Quotient.mk (relabelSetoid 2) twoBridges)
360 ≠ mu twoBridges
361
362/-- R15 is the imported disjoint-union gluing counterexample. -/
363def R15 : Prop :=
364 GluesGenerally (fun B => (uniformWeight : BoundedComplex B → ℝ)) ∧
365 classMass uniformWeight
366 (Quotient.mk (relabelSetoid (1 + 2 + 0)) (bouquet 2 0)) ≠
367 mu (bouquet 2 0)
368
369def R16 : Prop :=
370 ∀ (f : BoundedComplex 2 → ℝ), (∀ K, 0 ≤ f K) →
371 ∃ enc : BoundedComplex 2 → RecognitionLedger (Fin 2),
372 ∀ K, (enc K).cost 0 1 = f K
373
374def R17 : Prop :=
375 ∀ (enc : BoundedComplex 2 → RecognitionLedger (Fin 2))
376 (g : ℕ → ℝ) (ν : TriangulationClass 2 → ℝ),
377 (∀ K : BoundedComplex 2, K.nV = 2 →
378 ν (Quotient.mk (relabelSetoid 2) K) =
379 g (siteSymCard (enc K))) →
380 ¬ GaugeCountingPrinciple ν
381
382/-- R18 is the surviving selector target. OPEN. -/
383def R18 : Prop := AssumedRequired
384
385/-! ## Banked reason rows -/
386
387theorem R01_reason : R01 := by
388 intro B hB
389 exact R01_invariance_underdetermines B hB
390
391theorem R02_reason : R02 := by
392 intro B ν
393 exact R02_gcp_iff_gaugeOrbitMass ν
394
395theorem R03_reason : R03 := by
396 intro B
397 exact R03_gaugeOrbitMass_satisfies
398
399theorem R04_reason : R04 := by
400 intro B hB
401 exact R04_uniform_fails B hB
402
403theorem R05_reason : R05 := by
404 intro B
405 exact R05_pinned_count_is_complex B
406
407theorem R06_reason : R06 := by
408 intro B F
409 exact R06_pinned_weights_are_complex F
410
411theorem R07_reason : R07 :=
412 fun B w hinv => R07_invariant_enrichment_unique_gibbs B w hinv
413
414theorem R08_reason : R08 := by
415 intro c hc B
416 exact R08_equivariant_cost_no_factor hc B
417
418theorem R09_reason : R09 :=
419 R09_label_asymmetric_exists
420
421theorem R10_reason : R10 := by
422 intro B a K K' h
423 exact R10_indifference_family_underdetermines a h
424
425theorem R11_reason : R11 := by
426 intro B K
427 exact R11_orbit_stabilizer K
428
429theorem R12_refuted : R12 :=
430 Gap2GluingLawStationarity.bare_posting_does_not_force_insertion_stationarity
431
432theorem R13_refuted : R13 := by
433 intro u v w hu hv hw hne
434 exact gluing_and_posting_do_not_force_unit_fugacity hu hv hw hne
435
436theorem R14_refuted : R14 :=
437 size_blindness_not_forced_by_the_other_hypotheses
438
439theorem R15_refuted : R15 :=
440 gluing_alone_does_not_force_mu
441
442theorem R16_refuted : R16 := by
443 intro f hf
444 exact encoding_unconstrained f hf
445
446theorem R17_refuted : R17 := by
447 intro enc g ν hfactor
448 exact no_siteSymmetry_measure (hB := by norm_num) (hB1 := by norm_num)
449 enc g ν hfactor
450
451/-! ## R18: the booking-gauge wall (scoped refutation from survivors)
452
453The survivors R01–R17 leave one question: can any prior principle force the
454Gibbs numerator `a ≡ 1`? The absorption identity U07
455(`fugacity_absorbs_into_action`) is sharpened here into the obstruction.
456The split of the physical Boltzmann product into a sector fugacity and an
457action is a bookkeeping symmetry: `(a, S) ↦ (t·a, S + log t)` preserves the
458product pointwise (`R18_rebooking_preserves_product`). A prior that
459respects that symmetry, and in particular one that sees only the physical
460product weight (`ProductVisible`), cannot select `a ≡ 1`
461(`R18_no_rebooking_invariant_selector`, `R18_no_product_visible_selector`):
462if it is satisfiable at all, it admits a representative whose fugacity is
463not one (`R18_rebooking_invariant_admits_nonunit`).
464
465The literal `R18` Prop is also vacuously inhabitable, because
466`CorrectedMeasurePremise` packages three uninterpreted Props;
467`R18_vacuity_guard` records the trivial inhabitant so the row can never be
468scored by inhabiting the package. The honest content of the row is the
469wall.
470
471Survivor, with no automatic opposite: a prior outside the wall must pin the
472action independently of the measure. Derive the ledger action first; the
473fugacity booking is then a convention, and GCP for the counting measure is
474R03. That is the action-first lane, with the child census rows U12 (derive
475`GluingLaw`) and U13 (justified asymmetry) still open in
476`UnitFugacitySelector.lean`. -/
477
478/-- The rebooking gauge transformation preserves the physical Boltzmann
479product: scaling the sector fugacity by a positive `t` while shifting the
480action by `log t` leaves `fugacityWeight · exp(-S)` pointwise unchanged.
481This is the general step of which U07 (`fugacity_absorbs_into_action`) is
482the total-absorption case `t = 1/a`. -/
483theorem R18_rebooking_preserves_product {B : ℕ}
484 (a a' : ℕ → ℕ → ℕ → ℝ) (t : ℝ) (S : BoundedComplex B → ℝ)
485 (K : BoundedComplex B)
486 (ht : 0 < t) (ha' : a' K.nV K.nE K.nT = t * a K.nV K.nE K.nT) :
487 fugacityWeight a' K * Real.exp (-(S K + Real.log t))
488 = fugacityWeight a K * Real.exp (-(S K)) := by
489 unfold fugacityWeight
490 rw [ha', neg_add, Real.exp_add, Real.exp_neg, Real.exp_neg (Real.log t),
491 Real.exp_log ht]
492 have ht0 : (t : ℝ) ≠ 0 := ht.ne'
493 have hE0 : Real.exp (S K) ≠ 0 := Real.exp_ne_zero (S K)
494 have hV0 :
495 ((Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) : ℕ) : ℝ)
496 ≠ 0 := by
497 have hpos : 0 < Nat.factorial K.nV
498 * (Nat.factorial K.nE * Nat.factorial K.nT) :=
499 Nat.mul_pos (Nat.factorial_pos _)
500 (Nat.mul_pos (Nat.factorial_pos _) (Nat.factorial_pos _))
501 exact_mod_cast hpos.ne'
502 field_simp
503
504/-- **Rebooking invariance**: a prior on (fugacity, action) presentations
505respects the bookkeeping gauge. The doubling step suffices: it generates
506the contradiction at the two-point complex. -/
507def RebookingInvariant {B : ℕ}
508 (P : (ℕ → ℕ → ℕ → ℝ) → (BoundedComplex B → ℝ) → Prop) : Prop :=
509 ∀ (a : ℕ → ℕ → ℕ → ℝ) (S : BoundedComplex B → ℝ),
510 P a S → P (fun nV nE nT => 2 * a nV nE nT) (fun K => S K + Real.log 2)
511
512/-- **R18 wall, counterexample form.** A satisfiable rebooking-invariant
513prior always admits a presentation whose sector fugacity is not identically
514one on occupied complexes: double the fugacity and absorb `log 2` into the
515action. The non-unit value is witnessed at the two-point complex. -/
516theorem R18_rebooking_invariant_admits_nonunit {B : ℕ} (hB : 2 ≤ B)
517 (P : (ℕ → ℕ → ℕ → ℝ) → (BoundedComplex B → ℝ) → Prop)
518 (hgauge : RebookingInvariant P)
519 (a₀ : ℕ → ℕ → ℕ → ℝ) (S₀ : BoundedComplex B → ℝ) (h₀ : P a₀ S₀) :
520 ∃ (a : ℕ → ℕ → ℕ → ℝ) (S : BoundedComplex B → ℝ),
521 P a S ∧ ∃ K : BoundedComplex B, a K.nV K.nE K.nT ≠ 1 := by
522 by_cases h : a₀ 2 0 0 = 1
523 · refine ⟨fun nV nE nT => 2 * a₀ nV nE nT, fun K => S₀ K + Real.log 2,
524 hgauge a₀ S₀ h₀, MeasureInvarianceNoGo.twoPointComplex B hB, ?_⟩
525 show (2 : ℝ) * a₀ 2 0 0 ≠ 1
526 rw [h]
527 norm_num
528 · exact ⟨a₀, S₀, h₀, MeasureInvarianceNoGo.twoPointComplex B hB, h⟩
529
530/-- **R18 wall, selector-impossibility form.** No satisfiable
531rebooking-invariant prior forces the Gibbs numerator: if `P` held only of
532presentations with unit fugacity on occupied complexes, the doubled
533presentation would contradict the unit value at the two-point complex. -/
534theorem R18_no_rebooking_invariant_selector {B : ℕ} (hB : 2 ≤ B)
535 (P : (ℕ → ℕ → ℕ → ℝ) → (BoundedComplex B → ℝ) → Prop)
536 (hgauge : RebookingInvariant P)
537 (hsel : ∀ (a : ℕ → ℕ → ℕ → ℝ) (S : BoundedComplex B → ℝ),
538 P a S → ∀ K : BoundedComplex B, a K.nV K.nE K.nT = 1)
539 (a₀ : ℕ → ℕ → ℕ → ℝ) (S₀ : BoundedComplex B → ℝ) (h₀ : P a₀ S₀) :
540 False := by
541 have h1 : a₀ 2 0 0 = 1 :=
542 hsel a₀ S₀ h₀ (MeasureInvarianceNoGo.twoPointComplex B hB)
543 have h2 : (2 : ℝ) * a₀ 2 0 0 = 1 :=
544 hsel _ _ (hgauge a₀ S₀ h₀) (MeasureInvarianceNoGo.twoPointComplex B hB)
545 rw [h1] at h2
546 norm_num at h2
547
548/-- **Product-visible priors**: those that ask about the physical Boltzmann
549product only. Ledger-internal candidate priors (label indifference of the
550weight, gluing of the product, insertion stationarity of the product, orbit
551accounting) all have this form, because their inputs are functions of the
552product. -/
553def ProductVisible {B : ℕ}
554 (P : (ℕ → ℕ → ℕ → ℝ) → (BoundedComplex B → ℝ) → Prop) : Prop :=
555 ∃ Q : (BoundedComplex B → ℝ) → Prop,
556 ∀ (a : ℕ → ℕ → ℕ → ℝ) (S : BoundedComplex B → ℝ),
557 P a S ↔ Q (fun K => fugacityWeight a K * Real.exp (-(S K)))
558
559/-- Every product-visible prior is rebooking-invariant: the gauge step
560preserves the product pointwise. -/
561theorem R18_product_visible_is_rebooking_invariant {B : ℕ}
562 {P : (ℕ → ℕ → ℕ → ℝ) → (BoundedComplex B → ℝ) → Prop}
563 (hP : ProductVisible P) : RebookingInvariant P := by
564 obtain ⟨Q, hQ⟩ := hP
565 intro a S h
566 rw [hQ] at h ⊢
567 have hpt : (fun K : BoundedComplex B =>
568 fugacityWeight (fun nV nE nT => 2 * a nV nE nT) K *
569 Real.exp (-(S K + Real.log 2)))
570 = (fun K : BoundedComplex B =>
571 fugacityWeight a K * Real.exp (-(S K))) := by
572 funext K
573 exact R18_rebooking_preserves_product a (fun nV nE nT => 2 * a nV nE nT)
574 2 S K (by norm_num) rfl
575 rw [hpt]
576 exact h
577
578/-- **R18 wall, ledger-internal corollary.** No satisfiable product-visible
579prior forces the Gibbs numerator. -/
580theorem R18_no_product_visible_selector {B : ℕ} (hB : 2 ≤ B)
581 (P : (ℕ → ℕ → ℕ → ℝ) → (BoundedComplex B → ℝ) → Prop)
582 (hP : ProductVisible P)
583 (hsel : ∀ (a : ℕ → ℕ → ℕ → ℝ) (S : BoundedComplex B → ℝ),
584 P a S → ∀ K : BoundedComplex B, a K.nV K.nE K.nT = 1)
585 (a₀ : ℕ → ℕ → ℕ → ℝ) (S₀ : BoundedComplex B → ℝ) (h₀ : P a₀ S₀) :
586 False :=
587 R18_no_rebooking_invariant_selector hB P
588 (R18_product_visible_is_rebooking_invariant hP) hsel a₀ S₀ h₀
589
590/-- The R18 killing measurement, typed: over every cap with a two-point
591complex, no satisfiable rebooking-invariant prior selects unit fugacity,
592and the product-visible class sits inside the rebooking-invariant class. -/
593def R18Wall : Prop :=
594 ∀ (B : ℕ), 2 ≤ B →
595 (∀ (P : (ℕ → ℕ → ℕ → ℝ) → (BoundedComplex B → ℝ) → Prop),
596 RebookingInvariant P →
597 (∀ (a : ℕ → ℕ → ℕ → ℝ) (S : BoundedComplex B → ℝ),
598 P a S → ∀ K : BoundedComplex B, a K.nV K.nE K.nT = 1) →
599 ∀ (a₀ : ℕ → ℕ → ℕ → ℝ) (S₀ : BoundedComplex B → ℝ),
600 P a₀ S₀ → False)
601 ∧ (∀ (P : (ℕ → ℕ → ℕ → ℝ) → (BoundedComplex B → ℝ) → Prop),
602 ProductVisible P → RebookingInvariant P)
603
604/-- **R18 REFUTED (scoped).** The Gibbs numerator is not forcible by any
605prior invariant under the fugacity–action booking gauge, and every prior
606that sees only the physical product weight is such a prior. -/
607theorem R18_refuted : R18Wall := by
608 intro B hB
609 exact ⟨fun P hgauge hsel a₀ S₀ h₀ =>
610 R18_no_rebooking_invariant_selector hB P hgauge hsel a₀ S₀ h₀,
611 fun P hP => R18_product_visible_is_rebooking_invariant hP⟩
612
613/-- **Vacuity guard (decoy scored).** The literal `R18` Prop is inhabitable
614with zero content, because `CorrectedMeasurePremise` packages three
615uninterpreted Props. This trivial inhabitant is recorded so the row can
616never be scored by inhabiting the package: the honest discharge of R18 is
617the wall `R18_refuted` plus the named survivor, never this witness. -/
618theorem R18_vacuity_guard : R18 :=
619 ⟨⟨True, True, True⟩, True.intro, True.intro, True.intro⟩
620
621/-- R18 row verdict. -/
622def R18Status : String := "REFUTED_OVER_REBOOKING_INVARIANT_PRIORS"
623
624/-- First attack block on the corrected target (historical; R18 closed as
625a scoped wall, so the block is superseded by `secondAttackBlock`). -/
626def firstAttackBlock : List String :=
627 ["R18", "R09", "R10", "R07", "R11"]
628
629theorem firstAttackBlock_length : firstAttackBlock.length = 5 := by
630 decide
631
632/-- Second attack block on the twice-corrected target (historical; all
633three rows resolved in the child census `UnitFugacitySelector` on
6342026-08-07). The only priors outside the R18 wall pin the action
635independently of the measure, so the surviving obligation was
636action-first: derive the ledger cost the substrate posts, with the
637fugacity booking then a convention and GCP given by R03. The child census
638rows U12 (derive `GluingLaw`) and U13 (justified asymmetry) were the
639typed sub-lanes. -/
640def secondAttackBlock : List String :=
641 ["ACTION-FIRST ledger cost derivation", "U12", "U13"]
642
643theorem secondAttackBlock_length : secondAttackBlock.length = 3 := by
644 decide
645
646/-- Third attack block (2026-08-07 fifth pass). The child census resolved
647the second block: U13 is REFUTED (scoped, no product-visible cost prior
648selects unit fugacity), and U12 is THEOREM (the ledger-counted global
649balance forces detailed balance on the birth-death chain, which forces
650the inverse-factorial gluing law; see
651`UnitFugacitySelector.globalBalance_forces_detailedBalance` and
652`equilibrium_forces_gluingLaw`). The corrected measure premise is now
653contentfully inhabited by the child's `equilibriumPrior`
654(`U14_assumedRequired_inhabited`), superseding the `True`-package decoy
655this file pre-scored in `R18_vacuity_guard`. What survives of
656 "action-first" is exactly one organ: derive the equilibrium premise
657itself (the physical weight IS a stationary state of the ledger-counted
658recognition dynamics) from recognition law, the child's U15. The chain
659is forced and the late-time state is its unique output; under the
660parameter-free identification rule (2026-08-08) that reading is adopted
661as MODEL in `UnitFugacitySelector.U15_identification_adopted`. -/
662def thirdAttackBlock : List String := []
663
664theorem thirdAttackBlock_length : thirdAttackBlock.length = 0 := by
665 decide
666
667/-- Public name for the next necessary-reasons block. -/
668def nextAttackBlock : List String := thirdAttackBlock
669
670theorem nextAttackBlock_length : nextAttackBlock.length = 0 := by
671 decide
672
673/-- R18 block receipt: the wall is theorem, the literal target is vacuously
674inhabitable with the decoy scored, and the bookkeeping syncs. -/
675theorem R18_block_certified :
676 R18Wall ∧ R18 ∧ correctedFloorPlans.length = 5 ∧
677 nextAttackBlock.length = 0 ∧
678 R18Status = "REFUTED_OVER_REBOOKING_INVARIANT_PRIORS" :=
679 ⟨R18_refuted, R18_vacuity_guard, correctedFloorPlans_length,
680 nextAttackBlock_length, rfl⟩
681
682/-- The existing corrected floor plan is also exposed as the requested stub
683surface for later rows. -/
684def correctedFloorPlansStub : List CorrectedFloorPlan :=
685 correctedFloorPlans
686
687theorem correctedFloorPlansStub_length :
688 correctedFloorPlansStub.length = 5 := by
689 decide
690
691/- There is intentionally no composite certificate here. The banked rows
692remain individually inspectable, and `AssumedRequired` is not closed: its
693only inhabitant is the scored vacuity decoy `R18_vacuity_guard`. -/
694
695end
696
697#print axioms R18_rebooking_preserves_product
698#print axioms R18_rebooking_invariant_admits_nonunit
699#print axioms R18_no_rebooking_invariant_selector
700#print axioms R18_product_visible_is_rebooking_invariant
701#print axioms R18_no_product_visible_selector
702#print axioms R18_refuted
703#print axioms R18_vacuity_guard
704#print axioms R18_block_certified
705
706end GaugeCountingInevitableReasons
707end SevenGaps
708end Gravity
709end IndisputableMonolith
710