IndisputableMonolith.Gravity.SevenGaps.Gap2KindRule

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2PostingCostDerivation
   2import IndisputableMonolith.Gravity.Analysis.RecognitionDualEntryEnrichment4D
   3
   4/-!
   5# Gap 2, third arc: does the letter-cost space force the kind rule?
   6
   7The residual left by `Gap2PostingCostDerivation` is the kind clause: a letter's cost is a
   8function of its kind and of nothing else, with the same three reals at every complex.  That
   9module derived premise (i) and then the measure from a posted kind-only cost normalized at the
  10atoms, with no gluing premise, and it flagged `incidence_silence_derived := false`: whether the
  11substrate forces the kind rule was left open.  This module settles what can be settled in Lean
  12about that, at the layer where it is statable, and the answer has three parts, each of which is
  13a theorem rather than a reading.  **The scope is the letter-cost space, and the header says so
  14because a referee rightly objected when an earlier version asked "does the ledger force it":
  15the ledger's dual-entry lattice is one layer below `LetterCost`, and whether THAT forces the
  16rule is the open successor, not what is settled here.**
  17
  18## T1, the kind rule fails in the letter-cost space, and not only by incidence
  19
  20`incidenceCost` charges `t` for a proper edge letter and nothing for any other letter.  It is a
  21well-formed `LetterCost`, gauge-equivariant (`incidenceCost_equivariant`), not kind-only
  22(`incidenceCost_not_kindOnly`), and its posted weight is not size-blind
  23(`incidencePosting_not_sizeBlind`).  So the letter-cost space admits incidence-aware equivariant
  24charging rules that break the kind clause, and nothing in the definition of `LetterCost`
  25excludes them.
  26
  27The vertex count read as a vertex letter charge (`pairCost`) is equivariant
  28(`pairCost_equivariant`), not kind-only (`pairCost_not_kindOnly`), and size-blind at the level of
  29totals (`pairCost_costSizeBlind`).  So incidence is not the only way to fail the kind rule: a
  30non-constant counts-only charge fails it too.  Said with the scope a referee required: this is
  31one exhibited witness, not a comparison of countermodel sets, and "every size-function letter
  32charge fails" would be false since a constant size-function is kind-only.  Whether "reads sizes"
  33and "reads incidence" are independent is a definitional matter of which fields of `K` a charge
  34inspects, not a theorem here.
  35
  36## T2, where the exclusion lives: the measure formula, within this framework
  37
  38`GaugeHistoryMeasure` pins its counted histories to the balanced zero dual-entry state
  39(`CanonicalHistory.state_canonical`), and the tempting reading is that this pinning is what
  40excludes the countermodel.  Within the framework as it stands it does not, and the reason is
  41the type of `LetterCost`, which takes a complex and an alphabet letter and no dual-entry state.
  42The theorem `letter_cost_is_silent_on_the_state_space` is an `rfl` projection recording exactly
  43that, and its docstring now says what it cannot say: a cost notion defined on a state-bearing
  44carrier could depend on the state, and nothing here rules that out.  Inside the current cost
  45API, though, the pinning acts on histories and a cost is not a history, so the pinning cannot be
  46what admits or excludes a cost.  What excludes the countermodel's weight from the measure, in
  47this framework, is the measure formula: the class mass of the incidence posting at the
  48two-bridge class is `exp(-2t)/|Aut|`, not `1/|Aut|` (`countermodel_weight_classMass_ne_mu`),
  49because the Boltzmann numerator is not identically one while the gauge divisor is the same for
  50every invariant weight.
  51
  52The pinning's role is therefore upstream of the cost layer entirely: it makes the counted
  53histories countable (one per labeled complex, by `CanonicalHistory.fiber_unique`), which is what
  54lets the orbit count be finite and equal to the labeled-complex orbit count.  That is a counting
  55normalization, not a charge selection.
  56
  57## T3, the named premise, and what it costs
  58
  59Since the kind rule is not forced, the premise that closes the derivation is named:
  60`ChargesCountsOnly`, that a letter's charge is a function of the three counts and of the letter's
  61kind.  It gives the per-complex totals form with count-dependent rates
  62(`chargesCountsOnly_kindTotals_perComplex`), which is NOT the second arc's `FixedKindTotals`:
  63those rates are three fixed reals across all complexes, and the difference is `pairCost`, which
  64is counts-only with vertex rate `nV - 1` and so satisfies the new premise but not the fixed one.
  65The global kind rule is the special case where the three count functions are constant, and that
  66special case is what the atom normalizations then pin to zero.  **The premise is an authored
  67restriction on `LetterCost`, not a constraint the alphabet forces**: the alphabet's letters are
  68indexed, `indexCost` reads that index and is excluded by the premise, so the premise forbids
  69data the alphabet does carry.  What recommends it is that it is statable purely in counts and
  70kinds, that it is strictly weaker than kind-only (one-way witness `pairCost`; the converse
  71direction `KindOnly → ChargesCountsOnly` is immediate and not stated in this module), and that
  72the normalizations lift it from count-dependent rates to zero.  The physical content, said in
  73one sentence: a posting's charge may know how many cells of each kind the complex has, and which
  74kind the posting is, and nothing else.
  75
  76## What this arc does not settle
  77
  78Whether the ledger, at the dual-entry layer below `LetterCost`, forces `ChargesCountsOnly` is
  79open and is the honest successor question.  This arc showed the answer cannot come from the
  80posting alphabet's own structure, because the alphabet does not carry the dual-entry state and
  81the current cost API cannot see it.  The successor question is whether the dual-entry lattice
  82itself, the integer columns with unit flux, forces the charge to be counts-only, and that is a
  83question about `DualEntryStrainState`, not about `PostingAlphabet`.
  84-/
  85
  86namespace IndisputableMonolith
  87namespace Gravity
  88namespace SevenGaps
  89namespace Gap2KindRule
  90
  91open PathSumMeasure ExactShellGaugePreflight Gap2GaugeVolume Gap2GluingDerivation
  92open GaugeHistoryMeasure Gap2SizeBlindnessReach Gap2PostingCostDerivation
  93open Analysis.RecognitionDualEntryEnrichment4D
  94
  95noncomputable section
  96
  97/-! ## §1. T1: the countermodel needs no incidence; the vertex count suffices -/
  98
  99/-- The vertex charge of `pairCost` at a transported vertex letter: the transport of a vertex
 100letter is a vertex letter, and `pairCost` there reads the target's vertex count.  Stated
 101directly rather than by `cases` on the transported letter, which leaves a dependent match
 102`simp` will not close. -/
 103theorem pairCost_equivariant : Equivariant pairCost := by
 104  intro B K K' r a
 105  have hnv : K'.nV = K.nV := by
 106    have h : K.nV = K'.nV := by
 107      simpa using
 108        (Fintype.card_eq.mpr ⟨r.vEquiv⟩ : Fintype.card (Fin K.nV) = Fintype.card (Fin K'.nV))
 109    exact h.symm
 110  cases a with
 111  | inl v =>
 112    show (K'.nV : ℝ) - 1 = (K.nV : ℝ) - 1
 113    rw [hnv]
 114  | inr rest =>
 115    cases rest with
 116    | inl e => rfl
 117    | inr t => rfl
 118
 119/-- The one-vertex complex, the vertex atom (sizes (1,0,0)). -/
 120def oneVertex : BoundedComplex 1 where
 121  nV := 1
 122  nE := 0
 123  nT := 0
 124  hV := le_refl 1
 125  hE := Nat.zero_le 1
 126  hT := Nat.zero_le 1
 127  edgeVerts := fun e => e.elim0
 128  tetVerts := fun t => t.elim0
 129
 130/-- **THEOREM (the vertex-count charge is not kind-only).**  The charge is `↑nV - 1`, which is
 131`1` at the two-vertex complex and `0` at the one-vertex complex, so no single vertex rate
 132matches both.  The kind rule demands one real for every complex, and the count charge varies
 133with the count.  Note the two-vertex complex alone does not separate anything (the charge is
 134uniform over its two letters); the separation is across sizes. -/
 135theorem pairCost_not_kindOnly : ¬ KindOnly pairCost := by
 136  rintro ⟨cV, cE, cT, h⟩
 137  obtain ⟨hV, -, -⟩ := h 2 twoLoops
 138  obtain ⟨hV1, -, -⟩ := h 1 oneVertex
 139  have h2 := hV ⟨0, by decide⟩
 140  have h1 := hV1 ⟨0, by decide⟩
 141  have h2' : (1 : ℝ) = cV := by
 142    have := h2
 143    simp only [pairCost, twoLoops] at this
 144    norm_num at this
 145    exact this
 146  have h1' : (0 : ℝ) = cV := by
 147    have := h1
 148    simp only [pairCost, oneVertex] at this
 149    norm_num at this
 150    exact this
 151  rw [← h1'] at h2'
 152  norm_num at h2'
 153
 154/-- **THEOREM (the vertex-count charge is size-blind at the level of totals).**  The history
 155cost is `nV(nV-1)`, a function of the counts.  This is the second arc's
 156`historyCost_pairCost`, restated as `CostSizeBlind`. -/
 157theorem pairCost_costSizeBlind : CostSizeBlind pairCost := by
 158  intro B B' K L hv he ht
 159  rw [historyCost_pairCost, historyCost_pairCost, hv]
 160
 161/-- **THEOREM (the kind rule fails without any incidence).**  A failure of the kind clause by
 162counting rather than by incidence exists and is equivariant.  This is T1's sharpened verdict,
 163and its scope is stated exactly: one exhibited witness, `pairCost`.  What the theorem does not
 164contain, because the conjunction does not say it, is the English gloss that the countermodel
 165space is "strictly larger than the incidence family" or that it contains "every size-function
 166letter charge".  The first is a comparison of sets this module never defines, and the second is
 167false (a constant size-function is kind-only).  What is true and what the witness shows is that
 168a non-constant counts-only charge can fail the kind rule, so incidence is not the only way to
 169fail it.  Whether "reads sizes" and "reads incidence" are independent is a definitional matter
 170of which fields of `K` a charge inspects, not a theorem here. -/
 171theorem kind_rule_fails_by_counting :
 172    Equivariant pairCost ∧ ¬ KindOnly pairCost ∧ CostSizeBlind pairCost :=
 173  ⟨pairCost_equivariant, pairCost_not_kindOnly, pairCost_costSizeBlind⟩
 174
 175/-- **THEOREM (the kind rule fails by incidence too).**  The second arc's countermodel,
 176restated for comparison.  The two failures are independent: `pairCost` is size-blind and
 177`incidenceCost` is not; `incidenceCost` reads incidence and `pairCost` does not. -/
 178theorem kind_rule_fails_by_incidence (t : ℝ) (ht : t ≠ 0) :
 179    Equivariant (incidenceCost t) ∧ ¬ KindOnly (incidenceCost t) ∧
 180      ¬ SizeBlind (postedWeight (incidenceCost t)) :=
 181  ⟨incidenceCost_equivariant t, incidenceCost_not_kindOnly ht,
 182    incidencePosting_not_sizeBlind ht⟩
 183
 184/-! ## §2. T2: the exclusion lives in the measure formula, not the pinning -/
 185
 186/-- **THEOREM (a `LetterCost`, as defined, takes no state).**  `PostedBoundedHistory.mk K S`
 187projects to `K` under `.K`, and a `LetterCost` is a function of a complex and an alphabet
 188letter, so two posted histories on the same complex with different dual-entry states give the
 189same letter charge.  The proof is `rfl` and the statement is a projection: it says the current
 190cost API has no state argument, and nothing more.  What it does NOT say, because a type cannot
 191say it, is that no cost notion could ever depend on the state; a cost defined on
 192`PostedBoundedHistory` itself, rather than on `BoundedComplex`, could.  Within the framework as
 193it stands, though, the `state_canonical` pinning acts on histories and a cost is not a history,
 194so the pinning cannot be what admits or excludes a cost.  That framework-internal conclusion is
 195the T2 answer, and this theorem states its scope rather than leaving the stronger reading. -/
 196theorem letter_cost_is_silent_on_the_state_space (c : LetterCost) (B : ℕ)
 197    (K : BoundedComplex B) (S₁ S₂ : DualEntryStrainState (PostingAlphabet K))
 198    (a : PostingAlphabet K) :
 199    c B (PostedBoundedHistory.mk K S₁).K a = c B (PostedBoundedHistory.mk K S₂).K a := rfl
 200
 201/-- **THEOREM (the history cost is state-independent, same scope).**  The same projection at
 202the level of the total charge, with the same limit: about the current `LetterCost` API, not
 203about every cost notion one could define on a state-bearing carrier. -/
 204theorem history_cost_is_silent_on_the_state_space (c : LetterCost) (B : ℕ)
 205    (K : BoundedComplex B) (S₁ S₂ : DualEntryStrainState (PostingAlphabet K)) :
 206    historyCost c B (PostedBoundedHistory.mk K S₁).K
 207      = historyCost c B (PostedBoundedHistory.mk K S₂).K := rfl
 208
 209/-- **THEOREM (the measure formula is what excludes the escape).**  The class mass of the
 210incidence posting at the two-bridge class is `exp(-2t)` over the automorphism count, and for
 211`t ≠ 0` that is not the measure value `1/|Aut|`.  Every invariant weight shares the same gauge
 212divisor, so the difference is entirely in the Boltzmann numerator, which is not identically
 213one.  This restates the second arc's `incidencePosting_classMass_ne_mu` as the answer to T2's
 214question: the escape is excluded by the gauge-divisor formula for the class mass, not by any
 215canonicality condition on a state. -/
 216theorem countermodel_weight_classMass_ne_mu (t : ℝ) (ht : t ≠ 0) :
 217    classMass (postedWeight (incidenceCost t) 2)
 218        (Quotient.mk (relabelSetoid 2) twoBridges) ≠ mu twoBridges :=
 219  incidencePosting_classMass_ne_mu ht
 220
 221/-- **THEOREM (the pinning is a counting normalization, and that is all).**  The fiber of
 222counted histories over a labeled complex is a singleton, which is what makes the orbit count
 223equal the labeled-complex orbit count.  Said as a restatement of
 224`CanonicalHistory.fiber_unique`: the pinning's content is that there is exactly one counted
 225history per complex, not that some charges are admitted and others excluded.  (A `def`, not a
 226`theorem`: `Unique` is Type-valued.) -/
 227def pinning_is_a_counting_normalization (B : ℕ) (K : BoundedComplex B) :
 228    Unique {CH : CanonicalHistory B // CH.underlying = K} :=
 229  CanonicalHistory.fiber_unique K
 230
 231/-! ## §3. T3: the named premise, its strength, and its physical content -/
 232
 233/-- **The named premise.**  A letter's charge is a function of the three counts and of the
 234letter's kind: for each kind there is a function of the counts giving every letter of that kind
 235its charge, the same function at every complex.  Said carefully, this is an authored restriction
 236on `LetterCost`, not a constraint the alphabet forces: the alphabet's letters are indexed, and
 237`indexCost` reads that index and is excluded by this premise, so the premise forbids data the
 238alphabet does carry.  What recommends it is that it is statable purely in terms of counts and
 239kinds, the two things a letter's charge is allowed to depend on if it is to give a size-blind
 240totals form, and that it excludes both exhibited failures while admitting the count charge. -/
 241def ChargesCountsOnly (c : LetterCost) : Prop :=
 242  (∃ fV : ℕ → ℕ → ℕ → ℝ, ∀ (B : ℕ) (K : BoundedComplex B) (v : Fin K.nV),
 243    c B K (Sum.inl v) = fV K.nV K.nE K.nT)
 244  ∧ (∃ fE : ℕ → ℕ → ℕ → ℝ, ∀ (B : ℕ) (K : BoundedComplex B) (e : Fin K.nE),
 245    c B K (Sum.inr (Sum.inl e)) = fE K.nV K.nE K.nT)
 246  ∧ (∃ fT : ℕ → ℕ → ℕ → ℝ, ∀ (B : ℕ) (K : BoundedComplex B) (τ : Fin K.nT),
 247    c B K (Sum.inr (Sum.inr τ)) = fT K.nV K.nE K.nT)
 248
 249/-- **THEOREM (the named premise gives per-complex kind rates).**  Within one complex, every
 250letter of a kind shares one charge, so per-complex kind rates exist.  This is NOT the kind
 251rule: the rates vary with the complex's counts.  The global kind rule, one triple of reals for
 252all complexes, is the special case where the three count functions are constant, and this
 253theorem does not give that case. -/
 254theorem chargesCountsOnly_perComplex_kindRates (c : LetterCost) (h : ChargesCountsOnly c)
 255    (B : ℕ) (K : BoundedComplex B) :
 256    ∃ cV cE cT : ℝ,
 257      (∀ v : Fin K.nV, c B K (Sum.inl v) = cV)
 258        ∧ (∀ e : Fin K.nE, c B K (Sum.inr (Sum.inl e)) = cE)
 259        ∧ (∀ τ : Fin K.nT, c B K (Sum.inr (Sum.inr τ)) = cT) := by
 260  obtain ⟨⟨fV, hV⟩, ⟨fE, hE⟩, ⟨fT, hT⟩⟩ := h
 261  exact ⟨fV K.nV K.nE K.nT, fE K.nV K.nE K.nT, fT K.nV K.nE K.nT,
 262    fun v => hV B K v, fun e => hE B K e, fun τ => hT B K τ⟩
 263
 264/-- **THEOREM (the named premise gives the totals form, with count-dependent rates).**  The
 265block sum of each kind is the per-letter value times the count, where the value is the kind
 266function at that complex's counts.  This is NOT `FixedKindTotals`, whose rates are three fixed
 267reals across all complexes; it is the per-complex statement, and the difference is the whole
 268point of §3: a counts-only charge may vary its rates with the counts, as `pairCost` does with
 269vertex rate `nV - 1`.  The global kind rule is the special case where the three functions are
 270constant, and that special case is what the atom normalizations then pin to zero. -/
 271theorem chargesCountsOnly_kindTotals_perComplex (c : LetterCost) (h : ChargesCountsOnly c)
 272    (B : ℕ) (K : BoundedComplex B) :
 273    ∃ cV cE cT : ℝ,
 274      (∑ v : Fin K.nV, c B K (Sum.inl v)) = cV * (K.nV : ℝ)
 275        ∧ (∑ e : Fin K.nE, c B K (Sum.inr (Sum.inl e))) = cE * (K.nE : ℝ)
 276        ∧ (∑ τ : Fin K.nT, c B K (Sum.inr (Sum.inr τ))) = cT * (K.nT : ℝ) := by
 277  obtain ⟨⟨fV, hV⟩, ⟨fE, hE⟩, ⟨fT, hT⟩⟩ := h
 278  classical
 279  refine ⟨fV K.nV K.nE K.nT, fE K.nV K.nE K.nT, fT K.nV K.nE K.nT, ?_, ?_, ?_⟩
 280  · rw [Finset.sum_congr rfl (fun v _ => hV B K v), Finset.sum_const, Finset.card_univ,
 281      Fintype.card_fin, nsmul_eq_mul, mul_comm]
 282  · rw [Finset.sum_congr rfl (fun e _ => hE B K e), Finset.sum_const, Finset.card_univ,
 283      Fintype.card_fin, nsmul_eq_mul, mul_comm]
 284  · rw [Finset.sum_congr rfl (fun τ _ => hT B K τ), Finset.sum_const, Finset.card_univ,
 285      Fintype.card_fin, nsmul_eq_mul, mul_comm]
 286
 287/-- The **index charge**: each vertex letter is charged its own index.  Not counts-only,
 288because a function of the counts cannot give letter 0 charge 0 and letter 1 charge 1 at the
 289same sizes.  This is the witness that the named premise excludes per-letter data the alphabet
 290does not carry, while admitting count data it does. -/
 291def indexCost : LetterCost := fun _ _ a =>
 292  match a with
 293  | Sum.inl v => (v : ℝ)
 294  | Sum.inr _ => 0
 295
 296@[simp] theorem indexCost_inl (B : ℕ) (K : BoundedComplex B) (v : Fin K.nV) :
 297    indexCost B K (Sum.inl v) = (v : ℝ) := rfl
 298
 299/-- **THEOREM (the index charge is not counts-only).**  At the two-vertex complex, the two
 300vertex letters are charged `0` and `1`, so no single function of the counts gives both. -/
 301theorem indexCost_not_chargesCountsOnly : ¬ ChargesCountsOnly indexCost := by
 302  rintro ⟨⟨fV, hV⟩, -, -⟩
 303  have h0 := hV 2 twoLoops ⟨0, by decide⟩
 304  have h1 := hV 2 twoLoops ⟨1, by decide⟩
 305  simp only [indexCost_inl] at h0 h1
 306  -- h0 : ((⟨0,_⟩ : Fin 2) : ℝ) = fV ...; h1 : ((⟨1,_⟩ : Fin 2) : ℝ) = fV ...
 307  have h0' : (0 : ℝ) = fV twoLoops.nV twoLoops.nE twoLoops.nT := by
 308    have := h0
 309    norm_num at this
 310    exact this
 311  have h1' : (1 : ℝ) = fV twoLoops.nV twoLoops.nE twoLoops.nT := by
 312    have := h1
 313    norm_num at this
 314    exact this
 315  rw [← h0'] at h1'
 316  norm_num at h1'
 317
 318/-- **THEOREM (the named premise excludes the incidence countermodel).**  `ChargesCountsOnly`
 319rules out the incidence failure: a loop letter and a proper edge letter at the same sizes
 320(2,2,0) receive charges `0` and `t` from `incidenceCost`, and one function of the counts cannot
 321give both.  What it does NOT rule out is `pairCost`, which is counts-only; so the named premise
 322is not "the letter charge is trivial", it is "the letter charge reads nothing the alphabet does
 323not carry". -/
 324theorem chargesCountsOnly_excludes_incidence (t : ℝ) (ht : t ≠ 0) :
 325    ¬ ChargesCountsOnly (incidenceCost t) := by
 326  rintro ⟨-, ⟨fE, hE⟩, -⟩
 327  have hloop := hE 2 twoLoops ⟨0, by decide⟩
 328  have hbridge := hE 2 twoBridges ⟨0, by decide⟩
 329  simp only [incidenceCost_edge] at hloop hbridge
 330  -- loop edge: endpoints (0,0), so `if ... ≠ ... then t else 0` = 0
 331  -- bridge edge: endpoints (0,1), so the charge is t
 332  have hloop' : (0 : ℝ) = fE twoLoops.nV twoLoops.nE twoLoops.nT := by
 333    have := hloop
 334    norm_num [twoLoops] at this
 335    exact this
 336  have hbridge' : t = fE twoBridges.nV twoBridges.nE twoBridges.nT := by
 337    have := hbridge
 338    norm_num [twoBridges] at this
 339    exact this
 340  -- the two `fE` applications are at the same arguments (2,2,0)
 341  have hsame : fE twoLoops.nV twoLoops.nE twoLoops.nT
 342      = fE twoBridges.nV twoBridges.nE twoBridges.nT := rfl
 343  rw [hsame] at hloop'
 344  rw [← hbridge'] at hloop'
 345  exact ht hloop'.symm
 346
 347/-- **THEOREM (pairCost is counts-only).**  The vertex-count charge reads only the vertex
 348count, so it satisfies the named premise.  This is the theorem that keeps the premise honest:
 349it does not say letters are uncharged, it says charges read the counts. -/
 350theorem pairCost_chargesCountsOnly : ChargesCountsOnly pairCost := by
 351  refine ⟨⟨fun nV _ _ => (nV : ℝ) - 1, ?_⟩, ⟨fun _ _ _ => 0, ?_⟩, ⟨fun _ _ _ => 0, ?_⟩⟩
 352  · intro B K v
 353    simp only [pairCost]
 354  · intro B K e
 355    rfl
 356  · intro B K τ
 357    rfl
 358
 359/-- **THEOREM (kind rates are kind-only).**  A cost with constant per-kind letter rates across
 360all complexes is kind-only.  This is a restatement of `KindOnly` through its `KindRates`
 361definition, and the named premise plays no role in it: the three rate hypotheses are already
 362`KindRates`.  It is here so the module says explicitly, rather than implying, that the global
 363kind rule is the constant-function special case of the named premise; the closure into the
 364measure is then the second arc's `posting_cost_derives_mu`, cited and not re-proved.  The
 365earlier name of this theorem overclaimed a routing through `ChargesCountsOnly` and is
 366corrected. -/
 367theorem kindOnly_of_constant_rates (c : LetterCost)
 368    (cV cE cT : ℝ)
 369    (hV : ∀ (B : ℕ) (K : BoundedComplex B) (v : Fin K.nV), c B K (Sum.inl v) = cV)
 370    (hE : ∀ (B : ℕ) (K : BoundedComplex B) (e : Fin K.nE), c B K (Sum.inr (Sum.inl e)) = cE)
 371    (hT : ∀ (B : ℕ) (K : BoundedComplex B) (τ : Fin K.nT), c B K (Sum.inr (Sum.inr τ)) = cT) :
 372    KindOnly c :=
 373  ⟨cV, cE, cT, fun B K => ⟨hV B K, hE B K, hT B K⟩⟩
 374
 375/-! ## §4. Navigation index
 376
 377Flags only.  Two are deliberately `false`: the kind rule is not forced by the letter-cost
 378space, and whether the dual-entry lattice below it forces the named premise is open. -/
 379
 380structure KindRuleIndex : Type where
 381  /-- The kind rule fails in the letter-cost space by counting alone (`pairCost`). -/
 382  kind_rule_fails_by_counting : Bool
 383  /-- The kind rule fails in the letter-cost space by incidence (`incidenceCost`). -/
 384  kind_rule_fails_by_incidence : Bool
 385  /-- The cost layer cannot see the dual-entry state space, so the canonicality pinning
 386  cannot be what excludes the countermodel. -/
 387  exclusion_not_from_pinning : Bool
 388  /-- What excludes the countermodel's weight from the measure is the gauge-divisor formula:
 389  the class mass is `exp(-2t)/|Aut|`, not `1/|Aut|`. -/
 390  exclusion_is_measure_formula : Bool
 391  /-- The named premise gives the per-complex totals form with count-dependent rates. -/
 392  premise_gives_kindTotals : Bool
 393  /-- The named premise excludes the incidence countermodel and admits the count charge. -/
 394  premise_discriminates : Bool
 395  /-- NOT proved, and refuted as a reading of the letter-cost space: the kind rule is forced
 396  there.  It is not, by two independent countermodels. -/
 397  kind_rule_forced : Bool
 398  /-- NOT proved: the successor question, whether the dual-entry lattice forces the named
 399  premise.  This module's theorems say the premise is statable at the alphabet and that the
 400  state space is invisible there, so the answer must come from the lattice's own structure. -/
 401  lattice_forces_premise : Bool
 402
 403def kindRuleIndex : KindRuleIndex where
 404  kind_rule_fails_by_counting := true
 405  kind_rule_fails_by_incidence := true
 406  exclusion_not_from_pinning := true
 407  exclusion_is_measure_formula := true
 408  premise_gives_kindTotals := true
 409  premise_discriminates := true
 410  kind_rule_forced := false
 411  lattice_forces_premise := false
 412
 413theorem index_kind_rule_not_forced : kindRuleIndex.kind_rule_forced = false := rfl
 414
 415theorem index_lattice_question_open : kindRuleIndex.lattice_forces_premise = false := rfl
 416
 417end
 418
 419end Gap2KindRule
 420end SevenGaps
 421end Gravity
 422end IndisputableMonolith
 423