IndisputableMonolith.Gravity.SevenGaps.Gap2PostingLayerFloor

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2DynamicsKindRule
   2
   3/-!
   4# Gap 2, sixth arc: the pinned-carrier floor and the uniqueness wall
   5
   6Track A1.2 of `QG/plans/QG_Full_Theory_Completion_20260729.html` asks whether
   7`GaugeCountingPrinciple` can be derived from substrate structure richer than counting at the
   8posting layer.  The committed answer is no, and this module makes the no precise with kernel
   9content, after a referee read forced the honest version of it.  The answer has three parts:
  10what the pinned carrier provably contains, the uniqueness theorem that does the real
  11excluding, and the one route nothing excludes, which is the premise itself.
  12
  13**Part one: the pinned carrier, by design.**  `GaugeHistoryMeasure` builds counted histories
  14by pinning every history's dual-entry state to `balancedZeroState`, so that counted histories
  15are one per complex and the count does not inflate; the unpinned `PostedBoundedHistory` still
  16carries a free `DualEntryStrainState`.  §1 and §2 kernel-check what that design choice leaves:
  17on `CanonicalHistory` the count is exactly the complex count
  18(`canonical_count_eq_complex_count`), and every state-factored weight evaluated there is a
  19function of the complex alone (`state_factored_weight_is_complex_function`).  These are
  20theorems about the pinned carrier, not discoveries that the posting layer holds nothing.  The
  21free state exists one type up and the pin discards it; a derivation that routes through the
  22pinned counted carrier has only the complex to work with, and one that does not is in part
  23three.
  24
  25**Part two: the uniqueness wall, which was already in the library.**  The theorem that
  26actually excludes a derivation is `Gap2GaugeVolume.invariant_weight_gives_measure_iff`: among
  27relabeling-invariant labeled weights on complexes, the gauge-counting principle holds of the
  28class mass if and only if the weight is exactly the Gibbs weight.  So with relabeling
  29invariance fixed, demanding the principle forces the weight to be the very Gibbs form whose
  30selection *is* the premise.  No relabeling-invariant enrichment can derive the principle from
  31anything, because invariance plus the principle leaves no degree of freedom.  The same wall
  32stands at the cost layer: `Gap2PostingCostDerivation.equivariant_posts_mu_iff_numerator_one`
  33says an equivariant letter cost posts `mu` exactly when its Boltzmann numerator is identically
  34one, so no equivariant cost contributes a factor either.
  35
  36**Part three: the routes the wall does not touch, named exactly.**  Two routes are untouched
  37by §3, and the boundary claim is scoped to the weight-based classes the cited theorems
  38quantify over.  First, *premise-level* justifications of the Gibbs weight from a more basic
  39symmetry principle (indifference, exchangeability, maximum entropy): the wall forces any
  40relabeling-invariant weight satisfying the principle to *be* Gibbs, but says nothing about
  41deriving the Gibbs weight itself from something prior; that would be a reduction of the
  42premise, not a derivation from richer structure, and nothing here or in the library supplies
  43one.  Second, label-asymmetric structure, a cost or weight that distinguishes between
  44labelings of one complex: §4 exhibits one (`vertexIndexCost`, which charges by vertex index,
  45is not equivariant), so this route is inhabited.  A label-asymmetric derivation of the
  46principle would still have to *justify* label indifference rather than assume it, and label
  47indifference, each labeling counted once, equivalently the Gibbs weight `1/(nV! nE! nT!)`, is
  48the premise the measure rests on.  The library's cost arcs name the asymmetric case as the
  49non-equivariant case, which remains open.
  50
  51**The A1.2 verdict.**  On the pinned carrier there is nothing richer than the complex to
  52derive from.  For relabeling-invariant enrichments and equivariant posting costs, uniqueness
  53excludes every derivation of the principle from anything but the principle.  The untouched
  54routes are premise-level justifications of label indifference, symmetric or asymmetric; none
  55is supplied.  Combined with the fifth arc (the dynamics forces no charge restriction), the
  56measure now rests on one named physical premise, label indifference, and the frontier that
  57could discharge it is a derivation from a prior symmetry principle or from the actual posting
  58schedule nature executes, the same schedule the fifth arc named.
  59
  60## Honest tagging
  61
  62§1, §2 and §4 are THEOREM (kernel-checked in this module).  §3 re-stands existing THEOREMs
  63under names that say what they exclude here.  The `1/(nV! nE! nT!)` gauge volume is THEOREM
  64(`pairCount_eq_factorials`), and orbit-stabilizer accounting is THEOREM
  65(`orbitCard_mul_autCard`), recorded in §5 so the one factor the measure carries beyond
  66counting is visible as a theorem rather than a premise.
  67-/
  68
  69namespace IndisputableMonolith
  70namespace Gravity
  71namespace SevenGaps
  72namespace Gap2PostingLayerFloor
  73
  74open PathSumMeasure ExactShellGaugePreflight Gap2GaugeVolume Gap2GluingDerivation
  75open GaugeHistoryMeasure Gap2SizeBlindnessReach Gap2PostingCostDerivation Gap2KindRule
  76open Gap2LatticeKindRule Gap2DynamicsKindRule
  77open Analysis.RecognitionDualEntryEnrichment4D
  78
  79noncomputable section
  80
  81/-! ## §1. On the pinned carrier, counting is complex counting
  82
  83The pinned carrier `CanonicalHistory` is a *design choice* of the measure construction: the
  84state is fixed to `balancedZeroState` so counted histories are one per complex.  The collapse
  85this produces was first recorded as `Gap2MeasureStatusBinding.historyCarrier_equiv_plainCarrier`;
  86this section kernel-checks its cardinal form, which is the form the floor needs. -/
  87
  88/-- **THEOREM (pinned counting is complex counting).**  The number of pinned bounded histories
  89at bound `B` equals the number of bounded complexes at bound `B`.  Content: after the design
  90pin `state = balancedZeroState`, the counted history carries exactly the complex; the
  91dual-entry enrichment contributes no factor to the count.  Scope: this is a theorem about
  92`CanonicalHistory`, not about the unpinned `PostedBoundedHistory`, which still carries a free
  93state. -/
  94theorem canonical_count_eq_complex_count (B : ℕ) :
  95    Nat.card (GaugeHistoryMeasure.CanonicalHistory B) = Nat.card (BoundedComplex B) := by
  96  exact Nat.card_congr (GaugeHistoryMeasure.CanonicalHistory.equivUnderlying)
  97
  98/-! ## §2. On the pinned carrier, state-factored weights are functions of the complex -/
  99
 100/-- **THEOREM (state-factored weights collapse on the pinned carrier).**  If a weight on
 101histories factors as `F K s` (complex, state), then evaluated on the pinned carrier it equals
 102`g K` for a function of the complex alone: `F CH.underlying CH.H.state = g CH.underlying`,
 103because the pin forces `CH.H.state = balancedZeroState _`.  Scope: the collapse happens *on
 104`CanonicalHistory`*, where `state_canonical` pins `s`; it says nothing about weights on the
 105unpinned carrier.  Any derivation of the counting principle that routes through the pinned
 106counted carrier therefore receives nothing state-dependent from the posting layer; what it can
 107receive from the unpinned carrier is §4's question. -/
 108theorem state_factored_weight_is_complex_function {B : ℕ}
 109    (F : ∀ (K : BoundedComplex B), DualEntryStrainState (PostingAlphabet K) → ℝ) :
 110    ∃ g : BoundedComplex B → ℝ, ∀ CH : GaugeHistoryMeasure.CanonicalHistory B,
 111      F CH.underlying CH.H.state = g CH.underlying := by
 112  refine ⟨fun K => F K (balancedZeroState _), fun CH => ?_⟩
 113  exact congrArg (F CH.underlying) CH.state_canonical
 114
 115/-- **THEOREM (the pinned fiber is constant).**  Two pinned histories over the same underlying
 116complex are equal: the posted history carries only the complex and the state, the states are
 117both pinned, and the pinning proofs agree by proof irrelevance.  So the fiber of the pinning
 118over a complex is a subsingleton.  Scope: constancy holds because the pin makes it hold, which
 119is the design of `CanonicalHistory`, not a property discovered about the posting layer. -/
 120theorem canonical_state_fiber_constant {B : ℕ}
 121    (CH₁ CH₂ : GaugeHistoryMeasure.CanonicalHistory B)
 122    (h : CH₁.underlying = CH₂.underlying) : CH₁ = CH₂ := by
 123  obtain ⟨⟨K₁, s₁⟩, hc₁⟩ := CH₁
 124  obtain ⟨⟨K₂, s₂⟩, hc₂⟩ := CH₂
 125  change K₁ = K₂ at h
 126  subst h
 127  have hs : s₁ = s₂ := hc₁.trans hc₂.symm
 128  subst hs
 129  rfl
 130
 131/-! ## §3. The uniqueness wall: invariant enrichments cannot derive the principle
 132
 133The theorems in this section are not new; they are the load-bearing exclusions, re-stood under
 134names that say what they exclude for this arc.  The referee's point is accepted: §1 and §2
 135alone would only show the pinned carrier is empty, leaving every unpinned route open.  These
 136two theorems close the relabeling-invariant and equivariant routes outright. -/
 137
 138/-- **THEOREM (the uniqueness wall, Gap2GaugeVolume re-stood).**  Among relabeling-invariant
 139labeled weights on complexes, the gauge-counting principle holds of the class mass if and only
 140if the weight is the Gibbs weight pointwise.  Consequence for the derivation demand: with
 141relabeling invariance fixed, asking for the principle leaves no degree of freedom, so no
 142invariant enrichment can derive the principle from anything more primitive; the principle and
 143the Gibbs premise are the same assumption stated twice. -/
 144theorem invariant_enrichment_unique_gibbs (B : ℕ) (w : BoundedComplex B → ℝ)
 145    (hinv : ∀ K K', Equivalent K K' → w K = w K') :
 146    MeasureSubstrateBlocker.GaugeCountingPrinciple (classMass w) ↔
 147      ∀ K : BoundedComplex B, w K = gibbsWeight K :=
 148  invariant_weight_gives_measure_iff w hinv
 149
 150/-- **THEOREM (the uniqueness wall at the cost layer, Gap2PostingCostDerivation re-stood).**
 151An equivariant letter cost posts `mu` at bound `B` exactly when its Boltzmann numerator is
 152identically one.  Consequence for the derivation demand: no equivariant posting cost can
 153contribute a factor to the measure, whatever premise picks the cost out; asking an equivariant
 154cost for `mu` is asking for the Gibbs weight back.  The non-equivariant case is not covered
 155here and is §4. -/
 156theorem equivariant_cost_contributes_no_factor {c : LetterCost} (hc : Equivariant c) (B : ℕ) :
 157    (∀ K : BoundedComplex B,
 158        classMass (postedWeight c B) (Quotient.mk (relabelSetoid B) K) = mu K)
 159      ↔ ∀ K : BoundedComplex B, Real.exp (-(historyCost c B K)) = 1 :=
 160  equivariant_posts_mu_iff_numerator_one hc B
 161
 162/-! ## §4. The asymmetric route the wall does not touch, exhibited
 163
 164The wall of §3 quantifies over relabeling-invariant weights and equivariant costs.  Its
 165complement within the letter-cost class is the label-asymmetric costs, and for the no-go to
 166be honest about its own boundary that complement must be shown inhabited: there must exist a
 167letter cost that is *not* equivariant.  This section exhibits the simplest one, a cost that
 168reads the vertex label itself, and refutes its equivariance with a vertex swap on a complex
 169whose incidence conditions are vacuous.  A second untouched route, premise-level derivations
 170of the Gibbs weight from symmetric first principles, is not a letter-cost class at all and is
 171disclosed in the header rather than exhibited. -/
 172
 173/-- Two isolated vertices, no edges or tetrahedra: sizes `(2,0,0)`.  Every vertex bijection is
 174a relabeling of this complex because the incidence conditions are vacuous, which makes it the
 175cheapest place to exhibit label-asymmetry. -/
 176def twoIsoVerts : BoundedComplex 2 where
 177  nV := 2
 178  nE := 0
 179  nT := 0
 180  hV := le_refl 2
 181  hE := Nat.zero_le 2
 182  hT := Nat.zero_le 2
 183  edgeVerts := fun e => e.elim0
 184  tetVerts := fun t => t.elim0
 185
 186/-- The vertex swap as a self-relabeling of `twoIsoVerts`.  The edge and tet conditions are
 187vacuous (`Fin 0`), so the swap needs no incidence compatibility. -/
 188def twoIsoVertsSwap : Relabel twoIsoVerts twoIsoVerts where
 189  vEquiv := Equiv.swap ⟨0, by decide⟩ ⟨1, by decide⟩
 190  eEquiv := Equiv.refl _
 191  tEquiv := Equiv.refl _
 192  edge_comm := fun e => e.elim0
 193  tet_comm := fun t => t.elim0
 194
 195/-- The vertex-index cost: charge each vertex letter its index as a real, charge edge and
 196tetrahedron letters nothing.  It reads the label, so it is the simplest letter cost that is
 197not gauge-equivariant. -/
 198def vertexIndexCost : LetterCost := fun _ _ a =>
 199  match a with
 200  | Sum.inl v => ((v : ℕ) : ℝ)
 201  | _ => 0
 202
 203/-- **THEOREM (label-asymmetric costs exist).**  The vertex-index cost is not equivariant:
 204transporting vertex letter `0` along the swap gives vertex letter `1`, whose cost is `1 ≠ 0`.
 205So the class §3 does not cover is inhabited, and the one route the wall leaves open, a
 206label-asymmetric derivation of label indifference, is a route through real objects, not
 207through an empty type. -/
 208theorem vertexIndexCost_not_equivariant : ¬ Equivariant vertexIndexCost := by
 209  intro h
 210  have h1 := h 2 twoIsoVerts twoIsoVerts twoIsoVertsSwap (Sum.inl ⟨0, by decide⟩)
 211  have htransport : postingAlphEquiv twoIsoVertsSwap.vEquiv twoIsoVertsSwap.eEquiv
 212      twoIsoVertsSwap.tEquiv (Sum.inl ⟨0, by decide⟩) = Sum.inl (⟨1, by decide⟩ : Fin 2) := by
 213    show Sum.inl (Equiv.swap ⟨0, by decide⟩ (⟨1, by decide⟩ : Fin 2) ⟨0, by decide⟩) = _
 214    rw [Equiv.swap_apply_left]
 215  rw [htransport] at h1
 216  norm_num [vertexIndexCost] at h1
 217
 218/-- **THEOREM (the asymmetric case is inhabited).**  There exists a letter cost that is not
 219gauge-equivariant.  This is the honesty clause of the no-go: within the letter-cost class, the
 220structure the uniqueness wall does not cover is label-asymmetric structure, and such structure
 221exists.  What does not currently exist is a label-asymmetric derivation of label indifference;
 222that is the named open case.  The second untouched route, premise-level derivations of the
 223Gibbs weight from symmetric first principles, is outside the letter-cost class and is
 224disclosed in the module header. -/
 225theorem label_asymmetric_structure_exists : ∃ c : LetterCost, ¬ Equivariant c :=
 226  ⟨vertexIndexCost, vertexIndexCost_not_equivariant⟩
 227
 228/-! ## §5. The one factor beyond counting, as a theorem -/
 229
 230/-- **THEOREM (orbit-stabilizer, re-stood).**  The gauge orbit card of a complex times the
 231cardinality of its automorphism group is the label count `nV! * (nE! * nT!)`.  Recorded here
 232so the accounting the measure relies on is visible as a theorem of the library, not a premise:
 233the label count and the orbit count are both computed, and what the measure selects among the
 234results is the premise named in §6. -/
 235theorem irreducible_input_is_orbit_stabilizer {B : ℕ} (K : BoundedComplex B) :
 236    gaugeOrbitCard K * Nat.card (Aut K)
 237      = K.nV.factorial * (K.nE.factorial * K.nT.factorial) :=
 238  Gap2GaugeVolume.orbitCard_mul_autCard K
 239
 240/-! ## §6. The floor, the verdict, and the index -/
 241
 242/-- **THEOREM (the posting-layer floor, reframed).**  The five-part verdict of this arc at
 243bound `B`:
 244
 2451.  On the pinned carrier, counting is complex counting.
 2462.  On the pinned carrier, every state-factored weight is a function of the complex.
 2473.  Among relabeling-invariant labeled weights, the counting principle forces the Gibbs
 248    weight, so no invariant enrichment derives the principle from anything more primitive.
 2494.  No equivariant posting cost contributes a factor to the measure.
 2505.  Label-asymmetric costs exist: the asymmetric route the wall does not touch is inhabited.
 251
 252What the conjunction does not contain: any claim that the posting layer as a whole holds
 253nothing (the unpinned carrier carries a free state, and the fifth arc showed the dynamics
 254imposes no charge restriction); any claim that premise-level derivations of the Gibbs weight
 255from symmetric first principles (indifference, exchangeability, maximum entropy) are excluded,
 256because they are not and the wall is silent on premise reduction; any claim that the open
 257routes are closed (a label-asymmetric derivation of label indifference is neither exhibited
 258nor refuted here); and any completeness claim beyond the weight-based classes the cited
 259theorems quantify over.  The measure's remaining premise is exactly label indifference. -/
 260theorem posting_layer_floor (B : ℕ) :
 261    (Nat.card (GaugeHistoryMeasure.CanonicalHistory B) = Nat.card (BoundedComplex B)) ∧
 262    (∀ F : ∀ (K : BoundedComplex B), DualEntryStrainState (PostingAlphabet K) → ℝ,
 263      ∃ g : BoundedComplex B → ℝ, ∀ CH : GaugeHistoryMeasure.CanonicalHistory B,
 264        F CH.underlying CH.H.state = g CH.underlying) ∧
 265    (∀ w : BoundedComplex B → ℝ, (∀ K K', Equivalent K K' → w K = w K') →
 266      (MeasureSubstrateBlocker.GaugeCountingPrinciple (classMass w) ↔
 267        ∀ K : BoundedComplex B, w K = gibbsWeight K)) ∧
 268    (∀ c : LetterCost, Equivariant c →
 269      ((∀ K : BoundedComplex B,
 270          classMass (postedWeight c B) (Quotient.mk (relabelSetoid B) K) = mu K) ↔
 271        ∀ K : BoundedComplex B, Real.exp (-(historyCost c B K)) = 1)) ∧
 272    (∃ c : LetterCost, ¬ Equivariant c) :=
 273  ⟨canonical_count_eq_complex_count B,
 274   fun F => ⟨fun K => F K (balancedZeroState _),
 275     fun CH => congrArg (F CH.underlying) CH.state_canonical⟩,
 276   invariant_enrichment_unique_gibbs B,
 277   fun _c hc => equivariant_cost_contributes_no_factor hc B,
 278   label_asymmetric_structure_exists⟩
 279
 280/-- The index of the sixth arc.  Every flag is a Prop proved or refuted in `index_audit` from
 281the theorems of this module; nothing is assigned by fiat.  `premise_named_at` is documentation,
 282a pointer to where the measure's one remaining premise lives, and the audit does not check it
 283because it is a name, not a claim. -/
 284structure Index where
 285  pinned_carrier_count_is_complex_count : Prop
 286  pinned_state_fiber_is_constant : Prop
 287  invariant_enrichment_unique_gibbs : Prop
 288  equivariant_cost_contributes_no_factor : Prop
 289  label_asymmetric_structure_exists : Prop
 290  premise_named_at : String
 291
 292def index : Index where
 293  pinned_carrier_count_is_complex_count :=
 294    ∀ B : ℕ, Nat.card (GaugeHistoryMeasure.CanonicalHistory B) = Nat.card (BoundedComplex B)
 295  pinned_state_fiber_is_constant :=
 296    ∀ {B : ℕ} (CH₁ CH₂ : GaugeHistoryMeasure.CanonicalHistory B),
 297      CH₁.underlying = CH₂.underlying → CH₁ = CH₂
 298  invariant_enrichment_unique_gibbs :=
 299    ∀ (B : ℕ) (w : BoundedComplex B → ℝ), (∀ K K', Equivalent K K' → w K = w K') →
 300      (MeasureSubstrateBlocker.GaugeCountingPrinciple (classMass w) ↔
 301        ∀ K : BoundedComplex B, w K = gibbsWeight K)
 302  equivariant_cost_contributes_no_factor :=
 303    ∀ (c : LetterCost), Equivariant c → ∀ B : ℕ,
 304      ((∀ K : BoundedComplex B,
 305          classMass (postedWeight c B) (Quotient.mk (relabelSetoid B) K) = mu K) ↔
 306        ∀ K : BoundedComplex B, Real.exp (-(historyCost c B K)) = 1)
 307  label_asymmetric_structure_exists := ∃ c : LetterCost, ¬ Equivariant c
 308  premise_named_at := "label indifference (Gibbs weight 1/(nV! nE! nT!)); only a label-asymmetric derivation could discharge it"
 309
 310/-- The audit pinning every index flag to its theorem. -/
 311theorem index_audit : index.pinned_carrier_count_is_complex_count ∧
 312    index.pinned_state_fiber_is_constant ∧
 313    index.invariant_enrichment_unique_gibbs ∧
 314    index.equivariant_cost_contributes_no_factor ∧
 315    index.label_asymmetric_structure_exists := by
 316  refine ⟨?_, ?_, ?_, ?_, ?_⟩
 317  · intro B
 318    exact canonical_count_eq_complex_count B
 319  · intro B CH₁ CH₂ h
 320    exact canonical_state_fiber_constant CH₁ CH₂ h
 321  · intro B w hinv
 322    exact invariant_enrichment_unique_gibbs B w hinv
 323  · intro c hc B
 324    exact equivariant_cost_contributes_no_factor hc B
 325  · exact label_asymmetric_structure_exists
 326
 327end
 328
 329#print axioms canonical_count_eq_complex_count
 330#print axioms state_factored_weight_is_complex_function
 331#print axioms canonical_state_fiber_constant
 332#print axioms invariant_enrichment_unique_gibbs
 333#print axioms equivariant_cost_contributes_no_factor
 334#print axioms vertexIndexCost_not_equivariant
 335#print axioms label_asymmetric_structure_exists
 336#print axioms irreducible_input_is_orbit_stabilizer
 337#print axioms posting_layer_floor
 338#print axioms index_audit
 339
 340end Gap2PostingLayerFloor
 341end SevenGaps
 342end Gravity
 343end IndisputableMonolith
 344