/-
HachimojiN7Bridge.lean — Cross-check: HachimojiBase.card_eq ↔ n7_necessity

These two facts exist in separate modules:
  - HachimojiBase.card_eq      : Fintype.card HachimojiBase = 7   (CoreFormalism)
  - HachimojiN7.n7_necessity   : ∀ N, allOk N ↔ N = 7            (SilverSight)

They agree — but without this file they don't formally know about each other.
A session that modifies either (changes a predicate in n7_necessity, or adds a
constructor to HachimojiBase) breaks THIS theorem, providing a single point of
detection rather than two silently-diverging correct proofs.

Anti-drift role: this is the Ring 1 wire in the outward dependency spiral.
If it fails, stop and diagnose before touching anything downstream.
-/

import CoreFormalism.HachimojiManifoldAxiom
import SilverSight.HachimojiN7

open SilverSight.HachimojiN7

namespace SilverSight.HachimojiN7Bridge

-- ============================================================
-- §1  THE LINKING THEOREM
-- ============================================================

/-- The Hachimoji type's cardinality satisfies n7_necessity.
    Proof: card_eq gives 7; n7_necessity gives allOk 7 = true.
    If HachimojiBase gains or loses a constructor, card_eq changes,
    allOk (new count) = false, and this theorem breaks. -/
theorem hachimoji_card_matches_necessity :
    Fintype.card HachimojiBase = 7 ∧
    allOk (Fintype.card HachimojiBase) = true :=
  ⟨HachimojiBase.card_eq, by rw [HachimojiBase.card_eq]; exact n7_satisfies⟩

/-- Equivalently: the cardinality is the unique value satisfying all three constraints.
    This is the statement that the type IS the alphabet justified by n7_necessity. -/
theorem hachimoji_card_is_unique_valid :
    ∀ N : ℕ, allOk N = true ↔ N = Fintype.card HachimojiBase := by
  intro N
  rw [HachimojiBase.card_eq]
  exact n7_necessity N

-- ============================================================
-- §2  WITNESS
-- ============================================================

-- Belt-and-suspenders: both proofs evaluate to the same nat
#eval Fintype.card HachimojiBase  -- expect: 7
#eval allOk 7                     -- expect: true

end SilverSight.HachimojiN7Bridge