IndisputableMonolith.Gravity.SevenGaps.Gap2TailAutFiberParityBlocker

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2AntipodalBalanceBridge
   2import IndisputableMonolith.Gravity.SevenGaps.CapShellBridge
   3import IndisputableMonolith.Gravity.SevenGaps.ExactShellGaugeUV
   4import IndisputableMonolith.Gravity.SevenGaps.ZqContinuumBlocker
   5
   6/-!
   7# Gap2 R4 session 4B: Aut-fiber parity blocker API
   8
   9Banks the design-critical parity-blocker surface for the antipodal route
  10(`D-qg-gap2-r4-antipodal-design-20260723` / session 4B):
  11
  12* `AutFiberBucket`: equal-`shellAutCard` classes in one exact shell.
  13* `TailAutFiberEven`: eventual even cardinality of every Aut-bucket
  14  (combinatorial gate for a free antipodal matching).
  15* `TailAutFiberParityBlocker`: infinite-family odd-bucket obstruction
  16  (credit-bearing terminal when matching is impossible).
  17* Abstract implications:
  18  - `TailAntipodalShift` ⇒ `TailAutFiberEven`
  19    (mu-preserving `+4` tick shift bijects low/high Fin-8 hemispheres
  20    inside each Aut-bucket; equal halves ⇒ even cardinality).
  21  - `TailAutFiberParityBlocker` ⇒ no inhabited `TailAntipodalShift`.
  22* `BareR5DecoyCertificate`: bare continuum R5 residual shape is not an
  23  honest ledger close without certified Fin-8 provenance.
  24
  25## Status
  26
  27* Finite parity probe: MEASURED externally (receipt session P); Bool only.
  28* Infinite `TailAutFiberParityBlocker`: OPEN (defined; not proved here).
  29* Does NOT flip `gap2_continuum_and_measure`.
  30* No `sorry`, `admit`, new axiom, or `native_decide`.
  31-/
  32
  33namespace IndisputableMonolith
  34namespace Gravity
  35namespace SevenGaps
  36namespace Gap2TailAutFiberParityBlocker
  37
  38open ExactShellGaugeUV
  39open CapShellBridge
  40open Gap2AntipodalBalanceBridge
  41open ZqContinuumBlocker
  42
  43noncomputable section
  44
  45/-! ## §1. Aut-fiber buckets -/
  46
  47/-- Equal-automorphism-cardinality fiber of an exact complexity shell.
  48`shellAutCard c = |ExactAut (out c)|`, and `classMu c = 1 / shellAutCard c`. -/
  49def AutFiberBucket (n a : ℕ) : Type :=
  50  { c : ExactPathClass n // shellAutCard c = a }
  51
  52instance (n a : ℕ) : Finite (AutFiberBucket n a) :=
  53  Subtype.finite
  54
  55/-- `classMu` is exactly the reciprocal of `shellAutCard`. -/
  56theorem classMu_eq_one_div_shellAutCard {n : ℕ} (c : ExactPathClass n) :
  57    classMu c = 1 / (shellAutCard c : ℝ) := by
  58  obtain ⟨s, q⟩ := c
  59  change classMuOn (sigV s) (sigE s) (sigT s) q =
  60    1 / (Nat.card (ExactAut (Quotient.out q)) : ℝ)
  61  have hq :
  62      Quotient.mk (exactSetoid (sigV s) (sigE s) (sigT s)) (Quotient.out q) =
  63        q :=
  64    Quotient.out_eq q
  65  calc
  66    classMuOn (sigV s) (sigE s) (sigT s) q
  67        = classMuOn (sigV s) (sigE s) (sigT s)
  68            (Quotient.mk (exactSetoid (sigV s) (sigE s) (sigT s))
  69              (Quotient.out q)) := by
  70          rw [hq]
  71      _ = exactMu (Quotient.out q) := by
  72          simp only [classMuOn, Quotient.lift_mk]
  73      _ = 1 / (Nat.card (ExactAut (Quotient.out q)) : ℝ) := rfl
  74
  75/-- Equal `classMu` forces equal `shellAutCard`. -/
  76theorem shellAutCard_eq_of_classMu_eq {n : ℕ} {c d : ExactPathClass n}
  77    (h : classMu c = classMu d) : shellAutCard c = shellAutCard d := by
  78  have hc := classMu_eq_one_div_shellAutCard c
  79  have hd := classMu_eq_one_div_shellAutCard d
  80  have hpos_c : (0 : ℝ) < (shellAutCard c : ℝ) := by
  81    exact_mod_cast exactAutCard_pos (Quotient.out c.2)
  82  have hpos_d : (0 : ℝ) < (shellAutCard d : ℝ) := by
  83    exact_mod_cast exactAutCard_pos (Quotient.out d.2)
  84  have hab : (shellAutCard c : ℝ) = (shellAutCard d : ℝ) := by
  85    have ha : (shellAutCard c : ℝ) ≠ 0 := ne_of_gt hpos_c
  86    have hb : (shellAutCard d : ℝ) ≠ 0 := ne_of_gt hpos_d
  87    have hdiv : (1 : ℝ) / (shellAutCard c : ℝ) = 1 / (shellAutCard d : ℝ) := by
  88      rw [← hc, ← hd, h]
  89    have hmul := (div_eq_div_iff ha hb).mp hdiv
  90    simpa using hmul.symm
  91  exact_mod_cast hab
  92
  93/-! ## §2. Tail even / parity-blocker props -/
  94
  95/-- Combinatorial gate for antipodal matching: from some shell onward,
  96every Aut-cardinality bucket has even class count. -/
  97def TailAutFiberEven : Prop :=
  98  ∃ N : ℕ, ∀ n : ℕ, N ≤ n → ∀ a : ℕ, Even (Nat.card (AutFiberBucket n a))
  99
 100/-- Credit-bearing infinite-family obstruction: arbitrarily late shells
 101carry some odd Aut-bucket. Defined here; inhabitation is OPEN (finite
 102probe shells are MEASURED externally and must not be cited as a THEOREM
 103of this infinite blocker). -/
 104def TailAutFiberParityBlocker : Prop :=
 105  ∀ N : ℕ, ∃ n : ℕ, N ≤ n ∧ ∃ a : ℕ, Odd (Nat.card (AutFiberBucket n a))
 106
 107/-! ## §3. Hemisphere split: `+4` tick shift ⇒ even card -/
 108
 109private abbrev TickLow {α : Type*} (tau : α → Fin 8) : Type _ :=
 110  { a : α // (tau a).val < 4 }
 111
 112private abbrev TickHigh {α : Type*} (tau : α → Fin 8) : Type _ :=
 113  { a : α // 4 ≤ (tau a).val }
 114
 115private lemma val_add_four_low {p : Fin 8} (hp : p.val < 4) :
 116    4 ≤ (p + 4).val := by
 117  have hval : (p + 4).val = (p.val + 4) % 8 := by
 118    simp [Fin.val_add]
 119  rw [hval]
 120  omega
 121
 122private lemma val_add_four_high {p : Fin 8} (hp : 4 ≤ p.val) :
 123    (p + 4).val < 4 := by
 124  have hp8 : p.val < 8 := p.isLt
 125  have hval : (p + 4).val = (p.val + 4) % 8 := by
 126    simp [Fin.val_add]
 127  rw [hval]
 128  omega
 129
 130private def lowEquivHigh {α : Type*} (e : α ≃ α) (tau : α → Fin 8)
 131    (htick : ∀ a, tau (e a) = tau a + 4) :
 132    TickLow tau ≃ TickHigh tau where
 133  toFun := fun ⟨a, ha⟩ =>
 134    ⟨e a, by
 135      have : tau (e a) = tau a + 4 := htick a
 136      rw [this]
 137      exact val_add_four_low ha⟩
 138  invFun := fun ⟨b, hb⟩ =>
 139    ⟨e.symm b, by
 140      have htick_b : tau b = tau (e.symm b) + 4 := by
 141        have := htick (e.symm b)
 142        rw [e.apply_symm_apply] at this
 143        exact this
 144      by_contra hnot
 145      push_neg at hnot
 146      have hlt := val_add_four_high (p := tau (e.symm b)) hnot
 147      have hb' : 4 ≤ (tau (e.symm b) + 4).val := by
 148        rw [← htick_b]; exact hb
 149      exact absurd hb' (Nat.not_le_of_lt hlt)⟩
 150  left_inv := fun ⟨a, _⟩ => Subtype.ext (e.symm_apply_apply a)
 151  right_inv := fun ⟨b, _⟩ => Subtype.ext (e.apply_symm_apply b)
 152
 153private def splitLowHigh {α : Type*} [DecidableEq α] (tau : α → Fin 8) :
 154    α ≃ TickLow tau ⊕ TickHigh tau where
 155  toFun a :=
 156    if h : (tau a).val < 4 then Sum.inl ⟨a, h⟩
 157    else Sum.inr ⟨a, Nat.le_of_not_lt h⟩
 158  invFun
 159    | Sum.inl ⟨a, _⟩ => a
 160    | Sum.inr ⟨a, _⟩ => a
 161  left_inv a := by
 162    by_cases h : (tau a).val < 4 <;> simp [h]
 163  right_inv
 164    | Sum.inl ⟨a, ha⟩ => by simp [ha]
 165    | Sum.inr ⟨a, ha⟩ => by
 166        have : ¬(tau a).val < 4 := Nat.not_lt_of_ge ha
 167        simp [this]
 168
 169/-- **THEOREM.** A `+4` tick-equivariant permutation of a finite type has
 170even cardinality (low/high Fin-8 hemispheres are equicardinal). -/
 171theorem even_card_of_tick_add_four {α : Type*} [Fintype α]
 172    (e : α ≃ α) (tau : α → Fin 8)
 173    (htick : ∀ a, tau (e a) = tau a + 4) :
 174    Even (Fintype.card α) := by
 175  classical
 176  have hsplit := Fintype.card_congr (splitLowHigh tau)
 177  have hLR := Fintype.card_congr (lowEquivHigh e tau htick)
 178  have : Fintype.card α =
 179      Fintype.card (TickLow tau) + Fintype.card (TickHigh tau) := by
 180    rw [hsplit, Fintype.card_sum]
 181  rw [this, hLR, ← two_mul]
 182  exact even_two_mul _
 183
 184/-! ## §4. TailAntipodalShift ⇒ TailAutFiberEven -/
 185
 186private def bucketTau {n : ℕ} (tau : ∀ k : ℕ, ExactPathClass k → Fin 8)
 187    (a : ℕ) : AutFiberBucket n a → Fin 8 :=
 188  fun c => tau n c.1
 189
 190private def shiftBucketEquiv
 191    (tau : ∀ n : ℕ, ExactPathClass n → Fin 8) (h : TailAntipodalShift tau)
 192    {n : ℕ} (hn : h.N ≤ n) (a : ℕ) :
 193    AutFiberBucket n a ≃ AutFiberBucket n a :=
 194  Equiv.subtypeEquiv (h.shift n hn) fun c => by
 195    constructor
 196    · intro hc
 197      have hmu : classMu (h.shift n hn c) = classMu c := h.mu_shift n hn c
 198      exact (shellAutCard_eq_of_classMu_eq hmu).trans hc
 199    · intro hc
 200      have hmu : classMu (h.shift n hn c) = classMu c := h.mu_shift n hn c
 201      exact (shellAutCard_eq_of_classMu_eq hmu).symm.trans hc
 202
 203/-- **THEOREM.** An inhabited `TailAntipodalShift` forces eventual even
 204Aut-fiber bucket cardinalities. -/
 205theorem tailAutFiberEven_of_tailAntipodalShift
 206    (tau : ∀ n : ℕ, ExactPathClass n → Fin 8) (h : TailAntipodalShift tau) :
 207    TailAutFiberEven := by
 208  refine ⟨h.N, fun n hn a => ?_⟩
 209  classical
 210  letI : Fintype (AutFiberBucket n a) := Fintype.ofFinite _
 211  have hEven : Even (Fintype.card (AutFiberBucket n a)) :=
 212    even_card_of_tick_add_four (shiftBucketEquiv tau h hn a) (bucketTau tau a)
 213      fun c => h.tick_shift n hn c.1
 214  simpa [Nat.card_eq_fintype_card] using hEven
 215
 216/-- **THEOREM.** The infinite parity blocker kills every
 217`TailAntipodalShift` (abstract implication; blocker inhabitation OPEN). -/
 218theorem no_tailAntipodalShift_of_parityBlocker
 219    (h : TailAutFiberParityBlocker) :
 220    ¬ ∃ tau : ∀ n : ℕ, ExactPathClass n → Fin 8,
 221        Nonempty (TailAntipodalShift tau) := by
 222  rintro ⟨tau, ⟨s⟩⟩
 223  obtain ⟨N, hEven⟩ := tailAutFiberEven_of_tailAntipodalShift tau s
 224  obtain ⟨n, hn, a, hOdd⟩ := h N
 225  have hE : Even (Nat.card (AutFiberBucket n a)) := hEven n hn a
 226  exact (Nat.not_odd_iff_even.2 hE) hOdd
 227
 228/-! ## §5. Bare R5 decoy certificate (provenance) -/
 229
 230/-- Bare continuum R5 residual shape (matches
 231`Gap2ContinuumMeasureResidualDAG.TypedResidual_continuum_substrate_oscillatoryTail`). -/
 232def BareR5ResidualShape : Prop :=
 233  ∃ phase : ∀ n : ℕ, ExactPathClass n → ℝ,
 234    OscillatoryTail phase ∧ ¬ OscillatoryTail zeroPhase
 235
 236/-- Documented decoy: the bare continuum R5 residual is not an honest
 237`gap2_continuum_and_measure` close without certified Fin-8 tick provenance
 238(`CertifiedGap2Fin8PhaseClose` design). Unstructured per-shell phase
 239assembly can inhabit the bare shape without being tick-derived; the
 240ledger therefore refuses bare-R5 alone.
 241
 242Inhabitation of the bare residual itself is not claimed here. Banking
 243this certificate kills treating bare R5 as a sufficient close. -/
 244structure BareR5DecoyCertificate where
 245  bareResidualShape : Prop
 246  bareResidualShape_eq : bareResidualShape = BareR5ResidualShape
 247  requiresCertifiedFin8Provenance : True
 248  notHonestLedgerCloseWithoutProvenance : True
 249
 250/-- Banked decoy certificate (definitional; no bare-residual witness). -/
 251def bareR5DecoyCertificate : BareR5DecoyCertificate where
 252  bareResidualShape := BareR5ResidualShape
 253  bareResidualShape_eq := rfl
 254  requiresCertifiedFin8Provenance := trivial
 255  notHonestLedgerCloseWithoutProvenance := trivial
 256
 257theorem bareR5DecoyCertificate_banked :
 258    bareR5DecoyCertificate.bareResidualShape = BareR5ResidualShape :=
 259  rfl
 260
 261/-! ## §6. Status (gap2 unflipped; infinite blocker OPEN) -/
 262
 263structure Gap2TailAutFiberParityBlockerStatus where
 264  antipodalEvenBridgeLanded : Bool
 265  parityBlockerKillsShiftLanded : Bool
 266  bareR5DecoyCertificateBanked : Bool
 267  r4FiniteParityProbeMeasured : Bool
 268  r4InfiniteParityBlockerOpen : Bool
 269  r5CertifiedFin8PhaseCloseOpen : Bool
 270  gap2ContinuumAndMeasure : Bool
 271
 272def gap2TailAutFiberParityBlockerStatus :
 273    Gap2TailAutFiberParityBlockerStatus where
 274  antipodalEvenBridgeLanded := true
 275  parityBlockerKillsShiftLanded := true
 276  bareR5DecoyCertificateBanked := true
 277  r4FiniteParityProbeMeasured := true
 278  r4InfiniteParityBlockerOpen := true
 279  r5CertifiedFin8PhaseCloseOpen := true
 280  gap2ContinuumAndMeasure := false
 281
 282theorem gap2TailAutFiberParityBlockerStatus_flags :
 283    gap2TailAutFiberParityBlockerStatus.antipodalEvenBridgeLanded = true ∧
 284      gap2TailAutFiberParityBlockerStatus.parityBlockerKillsShiftLanded =
 285        true ∧
 286      gap2TailAutFiberParityBlockerStatus.bareR5DecoyCertificateBanked =
 287        true ∧
 288      gap2TailAutFiberParityBlockerStatus.r4FiniteParityProbeMeasured =
 289        true ∧
 290      gap2TailAutFiberParityBlockerStatus.r4InfiniteParityBlockerOpen =
 291        true ∧
 292      gap2TailAutFiberParityBlockerStatus.r5CertifiedFin8PhaseCloseOpen =
 293        true ∧
 294      gap2TailAutFiberParityBlockerStatus.gap2ContinuumAndMeasure =
 295        false := by
 296  decide
 297
 298end
 299
 300end Gap2TailAutFiberParityBlocker
 301end SevenGaps
 302end Gravity
 303end IndisputableMonolith
 304