IndisputableMonolith.Gravity.SevenGaps.Gap2LedgerGenerated

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2JDiamondRank
   2import IndisputableMonolith.Gravity.SevenGaps.Gap2GluingDerivation
   3
   4/-!
   5# Gap 2 / C14: the LedgerGenerated fork gate
   6
   7Pre-registered TRUE/FALSE measurement that decides the tilt fork for flag 8
   8(`gap2_measure_derived`).  A1.7 (`Gap2LetterCostDichotomy`) closed the bulk-
   9cancelling fixed-kind-totals class; its escape class is where a nonzero
  10history cost can still live.  This module asks whether the canonical
  11recognition cost `jCost` is ledger-generated in the sense frozen below.  The
  12enumeration harness and SJ spectra are those of C15
  13(`Gap2JDiamondRank`, `scripts/qg/qg_j_diamond_rank_20260730.py`, receipt
  14`scripts/qg/out/j_diamond_rank_20260730.json`: 437 classes at cap 4).
  15
  16## PRE-REGISTERED PREDICATE (MODEL, frozen before enumeration)
  17
  18**Definition (`LedgerGenerated`).** A letter cost `c` is *ledger-generated*
  19iff there exist a vertex charge `fV : ℤ → ℝ` and constants `cE cT : ℝ` such
  20that for every size cap `B`, every bounded complex `K`, and every letter of
  21`K`:
  22
  23* a vertex letter `v` is charged `fV (vertexImbalance K v)`, where
  24  `vertexImbalance K v = indeg K v - outdeg K v` is that letter's own
  25  double-entry posting row (debits minus credits);
  26* every edge letter is charged the constant `cE`;
  27* every top-cell letter is charged the constant `cT`.
  28
  29In particular the charge of a letter is computed from that letter's own
  30posting-row data alone.  Forbidden inputs: orbit sums, isomorphism-class
  31data, and any global census of `K` beyond the letter's own row.  Edge and
  32top-cell letters are not accounts; their posting row is empty and the charge
  33is therefore a constant (the null-row value).
  34
  35This definition is a MODEL choice: it is the gate's admissibility class, not
  36a derived theorem.  The cap-1-3 decisions below are MEASURED /
  37kernel-certified against it.
  38
  39## Decision procedure and outcomes
  40
  41Kernel-decide `LedgerGenerated (jCost κ)` (any `κ ≠ 0`) and the finite
  42restrictions `LedgerGeneratedAt cap (jCost 1)` at caps 1, 2, 3.  Tabulate
  43`historyCost (jCost 1)` on the C15 isomorphism classes at those caps
  44(exact rationals `SJ / 2`, since `historyCost = imbalanceSq / (2κ)` at
  45`κ = 1`).
  46
  47Outcome reading (bank only; do not act beyond this module):
  48
  49* `FALSE`: `jCost` outside the ledger-conservation class; μ-form closure
  50  lives; week-two primary becomes C18.
  51* `TRUE` with `historyCost` identically zero at all three caps: conservation
  52  forces numerator unity on the ledger class.
  53* `TRUE` with nonzero `historyCost` at any cap: **C27 hard stop** (the fork
  54  condition is measured true; the choice itself is reserved for Jon).
  55  Escalate to Jon.  No tilt construction, no flag move, no launch.
  56
  57Expected axiom footprint: `[propext, Classical.choice, Quot.sound]`, with
  58`native_decide` certificates disclosed as carrying
  59`Lean.ofReduceBool` / `Lean.trustCompiler`.
  60-/
  61
  62namespace IndisputableMonolith
  63namespace Gravity
  64namespace SevenGaps
  65namespace Gap2LedgerGenerated
  66
  67open PathSumMeasure GaugeHistoryMeasure Gap2PostingCostDerivation
  68open Gap2JEhrhartSpan Gap2JDiamondRank Gap2GluingDerivation
  69
  70variable {B : ℕ}
  71
  72/-! ## §1. The pre-registered predicate -/
  73
  74/-- **PRE-REGISTERED (MODEL).**  A letter cost is ledger-generated when each
  75letter's charge is a fixed function of that letter's own double-entry posting
  76row (debits minus credits on the letter's account), with edge and top-cell
  77letters carrying constant null-row values.  No orbit sums, no
  78isomorphism-class data, no global census. -/
  79def LedgerGenerated (c : LetterCost) : Prop :=
  80  ∃ (fV : ℤ → ℝ) (cE cT : ℝ),
  81    (∀ (B : ℕ) (K : BoundedComplex B) (v : Fin K.nV),
  82      c B K (Sum.inl v) = fV (vertexImbalance K v))
  83    ∧ (∀ (B : ℕ) (K : BoundedComplex B) (e : Fin K.nE),
  84      c B K (Sum.inr (Sum.inl e)) = cE)
  85    ∧ (∀ (B : ℕ) (K : BoundedComplex B) (t : Fin K.nT),
  86      c B K (Sum.inr (Sum.inr t)) = cT)
  87
  88/-- Finite restriction of `LedgerGenerated` to complexes whose three counts
  89are at most `cap`.  This is the per-cap decision the gate asks for. -/
  90def LedgerGeneratedAt (cap : ℕ) (c : LetterCost) : Prop :=
  91  ∃ (fV : ℤ → ℝ) (cE cT : ℝ),
  92    ∀ (B : ℕ) (K : BoundedComplex B),
  93      K.nV ≤ cap → K.nE ≤ cap → K.nT ≤ cap →
  94        (∀ v : Fin K.nV, c B K (Sum.inl v) = fV (vertexImbalance K v))
  95        ∧ (∀ e : Fin K.nE, c B K (Sum.inr (Sum.inl e)) = cE)
  96        ∧ (∀ t : Fin K.nT, c B K (Sum.inr (Sum.inr t)) = cT)
  97
  98theorem LedgerGenerated_implies_at {c : LetterCost} (h : LedgerGenerated c)
  99    (cap : ℕ) : LedgerGeneratedAt cap c := by
 100  obtain ⟨fV, cE, cT, hV, hE, hT⟩ := h
 101  exact ⟨fV, cE, cT, fun B K _ _ _ => ⟨hV B K, hE B K, hT B K⟩⟩
 102
 103/-! ## §2. Kernel decision: `jCost` is ledger-generated -/
 104
 105noncomputable section
 106
 107/-- The vertex charge of `jCost κ`: square of the posting-row net over twice
 108the Casimir. -/
 109def jCostVertexCharge (kappa : ℝ) (m : ℤ) : ℝ :=
 110  (m : ℝ) ^ 2 / (2 * kappa)
 111
 112/-- **MEASURED / kernel-certified: `LedgerGenerated (jCost κ)` is TRUE** for
 113every nonzero Casimir.  The witnessing `fV` is `m ↦ m² / (2κ)`; edge and
 114top-cell null-row values are zero. -/
 115theorem jCost_ledgerGenerated {kappa : ℝ} (_hk : kappa ≠ 0) :
 116    LedgerGenerated (jCost kappa) :=
 117  ⟨jCostVertexCharge kappa, 0, 0, by
 118    refine ⟨?_, ?_, ?_⟩
 119    · intro B K v
 120      simp only [jCost_inl, jCostVertexCharge]
 121    · intro B K e
 122      simp only [jCost_edge]
 123    · intro B K t
 124      simp only [jCost_tet]⟩
 125
 126/-- Per-cap decisions at caps 1, 2, 3: all TRUE, by the global certificate. -/
 127theorem jCost_ledgerGenerated_cap1 :
 128    LedgerGeneratedAt 1 (jCost 1) :=
 129  LedgerGenerated_implies_at (jCost_ledgerGenerated (by norm_num : (1 : ℝ) ≠ 0)) 1
 130
 131theorem jCost_ledgerGenerated_cap2 :
 132    LedgerGeneratedAt 2 (jCost 1) :=
 133  LedgerGenerated_implies_at (jCost_ledgerGenerated (by norm_num : (1 : ℝ) ≠ 0)) 2
 134
 135theorem jCost_ledgerGenerated_cap3 :
 136    LedgerGeneratedAt 3 (jCost 1) :=
 137  LedgerGenerated_implies_at (jCost_ledgerGenerated (by norm_num : (1 : ℝ) ≠ 0)) 3
 138
 139/-- Boolean mirrors of the per-cap decisions (TRUE at every named cap). -/
 140def jCost_ledgerGenerated_decision_cap1 : Bool := true
 141def jCost_ledgerGenerated_decision_cap2 : Bool := true
 142def jCost_ledgerGenerated_decision_cap3 : Bool := true
 143
 144theorem jCost_ledgerGenerated_decision_cap1_eq :
 145    jCost_ledgerGenerated_decision_cap1 = true := rfl
 146theorem jCost_ledgerGenerated_decision_cap2_eq :
 147    jCost_ledgerGenerated_decision_cap2 = true := rfl
 148theorem jCost_ledgerGenerated_decision_cap3_eq :
 149    jCost_ledgerGenerated_decision_cap3 = true := rfl
 150
 151/-! ## §3. Decoy: a global-census cost is not ledger-generated
 152
 153A gate that only ever returns TRUE has not been tested.  Charging every vertex
 154the ambient vertex count reads a global census, so equal posting rows at
 155different sizes disagree. -/
 156
 157/-- Decoy cost: every vertex letter is charged the complex's vertex census. -/
 158def censusVertexCost : LetterCost := fun _ K a =>
 159  match a with
 160  | Sum.inl _ => (K.nV : ℝ)
 161  | Sum.inr _ => 0
 162
 163/-- **The predicate discriminates.**  `censusVertexCost` is not ledger-generated:
 164the point and the two-point dust both have imbalance zero at every vertex, but
 165they charge 1 and 2 respectively. -/
 166theorem censusVertexCost_not_ledgerGenerated :
 167    ¬ LedgerGenerated censusVertexCost := by
 168  rintro ⟨fV, cE, cT, hV, hE, hT⟩
 169  have h1 := hV 1 (dust 1) ⟨0, by decide⟩
 170  have h2 := hV 2 (dust 2) ⟨0, by decide⟩
 171  have m1 : vertexImbalance (dust 1) (⟨0, by decide⟩ : Fin 1) = 0 := by decide
 172  have m2 : vertexImbalance (dust 2) (⟨0, by decide⟩ : Fin 2) = 0 := by decide
 173  simp only [censusVertexCost, dust_nV] at h1 h2
 174  have eq1 : (1 : ℝ) = fV 0 := by simpa [m1] using h1
 175  have eq2 : (2 : ℝ) = fV 0 := by simpa [m2] using h2
 176  linarith
 177
 178/-! ## §4. historyCost table for `jCost 1` at caps 1–3
 179
 180`historyCost (jCost 1) B K = (imbalanceSq K : ℝ) / 2`, so the exact rational
 181is `SJ / 2` with `SJ = imbalanceSq K ∈ ℤ`.  Provenance of the class census:
 182C15 receipt `scripts/qg/out/j_diamond_rank_20260730.json`. -/
 183
 184theorem historyCost_jCost_one (B : ℕ) (K : BoundedComplex B) :
 185    historyCost (jCost 1) B K = (imbalanceSq K : ℝ) / 2 := by
 186  rw [historyCost_jCost_eq]
 187  norm_num
 188
 189/-- Cap-1 loop: the only edge is a self-loop on one vertex. -/
 190def loop1Complex : BoundedComplex 1 where
 191  nV := 1
 192  nE := 1
 193  nT := 0
 194  hV := by decide
 195  hE := by decide
 196  hT := by decide
 197  edgeVerts := fun _ => (0, 0)
 198  tetVerts := fun t => t.elim0
 199
 200theorem imbalanceSq_point : imbalanceSq pointComplex = 0 := by decide
 201theorem imbalanceSq_edge : imbalanceSq edgeComplex = 2 := by decide
 202theorem imbalanceSq_path : imbalanceSq pathComplex = 2 := by decide
 203theorem imbalanceSq_loop1 : imbalanceSq loop1Complex = 0 := by decide
 204theorem imbalanceSq_empty_cap1 : imbalanceSq (emptyComplex 1) = 0 := by decide
 205
 206/-- Native-decide certificates for the integer charges used in the table.
 207Disclosed axiom footprint on these: `Lean.ofReduceBool`, `Lean.trustCompiler`
 208on top of the base triple. -/
 209theorem imbalanceSq_edge_native : imbalanceSq edgeComplex = 2 := by native_decide
 210theorem imbalanceSq_path_native : imbalanceSq pathComplex = 2 := by native_decide
 211theorem imbalanceSq_loop1_native : imbalanceSq loop1Complex = 0 := by native_decide
 212theorem imbalanceSq_loopPoint_native : imbalanceSq loopPointComplex = 0 := by
 213  native_decide
 214theorem imbalanceSq_fork_native : imbalanceSq forkComplex = 6 := by native_decide
 215
 216theorem historyCost_jCost_one_edge :
 217    historyCost (jCost 1) 4 edgeComplex = (1 : ℝ) := by
 218  rw [historyCost_edge (1 : ℝ) (by norm_num)]
 219  norm_num
 220
 221theorem historyCost_jCost_one_point :
 222    historyCost (jCost 1) 4 pointComplex = (0 : ℝ) :=
 223  historyCost_point 1
 224
 225theorem historyCost_jCost_one_path :
 226    historyCost (jCost 1) 4 pathComplex = (1 : ℝ) := by
 227  rw [historyCost_path (1 : ℝ) (by norm_num)]
 228  norm_num
 229
 230theorem historyCost_jCost_one_loopPoint :
 231    historyCost (jCost 1) 4 loopPointComplex = (0 : ℝ) :=
 232  historyCost_loopPoint 1
 233
 234theorem historyCost_jCost_one_fork :
 235    historyCost (jCost 1) 4 forkComplex = (3 : ℝ) := by
 236  rw [historyCost_fork (1 : ℝ) (by norm_num)]
 237  norm_num
 238
 239theorem historyCost_loop1 :
 240    historyCost (jCost 1) 1 loop1Complex = 0 := by
 241  rw [historyCost_jCost_one, imbalanceSq_loop1]
 242  norm_num
 243
 244theorem historyCost_empty_cap1 :
 245    historyCost (jCost 1) 1 (emptyComplex 1) = 0 := by
 246  rw [historyCost_jCost_one, imbalanceSq_empty_cap1]
 247  norm_num
 248
 249/-- **Cap 1 historyCost table (exact rationals).**  Every C15 class at cap 1
 250has `SJ = 0`, hence `historyCost (jCost 1) = 0`. -/
 251theorem historyCost_table_cap1 :
 252    historyCost (jCost 1) 1 (emptyComplex 1) = 0
 253      ∧ historyCost (jCost 1) 4 pointComplex = 0
 254      ∧ historyCost (jCost 1) 1 loop1Complex = 0 :=
 255  ⟨historyCost_empty_cap1, historyCost_jCost_one_point, historyCost_loop1⟩
 256
 257def historyCost_identically_zero_decision_cap1 : Bool := true
 258theorem historyCost_identically_zero_decision_cap1_eq :
 259    historyCost_identically_zero_decision_cap1 = true := rfl
 260
 261/-- **Cap 2: historyCost is NOT identically zero.**  The proper edge has
 262`historyCost (jCost 1) = 1`. -/
 263theorem historyCost_not_identically_zero_cap2 :
 264    historyCost (jCost 1) 4 edgeComplex ≠ 0 := by
 265  rw [historyCost_jCost_one_edge]
 266  norm_num
 267
 268def historyCost_identically_zero_decision_cap2 : Bool := false
 269theorem historyCost_identically_zero_decision_cap2_eq :
 270    historyCost_identically_zero_decision_cap2 = false := rfl
 271
 272/-- **Cap 3: historyCost is NOT identically zero.** -/
 273theorem historyCost_not_identically_zero_cap3 :
 274    historyCost (jCost 1) 4 edgeComplex ≠ 0
 275      ∧ historyCost (jCost 1) 4 pathComplex ≠ 0
 276      ∧ historyCost (jCost 1) 4 forkComplex ≠ 0 := by
 277  refine ⟨?_, ?_, ?_⟩
 278  · rw [historyCost_jCost_one_edge]; norm_num
 279  · rw [historyCost_jCost_one_path]; norm_num
 280  · rw [historyCost_jCost_one_fork]; norm_num
 281
 282def historyCost_identically_zero_decision_cap3 : Bool := false
 283theorem historyCost_identically_zero_decision_cap3_eq :
 284    historyCost_identically_zero_decision_cap3 = false := rfl
 285
 286/-! ## §5. Exact rational historyCost table (witness rows)
 287
 288Rows are `(nV, nE, SJ, historyCost = SJ/2)` for the named seed complexes that
 289live at caps ≤ 3.  Full per-class tables at caps 1–3 are MEASURED by
 290`scripts/qg/qg_ledger_generated_20260730.py` and recorded in
 291`scripts/qg/out/ledger_generated_20260730.json`. -/
 292
 293/-- Exact rational history cost of `jCost 1` as `SJ / 2`. -/
 294def historyCostRational (sj : ℤ) : ℚ := (sj : ℚ) / 2
 295
 296theorem historyCostRational_edge : historyCostRational 2 = (1 : ℚ) := by
 297  norm_num [historyCostRational]
 298theorem historyCostRational_fork : historyCostRational 6 = (3 : ℚ) := by
 299  norm_num [historyCostRational]
 300theorem historyCostRational_zero : historyCostRational 0 = (0 : ℚ) := by
 301  norm_num [historyCostRational]
 302
 303/-- Seed table: `(nV, nE, SJ, historyCostRational SJ)`. -/
 304def historyCostSeedTable : List (ℕ × ℕ × ℤ × ℚ) :=
 305  [(0, 0, 0, 0),
 306    (1, 0, 0, 0),
 307    (1, 1, 0, 0),
 308    (2, 1, 2, 1),
 309    (2, 1, 0, 0),
 310    (3, 2, 2, 1),
 311    (3, 2, 6, 3)]
 312
 313theorem historyCostSeedTable_length : historyCostSeedTable.length = 7 := rfl
 314
 315theorem historyCostSeedTable_edge_row :
 316    (2, 1, 2, (1 : ℚ)) ∈ historyCostSeedTable := by decide
 317
 318theorem historyCostSeedTable_edge_row_native :
 319    (2, 1, 2, (1 : ℚ)) ∈ historyCostSeedTable := by native_decide
 320
 321/-- MEASURED tallies (C15 harness, caps 1–3).  Provenance:
 322`scripts/qg/out/ledger_generated_20260730.json`. -/
 323structure CapHistoryTally where
 324  classes : ℕ
 325  sjAllZero : Bool
 326  maxAbsSJ : ℤ
 327  ledgerGeneratedDecision : Bool
 328
 329def measuredHistoryCaps : Fin 3 → CapHistoryTally :=
 330  ![{ classes := 3, sjAllZero := true, maxAbsSJ := 0,
 331      ledgerGeneratedDecision := true },
 332    { classes := 13, sjAllZero := false, maxAbsSJ := 8,
 333      ledgerGeneratedDecision := true },
 334    { classes := 68, sjAllZero := false, maxAbsSJ := 18,
 335      ledgerGeneratedDecision := true }]
 336
 337theorem measured_cap1_zero :
 338    (measuredHistoryCaps 0).sjAllZero = true
 339      ∧ (measuredHistoryCaps 0).ledgerGeneratedDecision = true := ⟨rfl, rfl⟩
 340
 341theorem measured_cap2_nonzero :
 342    (measuredHistoryCaps 1).sjAllZero = false
 343      ∧ (measuredHistoryCaps 1).ledgerGeneratedDecision = true := ⟨rfl, rfl⟩
 344
 345theorem measured_cap3_nonzero :
 346    (measuredHistoryCaps 2).sjAllZero = false
 347      ∧ (measuredHistoryCaps 2).ledgerGeneratedDecision = true := ⟨rfl, rfl⟩
 348
 349/-! ## §6. C27 hard-stop trigger
 350
 351Pre-registered: TRUE with nonzero historyCost at any cap arms C27. -/
 352
 353/-- **C27 trigger predicate.**  Ledger-generated at the cap, and history cost
 354not identically zero there. -/
 355def C27TriggerAt (cap : ℕ) (c : LetterCost) : Prop :=
 356  LedgerGeneratedAt cap c
 357    ∧ ∃ (B : ℕ) (K : BoundedComplex B),
 358        K.nV ≤ cap ∧ K.nE ≤ cap ∧ K.nT ≤ cap ∧ historyCost c B K ≠ 0
 359
 360theorem edgeComplex_fits_cap2 :
 361    edgeComplex.nV ≤ 2 ∧ edgeComplex.nE ≤ 2 ∧ edgeComplex.nT ≤ 2 := by
 362  native_decide
 363
 364theorem edgeComplex_fits_cap3 :
 365    edgeComplex.nV ≤ 3 ∧ edgeComplex.nE ≤ 3 ∧ edgeComplex.nT ≤ 3 := by
 366  native_decide
 367
 368/-- **C27 trigger armed at cap 2.** -/
 369theorem C27_trigger_armed_cap2 : C27TriggerAt 2 (jCost 1) := by
 370  refine ⟨jCost_ledgerGenerated_cap2, ?_⟩
 371  refine ⟨4, edgeComplex, edgeComplex_fits_cap2.1, edgeComplex_fits_cap2.2.1,
 372    edgeComplex_fits_cap2.2.2, historyCost_not_identically_zero_cap2⟩
 373
 374/-- **C27 trigger armed at cap 3.** -/
 375theorem C27_trigger_armed_cap3 : C27TriggerAt 3 (jCost 1) := by
 376  refine ⟨jCost_ledgerGenerated_cap3, ?_⟩
 377  refine ⟨4, edgeComplex, edgeComplex_fits_cap3.1, edgeComplex_fits_cap3.2.1,
 378    edgeComplex_fits_cap3.2.2, historyCost_not_identically_zero_cap2⟩
 379
 380/-- Boolean: C27 hard stop is armed. -/
 381def C27_hard_stop_armed : Bool := true
 382theorem C27_hard_stop_armed_eq : C27_hard_stop_armed = true := rfl
 383
 384/-- Cap 1 seeds do not alone arm C27: ledger-generated, history zero. -/
 385theorem C27_not_armed_by_cap1_seeds :
 386    LedgerGeneratedAt 1 (jCost 1)
 387      ∧ historyCost (jCost 1) 1 (emptyComplex 1) = 0
 388      ∧ historyCost (jCost 1) 4 pointComplex = 0
 389      ∧ historyCost (jCost 1) 1 loop1Complex = 0 :=
 390  ⟨jCost_ledgerGenerated_cap1, historyCost_empty_cap1,
 391    historyCost_jCost_one_point, historyCost_loop1⟩
 392
 393/-! ## §7. Verdict -/
 394
 395/-- **The C14 LedgerGenerated fork verdict.** -/
 396structure LedgerGeneratedVerdict : Prop where
 397  predicate_is_model : True
 398  jCost_is_ledgerGenerated : ∀ kappa : ℝ, kappa ≠ 0 → LedgerGenerated (jCost kappa)
 399  decisions_cap1_2_3 :
 400    LedgerGeneratedAt 1 (jCost 1)
 401      ∧ LedgerGeneratedAt 2 (jCost 1)
 402      ∧ LedgerGeneratedAt 3 (jCost 1)
 403  decoy_discriminates : ¬ LedgerGenerated censusVertexCost
 404  history_cap1_zero :
 405    historyCost (jCost 1) 1 (emptyComplex 1) = 0
 406      ∧ historyCost (jCost 1) 4 pointComplex = 0
 407      ∧ historyCost (jCost 1) 1 loop1Complex = 0
 408  history_cap2_nonzero : historyCost (jCost 1) 4 edgeComplex ≠ 0
 409  history_cap3_nonzero : historyCost (jCost 1) 4 forkComplex ≠ 0
 410  c27_armed_cap2 : C27TriggerAt 2 (jCost 1)
 411  c27_armed_cap3 : C27TriggerAt 3 (jCost 1)
 412
 413theorem ledgerGeneratedVerdict : LedgerGeneratedVerdict where
 414  predicate_is_model := trivial
 415  jCost_is_ledgerGenerated := fun _ hk => jCost_ledgerGenerated hk
 416  decisions_cap1_2_3 :=
 417    ⟨jCost_ledgerGenerated_cap1, jCost_ledgerGenerated_cap2, jCost_ledgerGenerated_cap3⟩
 418  decoy_discriminates := censusVertexCost_not_ledgerGenerated
 419  history_cap1_zero := historyCost_table_cap1
 420  history_cap2_nonzero := historyCost_not_identically_zero_cap2
 421  history_cap3_nonzero := (historyCost_not_identically_zero_cap3).2.2
 422  c27_armed_cap2 := C27_trigger_armed_cap2
 423  c27_armed_cap3 := C27_trigger_armed_cap3
 424
 425structure LedgerGeneratedIndex : Type where
 426  ledgerGenerated_jCost : Bool
 427  history_zero_cap1 : Bool
 428  history_zero_cap2 : Bool
 429  history_zero_cap3 : Bool
 430  c27_hard_stop_armed : Bool
 431  measure_flag_moved : Bool
 432
 433def ledgerGeneratedIndex : LedgerGeneratedIndex where
 434  ledgerGenerated_jCost := true
 435  history_zero_cap1 := true
 436  history_zero_cap2 := false
 437  history_zero_cap3 := false
 438  c27_hard_stop_armed := true
 439  measure_flag_moved := false
 440
 441theorem index_c27_armed : ledgerGeneratedIndex.c27_hard_stop_armed = true := rfl
 442theorem index_flag_unmoved : ledgerGeneratedIndex.measure_flag_moved = false := rfl
 443theorem index_jCost_true : ledgerGeneratedIndex.ledgerGenerated_jCost = true := rfl
 444
 445end
 446
 447/-! ## Axiom audit -/
 448
 449#print axioms jCost_ledgerGenerated
 450#print axioms jCost_ledgerGenerated_cap1
 451#print axioms jCost_ledgerGenerated_cap2
 452#print axioms jCost_ledgerGenerated_cap3
 453#print axioms censusVertexCost_not_ledgerGenerated
 454#print axioms historyCost_jCost_one
 455#print axioms imbalanceSq_edge
 456#print axioms imbalanceSq_edge_native
 457#print axioms imbalanceSq_loop1_native
 458#print axioms historyCost_jCost_one_edge
 459#print axioms historyCost_table_cap1
 460#print axioms historyCost_not_identically_zero_cap2
 461#print axioms historyCost_not_identically_zero_cap3
 462#print axioms C27_trigger_armed_cap2
 463#print axioms C27_trigger_armed_cap3
 464#print axioms ledgerGeneratedVerdict
 465#print axioms historyCostSeedTable_edge_row_native
 466
 467end Gap2LedgerGenerated
 468end SevenGaps
 469end Gravity
 470end IndisputableMonolith
 471