IndisputableMonolith.Gravity.SevenGaps.Gap2LetterCostDichotomyHostileProbe

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2LetterCostDichotomy
   2
   3/-!
   4Hostile review probe for `Gap2LetterCostDichotomy` (A1.7).
   5Uncommitted by design; primary commits only if review is not FATAL.
   6-/
   7
   8namespace IndisputableMonolith
   9namespace Gravity
  10namespace SevenGaps
  11namespace Gap2LetterCostDichotomyHostileProbe
  12
  13open Gap2LetterCostDichotomy
  14open PathSumMeasure ExactShellGaugePreflight Gap2GaugeVolume Gap2GluingDerivation
  15open Gap2PostingCostDerivation GaugeHistoryMeasure
  16
  17/-! ## Axiom audit: every report-named theorem -/
  18
  19#print axioms surface_and_kindTotals_force_zero
  20#print axioms the_measure_is_exactly_the_gauge_divisor
  21#print axioms atom_normalizations_are_derived
  22#print axioms equivariance_is_not_load_bearing
  23#print axioms fixed_kind_totals_is_load_bearing
  24#print axioms bulk_cancellation_is_load_bearing
  25#print axioms purity_of_the_surface_term_is_load_bearing
  26#print axioms the_two_relaxations_cannot_be_combined
  27#print axioms the_letter_level_fibre_is_not_a_point
  28#print axioms surface_at_positive_dilates_forces_zero
  29#print axioms surfaceArea_and_kindTotals_force_zero
  30#print axioms surface_and_fixedKindTotals_force_zero_historyCost
  31#print axioms letterCostDichotomyVerdict
  32#print axioms indexTiltCost_not_equivariant
  33#print axioms surfaceCost_surfaceTotal
  34#print axioms surfaceCost_not_fixedKindTotals
  35#print axioms index_no_triple
  36#print axioms index_flag_unmoved
  37
  38/-! ## Quantifier shape of the headline (type-level, no Equivariant binder) -/
  39
  40/-- The headline binders are family + KindTotalRates + SurfaceTotal; no Equivariant. -/
  41theorem headline_binders_are_as_claimed :
  42    ∀ (F : CensusDilateFamily) (c : LetterCost) (cV cE cT a e : ℝ),
  43      KindTotalRates c cV cE cT → SurfaceTotal F c a e →
  44        cV = 0 ∧ cE = 0 ∧ cT = 0 ∧ a = 0 ∧ e = 0 :=
  45  fun F _c _ _ _ _ _ hk hs => surface_and_kindTotals_force_zero F hk hs
  46
  47/-- SurfaceTotal is universal in N, not a five-point sample. -/
  48theorem surfaceTotal_is_forall_N (F : CensusDilateFamily) (c : LetterCost) (a e : ℝ) :
  49    SurfaceTotal F c a e ↔
  50      ∀ N : ℕ, historyCost c (F.cap N) (F.K N) = a * (N : ℝ) ^ 3 + e :=
  51  Iff.rfl
  52
  53/-- The history-zero corollary really quantifies over every complex and cap. -/
  54theorem history_zero_is_global (F : CensusDilateFamily) {c : LetterCost} {a e : ℝ}
  55    (h : FixedKindTotals c) (hs : SurfaceTotal F c a e) :
  56    ∀ (B : ℕ) (K : BoundedComplex B), historyCost c B K = 0 :=
  57  surface_and_fixedKindTotals_force_zero_historyCost F h hs
  58
  59/-! ## Witness recomputation by the kernel -/
  60
  61/-- Census closed forms at N = 0..5, kernel-checked. -/
  62theorem census_samples :
  63    censusV 0 = 1 ∧ censusE 0 = 0 ∧ censusT 0 = 0 ∧
  64    censusV 1 = 16 ∧ censusE 1 = 65 ∧ censusT 1 = 24 ∧
  65    censusV 2 = 81 ∧ censusE 2 = 544 ∧ censusT 2 = 384 ∧
  66    censusV 3 = 256 ∧ censusE 3 = 2145 ∧ censusT 3 = 1944 ∧
  67    censusV 4 = 625 ∧ censusE 4 = 5936 ∧ censusT 4 = 6144 ∧
  68    censusV 5 = 1296 ∧ censusE 5 = 13345 ∧ censusT 5 = 15000 := by
  69  simp [censusV, censusE, censusT]
  70
  71
  72/-- Rates (1,0,-1/24) give 4N³+6N²+4N+1 on flatFamily at N=0..5. -/
  73theorem purity_witness_samples :
  74    (∀ N ∈ ([0,1,2,3,4,5] : List ℕ),
  75      historyCost (kindRateCost 1 0 (-(1/24))) (flatFamily.cap N) (flatFamily.K N)
  76        = 4 * (N : ℝ) ^ 3 + 6 * (N : ℝ) ^ 2 + 4 * (N : ℝ) + 1) := by
  77  intro N hN
  78  have := (purity_of_the_surface_term_is_load_bearing flatFamily).2.2.2 N
  79  exact this
  80
  81/-- Rates (1,-1,7/12) give -24N³-12N²+1 on flatFamily. -/
  82theorem combined_relaxation_witness (N : ℕ) :
  83    historyCost (kindRateCost 1 (-1) (7/12)) (flatFamily.cap N) (flatFamily.K N)
  84      = (-24) * (N : ℝ) ^ 3 + (-12) * (N : ℝ) ^ 2 + 1 :=
  85  (the_two_relaxations_cannot_be_combined flatFamily).2.2.2 N
  86
  87/-- surfaceCost t totals exactly t·N³ on the census family. -/
  88theorem surfaceCost_total_is_tN3 (t : ℝ) (N : ℕ) :
  89    historyCost (surfaceCost t) (flatFamily.cap N) (flatFamily.K N) = t * (N : ℝ) ^ 3 := by
  90  have := surfaceCost_surfaceTotal flatFamily t N
  91  simpa using this
  92
  93/-- indexTiltCost fails equivariance: concrete letter values on two-point dust. -/
  94theorem indexTilt_concrete_charges (t : ℝ) :
  95    indexTiltCost t 2 (dust 2) (Sum.inl v0Dust2) = t ∧
  96    indexTiltCost t 2 (dust 2) (Sum.inl v1Dust2) = -t :=
  97  ⟨indexTiltCost_at_v0 t, indexTiltCost_at_v1 t⟩
  98
  99theorem indexTilt_block_sums_zero (t : ℝ) :
 100    KindTotalRates (indexTiltCost t) 0 0 0 :=
 101  indexTiltCost_kindTotalRates t
 102
 103/-- kindRateCost 1 0 0 has history 1 on one-vertex dust and is not surface-total. -/
 104theorem bulk_witness_dust :
 105    historyCost (kindRateCost 1 0 0) 1 (dust 1) = 1 := by
 106  simpa using historyCost_kindRateCost_dust_one (1 : ℝ) 0 0
 107
 108theorem bulk_witness_not_surface :
 109    ¬ ∃ a e : ℝ, SurfaceTotal flatFamily (kindRateCost 1 0 0) a e :=
 110  (bulk_cancellation_is_load_bearing flatFamily).2.2.2
 111
 112/-- FixedKindTotals inhabited (nonzero rates) and fibre member inhabited. -/
 113theorem fixedKindTotals_inhabited :
 114    FixedKindTotals (kindRateCost 1 0 0) :=
 115  kindRateCost_fixedKindTotals 1 0 0
 116
 117theorem fibre_member_centered (t : ℝ) (ht : t ≠ 0) :
 118    Equivariant (centeredIncidenceCost t) ∧
 119    FixedKindTotals (centeredIncidenceCost t) ∧
 120    SurfaceTotal flatFamily (centeredIncidenceCost t) 0 0 ∧
 121    historyCost (centeredIncidenceCost t) 1 (dust 1) = 0 := by
 122  have h := the_letter_level_fibre_is_not_a_point flatFamily ht
 123  exact ⟨h.1, h.2.1, h.2.2.1, h.2.2.2.2 1 (dust 1)⟩
 124
 125/-- Flags unmoved, rfl-checked. -/
 126theorem flags_unmoved :
 127    dichotomyIndex.triple_derived = false ∧
 128    dichotomyIndex.measure_flag_moved = false ∧
 129    dichotomyIndex.equivariance_used = false :=
 130  ⟨index_no_triple, index_flag_unmoved, index_equivariance_unused⟩
 131
 132/-- Headline proof does not mention Equivariant in its type. -/
 133example : ∀ (F : CensusDilateFamily) {c : LetterCost} {cV cE cT a e : ℝ},
 134    KindTotalRates c cV cE cT → SurfaceTotal F c a e →
 135      cV = 0 ∧ cE = 0 ∧ cT = 0 ∧ a = 0 ∧ e = 0 :=
 136  surface_and_kindTotals_force_zero
 137
 138#print axioms headline_binders_are_as_claimed
 139#print axioms census_samples
 140#print axioms combined_relaxation_witness
 141#print axioms surfaceCost_total_is_tN3
 142#print axioms indexTilt_concrete_charges
 143#print axioms fibre_member_centered
 144#print axioms flags_unmoved
 145
 146end Gap2LetterCostDichotomyHostileProbe
 147end SevenGaps
 148end Gravity
 149end IndisputableMonolith
 150