IndisputableMonolith.Gravity.SevenGaps.Gap2IncidenceSilenceVerdict

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2DynamicsKindRule
   2import IndisputableMonolith.Gravity.SevenGaps.FullTheoryLedger
   3
   4/-!
   5# Gap 2 incidence-silence verdict: aggregate linearity is not forced
   6
   7The OPEN target `C-gap2-does-the-substrate-force-incidence-silence` asked whether
   8the ledger layer forces aggregate linearity by kind (`FixedKindTotals`) on the
   9posting cost. Letter-level incidence silence as the boundary premise is already
  10dead (`N-route-gap2-letter-level-incidence-silence-as-the-named-premise`). This
  11module banks the scoped no-go for the corrected aggregate question.
  12
  13**Verdict, stated first: no.** Across the three ledger layers the library
  14examines, nothing forces `FixedKindTotals` / counts-only:
  15
  161. **Letter-cost space** (`Gap2PostingCostDerivation`, `Gap2KindRule`):
  17   `pairCost` is equivariant and size-blind at totals, yet
  18   `¬ FixedKindTotals pairCost` (`costSizeBlind_not_fixedKindTotals`).
  192. **Lattice state type** (`Gap2LatticeKindRule`): incidence-reading lattice
  20   charges need not be counts-only.
  213. **Posting dynamics** (`Gap2DynamicsKindRule`): every nonnegative ledger is
  22   reachable; an explicit schedule on `twoBridges` is not counts-only
  23   (`ledger_forces_countsOnly_at_no_layer`).
  24
  25**Named further premises (not derived here).** Discharging aggregate linearity
  26or counts-only therefore needs structure the examined layers do not supply:
  27
  28* `CountsOnlySchedule`: a physical law about the actual posting run nature
  29  executes (named in `Gap2DynamicsKindRule`), not a theorem about the space of
  30  runs.
  31* Label indifference / Gibbs `1/|Aut|`: the measure-selection premise named by
  32  the A1.2 floor (`Gap2PostingLayerFloor`), independent of charge restrictions.
  33
  34**What this module does not do.** It does not flip
  35`gap2_measure_derived` (already true under its banked close). It does not revive
  36letter-level incidence silence as the boundary. It does not claim a deeper
  37layer than the posting step is impossible; it says the library carries none,
  38and the live form of the premise is physical rather than ledger-forced.
  39
  40Companion report:
  41`QG/attack_full_theory_20260729/A69_Gap2_Incidence_Silence_Verdict_20260804.html`.
  42-/
  43
  44namespace IndisputableMonolith
  45namespace Gravity
  46namespace SevenGaps
  47namespace Gap2IncidenceSilenceVerdict
  48
  49open PathSumMeasure ExactShellGaugePreflight GaugeHistoryMeasure
  50open Gap2SizeBlindnessReach
  51open Gap2PostingCostDerivation
  52open Gap2KindRule
  53open Gap2LatticeKindRule
  54open Gap2DynamicsKindRule
  55open FullTheoryLedger
  56
  57noncomputable section
  58
  59/-! ## §1. Letter-cost layer: FixedKindTotals is not forced -/
  60
  61/-- **SCOPED NO-GO (letter-cost layer).** Aggregate linearity by kind is not
  62forced among equivariant, total-size-blind letter costs: `pairCost` is a
  63witness with `¬ FixedKindTotals`. THEOREM (re-export with named scope). -/
  64theorem fixedKindTotals_not_forced_in_letter_cost :
  65    Equivariant pairCost ∧ CostSizeBlind pairCost ∧ ¬ FixedKindTotals pairCost :=
  66  ⟨pairCost_equivariant, costSizeBlind_not_fixedKindTotals.1,
  67    costSizeBlind_not_fixedKindTotals.2⟩
  68
  69/-- Kind-only fails independently by counting and by incidence. THEOREM. -/
  70theorem kind_rule_fails_twice :
  71    (Equivariant pairCost ∧ ¬ KindOnly pairCost ∧ CostSizeBlind pairCost) ∧
  72      (Equivariant (incidenceCost 1) ∧ ¬ KindOnly (incidenceCost 1)) :=
  73  ⟨kind_rule_fails_by_counting,
  74   ⟨incidenceCost_equivariant 1, incidenceCost_not_kindOnly one_ne_zero⟩⟩
  75
  76/-! ## §2. Three-layer ledger no-go (counts-only) -/
  77
  78/-- **SCOPED NO-GO (three layers).** Counts-only / aggregate-linearity forcing
  79fails at letter-cost, lattice, and dynamics layers already examined. THEOREM. -/
  80theorem ledger_does_not_force_countsOnly :
  81    (¬ ChargesCountsOnly (incidenceCost 1)) ∧
  82    (¬ ChargesCountsOnly (incidencePhiLattice.toLetterCost)) ∧
  83    (∃ (sched : Schedule (PostingAlphabet twoBridges)),
  84      ¬ CountsOnlySchedule twoBridges sched) :=
  85  ledger_forces_countsOnly_at_no_layer
  86
  87/-! ## §3. Named further premises -/
  88
  89/-- The physical schedule law named when dynamics fails to force counts-only. -/
  90def namedSchedulePremise : String :=
  91  "CountsOnlySchedule: law about the actual posting run, not the space of runs"
  92
  93/-- The measure-selection premise named by the A1.2 posting-layer floor. -/
  94def namedMeasurePremise : String :=
  95  "label indifference / Gibbs weight 1/|Aut K|"
  96
  97/-- Both named further premises the incidence-silence OPEN hands forward. -/
  98structure NamedFurtherPremises where
  99  schedule_law : String
 100  measure_selection : String
 101
 102def namedFurtherPremises : NamedFurtherPremises where
 103  schedule_law := namedSchedulePremise
 104  measure_selection := namedMeasurePremise
 105
 106/-! ## §4. Measure flag unmoved -/
 107
 108/-- `gap2_measure_derived` stays at its banked value; this verdict flips nothing.
 109THEOREM (`rfl`). -/
 110theorem gap2_measure_derived_unmoved :
 111    fullTheoryBenchmarks.gap2_measure_derived = true :=
 112  rfl
 113
 114/-! ## §5. Certificate -/
 115
 116structure IncidenceSilenceVerdictCert : Prop where
 117  fixedKindTotals_not_forced :
 118    Equivariant pairCost ∧ CostSizeBlind pairCost ∧ ¬ FixedKindTotals pairCost
 119  three_layer_nogo :
 120    (¬ ChargesCountsOnly (incidenceCost 1)) ∧
 121    (¬ ChargesCountsOnly (incidencePhiLattice.toLetterCost)) ∧
 122    (∃ (sched : Schedule (PostingAlphabet twoBridges)),
 123      ¬ CountsOnlySchedule twoBridges sched)
 124  measure_flag_unmoved :
 125    fullTheoryBenchmarks.gap2_measure_derived = true
 126  further_premises_named :
 127    namedFurtherPremises.schedule_law = namedSchedulePremise ∧
 128      namedFurtherPremises.measure_selection = namedMeasurePremise
 129
 130theorem incidenceSilenceVerdictCert : IncidenceSilenceVerdictCert where
 131  fixedKindTotals_not_forced := fixedKindTotals_not_forced_in_letter_cost
 132  three_layer_nogo := ledger_does_not_force_countsOnly
 133  measure_flag_unmoved := gap2_measure_derived_unmoved
 134  further_premises_named := ⟨rfl, rfl⟩
 135
 136end
 137end Gap2IncidenceSilenceVerdict
 138end SevenGaps
 139end Gravity
 140end IndisputableMonolith
 141