IndisputableMonolith.Gravity.SevenGaps.Gap2LatticeKindRule

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2KindRule
   2
   3/-!
   4# Gap 2, fourth arc: does the dual-entry lattice force the counts-only premise?
   5
   6The third arc (`Gap2KindRule`) named the premise the posting-cost derivation needs:
   7`ChargesCountsOnly`, that a letter's charge is a function of the three cell counts and the
   8letter's kind.  It left one question open and flagged it `lattice_forces_premise := false`:
   9whether the dual-entry lattice itself, one layer below `LetterCost`, forces that premise.  This
  10module answers it.
  11
  12**The committed answer is no, twice over, and the second floor is the one that was not seen
  13coming.**  The lattice's charge is not a free real per letter; it is the strain of a
  14`DualEntryStrainState`, which is `phi * mag`: an integer column imbalance `phi = debit - credit`
  15capped at one quantum by `flux_unit`, times a nonnegative real magnitude `mag` that nothing in
  16the structure constrains.  So "the lattice" is two lattices, and the premise fails on each.
  17
  18* **The magnitude floor.**  `mag` is an arbitrary nonnegative real per letter, so the strain
  19  `phi * mag` is not even required to be an integer, and it can exceed the flux quantum:
  20  `magReadsIncidenceLattice` gives a proper edge magnitude `2` and a loop edge magnitude `1`,
  21  so with block-constant imbalances the strain reads incidence through the magnitude
  22  (`magReadsIncidenceLattice_strain_edge`, strain `2` on a proper edge).  What the referee
  23  correctly insisted on, and what is now stated: this shows the magnitude factor is free to
  24  read incidence, and it shows the strain is not capped by the flux quantum; it does NOT show a
  25  non-integer strain, because `1` and `2` are integers, and the witness is not offered as one.
  26
  27* **The flux floor.**  Even with every magnitude pinned to one, so the strain equals the
  28  integer imbalance `phi` and lies in `{-1, 0, +1}` per letter, `phi` may still read incidence:
  29  `incidencePhiLattice` puts a unit imbalance on exactly the proper edge letters, which is
  30  equivariant, not counts-only, and its induced letter cost is exactly the second arc's escape
  31  cost `incidenceCost 1`.  So the flux cap bounds the *imbalance*, not what the imbalance
  32  reads; and it bounds the strain only when the magnitude is also pinned, which the structure
  33  does not do.
  34
  35The honest named premise is therefore a conjunction, `LatticeChargesCountsOnly`: counts-only
  36imbalances AND counts-only magnitudes.  The two conjuncts are independent in substance, both
  37directions exhibited (`dual_premise_conjuncts_independent`): `incidencePhiLattice` has
  38counts-only magnitudes (all one) and a not counts-only imbalance, and `magReadsIncidenceLattice`
  39has counts-only imbalances (every edge letter imbalance `+1`) and a magnitude that reads
  40incidence.  What the lattice structure forces, as a theorem, is `flux_unit`
  41(`lattice_forces_flux_unit`): a per-letter cap of one quantum on the integer imbalance.  Said
  42exactly, that is the Lean content; the English gloss that this is "all" the structure forces
  43and that it is "silent" on incidence is a reading, and is flagged as such in §4 rather than
  44stated as a theorem.  It is a cap on the imbalance, not on the strain, and not a bound on the
  45magnitude factor.
  46
  47## What this settles and what it does not
  48
  49It settles that the counts-only premise is not a theorem of the dual-entry structure; it is an
  50additional physical assumption, now stated at the layer where the charge actually lives.  The
  51successor question, one layer down again, is whether anything in the ledger's *dynamics* (the
  52posting rules that produce these states, not the state type) forces counts-only imbalances and
  53magnitudes.  That is a question about `LedgerPostingAdjacency` and the posting run, not about
  54the state space, and it is flagged open in the index.
  55-/
  56
  57namespace IndisputableMonolith
  58namespace Gravity
  59namespace SevenGaps
  60namespace Gap2LatticeKindRule
  61
  62open PathSumMeasure ExactShellGaugePreflight Gap2GaugeVolume Gap2GluingDerivation
  63open GaugeHistoryMeasure Gap2SizeBlindnessReach Gap2PostingCostDerivation Gap2KindRule
  64open Analysis.RecognitionDualEntryEnrichment4D
  65
  66noncomputable section
  67
  68/-! ## §1. The lattice charge is a strain, and a lattice cost factors through it -/
  69
  70/-- A **lattice cost** assigns a dual-entry strain state to each complex's posting alphabet and
  71reads the charge as the strain.  This is the cost notion one layer below `LetterCost`: rather
  72than a free real per letter, a letter carries an integer imbalance and a real magnitude, and
  73the charge is their product.  The third arc's `letter_cost_is_silent_on_the_state_space` said a
  74`LetterCost` takes no state; a lattice cost is precisely the state-bearing carrier that theorem
  75left room for. -/
  76structure LatticeCost where
  77  charge : ∀ (B : ℕ) (K : BoundedComplex B), DualEntryStrainState (PostingAlphabet K)
  78
  79namespace LatticeCost
  80
  81variable (lc : LatticeCost)
  82
  83/-- The per-letter strain, the actual charge. -/
  84def strain (B : ℕ) (K : BoundedComplex B) (a : PostingAlphabet K) : ℝ :=
  85  (lc.charge B K).strain a
  86
  87/-- The induced letter cost, forgetting the lattice structure. -/
  88def toLetterCost : LetterCost := fun B K a => lc.strain B K a
  89
  90end LatticeCost
  91
  92/-! ## §2. Floor one: the magnitude is unconstrained, and can read the count or incidence -/
  93
  94/-- **The count-reading-magnitude witness.**  Each vertex letter carries a unit debit
  95(imbalance `+1`) and a magnitude equal to the vertex count; edge and tet letters carry zero.
  96Said plainly, this does NOT fail `ChargesCountsOnly`: the strain at a vertex letter is the
  97vertex count, which is a function of the counts, so the induced letter cost is counts-only and
  98this is not a countermodel to the third arc's premise.  Nor is it an independence witness for
  99the dual premise: its magnitude `nV` is counts-only, so it satisfies BOTH halves of
 100`LatticeChargesCountsOnly`.  Its only role is the observation that the magnitude factor is free
 101to read the count; the incidence-reading magnitude that does the independence work is
 102`magReadsIncidenceLattice`, and the countermodel to the third arc's premise is
 103`incidencePhiLattice`, in §3. -/
 104def pairMagLattice : LatticeCost where
 105  charge := fun _B K =>
 106    { debit := fun a => match a with
 107        | Sum.inl _ => 1
 108        | Sum.inr _ => 0
 109      credit := fun _ => 0
 110      mag := fun a => match a with
 111        | Sum.inl _ => (K.nV : ℝ)
 112        | Sum.inr _ => 0
 113      mag_nonneg := fun a => by
 114        cases a with
 115        | inl v => exact Nat.cast_nonneg K.nV
 116        | inr rest => exact le_rfl
 117      flux_unit := fun a => by
 118        cases a with
 119        | inl v => simp
 120        | inr rest => simp }
 121
 122/-- The strain of `pairMagLattice` at a vertex letter is the vertex count. -/
 123theorem pairMagLattice_strain_vertex (B : ℕ) (K : BoundedComplex B) (v : Fin K.nV) :
 124    pairMagLattice.strain B K (Sum.inl v) = (K.nV : ℝ) := by
 125  simp [LatticeCost.strain, pairMagLattice, DualEntryStrainState.strain,
 126    DualEntryStrainState.phi]
 127
 128/-- **THEOREM (the magnitude at a vertex letter is the vertex count).**  The Lean content is
 129exactly the `rfl` shown: `mag (Sum.inl v) = (K.nV : ℝ)`.  It does not, by itself, prove that
 130the imbalances are counts-only (they are, but that is a separate fact), that the magnitude is
 131non-constant across complexes (no second complex is mentioned), or that the dual premise must
 132pin the magnitude (that is a design conclusion, not a theorem).  What it exhibits is the
 133building block of those facts: the magnitude factor at a vertex letter is the vertex count,
 134which is a count and therefore permitted by a counts-only premise.  The count-reading-magnitude
 135observation is used in `lattice_does_not_force_counts_only`; the magnitude-reading-incidence
 136witness that does the independence work is `magReadsIncidenceLattice`. -/
 137theorem pairMagLattice_mag_reads_count (B : ℕ) (K : BoundedComplex B) (v : Fin K.nV) :
 138    (pairMagLattice.charge B K).mag (Sum.inl v) = (K.nV : ℝ) := rfl
 139
 140/-! ## §3. Floor two: unit flux caps the imbalance, not what the charge reads -/
 141
 142/-- **The incidence failure, on the lattice, through the imbalance.**  Each proper edge letter
 143carries a unit debit (imbalance `+1`), every other letter zero, every magnitude one.  The
 144strain is then the second arc's `incidenceCost 1`, restricted to the lattice: equivariant, not
 145counts-only, reading the incidence structure at the letter.  Said exactly, its strain takes
 146values in `{0, +1}` (credit is identically zero, so `-1` is never attained), which is a subset
 147of the flux range `{-1, 0, +1}` the cap permits.  This is the countermodel the integer flux
 148was supposed to exclude and does not. -/
 149def incidencePhiLattice : LatticeCost where
 150  charge := fun _B K =>
 151    { debit := fun a => match a with
 152        | Sum.inr (Sum.inl e) => if (K.edgeVerts e).1 ≠ (K.edgeVerts e).2 then 1 else 0
 153        | _ => 0
 154      credit := fun _ => 0
 155      mag := fun _ => 1
 156      mag_nonneg := fun _ => zero_le_one
 157      flux_unit := fun a => by
 158        cases a with
 159        | inl v => simp
 160        | inr rest =>
 161          cases rest with
 162          | inl e =>
 163            simp only
 164            by_cases h : (K.edgeVerts e).1 ≠ (K.edgeVerts e).2 <;> simp [h]
 165          | inr t => simp }
 166
 167/-- The induced letter cost of `incidencePhiLattice` is exactly `incidenceCost 1`. -/
 168theorem incidencePhiLattice_toLetterCost_eq :
 169    incidencePhiLattice.toLetterCost = incidenceCost 1 := by
 170  funext B K a
 171  cases a with
 172  | inl v =>
 173    simp [LatticeCost.toLetterCost, LatticeCost.strain, incidencePhiLattice,
 174      DualEntryStrainState.strain, DualEntryStrainState.phi, incidenceCost]
 175  | inr rest =>
 176    cases rest with
 177    | inl e =>
 178      simp only [LatticeCost.toLetterCost, LatticeCost.strain, incidencePhiLattice,
 179        DualEntryStrainState.strain, DualEntryStrainState.phi, incidenceCost]
 180      by_cases h : (K.edgeVerts e).1 ≠ (K.edgeVerts e).2 <;> simp [h]
 181    | inr t =>
 182      simp [LatticeCost.toLetterCost, LatticeCost.strain, incidencePhiLattice,
 183        DualEntryStrainState.strain, DualEntryStrainState.phi, incidenceCost]
 184
 185/-- **THEOREM (the flux floor).**  `incidencePhiLattice` has every letter on the integer-flux
 186lattice with magnitude one, so its strain is an honest integer imbalance in `{-1, 0, +1}`, and
 187it is not counts-only: its induced letter cost is the incidence cost, which the third arc
 188proved fails `ChargesCountsOnly`.  So unit flux caps the size of a letter's charge and is
 189silent on what the charge reads. -/
 190theorem incidencePhiLattice_not_countsOnly :
 191    ¬ ChargesCountsOnly (incidencePhiLattice.toLetterCost) := by
 192  rw [incidencePhiLattice_toLetterCost_eq]
 193  exact chargesCountsOnly_excludes_incidence 1 one_ne_zero
 194
 195/-- **THEOREM (the lattice does not force the counts-only premise).**  A lattice cost on the
 196integer-flux lattice whose imbalance reads incidence, so the induced letter cost is not
 197counts-only.  The first conjunct alone settles the English claim; the second is kept only as a
 198pointer to the structural fact (the magnitude is free to read the count) and does no work toward
 199the conclusion, which is why it is stated as a conjunction with an explicit note rather than
 200left to look load-bearing.  `ChargesCountsOnly` of the induced letter cost is an additional
 201premise, not a theorem of the lattice. -/
 202theorem lattice_does_not_force_counts_only :
 203    (∃ lc : LatticeCost, ¬ ChargesCountsOnly lc.toLetterCost)
 204      ∧ (∀ (B : ℕ) (K : BoundedComplex B) (v : Fin K.nV),
 205          (pairMagLattice.charge B K).mag (Sum.inl v) = (K.nV : ℝ)) :=
 206  ⟨⟨incidencePhiLattice, incidencePhiLattice_not_countsOnly⟩,
 207    fun B K v => pairMagLattice_mag_reads_count B K v⟩
 208
 209/-! ## §4. The honest named premise is a conjunction, and what the lattice does force -/
 210
 211/-- **The dual named premise.**  A lattice charge is counts-only when BOTH its imbalance and
 212its magnitude are counts-only functions of the letter's kind.  Said carefully, this is a
 213*stronger sufficient condition* than the third arc's `ChargesCountsOnly` lifted to the lattice
 214(that lift is `ChargesCountsOnly ∘ toLetterCost`): the product `phi * mag` can be counts-only
 215while a factor is not, so conjunct-wise counts-only implies but is not implied by counts-only
 216strain.  The two conjuncts are independent in substance, both directions exhibited in
 217`dual_premise_conjuncts_independent`: `incidencePhiLattice` satisfies the magnitude half (all
 218magnitudes one) and fails the imbalance half, and `magReadsIncidenceLattice` satisfies the
 219imbalance half (every edge imbalance `+1`) while its magnitude reads incidence.  `pairMagLattice`
 220is NOT an independence witness: its magnitude `nV` is counts-only, so it satisfies both halves. -/
 221def LatticeChargesCountsOnly (lc : LatticeCost) : Prop :=
 222  (∃ fV fE fT : ℕ → ℕ → ℕ → ℤ, ∀ (B : ℕ) (K : BoundedComplex B),
 223      (∀ v : Fin K.nV, (lc.charge B K).phi (Sum.inl v) = fV K.nV K.nE K.nT)
 224        ∧ (∀ e : Fin K.nE, (lc.charge B K).phi (Sum.inr (Sum.inl e)) = fE K.nV K.nE K.nT)
 225        ∧ (∀ τ : Fin K.nT, (lc.charge B K).phi (Sum.inr (Sum.inr τ)) = fT K.nV K.nE K.nT))
 226    ∧ (∃ gV gE gT : ℕ → ℕ → ℕ → ℝ, ∀ (B : ℕ) (K : BoundedComplex B),
 227      (∀ v : Fin K.nV, (lc.charge B K).mag (Sum.inl v) = gV K.nV K.nE K.nT)
 228        ∧ (∀ e : Fin K.nE, (lc.charge B K).mag (Sum.inr (Sum.inl e)) = gE K.nV K.nE K.nT)
 229        ∧ (∀ τ : Fin K.nT, (lc.charge B K).mag (Sum.inr (Sum.inr τ)) = gT K.nV K.nE K.nT))
 230
 231/-- **THEOREM (the lattice forces the flux cap).**  Every lattice cost has every letter's
 232imbalance capped at one quantum in absolute value.  That is the entire Lean content: the
 233statement is a projection of the structure field `flux_unit`, and it proves `|phi| ≤ 1` and
 234nothing more.  The English gloss that this is "the whole of" what the structure forces, and
 235that it is "silent" on incidence, index, and count-dependence, is a reading the theorem does
 236not carry (a type cannot prove a universal about all its own consequences), so it is recorded
 237here as commentary and not as the theorem.  What is theorem-shaped is the cap itself, and it is
 238a cap on the integer imbalance, not on the strain and not on the magnitude factor. -/
 239theorem lattice_forces_flux_unit (lc : LatticeCost) (B : ℕ) (K : BoundedComplex B)
 240    (a : PostingAlphabet K) :
 241    |(lc.charge B K).phi a| ≤ 1 :=
 242  (lc.charge B K).flux_unit a
 243
 244/-- **The second direction's witness.**  A lattice cost whose imbalances are counts-only
 245(every edge letter carries imbalance `+1`, vertices and tets `0`) but whose magnitude reads
 246incidence: a proper edge letter's magnitude is `2` and a loop edge's is `1`.  The strain at an
 247edge letter is then `2` on a proper edge and `1` on a loop, so the strain reads incidence
 248through the magnitude while the imbalance is counts-only.  This is the direction
 249`incidencePhiLattice` does not supply. -/
 250def magReadsIncidenceLattice : LatticeCost where
 251  charge := fun _B K =>
 252    { debit := fun a => match a with
 253        | Sum.inr (Sum.inl _e) => 1
 254        | _ => 0
 255      credit := fun _ => 0
 256      mag := fun a => match a with
 257        | Sum.inr (Sum.inl e) => if (K.edgeVerts e).1 ≠ (K.edgeVerts e).2 then 2 else 1
 258        | _ => 1
 259      mag_nonneg := fun a => by
 260        cases a with
 261        | inl v => exact zero_le_one
 262        | inr rest =>
 263          cases rest with
 264          | inl e =>
 265            by_cases h : (K.edgeVerts e).1 ≠ (K.edgeVerts e).2 <;> simp [h]
 266          | inr t => exact zero_le_one
 267      flux_unit := fun a => by
 268        cases a with
 269        | inl v => simp
 270        | inr rest =>
 271          cases rest with
 272          | inl e => simp
 273          | inr t => simp }
 274
 275/-- The strain of `magReadsIncidenceLattice` at an edge letter is `1 * mag`, which is `2` on a
 276proper edge and `1` on a loop, so the strain reads incidence through the magnitude while the
 277imbalance is counts-only. -/
 278theorem magReadsIncidenceLattice_strain_edge (B : ℕ) (K : BoundedComplex B) (e : Fin K.nE) :
 279    magReadsIncidenceLattice.strain B K (Sum.inr (Sum.inl e))
 280      = if (K.edgeVerts e).1 ≠ (K.edgeVerts e).2 then 2 else 1 := by
 281  simp only [LatticeCost.strain, magReadsIncidenceLattice, DualEntryStrainState.strain,
 282    DualEntryStrainState.phi]
 283  by_cases h : (K.edgeVerts e).1 ≠ (K.edgeVerts e).2 <;> simp [h]
 284
 285/-- **THEOREM (the strain can exceed the flux quantum).**  With `mag` free, the strain at a
 286proper edge is `1 * 2 = 2`, so the integer-flux cap on the imbalance does not cap the strain at
 287one quantum.  Said exactly: `2` is an integer, so this is NOT a non-integer strain witness, and
 288the theorem is not offered as one; what it exhibits is that the strain exceeds the flux cap
 289because the magnitude is unconstrained.  A genuinely non-integer strain (say `mag = 1/2`) is
 290equally constructible but is not needed for any claim here, so it is not added.  The earlier
 291title "need not lie on the integer lattice's values" was false for this witness and is
 292corrected. -/
 293theorem magReadsIncidenceLattice_strain_exceeds_flux :
 294    magReadsIncidenceLattice.strain 2 twoBridges (Sum.inr (Sum.inl ⟨0, by decide⟩)) = 2 := by
 295  simp only [LatticeCost.strain, magReadsIncidenceLattice, DualEntryStrainState.strain,
 296    DualEntryStrainState.phi, twoBridges]
 297  norm_num
 298
 299/-- **THEOREM (the two conjuncts are independent, both directions).**
 300Direction one: `incidencePhiLattice` has counts-only magnitudes (all one) and a not
 301counts-only imbalance.  Direction two: `magReadsIncidenceLattice` has counts-only imbalances
 302(every edge letter carries imbalance `+1`) and a magnitude that reads incidence.  So neither
 303half of the dual premise implies the other, and both must be assumed. -/
 304theorem dual_premise_conjuncts_independent :
 305    ((∃ gV gE gT : ℕ → ℕ → ℕ → ℝ, ∀ (B : ℕ) (K : BoundedComplex B),
 306        (∀ v : Fin K.nV, (incidencePhiLattice.charge B K).mag (Sum.inl v) = gV K.nV K.nE K.nT)
 307          ∧ (∀ e : Fin K.nE,
 308              (incidencePhiLattice.charge B K).mag (Sum.inr (Sum.inl e)) = gE K.nV K.nE K.nT)
 309          ∧ (∀ τ : Fin K.nT,
 310              (incidencePhiLattice.charge B K).mag (Sum.inr (Sum.inr τ)) = gT K.nV K.nE K.nT))
 311      ∧ ¬ ChargesCountsOnly (incidencePhiLattice.toLetterCost))
 312    ∧ ((∃ fV fE fT : ℕ → ℕ → ℕ → ℤ, ∀ (B : ℕ) (K : BoundedComplex B),
 313        (∀ v : Fin K.nV, (magReadsIncidenceLattice.charge B K).phi (Sum.inl v) = fV K.nV K.nE K.nT)
 314          ∧ (∀ e : Fin K.nE,
 315              (magReadsIncidenceLattice.charge B K).phi (Sum.inr (Sum.inl e)) = fE K.nV K.nE K.nT)
 316          ∧ (∀ τ : Fin K.nT,
 317              (magReadsIncidenceLattice.charge B K).phi (Sum.inr (Sum.inr τ)) = fT K.nV K.nE K.nT))
 318      ∧ (magReadsIncidenceLattice.strain 2 twoBridges (Sum.inr (Sum.inl ⟨0, by decide⟩)) = 2
 319          ∧ magReadsIncidenceLattice.strain 2 twoLoops (Sum.inr (Sum.inl ⟨0, by decide⟩)) = 1)) := by
 320  refine ⟨⟨⟨fun _ _ _ => 1, fun _ _ _ => 1, fun _ _ _ => 1, fun B K => ⟨?_, ?_, ?_⟩⟩,
 321    incidencePhiLattice_not_countsOnly⟩,
 322    ⟨⟨fun _ _ _ => 0, fun _ _ _ => 1, fun _ _ _ => 0, fun B K => ⟨?_, ?_, ?_⟩⟩, ?_, ?_⟩⟩
 323  · intro v; rfl
 324  · intro e; rfl
 325  · intro τ; rfl
 326  · intro v; simp [DualEntryStrainState.phi, magReadsIncidenceLattice]
 327  · intro e; simp [DualEntryStrainState.phi, magReadsIncidenceLattice]
 328  · intro τ; simp [DualEntryStrainState.phi, magReadsIncidenceLattice]
 329  · exact magReadsIncidenceLattice_strain_exceeds_flux
 330  · simp only [LatticeCost.strain, magReadsIncidenceLattice, DualEntryStrainState.strain,
 331      DualEntryStrainState.phi, twoLoops]
 332    norm_num
 333
 334/-! ## §5. Navigation index -/
 335
 336structure LatticeIndex : Type where
 337  /-- A lattice cost exists whose induced letter cost is not counts-only. -/
 338  countermodel_on_lattice : Bool
 339  /-- The magnitude factor is free to read the count even with block-constant integer columns. -/
 340  mag_reads_count : Bool
 341  /-- The integer-flux lattice admits an incidence-reading imbalance. -/
 342  flux_reads_incidence : Bool
 343  /-- The lattice structure forces the per-letter unit cap on the integer imbalance
 344  (`lattice_forces_flux_unit`).  The name says "only" as commentary; no theorem proves the
 345  exclusivity, since a type cannot prove a universal about all its own consequences. -/
 346  lattice_forces_only_flux : Bool
 347  /-- The named premise at this layer is a conjunction over imbalance and magnitude. -/
 348  premise_is_a_conjunction : Bool
 349  /-- NOT proved, and refuted: that the dual-entry lattice forces the counts-only premise. -/
 350  lattice_forces_premise : Bool
 351  /-- NOT proved: the successor, whether the ledger's posting dynamics (the run, not the state
 352  type) forces counts-only imbalances and magnitudes. -/
 353  dynamics_forces_premise : Bool
 354
 355def latticeIndex : LatticeIndex where
 356  countermodel_on_lattice := true
 357  mag_reads_count := true
 358  flux_reads_incidence := true
 359  lattice_forces_only_flux := true
 360  premise_is_a_conjunction := true
 361  lattice_forces_premise := false
 362  dynamics_forces_premise := false
 363
 364theorem index_lattice_not_forced : latticeIndex.lattice_forces_premise = false := rfl
 365
 366theorem index_dynamics_open : latticeIndex.dynamics_forces_premise = false := rfl
 367
 368end
 369
 370end Gap2LatticeKindRule
 371end SevenGaps
 372end Gravity
 373end IndisputableMonolith
 374