Theory Axiom_Free_Ontological_Trinity

(*
  Title:     Axiom_Free_Ontological_Trinity
  Author:     Yongdock Kim
  Date:       2026-03-16
  License:    BSD-3-Clause
 
  Abstract:
    This theory provides a formal verification of an axiom-free ontological argument
    and the necessity of the Trinity. Moving beyond traditional Anselmian "perfection,"
    this work defines a supreme truth (H) through the lens of "relative certainty"
    and epistemic possible-world semantics. Using Isabelle/HOL, we demonstrate that
    the unique logical fixed point satisfying maximal domain coverage and relational
    consistency is a triune structure (N=3). The proof is strictly definitional,
    avoiding the injection of external modal axioms (e.g., S5), thereby ensuring
    the structural integrity of the trinitarian closure within the U-layer logic.
*)
theory Axiom_Free_Ontological_Trinity
  imports Main

begin
(*
  =============================================================================
  PROJECT   : Formal Verification of the Ontological Argument and Trinity Necessity
  FRAMEWORK : U-layer Axiom-free Computational Metaphysics
  -----------------------------------------------------------------------------

  SUMMARY:
  This entry provides a purely definitional, axiom-free formalization of the
  ontological necessity of the Trinity (N = 3). By constructing a structural
  meritocracy on an abstract universe U, we demonstrate that the "Supreme Truth"
  (H_opt) uniquely converges to a triune configuration.

  1. CORE LOGIC PIPELINE (Purely Definitional & Order-Theoretic):
     • U-layer Foundations :  ⊢ (primitive) ⟹ SuppU ⟹ (preceq, approx)
     • Epistemic Mapping   :  Arg, Supports, ⋄e (Epistemic Possibility)
     • Maximality Criteria :  EH (Epistemic), PH (Philosophical), MaxNT (Relational)
     • Structural Pattern  :  Ternary Joint-Support (pair ⟶ third) Semantics

  2. AXIOMATIC AUDIT (Zero-Axiom Guarantee):
     • U-layer Logic       :  No user-added axiom. All results are definitionally derived over HOL(Main)
     • Modal Primitives    :  NONE. External modal postulates (e.g., S5) are avoided
                              to prevent "Modal Collapse."
     • Bridge Primitives   :  Arg is an uninterpreted bridge; no axioms are injected.

  3. KEY THEORETICAL ACHIEVEMENTS:
     • N = 3 Necessity     :  Mechanical exclusion of N = 1 (Singularity), N = 2 (Duality),
                              and N ≥ 4 (Indeterminacy) via "Trivial Collapse" proofs.
     • Consistency         :  Proof of consistency for H_opt via finite model search (Nitpick).
     • Non-modal Collapse        :  A reusable truthmaking pattern (T+S) that preserves
                              contingency for R, ensuring Trinity ⟹ ⋄R
                              without forcing Trinity ⟹ R.
     • Structural Irreducibility :  Ordinal/Cardinal argument showing that linear 3-element
                              orderings cannot preserve the triune joint-support symmetry.

  4. FILE ARCHITECTURE:
     • Formal Body         :  Ontological argument via Double Negation (DN).
     • Structuralism       :  Full U/EH/PH/Trinity machinery with "God Finality" wrapper.
     • Locales             :  Automated audit and discharge of core metaphysical constraints.
 
  =============================================================================
*)
section ‹1. Universe and primitive entailment›
text ‹We posit an abstract universe U and a primitive entailment @{text "⊢"} on U

  NOTICE: This entire development is strictly **axiom-free**.
  We do not use the ``axiom'' or any unproven modal postulates.
  All results are derived solely from definitions and the primitive entailment
  relation on the abstract universe U.
 ›

typedecl U
consts Entails :: "U ⇒ U ⇒ bool"  (infix "⊢" 60)


section ‹2. Support sets, preorder and equivalence on U›

definition SuppU :: "U ⇒ U set" where
  "SuppU u = {e. Entails e u}"

definition LeU :: "U ⇒ U ⇒ bool"  (infix "≼" 50) where
  "p ≼ q ⟷ SuppU p ⊆ SuppU q"

definition EqU :: "U ⇒ U ⇒ bool"  (infix "≈" 50) where
  "p ≈ q ⟷ SuppU p = SuppU q"


subsection ‹2.1  Basic calculus (preorder/equivalence; point tools)›

lemma LeU_refl[simp]: "p ≼ p" by (simp add: LeU_def)
lemma LeU_trans: "p ≼ q ⟹ q ≼ r ⟹ p ≼ r"
  by (simp add: LeU_def subset_trans)

lemma EqU_refl[simp]: "p ≈ p" by (simp add: EqU_def)
lemma EqU_sym:       "p ≈ q ⟹ q ≈ p" by (simp add: EqU_def)
lemma EqU_trans:     "p ≈ q ⟹ q ≈ r ⟹ p ≈ r" by (simp add: EqU_def)

lemma EqU_iff_sets: "p ≈ q ⟷ SuppU p = SuppU q"
  by (simp add: EqU_def)

lemma LeU_antisym_eq:
  assumes "p ≼ q" and "q ≼ p" shows "p ≈ q"
  using assms by (simp add: EqU_def LeU_def subset_antisym)

lemma EqU_iff_LeU_both: "p ≈ q ⟷ (p ≼ q ∧ q ≼ p)"
proof
  assume "p ≈ q"
  thus "p ≼ q ∧ q ≼ p" by (simp add: EqU_def LeU_def)
next
  assume "p ≼ q ∧ q ≼ p"
  then have "SuppU p ⊆ SuppU q" and "SuppU q ⊆ SuppU p"
    by (simp_all add: LeU_def)
  hence "SuppU p = SuppU q" by (rule subset_antisym)
  thus "p ≈ q" by (simp add: EqU_def)
qed

lemma SuppU_memI: "e ⊢ u ⟹ e ∈ SuppU u" by (simp add: SuppU_def)
lemma SuppU_memD: "e ∈ SuppU u ⟹ e ⊢ u" by (simp add: SuppU_def)

lemma LeU_pointI:
  assumes "∀e∈SuppU p. e ∈ SuppU q" shows "p ≼ q"
  using assms by (simp add: LeU_def subset_iff)

lemma le_pointwise:
  assumes "p ≼ q" and "e ⊢ p" shows "e ⊢ q"
proof -
  have "e ∈ SuppU p" using assms(2) by (simp add: SuppU_def)
  moreover from assms(1) have "SuppU p ⊆ SuppU q" by (simp add: LeU_def)
  ultimately have "e ∈ SuppU q" by blast
  thus "e ⊢ q" by (simp add: SuppU_def)
qed

named_theorems leU_pointwise_rules
lemmas le_pointwise_SuppU [leU_pointwise_rules] = le_pointwise


subsection ‹2.2  Useful @{text "≈"}-extensionality shifters›
lemma EqU_mono_left:  "p ≈ q ⟹ (p ≼ r) ⟷ (q ≼ r)" by (simp add: EqU_def LeU_def)
lemma EqU_mono_right: "p ≈ q ⟹ (r ≼ p) ⟷ (r ≼ q)" by (simp add: EqU_def LeU_def)
(* ===== strict order on U ===== *)
definition LtU :: "U ⇒ U ⇒ bool"  (infix "≺" 50) where
  "p ≺ q ⟷ (p ≼ q ∧ ¬ (q ≼ p))"


section ‹3. (Symbols only) Modal primitives for ``@{text "□"}/@{text "◇"}'' - no axioms here›
text ‹Several later definitions use the raw symbols ``@{text "□"}/@{text "◇"}'' syntactically (e.g., in
  generic ``truthmaking pattern'' locales). We introduce the symbols here as
  uninterpreted constants. Any S5-style axioms/rules appear.›

consts
  Box :: "bool ⇒ bool"  ("□ _" [60] 60)
  Dia :: "bool ⇒ bool"  ("◇ _" [60] 60)


section ‹4. Introduction of the Notion of ``Relative Certainty''(ReCert) ›
text‹ [Concept: Relative Certainty]
  ``P is relatively less certain than Q'' (denoted P @{text "≼"} Q) implies that
  the set of entailments supporting P is a subset of those supporting Q.
  Ontologically, this means Q is ``heavier'' or ``more fundamental'' than P,
  as Q is necessitated by every witness that necessitates P. ›


subsection ‹4.1  Bridge›
consts Arg :: "bool ⇒ U"

definition Supports :: "U ⇒ bool ⇒ bool" where
  "Supports e φ ≡ (e ⊢ Arg φ)"      (* φ holds at e *)

definition EDia :: "bool ⇒ bool"  ("◇⇩e _" [60]) where
  "◇⇩e ζ ≡ (∃e. Supports e ζ)"      (* epistemically possible *)

lemma epi_possible_supports_Arg: "◇⇩e ζ ⟹ ∃e. e ⊢ Arg ζ"
  by (simp add: EDia_def Supports_def)
(* --- Minimal bridge: Makes, point lemmas, and ≤ ↔ ∀e implication --- *)
definition Makes :: "U ⇒ bool ⇒ bool" where
  "Makes e X ≡ Supports e X"

lemma in_SuppU_Arg_iff [simp]:
  "e ∈ SuppU (Arg X) ⟷ Makes e X"
  unfolding SuppU_def Supports_def Makes_def by simp

lemma LeU_iff_all:
  "((Arg S) ≼ (Arg T)) ⟷ (∀e. Makes e S ⟶ Makes e T)"
  unfolding LeU_def SuppU_def Supports_def Makes_def by auto

lemma not_LeU_iff_exists_witness:
  "¬ ((Arg S) ≼ (Arg T)) ⟷ (∃a. Makes a S ∧ ¬ Makes a T)"
  by (simp add: LeU_iff_all)

corollary gap_equiv_witness_OmegaPsi_Phi':
  "¬ ((Arg (Ω ∧ Ψ)) ≼ (Arg Φ')) ⟷ (∃a. Makes a (Ω ∧ Ψ) ∧ ¬ Makes a Φ')"
  using not_LeU_iff_exists_witness[of "Ω ∧ Ψ" "Φ'"] by simp

lemma witness_breaks_back_imp:
  assumes "Makes a X" and "¬ Makes a Y"
  shows "¬ (∀e. Makes e X ⟶ Makes e Y)"
  using assms by blast
(* Strict order was defined earlier as LtU; define RelCert early (used later). *)
definition RelCert :: "bool ⇒ bool ⇒ bool" where
  "RelCert R S ≡ (Arg R) ≺ (Arg S)"

definition MoreCertain_pred :: "bool ⇒ bool ⇒ bool" where
  "MoreCertain_pred Φ' Φ ≡ (∀e. Makes e Φ' ⟶ Makes e Φ) ∧ ¬ (∀e. Makes e Φ ⟶ Makes e Φ')"


subsection ‹4.2  EH q: ``every epistemically possible truth support q''›

definition EH :: "U ⇒ bool" where
  "EH q ≡ (∀ζ. ◇⇩e ζ ⟶ (Arg ζ) ≼ q)"
text ‹[EH (Epistemic H)]
``Maximality over Epistemic Possibility''
A truth q satisfies EH if it serves as a necessary ground for every epistemically possible truth-bearer (@{text "◇"}\_e p).
(Definition: A truth-bearer p is epistemically possible if it has not yet been refuted by our current state of knowledge, thereby remaining a valid candidate for truth. This means that, regardless of whether p is inherently false or its negation simply remains unproven, from our current epistemic standpoint, its refutation is unknown.)
i.e., ``If it is epistemically possible, it is supported by q.''›

lemma EH_inclusion:
  assumes "EH q" "◇⇩e ζ" shows "(Arg ζ) ≼ q"
  using assms by (simp add: EH_def)

lemma EH_pointwise:
  assumes "EH q" "◇⇩e ζ" "Supports e ζ" shows "e ⊢ q"
proof -
  from EH_inclusion[OF assms(1,2)] have sub: "SuppU (Arg ζ) ⊆ SuppU q"
    by (simp add: LeU_def)
  from assms(3) have "e ∈ SuppU (Arg ζ)" by (simp add: Supports_def SuppU_def)
  hence "e ∈ SuppU q" using sub by blast
  thus "e ⊢ q" by (simp add: SuppU_def)
qed

lemma H_principle_from_EH_inclusion:
  assumes "EH (Arg Q)" "◇⇩e ζ" shows "(Arg ζ) ≼ (Arg Q)"
  using EH_inclusion[OF assms] .

lemma H_principle_from_EH_pointwise:
  assumes "EH (Arg Q)" "◇⇩e ζ" "Supports e ζ" shows "e ⊢ Arg Q"
  using EH_pointwise[OF assms] .

named_theorems EH_intros
lemmas EH_to_inclusion [EH_intros] = EH_inclusion
lemmas EH_to_pointwise [EH_intros] = EH_pointwise


section ‹5. Witness construction from the failure of EH ›
text‹
If a candidate q fails to satisfy EH, then there must exist an epistemically possible truth-bearer (denoted as @{text "ζ"}) that explicitly witnesses this failure by remaining unsupported by q.
›

theorem not_EH_witnessE:
  assumes "¬ EH q'" shows "∃ζ. ◇⇩e ζ ∧ ¬ ((Arg ζ) ≼ q')"
  using assms unfolding EH_def by blast

lemma witness_from_failure_of_EH:
  assumes "◇⇩e b" "◇⇩e c"
      and "(Arg b) ≼ (Arg a)" "(Arg c) ≼ (Arg a)"
      and "¬ ((Arg b) ≼ (Arg a')) ∨ ¬ ((Arg c) ≼ (Arg a'))"
  shows "¬ EH (Arg a')"
proof -
  have D: "¬ ((Arg b) ≼ (Arg a')) ∨ ¬ ((Arg c) ≼ (Arg a'))" using assms(5) by simp
  then show ?thesis
    proof
    assume L: "¬ ((Arg b) ≼ (Arg a'))"
    with assms(1) show ?thesis by (auto simp: EH_def)
  next
    assume R: "¬ ((Arg c) ≼ (Arg a'))"
    with assms(2) show ?thesis by (auto simp: EH_def)
  qed
qed


section ‹6. ``TrueNow'' basis: relative certainty via actual truths›
text ‹[TH (TrueNow H)]
  ``Maximality over Actuality''
  A truth q satisfies TH if it serves as a necessary ground for every truth-bearer that is actually true in the present world (TrueNow).
  (Definition: A truth-bearer p is ``TrueNow'' if it possesses an actualized truth value in our current reality (e0). Unlike epistemic possibility, which only requires the absence of refutation, TrueNow demands robust ontological actuality.)
  i.e., ``If it is an actualized truth, its ontological foundation is supported by q.''
  This firmly anchors the abstract universal logic (``U-layer'') to the concrete actual world (e0). ›

consts e0 :: U

definition TrueNow :: "bool ⇒ bool" where
  "TrueNow φ ≡ Supports e0 φ"

definition TSupp :: "U ⇒ bool set" where
  "TSupp q ≡ {φ. TrueNow φ ∧ (Arg φ) ≼ q}"

definition MoreCertainT :: "U ⇒ U ⇒ bool"  (infix "≺⇧T" 50) where
  "x ≺⇧T y ⟷ TSupp x ⊂ TSupp y"

definition TH :: "U ⇒ bool" where
  "TH q ≡ (∀φ. TrueNow φ ⟶ (Arg φ) ≼ q)"


subsection ‹6.1  Monotonicity and basic consequences›

lemma TSupp_mono:
  assumes "q ≼ r" shows "TSupp q ⊆ TSupp r"
proof
  fix φ assume "φ ∈ TSupp q"
  then have Tphi: "TrueNow φ" and A: "(Arg φ) ≼ q" by (simp_all add: TSupp_def)
  from LeU_trans[OF A assms] have "(Arg φ) ≼ r" .
  thus "φ ∈ TSupp r" using Tphi by (simp add: TSupp_def)
qed

lemma TSupp_strict_by_extra:
  assumes "TSupp x ⊆ TSupp y"
      and "TrueNow S" and "(Arg S) ≼ y" and "¬ ((Arg S) ≼ x)"
  shows "TSupp x ⊂ TSupp y"
proof (rule psubsetI)
  show "TSupp x ⊆ TSupp y" using assms(1) .
  have "S ∈ TSupp y" using assms(2,3) by (simp add: TSupp_def)
  moreover have "S ∉ TSupp x" using assms(2,4) by (simp add: TSupp_def)
  ultimately show "TSupp x ≠ TSupp y" by blast
qed

lemma more_true_supports_implies_less_than_T:
  assumes "TSupp (Arg Γ) ⊆ TSupp (Arg Φ)"
      and "TrueNow S" "(Arg S) ≼ (Arg Φ)" "¬ ((Arg S) ≼ (Arg Γ))"
  shows "(Arg Γ) ≺⇧T (Arg Φ)"
  unfolding MoreCertainT_def using TSupp_strict_by_extra[OF assms] .

lemma MoreCertainT_not_TH_left:
  assumes "(Arg Γ) ≺⇧T (Arg Φ)" shows "¬ TH (Arg Γ)"
proof
  assume "TH (Arg Γ)"
  then have A: "∀φ. TrueNow φ ⟶ (Arg φ) ≼ (Arg Γ)" by (simp add: TH_def)
  from assms have "TSupp (Arg Γ) ⊂ TSupp (Arg Φ)" by (simp add: MoreCertainT_def)
  then obtain S where Sin: "S ∈ TSupp (Arg Φ)" and Snot: "S ∉ TSupp (Arg Γ)"
    by (auto dest: psubsetD)
  from Sin have "TrueNow S" "(Arg S) ≼ (Arg Φ)" by (simp_all add: TSupp_def)
  from Snot have "¬ (TrueNow S ∧ (Arg S) ≼ (Arg Γ))" by (simp add: TSupp_def)
  with ‹TrueNow S› have "¬ ((Arg S) ≼ (Arg Γ))" by blast
  with A ‹TrueNow S› show False by blast
qed


section ‹7. Philosophical H (PH): ``PH q @{text "⟷"} (EH q @{text "∧"} TH q)''›
text ‹ [Definition: PH (Philosophical H)]
  ``Total Maximality (The Supreme Truth)''
  PH is the conjunction of EH and TH.
  A truth ``q'' satisfies PH if it grounds the entire domain of discourse (PDom),
  covering both what is ``Actually True'' and what is ``Epistemically Possible''.
 
  Formal Equivalence: PH q @{text "⟷"} (EH q AND TH q) ›

definition PDom :: "bool set" where
  "PDom ≡ {ζ. TrueNow ζ ∨ ◇⇩e ζ}"

definition PSupp :: "U ⇒ bool set" where
  "PSupp q ≡ {ζ. (TrueNow ζ ∨ ◇⇩e ζ) ∧ (Arg ζ) ≼ q}"

definition MoreCertainP :: "U ⇒ U ⇒ bool"  (infix "≺⇧P" 50) where
  "x ≺⇧P y ⟷ PSupp x ⊂ PSupp y"

definition PH :: "U ⇒ bool" where
  "PH q ≡ (∀ζ. (TrueNow ζ ∨ ◇⇩e ζ) ⟶ (Arg ζ) ≼ q)"


subsection ‹7.1  Basic facts, monotonicity, and extensionality›

lemma PH_imp_EH: "PH q ⟹ EH q" by (simp add: PH_def EH_def)
lemma PH_imp_TH: "PH q ⟹ TH q" by (simp add: PH_def TH_def)

lemma EH_TH_imp_PH:
  assumes "EH q" "TH q" shows "PH q"
proof -
  have "∀ζ. (TrueNow ζ ∨ ◇⇩e ζ) ⟶ (Arg ζ) ≼ q"
    using assms by (auto simp: EH_def TH_def)
  thus "PH q" by (simp add: PH_def)
qed

corollary PH_iff_EH_TH: "PH q ⟷ (EH q ∧ TH q)"
  using PH_imp_EH PH_imp_TH EH_TH_imp_PH by blast

lemma PH_pointwise_possible:
  assumes "PH q" "◇⇩e ζ" "Supports e ζ" shows "e ⊢ q"
  using assms PH_imp_EH EH_pointwise by blast

lemma PSupp_subset_PDom: "PSupp q ⊆ PDom" by (auto simp: PSupp_def PDom_def)

lemma PSupp_mono:
  assumes "q ≼ r" shows "PSupp q ⊆ PSupp r"
proof
  fix ζ assume "ζ ∈ PSupp q"
  then have D: "TrueNow ζ ∨ ◇⇩e ζ" and A: "(Arg ζ) ≼ q" by (simp_all add: PSupp_def)
  from LeU_trans[OF A assms] have "(Arg ζ) ≼ r" .
  thus "ζ ∈ PSupp r" using D by (simp add: PSupp_def)
qed

lemma PH_iff_PSupp_full: "PH q ⟷ PSupp q = PDom"
proof
  assume "PH q"
  then have A: "∀ζ. (TrueNow ζ ∨ ◇⇩e ζ) ⟶ (Arg ζ) ≼ q" by (simp add: PH_def)
  show "PSupp q = PDom"
  proof (intro set_eqI; intro iffI)
    fix ζ assume "ζ ∈ PSupp q"  thus "ζ ∈ PDom" by (simp add: PSupp_def PDom_def)
  next
    fix ζ assume "ζ ∈ PDom"
    then have D: "TrueNow ζ ∨ ◇⇩e ζ" by (simp add: PDom_def)
    hence "(Arg ζ) ≼ q" using A by blast
    thus "ζ ∈ PSupp q" using D by (simp add: PSupp_def)
  qed
next
  assume eq: "PSupp q = PDom"
  then show "PH q" unfolding PH_def PSupp_def PDom_def by blast
qed

lemma PH_no_strict_superior:
  assumes "PH q" shows "¬ (∃r. q ≺⇧P r)"
proof
  assume "∃r. q ≺⇧P r"
  then obtain r where r: "PSupp q ⊂ PSupp r" by (auto simp: MoreCertainP_def)
  from PH_iff_PSupp_full[of q] assms have eq: "PSupp q = PDom" by blast
  have "PDom ⊂ PSupp r" using r eq by simp
  then obtain ζ where "ζ ∈ PSupp r" and "ζ ∉ PDom" by (blast dest: psubsetD)
  from PSupp_subset_PDom[of r] have "PSupp r ⊆ PDom" .
  hence "ζ ∈ PDom" using ‹ζ ∈ PSupp r› by (rule subsetD)
  thus False using ‹ζ ∉ PDom› by blast
qed

lemma TSupp_extensional: "q ≈ r ⟹ TSupp q = TSupp r"
  by (intro set_eqI; simp add: TSupp_def EqU_mono_right)
lemma PSupp_extensional: "q ≈ r ⟹ PSupp q = PSupp r"
  by (intro set_eqI; simp add: PSupp_def EqU_mono_right)
lemma EH_extensional: "q ≈ r ⟹ EH q ⟷ EH r"
  by (simp add: EH_def EqU_mono_right)
lemma TH_extensional: "q ≈ r ⟹ TH q ⟷ TH r"
  by (simp add: TH_def EqU_mono_right)
lemma PH_extensional: "q ≈ r ⟹ PH q ⟷ PH r"
  by (simp add: PH_def EqU_mono_right)


section ‹7.2 Riemann toy (Core-only, no ontic bridge)›
text ‹
  Core layer only. Two U-points eI, eII and three propositions R, Phi, Phi'.
  We assume only local facts at eI. No ontic bridge (no Val/iw).
›

locale Riemann_Toy_Core =
  fixes eI eII :: U
    and R Phi Phi' :: bool
  assumes RI     : "Supports eI R"
      and RII    : "¬ Supports eII R"
      and PhiI   : "Supports eI Phi"
      and nPhiI' : "¬ Supports eI Phi'"
begin

text ‹Since R holds at eI, R is epistemically possible (EDia R).›
lemma EDia_R: "EDia R"
  using RI by (auto simp: EDia_def)

text ‹If Phi' fails at eI, then PH (Arg Phi') would contradict nPhiI'.›
lemma not_PH_of_Phi': "¬ PH (Arg Phi')"
proof
  assume "PH (Arg Phi')"
  have "eI ⊢ Arg Phi'"
  using PH_pointwise_possible[of ‹Arg Phi'› R eI] EDia_R RI ‹PH (Arg Phi')›
  by blast

  hence "Supports eI Phi'"
    by (simp add: Supports_def)
  thus False using nPhiI' by contradiction
qed

text ‹Helper: at eI, both R and Phi hold (just local evidence).›
lemma both_at_eI: "Supports eI R ∧ Supports eI Phi"
  using RI PhiI by simp

end


subsection ‹7.3 The H-principle: Structual Properties of Strict Subordination›
text ‹
  Below\_on K e : e is in PDom and Arg e @{text "≺"} Arg K (strictly less certain than K).
  H\_principle K Q : every such e supports Q (i.e., Arg e @{text "≼"} Q).
›

definition Below_on :: "bool ⇒ bool ⇒ bool" where
  "Below_on K e ≡ (e ∈ PDom ∧ (Arg e) ≺ (Arg K))"

definition H_principle :: "bool ⇒ U ⇒ bool" where
  "H_principle K Q ≡ (∀e. Below_on K e ⟶ (Arg e) ≼ Q)"

text ‹Minimal form: for Q = Arg K it follows immediately from the definition of @{text "≺"}.›
lemma H_principle_self:
  shows "H_principle K (Arg K)"
  unfolding H_principle_def Below_on_def
  by (intro allI impI; simp add: LtU_def)

text ‹It also transfers to any Q that is EqU-equivalent to Arg K.›
lemma H_principle_of_EqU:
  assumes "Q ≈ (Arg K)"
  shows   "H_principle K Q"
  unfolding H_principle_def Below_on_def
proof (intro allI impI)
  fix e assume "e ∈ PDom ∧ (Arg e) ≺ (Arg K)"
  then have "(Arg e) ≼ (Arg K)" by (simp add: LtU_def)
  moreover from assms have "(Arg K) ≼ Q" by (simp add: EqU_iff_LeU_both)
  ultimately show "(Arg e) ≼ Q" by (meson LeU_trans)
qed


section ‹8. Epistemic Frame: Definition of H\_negU\_strict and Derivation of EH›

subsection ‹8.1 Strong negative-form H (ban all equivalence/superiority; includes a non-vacuity guard)›

definition H_negU_strict :: "bool ⇒ bool" where
  "H_negU_strict q ≡
         (∀ζ∈PDom. ζ ≠ q ⟶ ¬ ((Arg q) ≺ (Arg ζ)))"

lemma H_negU_strict_no_at_or_above:
  assumes "H_negU_strict q" "ζ ∈ PDom" "ζ ≠ q"
  shows "¬ ((Arg q) ≺ (Arg ζ))"
  using assms by (simp add: H_negU_strict_def)

lemma possible_in_PDom: "◇⇩e ζ ⟹ ζ ∈ PDom"
  by (simp add: PDom_def)


subsection ‹8.2 Hmax: ``all current truths supported (TH) + strong negative-form''›

definition Hmax :: "bool ⇒ bool" where
  "Hmax q ≡ TH (Arg q) ∧ H_negU_strict q"

lemma Hmax_imp_TH: "Hmax q ⟹ TH (Arg q)"
  by (simp add: Hmax_def)

lemma Hmax_blocks_tautology:
  assumes "Hmax q" "q ≠ True" "◇⇩e True"
  shows "¬ ((Arg q) ≺ (Arg True))"
  using assms by (simp add: Hmax_def H_negU_strict_def PDom_def)


subsection ‹8.3 Strict epistemic variants: ``currently true'' excluded›
(* Possible but excluding what is currently true *)
definition EDia_strict :: "bool ⇒ bool" where
  "EDia_strict ζ ≡ EDia ζ ∧ ¬ TrueNow ζ"

notation EDia_strict ("◇⇩e' _" [60] 60)

lemma EDia_strict_imp_EDia: "EDia_strict ζ ⟹ EDia ζ"
  by (simp add: EDia_strict_def)

lemma TrueNow_imp_not_EDia_strict: "TrueNow ζ ⟹ ¬ EDia_strict ζ"
  by (simp add: EDia_strict_def)

text ‹Strict version of EH: covers only epistemic possibilities that are not currently true(TrueNow).›
definition EH_strict :: "U ⇒ bool" where
  "EH_strict q ≡ (∀ζ. EDia_strict ζ ⟶ (Arg ζ) ≼ q)"

lemma EH_imp_EH_strict: "EH q ⟹ EH_strict q"
  unfolding EH_def EH_strict_def EDia_strict_def by blast


lemma TrueNow_implies_EDia: "TrueNow ζ ⟹ EDia ζ"
  unfolding TrueNow_def EDia_def Supports_def by auto

lemma EH_from_strict_plus_TH:
  assumes "EH_strict q" and "TH q"
  shows "EH q"
  unfolding EH_def
proof (intro allI impI)
  fix ζ assume "EDia ζ"
  show "(Arg ζ) ≼ q"
  proof (cases "TrueNow ζ")
    case True
    with assms(2) show ?thesis by (simp add: TH_def)
  next
    case False
    from ‹EDia ζ› False have "EDia_strict ζ"
      by (simp add: EDia_strict_def)
    with assms(1) show ?thesis by (simp add: EH_strict_def)
  qed
qed


subsection ‹8.4 PDom/PSupp (strict version)›

definition PDom_strict :: "bool set" where
  "PDom_strict ≡ {ζ. TrueNow ζ ∨ EDia_strict ζ}"

definition PSupp_strict :: "U ⇒ bool set" where
  "PSupp_strict q ≡ {ζ. (TrueNow ζ ∨ EDia_strict ζ) ∧ (Arg ζ) ≼ q}"

lemma PSupp_strict_subset_PDom_strict: "PSupp_strict q ⊆ PDom_strict"
  by (auto simp: PSupp_strict_def PDom_strict_def)

lemma PSupp_strict_mono:
  assumes "q ≼ r" shows "PSupp_strict q ⊆ PSupp_strict r"
proof
  fix ζ assume "ζ ∈ PSupp_strict q"
  then have D: "TrueNow ζ ∨ EDia_strict ζ" and Aq: "(Arg ζ) ≼ q"
    by (simp_all add: PSupp_strict_def)
  from LeU_trans[OF Aq assms] have "(Arg ζ) ≼ r" .
  thus "ζ ∈ PSupp_strict r" using D by (simp add: PSupp_strict_def)
qed


subsection ‹8.5 PH(strict)›
text ‹Strict version of PH.›

definition PH_strict :: "U ⇒ bool" where
  "PH_strict q ≡ (∀ζ. (TrueNow ζ ∨ EDia_strict ζ) ⟶ (Arg ζ) ≼ q)"

lemma PH_strict_imp_TH: "PH_strict q ⟹ TH q"
  unfolding PH_strict_def TH_def by blast

lemma PH_strict_imp_EH_strict: "PH_strict q ⟹ EH_strict q"
  unfolding PH_strict_def EH_strict_def by blast

lemma TH_EHstrict_imp_PH_strict: "TH q ⟹ EH_strict q ⟹ PH_strict q"
  unfolding TH_def EH_strict_def PH_strict_def by blast

lemma PH_imp_PH_strict: "PH q ⟹ PH_strict q"
  unfolding PH_def PH_strict_def EDia_strict_def by blast

text ‹Equivalence with PSupp/PDom (strict).›
lemma PH_strict_iff_PSupp_strict_full:
  "PH_strict q ⟷ PSupp_strict q = PDom_strict"
proof
  assume H: "PH_strict q"
  then have A: "∀ζ. (TrueNow ζ ∨ EDia_strict ζ) ⟶ (Arg ζ) ≼ q"
    by (simp add: PH_strict_def)
  show "PSupp_strict q = PDom_strict"
  proof (intro set_eqI; intro iffI)
    fix ζ assume "ζ ∈ PSupp_strict q"
    thus "ζ ∈ PDom_strict"
      by (simp add: PSupp_strict_def PDom_strict_def)
  next
    fix ζ assume "ζ ∈ PDom_strict"
    then have D: "TrueNow ζ ∨ EDia_strict ζ"
      by (simp add: PDom_strict_def)
    with A have "(Arg ζ) ≼ q" by blast
    thus "ζ ∈ PSupp_strict q"
      using D by (simp add: PSupp_strict_def)
  qed
next
  assume eq: "PSupp_strict q = PDom_strict"
  show "PH_strict q"
  unfolding PH_strict_def
  proof (intro allI impI)
    fix ζ assume H: "TrueNow ζ ∨ EDia_strict ζ"
    have "ζ ∈ PDom_strict" using H by (simp add: PDom_strict_def)
    with eq have "ζ ∈ PSupp_strict q" by simp
    thus "(Arg ζ) ≼ q" by (simp add: PSupp_strict_def)
  qed
qed

text ‹Extensionality.›
lemma PH_strict_extensional:
  assumes "q ≈ r"
  shows   "PH_strict q ⟷ PH_strict r"
proof
  assume Hq: "PH_strict q"
  have "∀ζ. (TrueNow ζ ∨ EDia_strict ζ) ⟶ (Arg ζ) ≼ r"
    using Hq assms by (simp add: PH_strict_def EqU_mono_right)
  thus "PH_strict r" by (simp add: PH_strict_def)
next
  assume Hr: "PH_strict r"
  have "∀ζ. (TrueNow ζ ∨ EDia_strict ζ) ⟶ (Arg ζ) ≼ q"
    using Hr assms by (simp add: PH_strict_def EqU_mono_right)
  thus "PH_strict q" by (simp add: PH_strict_def)
qed

lemma PSupp_strict_extensional:
  assumes "q ≈ r"
  shows   "PSupp_strict q = PSupp_strict r"
proof (intro set_eqI)
  fix ζ
  have "(Arg ζ) ≼ q ⟷ (Arg ζ) ≼ r"
    using assms by (simp add: EqU_mono_right)
  thus "ζ ∈ PSupp_strict q ⟷ ζ ∈ PSupp_strict r"
    by (simp add: PSupp_strict_def)
qed


subsection ‹8.6 TH (one-way) and TSupp maximality: True vs q superiority›
text ‹We adopt **only one direction**:
  TH q @{text "⟹"} (@{text "∀"}x. TSupp x @{text "⊆"} TSupp q).›

lemma TH_implies_TSupp_max:
  assumes "TH q"
  shows "∀x. TSupp x ⊆ TSupp q"
proof
  fix x
  show "TSupp x ⊆ TSupp q"
  proof
    fix φ assume "φ ∈ TSupp x"
    then have T: "TrueNow φ" and Ax: "(Arg φ) ≼ x"
      by (simp_all add: TSupp_def)
    from assms T have "(Arg φ) ≼ q"
      by (simp add: TH_def)
    thus "φ ∈ TSupp q" using T by (simp add: TSupp_def)
  qed
qed

lemma Hmax_to_TSupp_max:
  assumes "Hmax q"
  shows "∀x. TSupp x ⊆ TSupp (Arg q)"
  using assms by (simp add: Hmax_def TH_implies_TSupp_max)


section ‹9. PDom-robustness lemmas + H\_opt @{text "⟹"} EH/TH/PH›
text ‹EDia/TrueNow imply inclusion into PDom; impossibility (@{text "¬"} EDia) is a trivial lower bound; and EH( @{text "⟹"} TH.›

lemma EDia_in_PDom' [simp]: "EDia ζ ⟹ ζ ∈ PDom"
  by (simp add: PDom_def)

lemma TrueNow_in_PDom' [simp]: "TrueNow ζ ⟹ ζ ∈ PDom"
  by (simp add: PDom_def)

lemma not_EDia_le_any:
  assumes "¬ EDia ζ"
  shows   "(Arg ζ) ≼ q"
  using assms
  unfolding LeU_def SuppU_def EDia_def Supports_def by auto

lemma EH_implies_TH:
  assumes "EH q"
  shows   "TH q"
  using assms
  unfolding EH_def TH_def
  using TrueNow_implies_EDia by blast

text ‹If EH fails, there exists a possible-true counterexample (i.e., failure of top-coverage over PDom).›
lemma not_EH_on_Arg_witness:
  assumes "¬ EH (Arg q)"
  shows   "∃ζ. EDia ζ ∧ ¬ ((Arg ζ) ≼ (Arg q))"
  using assms not_EH_witnessE by blast


subsection ‹9.1 Definition of H\_opt: strict anti-above + maximal nontrivial support›
text ‹
Maximizing Nontrivial Relational Supports among Heads.
We compare heads based on the cardinality of their nontrivial incoming support sets.

A support is defined as **nontrivial** into C only for patterns Arg(A @{text "∧"} B) @{text "≼"} Arg(C)
where A, B, and C are distinct (A @{text "≠"} B, A @{text "≠"} C, and B @{text "≠"} C).
Crucially, this excludes trivial logical properties such as plain @{text "∧"}-elimination
into one of the conjuncts.

MaxNT q signifies that q is a head whose set of nontrivial incoming edges
is cardinally at least as large as that of any other head (in the injection sense).
This identifies the most relationally coherent and robust truth structure.›

definition Head :: "bool ⇒ bool" where
  "Head q ≡ H_negU_strict q"

definition NT_pair_support :: "bool ⇒ bool ⇒ bool ⇒ bool" where
  "NT_pair_support A B C ≡
     A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ (Arg (A ∧ B) ≼ Arg C)"

definition NT_in_edges :: "bool ⇒ (bool × bool) set" where
  "NT_in_edges C ≡
     {(A,B). Head A ∧ Head B ∧ Head C ∧ NT_pair_support A B C}"
(* --- Cantor-style cardinal comparison via injections --- *)
definition le_card :: "'a set ⇒ 'b set ⇒ bool"  (infix "≼⇩c" 50) where
  "A ≼⇩c B ⟷ (∃f. inj_on f A ∧ f ` A ⊆ B)"

definition lt_card :: "'a set ⇒ 'b set ⇒ bool"  (infix "≺⇩c" 50) where
  "A ≺⇩c B ⟷ (A ≼⇩c B ∧ ¬ (B ≼⇩c A))"

definition eq_card :: "'a set ⇒ 'b set ⇒ bool"  (infix "≈⇩c" 50) where
  "A ≈⇩c B ⟷ (A ≼⇩c B ∧ B ≼⇩c A)"

lemma le_card_empty_left: "{} ≼⇩c B"
  unfolding le_card_def
  by (rule exI[where x="λx. undefined"]; auto)

definition MaxNT :: "bool ⇒ bool" where
  "MaxNT q ≡
     Head q ∧
     (∀r. Head r ⟶ NT_in_edges r ≼⇩c NT_in_edges q)"

definition H_opt :: "bool ⇒ bool" where
  "H_opt q ≡ MaxNT q"


subsection ‹9.2 Consequences of H\_opt (Cantor-size / MaxNT version)›

lemma Hopt_to_MaxNT:
  assumes HQ: "H_opt q"
  shows "MaxNT q"
  using HQ by (simp add: H_opt_def)

lemma NT_in_edges_empty_if_not_Head:
  assumes NH: "¬ Head C"
  shows "NT_in_edges C = {}"
  using NH by (auto simp: NT_in_edges_def)

lemma Hopt_score_ge_in_PDom:
  assumes HQ: "H_opt q" and Zin: "z ∈ PDom"
  shows "NT_in_edges z ≼⇩c NT_in_edges q"
proof (cases "Head z")
  case True
  have Bound: "∀r. Head r ⟶ NT_in_edges r ≼⇩c NT_in_edges q"
    using Hopt_to_MaxNT[OF HQ] by (auto simp: MaxNT_def)
  show ?thesis using Bound True by blast
next
  case False
  have "NT_in_edges z = {}" using NT_in_edges_empty_if_not_Head[OF False] .
  thus ?thesis using le_card_empty_left by simp
qed

lemma Hopt_score_tie:
  assumes HA: "H_opt A" and HB: "H_opt B"
  shows "NT_in_edges A ≈⇩c NT_in_edges B"
proof -
  have HeadA: "Head A" and HeadB: "Head B"
    using HA HB by (auto simp: H_opt_def MaxNT_def)

  have AB: "NT_in_edges A ≼⇩c NT_in_edges B"
    using HB HeadA by (auto simp: H_opt_def MaxNT_def)
  have BA: "NT_in_edges B ≼⇩c NT_in_edges A"
    using HA HeadB by (auto simp: H_opt_def MaxNT_def)

  show ?thesis by (simp add: eq_card_def AB BA)
qed


text ‹If H\_opt holds for K, the minimal form above also follows automatically.›
lemma Hopt_implies_H_principle:
  assumes "H_opt K"
  shows   "H_principle K (Arg K)"
  using H_principle_self by simp

lemma Hopt_implies_H_principle_EqU:
  assumes "H_opt K" "Q ≈ (Arg K)"
  shows   "H_principle K Q"
  using H_principle_of_EqU assms(2) by blast


subsection ‹9.3 Consistency of H\_opt (Cantor-size version)›

lemma Hopt_has_no_strictly_better_in_PDom:
  assumes HQ: "H_opt q"
  shows "¬ (∃z∈PDom. NT_in_edges q ≺⇩c NT_in_edges z)"
proof
  assume "∃z∈PDom. NT_in_edges q ≺⇩c NT_in_edges z"
  then obtain z where Zin: "z ∈ PDom" and lt: "NT_in_edges q ≺⇩c NT_in_edges z"
    by blast

  have ge: "NT_in_edges z ≼⇩c NT_in_edges q"
    using Hopt_score_ge_in_PDom[OF HQ Zin] .

  from lt have nz: "¬ (NT_in_edges z ≼⇩c NT_in_edges q)"
    by (simp add: lt_card_def)

  show False using ge nz by contradiction
qed

text ‹
The consistency result for @{term H_opt} is purely order-theoretic (MaxNT) and
does not require @{term "q"}(the argument of H\_opt) to be a tautology.  In particular,
even under the extra assumption @{term "q ≠ True"}, the same conclusion holds.
›
corollary Hopt_has_no_strictly_better_in_PDom_non_tautology:
  assumes HQ: "H_opt q"
      and nT: "q ≠ True"
  shows "¬ (∃z∈PDom. NT_in_edges q ≺⇩c NT_in_edges z)"
  using Hopt_has_no_strictly_better_in_PDom[OF HQ] .

subsection ‹9.4 Finality (H\_opt): No argument strictly above an H\_opt truth (proof route)›
text ‹If H\_opt q holds, then Arg q is final within PDom: no proposition in PDom has an
argument strictly above Arg q. The proof route is immediate: H\_opt q entails
H\_negU\_strict q, and H\_negU\_strict q already excludes any @{text "ζ"} @{text "∈"} PDom such that
Arg q @{text "≺"} Arg @{text "ζ"}. Hence no PDom-based definition can designate a proposition
strictly superior to q in argument strength; the search for a strictly higher
truth terminates at H\_opt.›

lemma argument_finality_PDom:
  assumes HQ: "H_opt q"
  shows "∀ζ∈PDom. ¬ ((Arg q) ≺ (Arg ζ))"
proof (intro ballI)
  fix ζ assume Zin: "ζ ∈ PDom"
  have HN: "H_negU_strict q"
    using HQ by (auto simp: H_opt_def MaxNT_def Head_def)
  show "¬ ((Arg q) ≺ (Arg ζ))"
  proof (cases "ζ = q")
    case True
    then show ?thesis by (simp add: LtU_def)
  next
    case False
    then show ?thesis using HN Zin by (simp add: H_negU_strict_def)
  qed
qed

text ‹If a definition D only ranges over PDom, then it cannot designate an argument strictly superior to Arg q under H\_opt q.›
lemma argument_finality_for_defs:
  assumes HQ: "H_opt q"
      and Drng: "∀r. D r ⟶ r ∈ PDom"
  shows "¬ (∃r. D r ∧ (Arg q) ≺ (Arg r))"
proof
  assume "∃r. D r ∧ (Arg q) ≺ (Arg r)"
  then obtain r where Dr: "D r" and Lt: "(Arg q) ≺ (Arg r)" by blast
  from Drng Dr have Rin: "r ∈ PDom" by blast
  from argument_finality_PDom[OF HQ] Rin have "¬ ((Arg q) ≺ (Arg r))" by blast
  with Lt show False by blast
qed

text ‹Pointwise corollaries.›
corollary argument_finality_point:
  assumes HQ: "H_opt q" and Rin: "r ∈ PDom"
  shows "¬ ((Arg q) ≺ (Arg r))"
  using argument_finality_PDom[OF HQ] Rin by blast

corollary argument_finality_possible:
  assumes HQ: "H_opt q" and Er: "EDia r"
  shows "¬ ((Arg q) ≺ (Arg r))"
proof -
  have Rin: "r ∈ PDom"
    using Er by (auto simp: PDom_def EDia_def TrueNow_def)
  show ?thesis using argument_finality_PDom[OF HQ] Rin by blast
qed

corollary argument_finality_true:
  assumes HQ: "H_opt q" and Tr: "TrueNow r"
  shows "¬ ((Arg q) ≺ (Arg r))"
proof -
  have Rin: "r ∈ PDom"
    using Tr by (auto simp: PDom_def TrueNow_def EDia_def)
  show ?thesis using argument_finality_PDom[OF HQ] Rin by blast
qed

corollary no_definition_strictly_superior_than_H_opt:
  assumes HQ: "H_opt q" and Drng: "∀r. D r ⟶ r ∈ PDom"
  shows "¬ (∃r. D r ∧ (Arg q) ≺ (Arg r))"
  using argument_finality_for_defs[OF HQ Drng] .

subsection ‹9.5 Flat-model consistency witness for ‹∃q. H_opt q››
text ‹
  Purpose. Provide a concrete toy model (one-point world, always-true entailment,
  constant ‹Arg›) in which ‹H_opt q› holds for any ‹q›. This shows the existential
  ‹∃q. H_opt q› is satisfiable (hence not explosive) relative to the U-style
  definitions below, without touching the main development.

  **This adds no axioms; purely a satisfiability witness.**

  **Not a semantics claim.** The construction is intentionally ``flat''
  (single world; entailment always true), so many propositions come out trivially true.
  It is **not** offered as an intended or endorsable semantics of the main theory,
  but solely as a **consistency witness**: there exists at least one interpretation
  making @{text "<exists>"}H\_opt q true without contradiction.

  **No dependency back into the core.** No main lemma or theorem should depend on
  this appendix. Keep it documentation/check-only, so the core results cannot be
  criticized as relying on a trivial model.
›

text ‹Concrete flat model **without** locales/interpretations (zero friction).›
type_synonym U1 = unit
(* Flat Arg / order: everything is equal, so ≤ is always true and < is always false. *)
definition Arg_F :: "bool ⇒ U1" where
  "Arg_F _ ≡ ()"

definition Le_F :: "U1 ⇒ U1 ⇒ bool" where
  "Le_F _ _ ≡ True"

definition Lt_F :: "U1 ⇒ U1 ⇒ bool" where
  "Lt_F p q ≡ Le_F p q ∧ ¬ Le_F q p"

lemma Le_F_true[simp]: "Le_F p q"
  by (simp add: Le_F_def)

lemma not_Lt_F[simp]: "¬ Lt_F p q"
  by (simp add: Lt_F_def Le_F_def)
(* PDom in the flat witness: everything is in the domain. *)
definition PDom_F :: "bool set" where
  "PDom_F ≡ UNIV"

lemma PDom_F_all[simp]: "z ∈ PDom_F"
  by (simp add: PDom_F_def)
(* Head filter in the MaxNT development: anti-above on PDom (always satisfied here). *)
definition H_negU_strict_F :: "bool ⇒ bool" where
  "H_negU_strict_F q ≡
     (∀z∈PDom_F. z ≠ q ⟶ ¬ (Lt_F (Arg_F q) (Arg_F z)))"

definition Head_F :: "bool ⇒ bool" where
  "Head_F q ≡ H_negU_strict_F q"

lemma Head_F_true[simp]: "Head_F q"
  by (simp add: Head_F_def H_negU_strict_F_def)
(* Nontrivial pair-support among heads (same shape as MaxNT definition). *)
definition NT_pair_support_F :: "bool ⇒ bool ⇒ bool ⇒ bool" where
  "NT_pair_support_F A B C ≡
     A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ (Le_F (Arg_F (A ∧ B)) (Arg_F C))"

definition NT_in_edges_F :: "bool ⇒ (bool × bool) set" where
  "NT_in_edges_F C ≡
     {(A,B). Head_F A ∧ Head_F B ∧ Head_F C ∧ NT_pair_support_F A B C}"
(* Helper: no three distinct booleans exist. *)
lemma no_three_distinct_bools:
  fixes A B C :: bool
  shows "A = B ∨ A = C ∨ B = C"
  by (cases A; cases B; cases C; auto)

lemma NT_pair_support_F_false[simp]: "¬ NT_pair_support_F A B C"
  by (simp add: NT_pair_support_F_def no_three_distinct_bools)

lemma NT_in_edges_F_empty[simp]: "NT_in_edges_F C = {}"
  by (auto simp: NT_in_edges_F_def)
(* Cardinal comparison reflexivity (handy for MaxNT). *)
lemma le_card_refl: "X ≼⇩c X"
  unfolding le_card_def
  by (rule exI[where x="λx. x"]; auto)
(* MaxNT / H_opt shape (MaxNT-based). *)
definition MaxNT_F :: "bool ⇒ bool" where
  "MaxNT_F q ≡
     Head_F q ∧ (∀r. Head_F r ⟶ NT_in_edges_F r ≼⇩c NT_in_edges_F q)"

definition H_opt_MaxNT_F :: "bool ⇒ bool" where
  "H_opt_MaxNT_F q ≡ MaxNT_F q"

lemma MaxNT_F_all[simp]: "MaxNT_F q"
  unfolding MaxNT_F_def
  by (simp add: le_card_refl)

lemma H_opt_MaxNT_F_all[simp]: "H_opt_MaxNT_F q"
  by (simp add: H_opt_MaxNT_F_def)

corollary exists_H_opt_MaxNT_F: "∃q. H_opt_MaxNT_F q"
  by (rule exI[where x=True], simp)
text ‹
  Reading. The MaxNT/NT\_in\_edges shape is satisfiable in a concrete flat toy model.
  This witnesses non-explosiveness of the definitional pattern, without affecting the core.
›


section ‹10. Supplemental Ontic Frame: A Semantic Interpretation›
text ‹ [Note on the Supplemental Nature of this Section]
  The core proof of H\_opt and the Trinitarian structure is self-contained
  within the abstract U-logic. This section provides an **optional
  interpretative bridge** to standard possible-world semantics.
 
  By mapping model propositions to sets of worlds, we demonstrate that
  our universal logic is fully compatible with classical ontic frames.
  This serves as a semantic verification (Application) rather than
  a necessary foundation for the main argument. ›

locale FullIdBridge =
  fixes Val :: "'W ⇒ bool ⇒ bool"    (* truth function of the model: ζ is true at w *)
    and iw  :: "'W ⇒ U"               (* embedding of model worlds into U-worlds *)
  assumes surj_iw: "∀e. ∃w. e = iw w"
      and bridge:  "∀w ζ. (iw w ⊢ Arg ζ) ⟷ Val w ζ"
begin

definition Arg0 :: "bool ⇒ 'W set" where
  "Arg0 ζ ≡ {w. Val w ζ}"

definition EDia0 :: "bool ⇒ bool" where
  "EDia0 ζ ≡ (∃w. Val w ζ)"

lemma SuppU_Arg_id:
  "SuppU (Arg ζ) = { iw w | w. Val w ζ }"
proof (intro set_eqI iffI)
  fix e assume "e ∈ SuppU (Arg ζ)"
  then have "e ⊢ Arg ζ" by (simp add: SuppU_def)
  from surj_iw obtain w where "e = iw w" by blast
  from ‹e = iw w› ‹e ⊢ Arg ζ› have "Val w ζ" by (simp add: bridge)
  thus "e ∈ { iw w | w. Val w ζ }" using ‹e = iw w› by blast
next
 
  fix e assume "e ∈ { iw w | w. Val w ζ }"
  then obtain w where "e = iw w" and "Val w ζ" by blast
  hence "iw w ⊢ Arg ζ" by (simp add: bridge)
  thus "e ∈ SuppU (Arg ζ)" using ‹e = iw w› by (simp add: SuppU_def)
qed

lemma Dia_equiv: "EDia ζ ⟷ EDia0 ζ"
proof
  assume "EDia ζ"
  then obtain e where "Supports e ζ" by (auto simp: EDia_def)
  hence "e ⊢ Arg ζ" by (simp add: Supports_def)
  from surj_iw obtain w where "e = iw w" by blast
  with ‹e ⊢ Arg ζ› have "Val w ζ" by (simp add: bridge)
  thus "EDia0 ζ" by (auto simp: EDia0_def)
next
  assume "EDia0 ζ"
  then obtain w where "Val w ζ" by (auto simp: EDia0_def)
  hence "(iw w) ⊢ Arg ζ" by (simp add: bridge)
  hence "Supports (iw w) ζ" by (simp add: Supports_def)
  thus "EDia ζ" by (auto simp: EDia_def)
qed

lemma LeU_iff_subset: "(Arg ζ) ≼ (Arg t) ⟷ Arg0 ζ ⊆ Arg0 t"
proof
   assume le: "(Arg ζ) ≼ (Arg t)"
  show "Arg0 ζ ⊆ Arg0 t"
  proof
    fix w assume "w ∈ Arg0 ζ"
    hence "Val w ζ" by (simp add: Arg0_def)
    hence "iw w ⊢ Arg ζ" by (simp add: bridge)
    from le have "SuppU (Arg ζ) ⊆ SuppU (Arg t)" by (simp add: LeU_def)
    hence "iw w ⊢ Arg t" using ‹iw w ⊢ Arg ζ› by (auto simp: SuppU_def)
    hence "Val w t" by (simp add: bridge)
    thus "w ∈ Arg0 t" by (simp add: Arg0_def)
  qed
next
  assume sub: "Arg0 ζ ⊆ Arg0 t"
  show "(Arg ζ) ≼ (Arg t)"
    unfolding LeU_def SuppU_Arg_id
  proof (intro subsetI)
    fix e assume "e ∈ { iw w | w. Val w ζ }"
    then obtain w where ew: "e = iw w" and vζ: "Val w ζ" by blast
    from sub vζ have "Val w t" by (auto simp: Arg0_def)
    thus "e ∈ { iw w | w. Val w t }" using ew by blast
  qed
qed

end  (* locale FullIdBridge *)
(* ---------- Riemann toy model: two worlds (I, II) ---------- *)
datatype W = I | II

locale Riemann_Toy =
  FullIdBridge Val iw for Val :: "W ⇒ bool ⇒ bool" and iw :: "W ⇒ U"
+ fixes R Φ Φ' :: bool
assumes RI:     "Val I R"
    and RII:    "¬ Val II R"
    and PhiI:   "Val I Φ"
    and nPhi'I: "¬ Val I Φ'"
begin

lemma Arg0_R_is_I: "Arg0 R = {w. w = I}"
proof (intro set_eqI; intro iffI)
  (* -> *)
  fix w assume "w ∈ Arg0 R"
  then have Vw: "Val w R" by (simp add: Arg0_def)
  show "w ∈ {w. w = I}"
  proof (cases w)
    case I
    then show ?thesis by simp
  next
    case II
    from Vw II have "Val II R" by simp
    with RII show ?thesis by contradiction
  qed
next
 
  fix w assume "w ∈ {w. w = I}"
  then have "w = I" by simp
  with RI show "w ∈ Arg0 R" by (simp add: Arg0_def)
qed

lemma EDia0_R: "EDia0 R"
  unfolding EDia0_def using RI by auto

lemma EDia_R: "EDia R"
  using Dia_equiv EDia0_R by simp

lemma R_supports_Phi_model: "Arg0 R ⊆ Arg0 Φ"
  using Arg0_R_is_I PhiI by (auto simp: Arg0_def)

lemma R_not_support_Phi'_model: "¬ (Arg0 R ⊆ Arg0 Φ')"
proof
  assume "Arg0 R ⊆ Arg0 Φ'"
  hence "I ∈ Arg0 Φ'" using Arg0_R_is_I by simp
  thus False by (simp add: Arg0_def nPhi'I)
qed

lemma R_supports_Phi_U: "(Arg R) ≼ (Arg Φ)"
  using LeU_iff_subset R_supports_Phi_model by blast

lemma R_not_support_Phi'_U: "¬ ((Arg R) ≼ (Arg Φ'))"
  using LeU_iff_subset R_not_support_Phi'_model by blast

lemma not_PH_of_Phi': "¬ PH (Arg Φ')"
proof
  assume "PH (Arg Φ')"
  from this EDia_R have "(Arg R) ≼ (Arg Φ')" by (auto simp: PH_def)
  with R_not_support_Phi'_U show False by contradiction
qed

end


section ‹11. Vacuity Diagnosis: NT\_edge-death empties relational maximality, while N=3 remains the unique structural fixed point›
text ‹
 Design note (two-tier MaxNT).

  - MaxNT (Section 9) is the ranking core: it compares nontrivial incoming patterns
    under the minimal pairwise-distinctness guard A @{text "≠"} B, A @{text "≠"} C, and B @{text "≠"} C.
    This is the weaker, refactor-stable notion of relational maximality.

  - MaxNT\_edge (Section 11) is the non-vacuity strengthening: it rebuilds incoming
    support using NT\_edge, which additionally enforces non-collapse
    (no conjunction-elimination equivalence). Thus MaxNT\_edge is strictly stronger
    and exists only when genuine relational structure is possible.

  Therefore Section 11 is diagnostic: it shows that if NT\_edge is globally impossible,
  then every edge-based incoming-support set is empty, and the Cantor-style comparison
  used in MaxNT\_edge becomes vacuous. Hence MaxNT\_edge collapses to Head-only.

  This vacuity affects informational/relational content only; it does not by itself
  undermine the independent structural necessity of the triune fixed point (N=3).›

text ‹
 Philosophical background.

  In this development, MaxNT is intended to capture a ``supreme truth'' in a strong sense:
  not merely a truth that is final, but one whose superiority is expressed through
  maximal non-trivial relational support. Thus the real issue is not finality alone,
  but whether maximality is sustained by genuine relational content rather than by
  an informationally empty structure.

  Section 11 isolates exactly this issue. It introduces NT\_edge and the rebuilt notion
  MaxNT\_edge in order to diagnose whether the incoming relational structure remains
  genuinely non-trivial. Here, ``non-trivial'' means that a conjunction-based support
  does not collapse back into mere conjunction-elimination equivalence with one of
  its conjuncts.

  The goal of this section is therefore diagnostic, not destructive.
  We prove the following conditional:

    if NT\_edge is globally impossible (NT\_dead),
    then every NT\_in\_edges\_edge set is empty,
    and the Cantor-style comparison used in MaxNT\_edge becomes vacuous.

  Hence MaxNT\_edge collapses to a purely formal head-condition:
  its maximality remains syntactically satisfiable, but only vacuously,
  because all edge-based relational content has disappeared.

  Crucially, this vacuity does not undermine the independent structural necessity
  of the triune fixed point. Even if relational support becomes informationally empty
  through collapse, the exclusion results against N=1, N=2, and N@{text "≥"}4 remain intact.
  Thus N=3 persists as the unique consistency-preserving fixed point.

  This section therefore establishes the precise message:

    ``If NT\_edge dies, relational maximality becomes vacuous;
     but the structural necessity of N=3 does not collapse.''

  No axioms are introduced here. NT\_dead is a definitional diagnostic hypothesis
  used only to prove a conditional vacuity theorem.
›
(* ------------------------------------------------------------------------- *)
(* 11.0  Non-trivial edge (same meaning as earlier NT_edge)            *)
(* ------------------------------------------------------------------------- *)
definition NT_edge :: "bool ⇒ bool ⇒ bool ⇒ bool" where
  "NT_edge A B C ⟷
     (Arg (A ∧ B) ≼ Arg C) ∧
     ¬ (Arg (A ∧ B) ≈ Arg A) ∧
     ¬ (Arg (A ∧ B) ≈ Arg B)"
(* ------------------------------------------------------------------------- *)
(* 11.1  Global “edge death” hypothesis                                     *)
(* ------------------------------------------------------------------------- *)
definition NT_dead :: bool where
  "NT_dead ≡ (∀A B C. ¬ NT_edge A B C)"
(* ------------------------------------------------------------------------- *)
(* 11.2  NT_in_edges rebuilt directly on NT_edge (refactor-friendly)        *)
(*         (Depends on Head :: bool ⇒ bool from Section 9.1)          *)
(* ------------------------------------------------------------------------- *)
definition NT_in_edges_edge :: "bool ⇒ (bool × bool) set" where
  "NT_in_edges_edge C ≡
     {(A,B). Head A ∧ Head B ∧ Head C ∧
            A ≠ B ∧ A ≠ C ∧ B ≠ C ∧
            NT_edge A B C}"
(* ------------------------------------------------------------------------- *)
(* 11.3  MaxNT rebuilt on NT_in_edges_edge (Cantor-style comparison)        *)
(*         (Depends on ≼⇩c and le_card_empty_left from Section 9.1)   *)
(* ------------------------------------------------------------------------- *)
definition MaxNT_edge :: "bool ⇒ bool" where
  "MaxNT_edge q ≡
     Head q ∧
     (∀r. Head r ⟶ NT_in_edges_edge r ≼⇩c NT_in_edges_edge q)"

definition Nontrivial_MaxNT_edge :: "bool ⇒ bool" where
  "Nontrivial_MaxNT_edge q ≡ MaxNT_edge q ∧ NT_in_edges_edge q ≠ {}"


subsection ‹11.1 NT\_dead @{text "⟹"} all edge-sets are empty›

lemma NT_in_edges_edge_empty_if_NT_dead:
  assumes D: NT_dead
  shows "NT_in_edges_edge C = {}"
  using D
  unfolding NT_dead_def NT_in_edges_edge_def
  by auto


subsection ‹11.2 Vacuity theorem: MaxNT\_edge collapses to Head›

theorem MaxNT_edge_iff_Head_if_NT_dead:
  assumes D: NT_dead
  shows "MaxNT_edge q ⟷ Head q"
proof
 
  assume "MaxNT_edge q"
  thus "Head q" by (simp add: MaxNT_edge_def)
next
 
  assume Hq: "Head q"
  show "MaxNT_edge q"
    unfolding MaxNT_edge_def
  proof (intro conjI allI impI)
    show "Head q" by (rule Hq)

    fix r assume Hr: "Head r"
    have Er: "NT_in_edges_edge r = {}"
      using NT_in_edges_edge_empty_if_NT_dead[OF D] .
    have Eq: "NT_in_edges_edge q = {}"
      using NT_in_edges_edge_empty_if_NT_dead[OF D] .

    show "NT_in_edges_edge r ≼⇩c NT_in_edges_edge q"
      by (simp add: Er Eq le_card_empty_left)
  qed
qed


subsection ‹11.3 Consequence: ``Meaningful MaxNT'' becomes impossible under NT\_dead›

corollary no_Nontrivial_MaxNT_edge_if_NT_dead:
  assumes D: NT_dead
  shows "¬ (∃q. Nontrivial_MaxNT_edge q)"
proof
  assume "∃q. Nontrivial_MaxNT_edge q"
  then obtain q where H: "Nontrivial_MaxNT_edge q" by blast
  hence NE: "NT_in_edges_edge q ≠ {}"
    by (simp add: Nontrivial_MaxNT_edge_def)
  moreover have "NT_in_edges_edge q = {}"
    using NT_in_edges_edge_empty_if_NT_dead[OF D] .
  ultimately show False by contradiction

qed

subsection ‹11.4 Derived corollaries (optional)›
text ‹
  This subsection records small but useful consequences of the vacuity theorem.

  Under NT\_dead, the Cantorian maximality comparison is empty-vacuous, so:

    (i) Any Head automatically satisfies MaxNT\_edge (maximality becomes trivial).
    (ii) Any two MaxNT\_edge candidates are indistinguishable at the level of
         their incoming edge-sets (both are empty).

  These are not new assumptions; they are direct corollaries of Sections 11.1–11.2.
  Their role is purely expositional: they make the ``vacuity collapse'' behavior
  visible in lightweight lemmas that can be reused later.
›

corollary Head_implies_MaxNT_edge_under_NT_dead:
  assumes D: NT_dead and Hq: "Head q"
  shows "MaxNT_edge q"
  using MaxNT_edge_iff_Head_if_NT_dead[OF D] Hq by blast

corollary MaxNT_edge_is_tied_under_NT_dead:
  assumes D: NT_dead and A: "MaxNT_edge x" and B: "MaxNT_edge y"
  shows "NT_in_edges_edge x = NT_in_edges_edge y"
  using NT_in_edges_edge_empty_if_NT_dead[OF D] by simp


subsection ‹11.5 One-to-one collapse route: (1-to-1) @{text "⟹"} NT\_dead @{text "⟹"} vacuity›
text ‹
  This subsection makes explicit (as lemmas) the intended bridge:

    (1) If the theory enforces a global 1-to-1 comparability of grounds
        (a total preorder on Arg-images),
    then every conjunction collapses to one conjunct (trivial collapse).

    (2) Hence no NT\_edge can survive (NT\_dead).

    (3) Therefore, by Section 11.2, MaxNT\_edge collapses to Head-only (vacuity).

  Importantly, no axioms are introduced: the 1-to-1 condition and the conjunction
  grammar rules (MCL/MCI) are stated as *assumptions* of conditional theorems.
›

lemma conj_le_left_from_MCL:
  assumes MCL: "⋀e X Y. Makes e (X ∧ Y) ⟹ Makes e X"
  shows "Arg (X ∧ Y) ≼ Arg X"
  unfolding LeU_iff_all
  using MCL by blast

lemma Subordination_implies_Trivial_Collapse_left:
  assumes AB : "Arg A ≼ Arg B"
      and MCL: "⋀e X Y. Makes e (X ∧ Y) ⟹ Makes e X"
      and MCI: "⋀e X Y. Makes e X ⟹ Makes e Y ⟹ Makes e (X ∧ Y)"
  shows "Arg (A ∧ B) ≈ Arg A"
proof -
  have le1: "Arg (A ∧ B) ≼ Arg A"
    using conj_le_left_from_MCL[OF MCL] .

  have AB_pt: "∀e. Makes e A ⟶ Makes e B"
    using AB by (simp add: LeU_iff_all)

  have le2: "Arg A ≼ Arg (A ∧ B)"
  proof (simp add: LeU_iff_all, intro allI impI)
    fix e assume eA: "Makes e A"
    have eB: "Makes e B" using AB_pt eA by blast
    show "Makes e (A ∧ B)" using MCI[OF eA eB] .
  qed

  show ?thesis
    using LeU_antisym_eq[OF le1 le2] .
qed

lemma Subordination_kills_NT_edge_left:
  assumes AB : "Arg A ≼ Arg B"
      and MCL: "⋀e X Y. Makes e (X ∧ Y) ⟹ Makes e X"
      and MCI: "⋀e X Y. Makes e X ⟹ Makes e Y ⟹ Makes e (X ∧ Y)"
  shows "¬ NT_edge A B C"
proof
  assume E: "NT_edge A B C"
  have collapse: "Arg (A ∧ B) ≈ Arg A"
    using Subordination_implies_Trivial_Collapse_left[OF AB MCL MCI] .
  from E have ncollapse: "¬ (Arg (A ∧ B) ≈ Arg A)"
    by (simp add: NT_edge_def)
  show False using collapse ncollapse by contradiction
qed

lemma Subordination_kills_NT_edge_right:
  assumes BA : "Arg B ≼ Arg A"
      and MCL: "⋀e X Y. Makes e (X ∧ Y) ⟹ Makes e X"
      and MCI: "⋀e X Y. Makes e X ⟹ Makes e Y ⟹ Makes e (X ∧ Y)"
  shows "¬ NT_edge A B C"
proof
  assume E: "NT_edge A B C"
  have collapse: "Arg (A ∧ B) ≈ Arg B"
    using Subordination_implies_Trivial_Collapse_left[OF BA MCL MCI]
    by (simp add: ac_simps)
  from E have ncollapse: "¬ (Arg (A ∧ B) ≈ Arg B)"
    by (simp add: NT_edge_def)
  show False using collapse ncollapse by contradiction
qed

definition OneToOne :: bool where
  "OneToOne ≡ (∀A B. Arg A ≼ Arg B ∨ Arg B ≼ Arg A)"

lemma OneToOne_implies_NT_dead:
  assumes O  : OneToOne
      and MCL: "⋀e X Y. Makes e (X ∧ Y) ⟹ Makes e X"
      and MCI: "⋀e X Y. Makes e X ⟹ Makes e Y ⟹ Makes e (X ∧ Y)"
  shows NT_dead
  unfolding NT_dead_def OneToOne_def
proof (intro allI)
  fix A B C
  have "Arg A ≼ Arg B ∨ Arg B ≼ Arg A" using O [unfolded OneToOne_def] by blast
  thus "¬ NT_edge A B C"
  proof
    assume AB: "Arg A ≼ Arg B"
    show "¬ NT_edge A B C"
      using Subordination_kills_NT_edge_left[OF AB MCL MCI] .
  next
    assume BA: "Arg B ≼ Arg A"
    show "¬ NT_edge A B C"
      using Subordination_kills_NT_edge_right[OF BA MCL MCI] .
  qed
qed


section ‹12. TriSupport\_Joint and Ternary Semantics (No 1-to-1)›
text ‹
  We redefine the trinitarian support to strictly exclude any 1-to-1
  subordination. It mandates a pure ternary joint-support structure:
  the conjunction of any two heads necessitates the third, while
  no single head necessitates another. This guarantees Borromean stability.
›

text ‹
  1. Joint support (Ternary Support)
  2. Consistency Requirement for Non-triviality(Strict exclusion of 1-to-1 individual support (No mutual subordination))
›
definition TriSupport_Joint :: "bool ⇒ bool ⇒ bool ⇒ bool" where
  "TriSupport_Joint a b c ≡
     (Arg (b ∧ c) ≼ Arg a) ∧
     (Arg (c ∧ a) ≼ Arg b) ∧
     (Arg (a ∧ b) ≼ Arg c) ∧
     ¬ (Arg a ≼ Arg b) ∧ ¬ (Arg b ≼ Arg a) ∧
     ¬ (Arg b ≼ Arg c) ∧ ¬ (Arg c ≼ Arg b) ∧
     ¬ (Arg c ≼ Arg a) ∧ ¬ (Arg a ≼ Arg c)"


subsection ‹12.1 Symmetries and permutations›

lemma TriSupport_Joint_perm12:
  "TriSupport_Joint a b c ⟹ TriSupport_Joint b a c"
  by (auto simp: TriSupport_Joint_def ac_simps)

lemma TriSupport_Joint_perm23:
  "TriSupport_Joint a b c ⟹ TriSupport_Joint a c b"
  by (auto simp: TriSupport_Joint_def ac_simps)

lemma TriSupport_Joint_rotate:
  "TriSupport_Joint a b c ⟹ TriSupport_Joint b c a"
  by (auto simp: TriSupport_Joint_def ac_simps)


subsection ‹12.2 Ternary Semantics (pair @{text "→"} third)›
text ‹
  To extract the pointwise semantics (Supports e ...), we assume a standard
  conjunction-introduction rule (MCI) for the ``Supports'' relation, bridging
  the logical AND with the semantic evaluation at point e.
›

lemma TriSupport_Joint_bc_to_a:
  assumes "TriSupport_Joint a b c"
      and MCI: "⋀e X Y. Supports e X ⟹ Supports e Y ⟹ Supports e (X ∧ Y)"
      and "Supports e b" and "Supports e c"
  shows "Supports e a"
proof -
  from assms(1) have "(Arg (b ∧ c)) ≼ (Arg a)" by (simp add: TriSupport_Joint_def)
  hence "∀x. Makes x (b ∧ c) ⟶ Makes x a" by (simp add: LeU_iff_all)
  moreover have "Makes e (b ∧ c)"
    using MCI[OF assms(3) assms(4)] by (simp add: Makes_def Supports_def)
  ultimately show "Supports e a" by (simp add: Makes_def Supports_def)
qed

lemma TriSupport_Joint_semantics:
  assumes "TriSupport_Joint a b c"
      and MCI: "⋀e X Y. Supports e X ⟹ Supports e Y ⟹ Supports e (X ∧ Y)"
  shows "∀e. (Supports e b ∧ Supports e c) ⟶ Supports e a"
    and "∀e. (Supports e c ∧ Supports e a) ⟶ Supports e b"
    and "∀e. (Supports e a ∧ Supports e b) ⟶ Supports e c"
proof -
  { fix e have "(Supports e b ∧ Supports e c) ⟶ Supports e a"
      using TriSupport_Joint_bc_to_a[OF assms(1) MCI] by blast }
  thus "∀e. (Supports e b ∧ Supports e c) ⟶ Supports e a" by blast
 
  { fix e have "(Supports e c ∧ Supports e a) ⟶ Supports e b"
      using TriSupport_Joint_bc_to_a[OF TriSupport_Joint_rotate[OF assms(1)] MCI] by blast }
  thus "∀e. (Supports e c ∧ Supports e a) ⟶ Supports e b" by blast
 
  { fix e have "(Supports e a ∧ Supports e b) ⟶ Supports e c"
      using TriSupport_Joint_bc_to_a[OF TriSupport_Joint_rotate[OF TriSupport_Joint_rotate[OF assms(1)]] MCI] by blast }
  thus "∀e. (Supports e a ∧ Supports e b) ⟶ Supports e c" by blast
qed


section ‹13. Proof of n=3 necessity (cardinality; assumption-free)›
text ‹
  This section formalizes the ``Structural Necessity of the Trinity'' using an
  epistemic refutation domain (PDom\_ep). The proof architecture adopts a
  non-axiomatic approach, deriving the uniqueness of n=3 from the following
  definitional constraints:

  1. **Refutation-based Epistecmic Possibility (EDia\_ep):** Defines epistemic possibility as the
     absence of formal refutation within the current evidence state.
  2. **Maximal Non-Trivial Support (MaxNT\_ep):** Identifies optimal heads
     (H\_opt\_ep) by comparing the cardinality of their non-trivial relational
     support sets (NT\_in\_edges\_ep).
  3. **Categorical Exclusion:** By defining N1, N2, and N4+ exact configurations,
     we set the stage for proving that only N3 satisfies the structural
     equilibrium between ``Relational Richness'' and ``Ontological Maximality.''

   *Note:* The use of Cantor-style cardinal comparison ensures that the
  ranking of optimal truths is independent of finite model constraints,
  grounding the Triune necessity in pure set-theoretic relations.
›


subsection ‹13.1 Ref-domain (H\_opt\_ep)›

consts Ref :: "bool ⇒ bool"    
text ‹
  Definition:
(1) Refuted(p): truth-bearer p is in a currently refuted state (a proof of falsity exists
within the current system).
(2) Negation of Refuted(p): truth-bearer p is in a currently unrefuted state (no proof of falsity
exists)
so, EDia\_ep(p) @{text "⟷"} negation of Refuted(p)

    EDia\_ep @{text "φ"}  means: ``not refuted yet (given the current evidence state)''.
  Formally, EDia\_ep is definitional negation of Ref.
›

definition EDia_ep :: "bool ⇒ bool" where
  "EDia_ep z ≡ ¬ Ref z"

definition PDom_ep :: "bool set" where
  "PDom_ep ≡ {z. TrueNow z ∨ EDia_ep z}"

definition Comparable_PDom_ep_on :: "bool ⇒ bool" where
  "Comparable_PDom_ep_on q ≡
     (∀z. z ∈ PDom_ep ⟶ ((Arg z) ≼ (Arg q) ∨ (Arg q) ≼ (Arg z)))"

definition H_negU_strict_ep :: "bool ⇒ bool" where
  "H_negU_strict_ep q ≡
     (∀z. z ∈ PDom_ep ⟶ z ≠ q ⟶ ¬ ((Arg q) ≺ (Arg z)))"

definition Head_ep :: "bool ⇒ bool" where
  "Head_ep q ≡ EDia_ep q ∧ H_negU_strict_ep q"
text ‹
Nontrivial pair-support among heads.
We exclude trivial targets C=A or C=B so plain @{text "∧"}-elimination does not count.
›
definition NT_pair_support_ep :: "bool ⇒ bool ⇒ bool ⇒ bool" where
  "NT_pair_support_ep A B C ≡
     A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ (Arg (A ∧ B) ≼ Arg C)"

definition NT_in_edges_ep :: "bool ⇒ (bool × bool) set" where
  "NT_in_edges_ep C ≡
     {(A,B). Head_ep A ∧ Head_ep B ∧ Head_ep C ∧ NT_pair_support_ep A B C}"
(* ---------------- Cantor-style cardinal comparison ---------------- *)
lemmas le_card_empty_left_ep = le_card_empty_left

definition MaxNT_ep :: "bool ⇒ bool" where
  "MaxNT_ep q ≡
     Head_ep q
   ∧ (∀r. EDia_ep r ⟶ NT_in_edges_ep r ≼⇩c NT_in_edges_ep q)"

definition H_opt_ep :: "bool ⇒ bool" where
  "H_opt_ep q ≡ MaxNT_ep q"

lemma Hopt_ep_to_MaxNT_ep:
  assumes "H_opt_ep q"
  shows "MaxNT_ep q"
  using assms by (simp add: H_opt_ep_def)

lemma NT_in_edges_ep_empty_if_not_Head_ep:
  assumes "¬ Head_ep C"
  shows "NT_in_edges_ep C = {}"
  using assms by (auto simp: NT_in_edges_ep_def)

lemma Hopt_ep_score_ge_EDia:
  assumes HQ: "H_opt_ep q" and EZ: "EDia_ep z"
  shows "NT_in_edges_ep z ≼⇩c NT_in_edges_ep q"
  using HQ EZ by (auto simp: H_opt_ep_def MaxNT_ep_def)

lemma Hopt_ep_score_ge_any:
  assumes HQ: "H_opt_ep q"
  shows "NT_in_edges_ep z ≼⇩c NT_in_edges_ep q"
proof (cases "Head_ep z")
  case True
  then have "EDia_ep z" by (simp add: Head_ep_def)
  thus ?thesis using Hopt_ep_score_ge_EDia[OF HQ] by blast
next
  case False
  have "NT_in_edges_ep z = {}"
    using NT_in_edges_ep_empty_if_not_Head_ep[OF False] .
  thus ?thesis using le_card_empty_left_ep by simp
qed

lemma Hopt_ep_score_tie:
  assumes HA: "H_opt_ep A" and HB: "H_opt_ep B"
  shows "NT_in_edges_ep A ≈⇩c NT_in_edges_ep B"
proof -
  have AB: "NT_in_edges_ep A ≼⇩c NT_in_edges_ep B"
    using Hopt_ep_score_ge_any[OF HB, of A] by simp
  have BA: "NT_in_edges_ep B ≼⇩c NT_in_edges_ep A"
    using Hopt_ep_score_ge_any[OF HA, of B] by simp
  show ?thesis by (simp add: eq_card_def AB BA)
qed

lemma le_card_imp_card_le_if_finite:
  assumes "A ≼⇩c B" and "finite B"
  shows "card A ≤ card B"
proof -
  obtain f where inj: "inj_on f A" and img: "f ` A ⊆ B"
    using assms(1) unfolding le_card_def by blast
  have fin_img: "finite (f ` A)" using assms(2) img finite_subset by blast
  have cA: "card (f ` A) = card A" using inj fin_img by (simp add: card_image)
  have "card (f ` A) ≤ card B" using assms(2) img fin_img by (simp add: card_mono)
  thus ?thesis using cA by simp
qed

definition EqNT_ep :: "bool ⇒ bool ⇒ bool" (infix "≈⇩NT" 50) where
  "X ≈⇩NT Y ≡ NT_in_edges_ep X = NT_in_edges_ep Y"

definition Distinct_ep :: "bool ⇒ bool ⇒ bool" where
  "Distinct_ep X Y ≡ X ≠ Y ∧ ¬ (X ≈⇩NT Y)"
(* -------------------------------------------------------------------------- *)
(* Semantic block (Arg/Makes/EntailsU/EH) kept intact, NOT derived from MaxNT. *)
(* -------------------------------------------------------------------------- *)
definition EntailsU :: "bool ⇒ bool ⇒ bool" (infix "⟶⇩U" 55) where
  "e ⟶⇩U Q ≡ (Arg e) ≼ (Arg Q)"

definition StrictBelow :: "bool ⇒ bool ⇒ bool" where
  "StrictBelow e K ≡ (e ⟶⇩U K) ∧ ¬ (K ⟶⇩U e)"

definition NotHoptArg :: "bool ⇒ bool" where
  "NotHoptArg X ≡ ¬ H_opt_ep X"

definition TextPremises :: "bool ⇒ bool ⇒ bool" where
  "TextPremises e K ≡
       EDia_ep e
    ∧ (e ⟶⇩U K)
    ∧ ¬ (K ⟶⇩U e)
    ∧ e ≠ K
    ∧ NotHoptArg e"

lemma TextPremisesD:
  assumes "TextPremises e K"
  shows   "EDia_ep e"
          "e ⟶⇩U K"
          "¬ (K ⟶⇩U e)"
          "e ≠ K"
          "NotHoptArg e"
  using assms by (auto simp: TextPremises_def)

definition EH_ep where
  "EH_ep U ≡ (∀z. EDia_ep z ⟶ (Arg z) ≼ U)"

lemma EH_epD:
  assumes "EH_ep U" and "EDia_ep z"
  shows "(Arg z) ≼ U"
  using assms by (simp add: EH_ep_def)

lemma H_principle_ep_basic:
  assumes EH: "EH_ep (Arg Q)"
      and TP: "TextPremises e K"
  shows "(Arg e) ≼ (Arg Q)"
proof -
  from TextPremisesD[OF TP] have Ee: "EDia_ep e" by auto
  show ?thesis using EH_epD[OF EH Ee] .
qed

corollary H_principle_ep_basic_EntailsU:
  assumes EH: "EH_ep (Arg Q)" and TP: "TextPremises e K"
  shows   "e ⟶⇩U Q"
  using H_principle_ep_basic[OF EH TP] by (simp add: EntailsU_def)

lemma not_EH_ep_if_ep_possible_fails_to_support:
  assumes TP: "TextPremises e K"
      and N:  "¬ ((Arg e) ≼ (Arg Q))"
  shows "¬ EH_ep (Arg Q)"
proof
  assume EH: "EH_ep (Arg Q)"
  from H_principle_ep_basic[OF EH TP] have "(Arg e) ≼ (Arg Q)" .
  with N show False by contradiction
qed

subsection ‹13.2 Consistency for H\_opt\_ep (Cantor-size version)›

lemma Hopt_ep_has_no_strictly_better_in_PDom_ep:
  assumes HQ: "H_opt_ep q"
  shows "¬ (∃z∈PDom_ep. NT_in_edges_ep q ≺⇩c NT_in_edges_ep z)"
proof
  assume "∃z∈PDom_ep. NT_in_edges_ep q ≺⇩c NT_in_edges_ep z"
  then obtain z where Zin: "z ∈ PDom_ep" and lt: "NT_in_edges_ep q ≺⇩c NT_in_edges_ep z"
    by blast

  have ge: "NT_in_edges_ep z ≼⇩c NT_in_edges_ep q"
    using Hopt_ep_score_ge_any[OF HQ, of z] by simp

  from lt have nz: "¬ (NT_in_edges_ep z ≼⇩c NT_in_edges_ep q)"
    by (simp add: lt_card_def)

  show False using ge nz by contradiction
qed

corollary Hopt_ep_has_no_strictly_better_in_PDom_ep_non_tautology:
  assumes HQ: "H_opt_ep q"
      and nT: "q ≠ True"
  shows "¬ (∃z∈PDom_ep. NT_in_edges_ep q ≺⇩c NT_in_edges_ep z)"
  using Hopt_ep_has_no_strictly_better_in_PDom_ep[OF HQ] .


subsection ‹13.3 Rescue block: Hopt3 @{text "⟹"} N3 (with pure joint support)›
text ‹
  Hopt3 now explicitly requires the TriSupport\_Joint structure,
  guaranteeing that the three optimal heads do not subordinate each other,
  but strictly co-support the third.
›

definition Hopt3 :: "bool ⇒ bool ⇒ bool ⇒ bool" where
  "Hopt3 a b c ≡
     H_opt a ∧ H_opt b ∧ H_opt c ∧
     EDia a ∧ EDia b ∧ EDia c ∧
     TriSupport_Joint a b c"

lemma Hopt3_implies_trinity_joint:
  assumes "Hopt3 a b c"
  shows   "TriSupport_Joint a b c"
  using assms by (simp add: Hopt3_def)

definition N3 :: bool where
  "N3 ≡ (∃a b c.
          H_opt a ∧ H_opt b ∧ H_opt c ∧
          TriSupport_Joint a b c ∧
          (∀e. Supports e b ∧ Supports e c ⟶ Supports e a) ∧
          (∀e. Supports e c ∧ Supports e a ⟶ Supports e b) ∧
          (∀e. Supports e a ∧ Supports e b ⟶ Supports e c))"

lemma OnlyN3_from_Hopt3_unboxed:
  assumes H3: "Hopt3 a b c"
      and MCI: "⋀e X Y. Supports e X ⟹ Supports e Y ⟹ Supports e (X ∧ Y)"
  shows N3
proof -
  have TS: "TriSupport_Joint a b c"
    using Hopt3_implies_trinity_joint[OF H3] .

  have Sbc_a: "∀e. Supports e b ∧ Supports e c ⟶ Supports e a"
    using TriSupport_Joint_semantics(1)[OF TS MCI] .
  have Sca_b: "∀e. Supports e c ∧ Supports e a ⟶ Supports e b"
    using TriSupport_Joint_semantics(2)[OF TS MCI] .
  have Sab_c: "∀e. Supports e a ∧ Supports e b ⟶ Supports e c"
    using TriSupport_Joint_semantics(3)[OF TS MCI] .

  from H3 have Ha: "H_opt a" and Hb: "H_opt b" and Hc: "H_opt c"
    by (auto simp: Hopt3_def)

  have "∃a b c. H_opt a ∧ H_opt b ∧ H_opt c ∧
        TriSupport_Joint a b c ∧
        (∀e. Supports e b ∧ Supports e c ⟶ Supports e a) ∧
        (∀e. Supports e c ∧ Supports e a ⟶ Supports e b) ∧
        (∀e. Supports e a ∧ Supports e b ⟶ Supports e c)"
    using Ha Hb Hc TS Sbc_a Sca_b Sab_c
    by (intro exI[of _ a] exI[of _ b] exI[of _ c]) blast

  thus N3 by (simp add: N3_def)
qed

lemma OnlyN3_epi_unboxed:
  assumes Witnesses: "(∃x. H_opt x) ⟶ (∃a b c. Hopt3 a b c)"
      and MCI: "⋀e X Y. Supports e X ⟹ Supports e Y ⟹ Supports e (X ∧ Y)"
  shows "(∃x. H_opt x) ⟶ N3"
proof
  assume Hex: "∃x. H_opt x"
  have "∃a b c. Hopt3 a b c" using Witnesses Hex by (rule mp)
  then obtain a b c where H3: "Hopt3 a b c" by blast
  show N3 using OnlyN3_from_Hopt3_unboxed[OF H3 MCI] .
qed

lemmas OnlyN3_epi_possible_proved = OnlyN3_epi_unboxed
lemmas OnlyN3_epi_boxed           = OnlyN3_epi_possible_proved


section ‹14. n@{text "≥"}4 exclusion›


subsection ‹14.1 Boolean reading at our world (discharging Ep\_Conj\_ locales)›

locale Boolean_at_our_world =
  fixes Val :: "'w ⇒ bool ⇒ bool" and w0 :: "'w" ("w⇩0")
  assumes and_hom: "⋀A B. Val w0 (A ∧ B) = (Val w0 A ∧ Val w0 B)"
  assumes Ref_is_false_at_w0: "⋀φ. Ref φ ⟷ ¬ Val w0 φ"
begin

lemma Ref_and_sound_global:
  "Ref (A ∧ B) ⟶ (Ref A ∨ Ref B)" for A B :: bool
  using Ref_is_false_at_w0 and_hom by auto

lemma Ref_and_complete_global:
  "(Ref A ∨ Ref B) ⟶ Ref (A ∧ B)" for A B :: bool
  using Ref_is_false_at_w0 and_hom by auto

end

context
  fixes Val :: "'w ⇒ bool ⇒ bool"
    and w⇩0 :: "'w"
  assumes and_hom_w0: "⋀A B. Val w⇩0 (A ∧ B) = (Val w⇩0 A ∧ Val w⇩0 B)"
  assumes Ref_is_false_at_w0: "⋀φ. Ref φ ⟷ ¬ Val w⇩0 φ"
begin

interpretation OurWorld: Boolean_at_our_world Val w⇩0
  by (unfold_locales) (simp_all add: and_hom_w0 Ref_is_false_at_w0)

end


subsection ‹14.2 From ``NotRef ((@{text "Φ"} @{text "∧"} @{text "Ω"}) @{text "∧"} @{text "Ψ"})''
to ``EDia\_ep (@{text "Ω"} @{text "∧"} @{text "Ψ"})''(ES) — no global axioms›

context Boolean_at_our_world
begin

lemma EDia_ep_iff_notRef [simp]:
  "EDia_ep phi ⟷ ¬ Ref phi"
  by (simp add: EDia_ep_def)

lemma notRef_pair_from_notRef_triple_plain:
  assumes RCW: "!!X Y. Ref X ⟹ Ref (X ∧ Y)"              (* weak conjunctive monotonicity *)
      and NRT: "¬ Ref ((Phi ∧ Omega) ∧ Psi)"            (* "not yet refuted" for the triple *)
  shows "¬ Ref (Omega ∧ Psi)"
proof
  assume ROP: "Ref (Omega ∧ Psi)"
  hence "Ref ((Omega ∧ Psi) ∧ Phi)" using RCW by blast
  hence "Ref ((Phi ∧ Omega) ∧ Psi)" by (simp add: ac_simps)
  thus False using NRT by contradiction
qed

corollary EDia_ep_pair_from_notRef_triple_plain:
  assumes RCW: "!!X Y. Ref X ⟹ Ref (X ∧ Y)"
      and NRT: "¬ Ref ((Phi ∧ Omega) ∧ Psi)"
  shows "EDia_ep (Omega ∧ Psi)"
  using notRef_pair_from_notRef_triple_plain[OF RCW NRT] by simp

end


subsection ‹14.3 Coverage + witness gap @{text "⇒"} MoreCertain @{text "Φ"}' @{text "Φ"}›

lemma not_LeU_iff_exists_witness_v2:
  "¬ ((Arg S) ≼ (Arg T)) ⟷ (∃a. Makes a S ∧ ¬ Makes a T)"
  by (simp add: LeU_iff_all)

corollary gap_equiv_witness_OmegaPsi_Phi'_v2:
  "¬ ((Arg (Ω ∧ Ψ)) ≼ (Arg Φ')) ⟷
   (∃a. Makes a (Ω ∧ Ψ) ∧ ¬ Makes a Φ')"
  using not_LeU_iff_exists_witness_v2[of "Ω ∧ Ψ" "Φ'"] by simp

lemma witness_breaks_back_imp_v2:
  assumes "Makes a X" and "¬ Makes a Y"
  shows "¬ (∀e. Makes e X ⟶ Makes e Y)"
  using assms by blast

lemma relcert_from_cov_and_gap_min_witness_v2:
  assumes Cov   : "(Arg Φ') ≼ (Arg Φ)"
      and GapΦ: "(Arg (Ω ∧ Ψ)) ≼ (Arg Φ)"
      and W     : "∃a. Makes a (Ω ∧ Ψ) ∧ ¬ Makes a Φ'"
  shows "MoreCertain_pred Φ' Φ"  "RelCert Φ' Φ"
proof -
  obtain a where aS: "Makes a (Ω ∧ Ψ)" and n_aΦ': "¬ Makes a Φ'"
    using W by blast

  have S_to_Φ: "∀e. Makes e (Ω ∧ Ψ) ⟶ Makes e Φ"
    using GapΦ by (simp add: LeU_iff_all)
  have aΦ: "Makes a Φ" using S_to_Φ aS by blast

  have Front: "∀e. Makes e Φ' ⟶ Makes e Φ"
    using Cov by (simp add: LeU_iff_all)

  have BackBreak: "¬ (∀e. Makes e Φ ⟶ Makes e Φ')"
    using witness_breaks_back_imp_v2[OF aΦ n_aΦ'] .

  have MC: "MoreCertain_pred Φ' Φ"
    by (simp add: MoreCertain_pred_def Front BackBreak)

  have Not_rev: "¬ ((Arg Φ) ≼ (Arg Φ'))"
  proof
    assume rev: "(Arg Φ) ≼ (Arg Φ')"
    hence "∀e. Makes e Φ ⟶ Makes e Φ'" by (simp add: LeU_iff_all)
    hence "Makes a Φ'" using aΦ by blast
    with n_aΦ' show False by contradiction
  qed

  have RC: "RelCert Φ' Φ"
    by (simp add: RelCert_def LtU_def Cov Not_rev)

  show "MoreCertain_pred Φ' Φ"  "RelCert Φ' Φ" by (simp_all add: MC RC)
qed

lemma coverage_from_Hopt_ep':
  assumes Cov: "(Arg Φ') ≼ (Arg Φ)"
  shows "(Arg Φ') ≼ (Arg Φ)"
  using Cov .

lemma gap1_from_Hopt_ep':
  assumes GapΦ: "(Arg (Ω ∧ Ψ)) ≼ (Arg Φ)"
  shows "(Arg (Ω ∧ Ψ)) ≼ (Arg Φ)"
  using GapΦ .

corollary relcert_from_Hopt_ep_and_EDiaS_witness:
  assumes HΦ  : "H_opt_ep Φ"
      and TPΦ': "TextPremises Φ' K1"
      and TPS   : "TextPremises (Ω ∧ Ψ) K0"
      and Cov0  : "(Arg Φ') ≼ (Arg Φ)"
      and Gap0  : "(Arg (Ω ∧ Ψ)) ≼ (Arg Φ)"
      and W     : "∃a. Makes a (Ω ∧ Ψ) ∧ ¬ Makes a Φ'"
  shows "MoreCertain_pred Φ' Φ"  and "RelCert Φ' Φ"
proof -
  have Cov: "(Arg Φ') ≼ (Arg Φ)"
    using coverage_from_Hopt_ep'[OF Cov0] .
  have GapΦ: "(Arg (Ω ∧ Ψ)) ≼ (Arg Φ)"
    using gap1_from_Hopt_ep'[OF Gap0] .

  obtain a where aS: "Makes a (Ω ∧ Ψ)" and nΦ': "¬ Makes a Φ'"
    using W by blast

  have S_to_Φ: "∀e. Makes e (Ω ∧ Ψ) ⟶ Makes e Φ"
    using GapΦ by (simp add: LeU_iff_all)
  have aΦ: "Makes a Φ" using aS S_to_Φ by blast

  have Front: "∀e. Makes e Φ' ⟶ Makes e Φ"
    using Cov by (simp add: LeU_iff_all)

  have BackBreak: "¬ (∀e. Makes e Φ ⟶ Makes e Φ')"
    using aΦ nΦ' by blast

  have MC: "MoreCertain_pred Φ' Φ"
    by (simp add: MoreCertain_pred_def Front BackBreak)

  have Not_rev: "¬ ((Arg Φ) ≼ (Arg Φ'))"
  proof
    assume rev: "(Arg Φ) ≼ (Arg Φ')"
    hence "∀e. Makes e Φ ⟶ Makes e Φ'" by (simp add: LeU_iff_all)
    hence "Makes a Φ'" using aΦ by blast
    with nΦ' show False by contradiction
  qed

  have RC: "RelCert Φ' Φ"
    by (simp add: RelCert_def LtU_def Cov Not_rev)

  show "MoreCertain_pred Φ' Φ"  "RelCert Φ' Φ"
    by (simp_all add: MC RC)
qed


subsection ‹14.4 n@{text "≥"}4 exclusion  proof by Superfluous-removal›

locale Band_Collapse_Superfluous =
  fixes Ω Ψ Φ :: bool
  assumes ES:  "EDia_ep (Ω ∧ Ψ)"
      and Cov: "Arg (Ω ∧ Ψ) ≼ Arg Φ"
      and NS:
        "((Arg (Ω ∧ Ψ)) ≼ Arg Φ) ⟹
         (∀Y. H_opt_ep Y ⟶ EDia_ep Y ⟶
              Arg ((Ω ∧ Ψ) ∧ Y) ≼ Arg Φ ⟶
              Arg ((Ω ∧ Ψ) ∧ Y) ≈ Arg (Ω ∧ Ψ))"
      and MCL: "⋀e A B. Makes e (A ∧ B) ⟹ Makes e A"
      and MCR: "⋀e A B. Makes e (A ∧ B) ⟹ Makes e B"
begin

lemma conj_le_left[simp]:  "Arg (A ∧ B) ≼ Arg A"
  unfolding LeU_iff_all by (auto dest: MCL)

lemma conj_le_right[simp]: "Arg (A ∧ B) ≼ Arg B"
  unfolding LeU_iff_all by (auto dest: MCR)

lemma pulled_eq_and_below_Phi:
  assumes HY: "H_opt_ep Y" and EY: "EDia_ep Y"
  shows  "Arg ((Ω ∧ Ψ) ∧ Y) ≼ Arg Φ"
     and "Arg ((Ω ∧ Ψ) ∧ Y) ≈ Arg (Ω ∧ Ψ)"
proof -
  have step1: "Arg ((Ω ∧ Ψ) ∧ Y) ≼ Arg (Ω ∧ Ψ)"
    by (rule conj_le_left)

  have CovY: "Arg ((Ω ∧ Ψ) ∧ Y) ≼ Arg Φ"
    using step1 Cov by (rule LeU_trans)

  have Eq: "Arg ((Ω ∧ Ψ) ∧ Y) ≈ Arg (Ω ∧ Ψ)"
    using NS[OF Cov] HY EY CovY by blast

  show "Arg ((Ω ∧ Ψ) ∧ Y) ≼ Arg Φ" by (rule CovY)
  show "Arg ((Ω ∧ Ψ) ∧ Y) ≈ Arg (Ω ∧ Ψ)" by (rule Eq)
qed

lemma pulled_pair_collapse_in_band:
  assumes HY1: "H_opt_ep Y⇩1" and EY1: "EDia_ep Y⇩1"
      and HY2: "H_opt_ep Y⇩2" and EY2: "EDia_ep Y⇩2"
  shows "(Arg ((Ω ∧ Ψ) ∧ Y⇩1)) ≈ (Arg ((Ω ∧ Ψ) ∧ Y⇩2))"
proof -
  have "Arg ((Ω ∧ Ψ) ∧ Y⇩1) ≈ Arg (Ω ∧ Ψ)"
    using pulled_eq_and_below_Phi[OF HY1 EY1] by blast
  moreover
  have "Arg ((Ω ∧ Ψ) ∧ Y⇩2) ≈ Arg (Ω ∧ Ψ)"
    using pulled_eq_and_below_Phi[OF HY2 EY2] by blast
  ultimately show ?thesis by (meson EqU_sym EqU_trans)
qed

lemma no_three_distinct_classes_in_band:
  assumes HY1: "H_opt_ep Y⇩1" and EY1: "EDia_ep Y⇩1"
      and HY2: "H_opt_ep Y⇩2" and EY2: "EDia_ep Y⇩2"
      and HY3: "H_opt_ep Y⇩3" and EY3: "EDia_ep Y⇩3"
  shows "¬ (¬ (Arg ((Ω ∧ Ψ) ∧ Y⇩1) ≈ Arg ((Ω ∧ Ψ) ∧ Y⇩2)) ∧
             ¬ (Arg ((Ω ∧ Ψ) ∧ Y⇩1) ≈ Arg ((Ω ∧ Ψ) ∧ Y⇩3)) ∧
             ¬ (Arg ((Ω ∧ Ψ) ∧ Y⇩2) ≈ Arg ((Ω ∧ Ψ) ∧ Y⇩3)))"
proof -
  have E12: "Arg ((Ω ∧ Ψ) ∧ Y⇩1) ≈ Arg ((Ω ∧ Ψ) ∧ Y⇩2)"
    using pulled_pair_collapse_in_band[OF HY1 EY1 HY2 EY2] .
  have E13: "Arg ((Ω ∧ Ψ) ∧ Y⇩1) ≈ Arg ((Ω ∧ Ψ) ∧ Y⇩3)"
    using pulled_pair_collapse_in_band[OF HY1 EY1 HY3 EY3] .
  have E23: "Arg ((Ω ∧ Ψ) ∧ Y⇩2) ≈ Arg ((Ω ∧ Ψ) ∧ Y⇩3)"
    using pulled_pair_collapse_in_band[OF HY2 EY2 HY3 EY3] .
  show ?thesis using E12 E13 E23 by blast
qed

lemma all_pulled_equiv_in_band:
  assumes "finite S" and "∀Y∈S. H_opt_ep Y ∧ EDia_ep Y"
  shows "∃Q. ∀Y∈S. Arg ((Ω ∧ Ψ) ∧ Y) ≈ Q"
proof (cases "S = {}")
  case True then show ?thesis by simp
next
  case False
  obtain Y⇩0 where Y0S: "Y⇩0 ∈ S" by (use False in auto)
  have HY0: "H_opt_ep Y⇩0" and EY0: "EDia_ep Y⇩0"
    using assms(2) Y0S by blast+
  define Q where "Q ≡ Arg ((Ω ∧ Ψ) ∧ Y⇩0)"

  have base: "∀Y∈S. Arg ((Ω ∧ Ψ) ∧ Y) ≈ Q"
  proof
    fix Y assume YS: "Y ∈ S"
    have HY: "H_opt_ep Y" and EY: "EDia_ep Y"
      using assms(2) YS by blast+
    have "Arg ((Ω ∧ Ψ) ∧ Y) ≈ Arg ((Ω ∧ Ψ) ∧ Y⇩0)"
      using pulled_pair_collapse_in_band[OF HY EY HY0 EY0] .
    thus "Arg ((Ω ∧ Ψ) ∧ Y) ≈ Q" by (simp add: Q_def)
  qed

  show ?thesis by (intro exI[of _ Q]) (rule base)
qed

end


subsection ‹14.5 Proof of sandwich existence (no-1, no-2, no-4+, no-superfluous)›

lemma conj_le_S:
  assumes MCL: "⋀e A B. Makes e (A ∧ B) ⟹ Makes e A"
  shows "Arg ((Ω ∧ Ψ) ∧ Y) ≼ Arg (Ω ∧ Ψ)"
proof (unfold LeU_iff_all, intro allI impI)
  fix e
  assume "Makes e ((Ω ∧ Ψ) ∧ Y)"
  then show "Makes e (Ω ∧ Ψ)"
    using MCL by blast
qed

lemma S_le_Phi_via_basic:
  assumes TP_S: "TextPremises (Ω ∧ Ψ) Φ"
  shows "Arg (Ω ∧ Ψ) ≼ Arg Φ"
proof -
  from TextPremisesD[OF TP_S] have "(Ω ∧ Ψ) ⟶⇩U Φ" by auto
  thus ?thesis by (simp add: EntailsU_def)
qed

lemma conj_le_Phi:
  assumes MCL: "⋀e A B. Makes e (A ∧ B) ⟹ Makes e A"
      and Cov: "Arg (Ω ∧ Ψ) ≼ Arg Φ"
  shows "Arg ((Ω ∧ Ψ) ∧ Y) ≼ Arg Φ"
proof -
  have L1: "Arg ((Ω ∧ Ψ) ∧ Y) ≼ Arg (Ω ∧ Ψ)"
    using conj_le_S[OF MCL] .
  show ?thesis using L1 Cov by (rule LeU_trans)
qed

lemma N3_sandwich_expanded_noCmp:
  fixes Ω Ψ Φ :: bool
  assumes ES: "EDia_ep (Ω ∧ Ψ)"
      and Cov: "Arg (Ω ∧ Ψ) ≼ Arg Φ"
      and NS:  "((Arg (Ω ∧ Ψ)) ≼ Arg Φ) ⟹
                (∀Δ. H_opt_ep Δ ⟶ EDia_ep Δ ⟶
                      Arg ((Ω ∧ Ψ) ∧ Δ) ≼ Arg Φ ⟶
                      Arg ((Ω ∧ Ψ) ∧ Δ) ≈ Arg (Ω ∧ Ψ))"
      and Ex:  "∃Y. H_opt_ep Y ∧ EDia_ep Y"
      and MCL: "⋀e A B. Makes e (A ∧ B) ⟹ Makes e A"
      and MCR: "⋀e A B. Makes e (A ∧ B) ⟹ Makes e B"
  shows "∃Y. H_opt_ep Y ∧ EDia_ep Y ∧
            Arg (Ω ∧ Ψ) ≼ Arg Y ∧
            Arg ((Ω ∧ Ψ) ∧ Y) ≼ Arg Φ ∧
            Arg ((Ω ∧ Ψ) ∧ Y) ≈ Arg (Ω ∧ Ψ)"
proof -
  obtain Y where HY: "H_opt_ep Y" and EY: "EDia_ep Y"
    using Ex by blast

  have Conj_le_S: "Arg ((Ω ∧ Ψ) ∧ Y) ≼ Arg (Ω ∧ Ψ)"
    using conj_le_S[OF MCL] .

  have Conj_le_Phi: "Arg ((Ω ∧ Ψ) ∧ Y) ≼ Arg Φ"
    using Conj_le_S Cov by (rule LeU_trans)

  have Eq: "Arg ((Ω ∧ Ψ) ∧ Y) ≈ Arg (Ω ∧ Ψ)"
    using NS[OF Cov] HY EY Conj_le_Phi by blast

  have Conj_le_Y: "Arg ((Ω ∧ Ψ) ∧ Y) ≼ Arg Y"
  proof (unfold LeU_iff_all, intro allI impI)
    fix e
    assume "Makes e ((Ω ∧ Ψ) ∧ Y)"
    then show "Makes e Y" using MCR by blast
  qed

  have BOTH:
    "Arg ((Ω ∧ Ψ) ∧ Y) ≼ Arg (Ω ∧ Ψ) ∧
     Arg (Ω ∧ Ψ) ≼ Arg ((Ω ∧ Ψ) ∧ Y)"
    using Eq by (simp add: EqU_iff_LeU_both)

  have S_le_Conj: "Arg (Ω ∧ Ψ) ≼ Arg ((Ω ∧ Ψ) ∧ Y)"
    using BOTH by blast

  have S_le_Y: "Arg (Ω ∧ Ψ) ≼ Arg Y"
    using S_le_Conj Conj_le_Y by (rule LeU_trans)

  show ?thesis
    by (intro exI[of _ Y]) (use HY EY S_le_Y Conj_le_Phi Eq in blast)
qed

lemma W_from_gap:
  assumes "¬ ((Arg (Ω ∧ Ψ)) ≼ (Arg Φ'))"
  shows   "∃a. Makes a (Ω ∧ Ψ) ∧ ¬ Makes a Φ'"
  using assms by (simp add: not_LeU_iff_exists_witness)


subsection ‹14.6 N@{text "≥"}4 exclusion at realization level›

context Band_Collapse_Superfluous
begin

abbreviation S :: bool where "S ≡ (Ω ∧ Ψ)"

lemma EqU_imp_LeU_L:
  "(Arg X) ≈ (Arg Y) ⟹ (Arg X) ≼ (Arg Y)"
  unfolding EqU_def LeU_def by auto

lemma EqU_imp_LeU_R:
  "(Arg X) ≈ (Arg Y) ⟹ (Arg Y) ≼ (Arg X)"
  unfolding EqU_def LeU_def by auto

lemma LeU_imp_transfer:
  "(Arg X) ≼ (Arg Y) ⟹ Makes e X ⟹ Makes e Y"
  unfolding LeU_iff_all by blast

lemma share_witness_if_real_NS:
  assumes RS: "∃a. Makes a S"
      and HY: "H_opt_ep Y" and EY: "EDia_ep Y"
  shows "∃a. Makes a S ∧ Makes a (S ∧ Y)"
proof -
  obtain a where aS: "Makes a S" using RS by blast
  have Eq: "Arg (S ∧ Y) ≈ Arg S"
    using pulled_eq_and_below_Phi[OF HY EY] by blast
  have Sub: "Arg S ≼ Arg (S ∧ Y)"
    by (rule EqU_imp_LeU_R[OF Eq])
  have aSY: "Makes a (S ∧ Y)"
    by (rule LeU_imp_transfer[OF Sub aS])
  show ?thesis by (intro exI[of _ a]) (use aS aSY in blast)
qed

lemma uniform_realization_for_finite_family:
  fixes Y :: "'i ⇒ bool" and I :: "'i set"
  assumes RS:  "∃a. Makes a S"
      and FIN: "finite I"
      and HY:  "∀i∈I. H_opt_ep (Y i)"
      and EY:  "∀i∈I. EDia_ep (Y i)"
  shows "∃a. ∀i∈I. Makes a (S ∧ Y i)"
proof -
  obtain a where aS: "Makes a S" using RS by blast
  have step: "⋀i. i∈I ⟹ Makes a (S ∧ Y i)"
  proof -
    fix i assume iI: "i∈I"
    have HYi: "H_opt_ep (Y i)" using HY iI by blast
    have EYi: "EDia_ep (Y i)" using EY iI by blast
    have Eq:  "Arg (S ∧ Y i) ≈ Arg S"
      using pulled_eq_and_below_Phi[OF HYi EYi] by blast
    have Sub: "Arg S ≼ Arg (S ∧ Y i)"
      by (rule EqU_imp_LeU_R[OF Eq])
    show "Makes a (S ∧ Y i)"
      by (rule LeU_imp_transfer[OF Sub aS])
  qed
  show ?thesis by (intro exI[of _ a] ballI step)
qed

lemma no_four_distinct_classes_in_band_pre132:
  assumes HY1: "H_opt_ep Y1" and EY1: "EDia_ep Y1"
      and HY2: "H_opt_ep Y2" and EY2: "EDia_ep Y2"
      and HY3: "H_opt_ep Y3" and EY3: "EDia_ep Y3"
      and HY4: "H_opt_ep Y4" and EY4: "EDia_ep Y4"
  shows "¬ (¬ (Arg (S ∧ Y1) ≈ Arg (S ∧ Y2)) ∧
             ¬ (Arg (S ∧ Y1) ≈ Arg (S ∧ Y3)) ∧
             ¬ (Arg (S ∧ Y1) ≈ Arg (S ∧ Y4)) ∧
             ¬ (Arg (S ∧ Y2) ≈ Arg (S ∧ Y3)) ∧
             ¬ (Arg (S ∧ Y2) ≈ Arg (S ∧ Y4)) ∧
             ¬ (Arg (S ∧ Y3) ≈ Arg (S ∧ Y4)))"
proof -
  have E12: "Arg (S ∧ Y1) ≈ Arg (S ∧ Y2)"
    using pulled_pair_collapse_in_band[OF HY1 EY1 HY2 EY2] .
  have E13: "Arg (S ∧ Y1) ≈ Arg (S ∧ Y3)"
    using pulled_pair_collapse_in_band[OF HY1 EY1 HY3 EY3] .
  have E14: "Arg (S ∧ Y1) ≈ Arg (S ∧ Y4)"
    using pulled_pair_collapse_in_band[OF HY1 EY1 HY4 EY4] .
  have E23: "Arg (S ∧ Y2) ≈ Arg (S ∧ Y3)"
    using pulled_pair_collapse_in_band[OF HY2 EY2 HY3 EY3] .
  have E24: "Arg (S ∧ Y2) ≈ Arg (S ∧ Y4)"
    using pulled_pair_collapse_in_band[OF HY2 EY2 HY4 EY4] .
  have E34: "Arg (S ∧ Y3) ≈ Arg (S ∧ Y4)"
    using pulled_pair_collapse_in_band[OF HY3 EY3 HY4 EY4] .
  show ?thesis using E12 E13 E14 E23 E24 E34 by blast
qed

end


subsection ‹14.7 Minimal nonempty core @{text "Ω"}@{text "∧"}@{text "Ψ"} and no new independent pillar via @{text "Δ"}›

locale Band_Collapse_From_Hopt =
  fixes Ω Ψ Φ :: bool
  assumes ES:  "EDia_ep (Ω ∧ Ψ)"
      and Cov: "Arg (Ω ∧ Ψ) ≼ Arg Φ"
      and MCL: "⋀e A B. Makes e (A ∧ B) ⟹ Makes e A"
      and MCR: "⋀e A B. Makes e (A ∧ B) ⟹ Makes e B"
      and MCI: "⋀e A B. Makes e A ⟹ Makes e B ⟹ Makes e (A ∧ B)"
begin

lemma conj_le_left[simp]:  "Arg (A ∧ B) ≼ Arg A"
  unfolding LeU_iff_all by (auto dest: MCL)

lemma conj_le_right[simp]: "Arg (A ∧ B) ≼ Arg B"
  unfolding LeU_iff_all by (auto dest: MCR)

end


subsection ‹14.8 NS(No-Superfluous) locale assumption dischare›
text ‹
  NS (``No-Superfluous'') is the redundancy filter for the core.
  It states that if a candidate Y is itself H-optimal and epistemically admissible,
  and if the enlarged conjunction (S @{text "∧"} Y) still remains within the Phi-band,
  then this enlargement contributes no genuinely new Arg-content:
  Arg (S @{text "∧"} Y) must be Arg-equivalent to Arg S.

  Hence NS blocks superfluous duplication of the core inside the admissible band.›

text ‹
STRUCTURAL ROLE OF THIS SUBSECTION:
  The ``Discharge Engine'' for the Band @{text "≈"}-Collapse (N @{text "≥"} 4 Exclusion)

  In Sections 14.4 - 14.6, we proved that 4 or more independent supreme heads
  (N @{text "≥"} 4) will inevitably undergo an @{text "≈"}-collapse. However, that proof temporarily
  relied on a structural assumption called ``NS'' (No-Superfluous).

  If we left ``NS'' as an unproven assumption, it would act as a hidden axiom,
  fatally weakening the strictly axiom-free claim of this development.

  The core purpose of Section 14.8 is to completely eliminate (discharge)
  this ``NS'' assumption. We mathematically prove that ``NS'' is NOT an external
  metaphysical axiom, but an inescapable analytic consequence derived purely from
  basic Boolean logic (MCL, MCI) combined with the foundational H-Principle.

  The Proof Mechanism (The Sandwich Compression in ``core\_conj\_equiv\_basic''):
  1. Bounded from above (via MCL): Arg(S @{text "∧"} Y) @{text "≼"} Arg(S)
     - A logical conjunction cannot contain more foundational support than its parts.
  2. Bounded from below (via MCI + H-Principle): Arg(S) @{text "≼"} Arg(S @{text "∧"} Y)
     - Because Y is an optimal head (H\_opt), it already covers all possibilities
       of the core S. Thus, adding Y via conjunction provides no new independent
       support.
  3. @{text "≈"}-Collapse: Squeezed from both sides, Arg(S @{text "∧"} Y) @{text "≈"} Arg(S) is strictly forced.

  Conclusion: Any attempt to add a new optimal pillar (Y) to an existing optimal
  core (S) yields exactly zero new epistemic coverage. The system is structurally
  locked, making N @{text "≥"} 4 logically impossible without needing any external axioms. ›

definition NS_restricted :: "bool ⇒ bool ⇒ bool" where
  "NS_restricted S Φ ≡
     (∀Y. H_opt_ep Y ⟶ EDia_ep Y ⟶
          Arg (S ∧ Y) ≼ Arg Φ ⟶
          Arg (S ∧ Y) ≈ Arg S)"
text ‹ Restricted NS: no admissible H-opt extension of S yields a genuinely new layer below Phi.›

lemma NSIOF_from_NS_restricted:
  "NS_restricted S Φ ⟶
     (Arg S ≼ Arg Φ ⟶
      (∀Y. H_opt_ep Y ⟶ EDia_ep Y ⟶
           Arg (S ∧ Y) ≼ Arg Φ ⟶
           Arg (S ∧ Y) ≈ Arg S))"
  by (simp add: NS_restricted_def)

definition Pull_de :: "bool ⇒ bool ⇒ bool" where
  "Pull_de S Φ ≡ NS_restricted S Φ"

abbreviation Pull_NS :: "bool ⇒ bool ⇒ bool" where
  "Pull_NS S Φ ≡ Pull_de S Φ"

lemma NS_restricted_132_from_Pull:
  "Pull_de S Φ ⟶ NS_restricted S Φ"
  by (simp add: Pull_de_def)

lemma EqU_from_LeU:
  assumes XY: "X ≼ Y" and YX: "Y ≼ X"
  shows "X ≈ Y"
proof -
  have "SuppU X ⊆ SuppU Y" using XY unfolding LeU_def by blast
  moreover have "SuppU Y ⊆ SuppU X" using YX unfolding LeU_def by blast
  ultimately have "SuppU X = SuppU Y" by (rule subset_antisym)
  thus ?thesis unfolding EqU_def by simp
qed

lemma core_conj_equiv_basic:
  fixes Ω Ψ Y :: bool
  assumes ES       : "EDia_ep (Ω ∧ Ψ)"    
      and HY       : "H_opt_ep Y"                
      and EY       : "EDia_ep Y"                
      and Core_to_Y: "Arg (Ω ∧ Ψ) ≼ Arg Y"
      and MCL      : "⋀e A B. Makes e (A ∧ B) ⟹ Makes e A"
      and MCI      : "⋀e A B. Makes e A ⟹ Makes e B ⟹ Makes e (A ∧ B)"
  shows "Arg ((Ω ∧ Ψ) ∧ Y) ≈ Arg (Ω ∧ Ψ)"
proof -
  (* 1) left projection: (S ∧ Y) ⪯ S *)
  have conj_le_left: "Arg (A ∧ B) ≼ Arg A" for A B
    unfolding LeU_iff_all by (auto dest: MCL)
  have sub1: "Arg ((Ω ∧ Ψ) ∧ Y) ≼ Arg (Ω ∧ Ψ)"
    by (rule conj_le_left)
  (* 2) S ⪯ (S ∧ Y): from Core_to_Y + ∧-intro on Makes *)
  have sub2: "Arg (Ω ∧ Ψ) ≼ Arg ((Ω ∧ Ψ) ∧ Y)"
  proof (unfold LeU_iff_all, intro allI impI)
    fix e assume eS: "Makes e (Ω ∧ Ψ)"
    have S_to_Y: "∀f. Makes f (Ω ∧ Ψ) ⟶ Makes f Y"
      using Core_to_Y by (simp add: LeU_iff_all)
    have eY: "Makes e Y" using S_to_Y eS by blast
    show "Makes e ((Ω ∧ Ψ) ∧ Y)"
      using MCI[OF eS eY] .
  qed

  show ?thesis
    by (rule EqU_from_LeU[OF sub1 sub2])
qed

text ‹-- ES bridge inside the world-locale --›
context Boolean_at_our_world
begin

lemma ES_from_notRef_triple:
  assumes RCW: "⋀X Y. Ref X ⟹ Ref (X ∧ Y)"
      and NRT: "¬ Ref ((Φ ∧ Ω) ∧ Ψ)"
  shows "EDia_ep (Ω ∧ Ψ)"
  using EDia_ep_pair_from_notRef_triple_plain[OF RCW NRT] .

text ‹-- NS discharge (EH-free) --›
lemma NS_discharge_from_ES:
  fixes Phi Omega Psi :: bool
  assumes ES  : "EDia_ep (Omega ∧ Psi)"
      and MCL : "⋀e A B. Makes e (A ∧ B) ⟹ Makes e A"
      and MCI : "⋀e A B. Makes e A ⟹ Makes e B ⟹ Makes e (A ∧ B)"
      and Core_to_Y_rule: "⋀Y. H_opt_ep Y ⟹ Arg (Omega ∧ Psi) ≼ Arg Y"
  shows "NS_restricted (Omega ∧ Psi) Phi"
proof -
  show ?thesis
    unfolding NS_restricted_def
  proof (intro allI impI)
    fix Y
    assume HY: "H_opt_ep Y"
    assume EY: "EDia_ep Y"
    assume Band: "Arg ((Omega ∧ Psi) ∧ Y) ≼ Arg Phi"  

    have core_to_Y: "Arg (Omega ∧ Psi) ≼ Arg Y"
      using Core_to_Y_rule[OF HY] .

  have sub1: "Arg ((Omega ∧ Psi) ∧ Y) ≼ Arg (Omega ∧ Psi)"
proof (unfold LeU_iff_all, intro allI impI)
  fix e
  assume eSY: "Makes e ((Omega ∧ Psi) ∧ Y)"
  show "Makes e (Omega ∧ Psi)"
    using MCL[OF eSY] .
qed

    have sub2: "Arg (Omega ∧ Psi) ≼ Arg ((Omega ∧ Psi) ∧ Y)"
    proof (unfold LeU_iff_all, intro allI impI)
      fix e
      assume eS: "Makes e (Omega ∧ Psi)"
      have eY: "Makes e Y"
      proof -
        have S_to_Y: "∀f. Makes f (Omega ∧ Psi) ⟶ Makes f Y"
          using core_to_Y by (simp add: LeU_iff_all)
        show "Makes e Y" using S_to_Y eS by blast
      qed
      show "Makes e ((Omega ∧ Psi) ∧ Y)"
        using MCI[OF eS eY] .
    qed

    show "Arg ((Omega ∧ Psi) ∧ Y) ≈ Arg (Omega ∧ Psi)"
      by (rule EqU_from_LeU[OF sub1 sub2])
  qed
qed

lemma NS_discharge:
  fixes Phi Omega Psi :: bool
  assumes RCW  : "⋀X Y. Ref X ⟹ Ref (X ∧ Y)"
      and NRT  : "¬ Ref ((Phi ∧ Omega) ∧ Psi)"
      and MCL  : "⋀e A B. Makes e (A ∧ B) ⟹ Makes e A"
      and MCR  : "⋀e A B. Makes e (A ∧ B) ⟹ Makes e B"  
      and MCI  : "⋀e A B. Makes e A ⟹ Makes e B ⟹ Makes e (A ∧ B)"
      and Core_to_Y_rule: "⋀Y. H_opt_ep Y ⟹ Arg (Omega ∧ Psi) ≼ Arg Y"
  shows "NS_restricted (Omega ∧ Psi) Phi"
proof -
  have ES: "EDia_ep (Omega ∧ Psi)"
    by (rule ES_from_notRef_triple[OF RCW NRT])

  show ?thesis
  proof (rule NS_discharge_from_ES)
    show "EDia_ep (Omega ∧ Psi)" by (rule ES)
    show "⋀e A B. Makes e (A ∧ B) ⟹ Makes e A" by (rule MCL)
    show "⋀e A B. Makes e A ⟹ Makes e B ⟹ Makes e (A ∧ B)" by (rule MCI)
    show "⋀Y. H_opt_ep Y ⟹ Arg (Omega ∧ Psi) ≼ Arg Y" by (rule Core_to_Y_rule)
  qed
qed

lemma NS_with_Cov:
  fixes Phi Omega Psi :: bool
  assumes ES  : "EDia_ep (Omega ∧ Psi)"
      and MCL : "⋀e A B. Makes e (A ∧ B) ⟹ Makes e A"
      and MCI : "⋀e A B. Makes e A ⟹ Makes e B ⟹ Makes e (A ∧ B)"
      and Cov0: "Arg (Omega ∧ Psi) ≼ Arg Phi"
      and Core_to_Y_rule: "⋀Y. H_opt_ep Y ⟹ Arg (Omega ∧ Psi) ≼ Arg Y"
  shows "NS_restricted (Omega ∧ Psi) Phi"
    and "Arg (Omega ∧ Psi) ≼ Arg Phi"
proof -
  have NSre: "NS_restricted (Omega ∧ Psi) Phi"
    by (rule NS_discharge_from_ES[OF ES MCL MCI Core_to_Y_rule])
  show "NS_restricted (Omega ∧ Psi) Phi" by (rule NSre)
  show "Arg (Omega ∧ Psi) ≼ Arg Phi" by (rule Cov0)
qed

end


section ‹15. n=1 exclusion›

text ‹
  Intuition:
  Structurally, a solitary top element in an impoverished
  comparison domain may still fail to be genuinely unsurpassable, since a richer
  domain could in principle contain a stronger candidate. By contrast, a co-maximal
  structure realized within a comparison domain already saturated by the strongest
  admissible candidates removes that possibility altogether. Hence the decisive issue
  is not merely whether a candidate is ``top'', but whether its top-status is realized
  within the maximally relevant comparison space.
›
subsection ‹15.1 Formal Preliminaries for Singularity Exclusion›
(* --- Epistemic possibility as "not refuted" --- *)
abbreviation Refuted_ep :: "bool ⇒ bool" where
  "Refuted_ep ≡ Ref"

locale Refuted_Backprop =
  assumes ref_back: "⋀P Q. (P ⟶ Q) ⟹ Refuted_ep Q ⟹ Refuted_ep P"
begin

lemma EDia_ep_forward:
  assumes imp: "P ⟶ Q" and possP: "EDia_ep P"
  shows "EDia_ep Q"
  unfolding EDia_ep_def
proof
  assume rq: "Refuted_ep Q"
  have rp: "Refuted_ep P" using ref_back imp rq by blast
  show False
    using possP rp
    unfolding EDia_ep_def
    by blast
qed

end

typedecl P

consts
  AndP  :: "P ⇒ P ⇒ P"  (infixr "⊓" 70)
  ArgP  :: "P ⇒ U"
  HeadP :: "P ⇒ bool"

abbreviation LeP (infix "≼P" 50) where
  "x ≼P y ≡ (ArgP x ≼ ArgP y)"

definition NT_pair_supportP :: "P ⇒ P ⇒ P ⇒ bool" where
  "NT_pair_supportP A B C ≡
     A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ (ArgP (A ⊓ B) ≼ ArgP C)"

definition NT_in_edgesP :: "P ⇒ (P × P) set" where
  "NT_in_edgesP C ≡
     {(A,B). HeadP A ∧ HeadP B ∧ HeadP C ∧ NT_pair_supportP A B C}"
(* Cardinal-compare with a fresh name / notation to avoid clashes *)
definition le_cardP :: "'a set ⇒ 'b set ⇒ bool"  (infix "≼⇩cP" 50) where
  "A ≼⇩cP B ⟷ (∃f. inj_on f A ∧ f ` A ⊆ B)"

definition MaxNTP :: "P ⇒ bool" where
  "MaxNTP q ≡ HeadP q ∧ (∀r. HeadP r ⟶ NT_in_edgesP r ≼⇩cP NT_in_edgesP q)"

definition H_optP :: "P ⇒ bool" where
  "H_optP q ≡ MaxNTP q"

lemma nonempty_not_le_cardP_empty:
  assumes "A ≠ {}"
  shows "¬ (A ≼⇩cP {})"
  using assms
  unfolding le_cardP_def
  by auto

lemma HoptP_edges_nonempty_if_exists_head_nonempty:
  assumes ex: "∃r. HeadP r ∧ NT_in_edgesP r ≠ {}"
      and HQ: "H_optP q"
  shows "NT_in_edgesP q ≠ {}"
proof
  assume E: "NT_in_edgesP q = {}"
  from ex obtain r where Hr: "HeadP r" and Nr: "NT_in_edgesP r ≠ {}" by blast
  have rq: "NT_in_edgesP r ≼⇩cP NT_in_edgesP q"
    using HQ Hr by (simp add: H_optP_def MaxNTP_def)

  show False
    using rq E Nr nonempty_not_le_cardP_empty
    by (metis)
qed

lemma not_all_HoptP_empty_if_exists_head_nonempty:
  assumes exH: "∃q. H_optP q"
      and exN: "∃r. HeadP r ∧ NT_in_edgesP r ≠ {}"
  shows "¬ (∀q. H_optP q ⟶ NT_in_edgesP q = {})"
proof
  assume All: "∀q. H_optP q ⟶ NT_in_edgesP q = {}"
  from exH obtain q where HQ: "H_optP q" by blast
  have "NT_in_edgesP q ≠ {}"
    using HoptP_edges_nonempty_if_exists_head_nonempty[OF exN HQ] .
  moreover have "NT_in_edgesP q = {}" using All HQ by blast
  ultimately show False by blast
qed

locale Epistemic_N1_Exclusion = Refuted_Backprop
begin

lemma epistemic_n1_nonclosure:
  assumes exH: "∃q. H_optP q"
      and poss_nonempty_head: "EDia_ep (∃r. HeadP r ∧ NT_in_edgesP r ≠ {})"
  shows "EDia_ep (¬ (∀q. H_optP q ⟶ NT_in_edgesP q = {}))"
proof -
  have imp:
    "(∃r. HeadP r ∧ NT_in_edgesP r ≠ {})
     ⟶ ¬ (∀q. H_optP q ⟶ NT_in_edgesP q = {})"
    using exH not_all_HoptP_empty_if_exists_head_nonempty
    by blast
  show ?thesis
    using EDia_ep_forward[OF imp poss_nonempty_head] .
qed

end


subsection ‹15.2 Main proof: N=1 exclusion via edge-nonempty possibility›

abbreviation EdgeExist :: bool where
  "EdgeExist ≡ (∃r. HeadP r ∧ NT_in_edgesP r ≠ {})"
(* Exactly one Head (P-version) *)
definition ExactlyOneHeadP :: bool where
  "ExactlyOneHeadP ⟷
     (∃A0. HeadP A0 ∧ (∀C. HeadP C ⟶ C = A0))"
text ‹
  =====================  Epistemic status of @{term EdgeExist}  =====================

  We use the edge-existence proposition

    @{term EdgeExist}  @{text "≡"}  (@{text "∃"}r. HeadP r @{text "∧"} NT\_in\_edgesP r @{text "≠"} {})

  as an epistemic (EDia\_ep) premise in the A-style MaxNT-candidate exclusions.

  (A) Model-backed confirmation (Sections 8,9 of @{file Diagnostics_Nitpick.thy}).
 Sections 8,9 of @{file Diagnostics_Nitpick.thy} provides a concrete satisfiable witness model (e.g., via Nitpick)
  in which there are distinct heads and at least one head has nonempty in-edges.
  Hence @{term EdgeExist} is not merely ``unrefuted'': it is explicitly satisfiable.
  Under the intended reading of EDia\_ep as ``not refuted / consistent with the
  current definitions'', this supports the premise:

    EDia\_ep @{term EdgeExist}.

  (B) Even without an explicit model.
  Even if we do not appeal to the Sections 8,9 of @{file Diagnostics_Nitpick.thy} witness, the epistemic role of
  @{term EdgeExist} can still be stated as a non-refutation condition:
  unless the theory derives a refutation of @{term EdgeExist} (or an equivalent
  proof of impossibility), @{term EdgeExist} remains epistemically live, so
  EDia\_ep @{term EdgeExist} is admissible as a ``not yet refuted'' premise.

  Note.
  - The witness model strengthens the premise from ``not refuted'' to ``witnessed
    satisfiable''.
  - The candidate-exclusion proofs below do not hard-code any specific model;
    they only consume EDia\_ep @{term EdgeExist} as an epistemic available truth-bearer.
›

lemma NT_in_edgesP_nonempty_imp_three_distinct_heads:
  assumes Nr: "NT_in_edgesP r ≠ {}"
  shows "∃A B. HeadP A ∧ HeadP B ∧ HeadP r ∧ A ≠ B ∧ A ≠ r ∧ B ≠ r"
proof -
  have "∃x. x ∈ NT_in_edgesP r" using Nr by auto
  then obtain x where xin: "x ∈ NT_in_edgesP r" by blast
  then obtain A B where Pair: "x = (A,B)" by (cases x) auto
  have InEdges: "(A,B) ∈ NT_in_edgesP r" using xin Pair by simp
  have HA: "HeadP A" and HB: "HeadP B" and Hr: "HeadP r"
      and NT: "NT_pair_supportP A B r"
    using InEdges unfolding NT_in_edgesP_def by auto
  have Dist: "A ≠ B ∧ A ≠ r ∧ B ≠ r"
    using NT unfolding NT_pair_supportP_def by auto
  show ?thesis using HA HB Hr Dist by blast
qed
(* ---------------------------------------------------------
   (1) EdgeExist => not ExactlyOneHeadP
   --------------------------------------------------------- *)
lemma not_ExactlyOneHeadP_if_exists_head_edges_nonempty:
  assumes ex: "EdgeExist"
  shows "¬ ExactlyOneHeadP"
proof
  assume One: "ExactlyOneHeadP"
  from One obtain A0 where HA0: "HeadP A0"
    and RANGE: "∀C. HeadP C ⟶ C = A0"
    unfolding ExactlyOneHeadP_def by blast

  from ex obtain r where Hr: "HeadP r" and Nr: "NT_in_edgesP r ≠ {}" by blast
  from NT_in_edgesP_nonempty_imp_three_distinct_heads[OF Nr]
  obtain A B where HA: "HeadP A" and HB: "HeadP B"
    and Dist: "A ≠ B" "A ≠ r" "B ≠ r"
    by blast

  have Aeq: "A = A0" using RANGE HA by blast
  have Beq: "B = A0" using RANGE HB by blast
  show False using Dist(1) Aeq Beq by blast
qed

lemma Edge_implies_notOneHead:
  shows "EdgeExist ⟶ ¬ ExactlyOneHeadP"
  using not_ExactlyOneHeadP_if_exists_head_edges_nonempty by blast
(* ---------------------------------------------------------
   (2) ExactlyOneHeadP -> all heads have empty edges
   (this is the formal “0 support” consequence of N=1)
   --------------------------------------------------------- *)
lemma ExactlyOneHeadP_imp_all_heads_edges_empty:
  assumes One: "ExactlyOneHeadP"
  shows "∀r. HeadP r ⟶ NT_in_edgesP r = {}"
proof (intro allI impI)
  fix r assume Hr: "HeadP r"
  show "NT_in_edgesP r = {}"
  proof (rule ccontr)
    assume Nr: "NT_in_edgesP r ≠ {}"
    from NT_in_edgesP_nonempty_imp_three_distinct_heads[OF Nr]
    obtain A B where HA: "HeadP A" and HB: "HeadP B"
      and Dist: "A ≠ B" "A ≠ r" "B ≠ r"
      by blast

    from One obtain A0 where HA0: "HeadP A0"
      and RANGE: "∀C. HeadP C ⟶ C = A0"
      unfolding ExactlyOneHeadP_def by blast

    have Aeq: "A = A0" using RANGE HA by blast
    have Beq: "B = A0" using RANGE HB by blast
    have req: "r = A0" using RANGE Hr by blast
    show False using Dist Aeq Beq req by metis
  qed
qed
(* ========================================================= *)
(* 0<1 support articulation (explicit, for readability)        *)
(* ========================================================= *)
(* “All edges empty” = every head has 0 in-edges. *)
definition AllEdgesEmpty :: bool where
  "AllEdgesEmpty ≡ (∀r. HeadP r ⟶ NT_in_edgesP r = {})"

text ‹This lemma does not assert that any edge actually exists, or that EdgeExist is true. It proves only the incompatibility claim: ExactlyOneHeadP and EdgeExist cannot both hold at the same time.›
lemma ExactlyOneHeadP_imp_AllEdgesEmpty:
  assumes One: "ExactlyOneHeadP"
  shows "AllEdgesEmpty"
  using ExactlyOneHeadP_imp_all_heads_edges_empty[OF One]
  unfolding AllEdgesEmpty_def by blast
(* “EdgeExist” = there exists at least one head with >=1 in-edges (nonempty). *)
lemma EdgeExist_imp_not_AllEdgesEmpty:
  assumes ex: "EdgeExist"
  shows "¬ AllEdgesEmpty"
proof
  assume AE: "AllEdgesEmpty"
  obtain r where Hr: "HeadP r" and Nr: "NT_in_edgesP r ≠ {}"
    using ex by blast
  have "NT_in_edgesP r = {}"
    using AE Hr unfolding AllEdgesEmpty_def by blast
  thus False using Nr by blast
qed
(* Therefore: (ExactlyOneHeadP ∧ EdgeExist) is impossible = “0 cannot coexist with 1”. *)
lemma OneHead_and_edge_False:
  shows "(ExactlyOneHeadP ∧ EdgeExist) ⟶ False"
proof
  assume H: "ExactlyOneHeadP ∧ EdgeExist"
  have One: "ExactlyOneHeadP" using H by blast
  have ex: "EdgeExist" using H by blast
  have AE: "AllEdgesEmpty" using ExactlyOneHeadP_imp_AllEdgesEmpty[OF One] .
  have nAE: "¬ AllEdgesEmpty" using EdgeExist_imp_not_AllEdgesEmpty[OF ex] .
  show False using AE nAE by blast
qed
(* ---------------------------------------------------------
   EDia forward lemma (same as N=2 proof)
   --------------------------------------------------------- *)
lemma notEdia_back_from_ref_back:
  assumes ref_back: "⋀P Q. (P ⟶ Q) ⟹ Ref Q ⟹ Ref P"
  shows "⋀P Q. (P ⟶ Q) ⟹ ¬ EDia_ep Q ⟹ ¬ EDia_ep P"
  using ref_back by (simp add: EDia_ep_def)

lemma ref_back_from_notEdia_back:
  assumes notEdia_back: "⋀P Q. (P ⟶ Q) ⟹ ¬ EDia_ep Q ⟹ ¬ EDia_ep P"
  shows "⋀P Q. (P ⟶ Q) ⟹ Ref Q ⟹ Ref P"
  using notEdia_back by (simp add: EDia_ep_def)
text ‹
  Refutation back-propagation (ref\_back) and the EDia\_ep formulation
  (notEdia\_back) are definitionally equivalent since EDia\_ep @{text "≡"} @{text "¬"}Ref.
›

lemma EDia_ep_forward0:
  assumes notEdia_back:
            "⋀P Q. (P ⟶ Q) ⟹ ¬ EDia_ep Q ⟹ ¬ EDia_ep P"
      and imp: "P ⟶ Q"
      and possP: "EDia_ep P"
  shows "EDia_ep Q"
proof (rule ccontr)
  assume nQ: "¬ EDia_ep Q"
  have nP: "¬ EDia_ep P" using notEdia_back[OF imp nQ] .
  show False using possP nP by blast
qed
(* ---------------------------------------------------------
   stronger_edge / MaxNT_candidate (same as N=2 candidate block)
   --------------------------------------------------------- *)
definition stronger_edge :: "bool ⇒ bool ⇒ bool" where
  "stronger_edge Q P ≡
     EDia_ep (Q ∧ EdgeExist) ∧ ¬ EDia_ep (P ∧ EdgeExist)"

definition MaxNT_candidate :: "bool ⇒ bool" where
  "MaxNT_candidate P ≡
     EDia_ep P ∧ (∀Q. EDia_ep Q ⟶ ¬ stronger_edge Q P)"
(* ---------------------------------------------------------
   Final: N=1 disqualified as MaxNT_candidate (N=2 style)
   --------------------------------------------------------- *)
text ‹
Sections 8,9 of @{file Diagnostics_Nitpick.thy} provide a concrete satisfiable witness
(found by Nitpick). This computational witness corroborates that
@{term EdgeExist} is epistemically admissible under the intended reading
of @{term EDia_ep} as ``not refuted.''

In other words, the existence of a non-empty NT-edge structure is not
definitionally blocked by the framework, and thus
@{term "EDia_ep EdgeExist"} is justified at the epistemic level.
›

lemma N1_fails_MaxNT_final:
  assumes poss_edge: "EDia_ep EdgeExist"
      and notEdia_back:
            "⋀P Q. (P ⟶ Q) ⟹ ¬ EDia_ep Q ⟹ ¬ EDia_ep P"
      and notEdia_False: "¬ EDia_ep False"
  shows "¬ MaxNT_candidate ExactlyOneHeadP"
proof
  assume CandN1: "MaxNT_candidate ExactlyOneHeadP"
  (* 1) EdgeExist -> (not OneHead ∧ EdgeExist) *)
  have imp_notN1:
  "EdgeExist ⟶ ¬ ExactlyOneHeadP"
  using Edge_implies_notOneHead .
  have imp_to_conj:
    "EdgeExist ⟶ (¬ ExactlyOneHeadP ∧ EdgeExist)"
     using imp_notN1 by blast

  have poss_notN1_and_edge:
    "EDia_ep (¬ ExactlyOneHeadP ∧ EdgeExist)"
    using EDia_ep_forward0[OF notEdia_back imp_to_conj poss_edge] .
  (* 2) Therefore ¬ EDia_ep (OneHead ∧ EdgeExist) (0 cannot coexist with 1) *)
  have not_possN1_and_edge:
    "¬ EDia_ep (ExactlyOneHeadP ∧ EdgeExist)"
  proof
    assume poss: "EDia_ep (ExactlyOneHeadP ∧ EdgeExist)"
    have nPoss:
      "¬ EDia_ep (ExactlyOneHeadP ∧ EdgeExist)"
      using notEdia_back[OF OneHead_and_edge_False notEdia_False] .
    show False using poss nPoss by blast
  qed
  (* 3) Extract poss_notN1 *)
  have poss_notN1: "EDia_ep (¬ ExactlyOneHeadP)"
  proof -
    have imp1: "(¬ ExactlyOneHeadP ∧ EdgeExist) ⟶ (¬ ExactlyOneHeadP)" by blast
    show ?thesis
      using EDia_ep_forward0[OF notEdia_back imp1 poss_notN1_and_edge] .
  qed
  (* 4) (not OneHead) is stronger than OneHead, contradiction to candidacy *)
  have strong: "stronger_edge (¬ ExactlyOneHeadP) ExactlyOneHeadP"
    unfolding stronger_edge_def
    using poss_notN1_and_edge not_possN1_and_edge by blast

  have no_stronger:
    "¬ stronger_edge (¬ ExactlyOneHeadP) ExactlyOneHeadP"
    using CandN1 poss_notN1
    unfolding MaxNT_candidate_def by blast

  show False using strong no_stronger by blast
qed


section ‹16. N=2 exclusion: N=2 cannot exceed N=1 in MaxNT (mutual vs. non-mutual cases)›

subsection ‹16.1 Support-count machinery (NT\_in\_edges-based)›

definition support_edges_ep :: "bool ⇒ (bool × bool) set" where
  "support_edges_ep X ≡ NT_in_edges_ep X"

definition support_count_ep :: "bool ⇒ nat" where
  "support_count_ep X ≡ card (support_edges_ep X)"

subsection ‹16.2 Case split predicates›

definition Mutual_leU_ep :: "bool ⇒ bool ⇒ bool" where
  "Mutual_leU_ep X Y ≡ (Arg X ≼ Arg Y ∧ Arg Y ≼ Arg X)"

definition No_cross_support_ep :: "bool ⇒ bool ⇒ bool" where
  "No_cross_support_ep X Y ≡
     (¬ (∃S. NT_pair_support_ep X S Y) ∧ ¬ (∃S. NT_pair_support_ep Y S X))"

definition Nonmutual_symmetric_ep :: "bool ⇒ bool ⇒ bool" where
  "Nonmutual_symmetric_ep X Y ≡
     No_cross_support_ep X Y ∧ support_edges_ep X = support_edges_ep Y"

paragraph ‹Case (1): mutual (Arg-level) support @{text "⇒"} Arg-collapse ›

lemma case_mutual_leU_ep:
  assumes two: "TwoHypostases_ep Ω Π"
      and mut: "Mutual_leU_ep Ω Π"
      and EqU_iff_LeU_both_assm:
        "⋀A B. (A ≈ B) ⟷ (A ≼ B ∧ B ≼ A)"
      and TwoHypostases_noEqArg:
        "⋀Ω Π. TwoHypostases_ep Ω Π ⟹ ¬ (Arg Ω ≈ Arg Π)"
  shows False
proof -
  have eq: "Arg Ω ≈ Arg Π"
    using mut EqU_iff_LeU_both_assm by (auto simp: Mutual_leU_ep_def)
  show False
    using TwoHypostases_noEqArg[OF two] eq by blast
qed

paragraph ‹Case (2): nonmutual symmetric @{text "⇒"} equal counts›

lemma case_nonmutual_equal_count_ep:
  assumes sym: "Nonmutual_symmetric_ep Ω Π"
  shows "support_count_ep Ω = support_count_ep Π"
  using sym
  by (simp add: Nonmutual_symmetric_ep_def support_count_ep_def)


subsection ‹16.3 Clean case split lemma›

theorem N2_cases:
  assumes two: "TwoHypostases_ep Ω Π"
    and EqU_iff_LeU_both_assm: "⋀A B. (A ≈ B) ⟷ (A ≼ B ∧ B ≼ A)"
    and TwoHypostases_noEqArg: "⋀Ω Π. TwoHypostases_ep Ω Π ⟹ ¬ (Arg Ω ≈ Arg Π)"
  shows "Mutual_leU_ep Ω Π ⟹ False"
    and "Nonmutual_symmetric_ep Ω Π ⟹ support_count_ep Ω = support_count_ep Π"
proof -
  { assume mut: "Mutual_leU_ep Ω Π"
     show False
      apply (rule case_mutual_leU_ep [where Ω=Ω and Π=Π])
      using two apply assumption
      using mut apply assumption
      using EqU_iff_LeU_both_assm apply assumption
      using TwoHypostases_noEqArg apply assumption
      done }

  { assume sym: "Nonmutual_symmetric_ep Ω Π"
       show "support_count_ep Ω = support_count_ep Π"
      using case_nonmutual_equal_count_ep [OF sym]
      by simp }
qed

subsection ‹16.4 Explicit tie statement: if N=2 is nonmutual symmetric, it cannot exceed N=1›

lemma N2_tie_cannot_exceed_N1:
  assumes sym: "Nonmutual_symmetric_ep Ω Π"
  shows "support_count_ep Ω = support_count_ep Π"
    and "¬ (support_count_ep Ω > support_count_ep Π)"
    and "¬ (support_count_ep Π > support_count_ep Ω)"
proof -
  have eq: "support_count_ep Ω = support_count_ep Π"
    using case_nonmutual_equal_count_ep[OF sym] .
  show "support_count_ep Ω = support_count_ep Π" using eq .
  show "¬ (support_count_ep Ω > support_count_ep Π)" using eq by simp
  show "¬ (support_count_ep Π > support_count_ep Ω)" using eq by simp
qed

subsection ‹16.5 Nonmutual symmetric @{text "⇒"} indistinguishable (so not a genuine N=2 split)›

lemma Nonmutual_symmetric_imp_EqNT_ep:
  assumes sym: "Nonmutual_symmetric_ep X Y"
  shows "X ≈⇩NT Y"
  using sym
  by (simp add: Nonmutual_symmetric_ep_def EqNT_ep_def support_edges_ep_def)

corollary Nonmutual_symmetric_not_Distinct_ep:
  assumes sym: "Nonmutual_symmetric_ep X Y"
  shows "¬ Distinct_ep X Y"
  using sym
  by (simp add: Distinct_ep_def Nonmutual_symmetric_imp_EqNT_ep)

text ‹
  In the nonmutual symmetric case, the two candidates are tied and also NT-indistinguishable,
  hence they cannot serve as two distinct hypostases in the sense of @{term Distinct_ep}.
›

corollary Nonmutual_symmetric_blocks_two_witness:
  assumes sym: "Nonmutual_symmetric_ep Ω Π"
  shows "¬ (Distinct_ep Ω Π)"
  using Nonmutual_symmetric_not_Distinct_ep[OF sym] .
(* ===================== N=2 exclusion (N=1 exclusion style) ===================== *)
subsection ‹16.6 Main proof: N=2 exclusion (epistemic candidate only)›

definition ExactlyTwoHeadsP :: bool where
  "ExactlyTwoHeadsP ⟷
    (∃A0 B0.
      A0 ≠ B0 ∧ HeadP A0 ∧ HeadP B0 ∧
      (∀C. HeadP C ⟶ (C = A0 ∨ C = B0)))"
(* Reuse the same EdgeExist abbreviation already introduced earlier:
   EdgeExist ≡ (∃r. HeadP r ∧ NT_in_edgesP r ≠ {}) *)
lemma Edge_blocks_N2: "EdgeExist ⟶ ¬ ExactlyTwoHeadsP"
proof
  assume E: "EdgeExist"
  show "¬ ExactlyTwoHeadsP"
  proof
    assume Two: "ExactlyTwoHeadsP"
    then obtain A0 B0 where
      AB0: "A0 ≠ B0" and
      HA0: "HeadP A0" and HB0: "HeadP B0" and
      RANGE: "∀C. HeadP C ⟶ (C = A0 ∨ C = B0)"
      unfolding ExactlyTwoHeadsP_def by blast

    obtain r where Hr: "HeadP r" and Nr: "NT_in_edgesP r ≠ {}"
      using E by blast

    obtain x where xin: "x ∈ NT_in_edgesP r"
      using Nr by blast
    then obtain A B where xAB: "x = (A,B)"
      by (cases x) auto
    have InEdges: "(A,B) ∈ NT_in_edgesP r"
      using xin xAB by simp

    have HA: "HeadP A" and HB: "HeadP B" and Hr': "HeadP r"
      and NT: "NT_pair_supportP A B r"
      using InEdges unfolding NT_in_edgesP_def by auto

    have Dist: "A ≠ B" "A ≠ r" "B ≠ r"
      using NT unfolding NT_pair_supportP_def by auto

    have A01: "A = A0 ∨ A = B0" using RANGE HA by blast
    have B01: "B = A0 ∨ B = B0" using RANGE HB by blast
    have r01: "r = A0 ∨ r = B0" using RANGE Hr' by blast

    show False using AB0 A01 B01 r01 Dist by metis
  qed
qed

definition MaxNT_candidate_N2 :: "bool ⇒ bool" where
  "MaxNT_candidate_N2 P ≡
     EDia_ep P ∧ (∀Q. EDia_ep Q ⟶ ¬ stronger_edge Q P)"
(* Final verdict (candidate knockout): epistemic only.
   Uses the proved structural lemma Edge_blocks_N2, no extra assumes. *)
lemma N2_fails_MaxNT_final:
  assumes poss_edge: "EDia_ep EdgeExist"
      and notEdia_back:
            "⋀P Q. (P ⟶ Q) ⟹ ¬ EDia_ep Q ⟹ ¬ EDia_ep P"
      and notEdia_False: "¬ EDia_ep False"
  shows "¬ MaxNT_candidate_N2 ExactlyTwoHeadsP"
proof
  assume CandN2: "MaxNT_candidate_N2 ExactlyTwoHeadsP"
  (* 1) EdgeExist -> (not N2 ∧ EdgeExist) *)
  have imp_to_conj:
    "EdgeExist ⟶ (¬ ExactlyTwoHeadsP ∧ EdgeExist)"
    using Edge_blocks_N2 by blast
  (* 2) From poss_edge, forward to poss (notN2 and EdgeExist) *)
  have poss_notN2_and_edge:
    "EDia_ep (¬ ExactlyTwoHeadsP ∧ EdgeExist)"
    using EDia_ep_forward0[OF notEdia_back imp_to_conj poss_edge] .
  (* 3) (N2 ∧ EdgeExist) -> False, hence not EDia_ep (N2 ∧ EdgeExist) *)
  have N2_and_edge_False:
    "(ExactlyTwoHeadsP ∧ EdgeExist) ⟶ False"
  proof
    assume H: "ExactlyTwoHeadsP ∧ EdgeExist"
    have Two: "ExactlyTwoHeadsP" and E: "EdgeExist" using H by blast+
    have nTwo: "¬ ExactlyTwoHeadsP" using Edge_blocks_N2 E by blast
    show False using Two nTwo by blast
  qed

  have not_possN2_and_edge:
    "¬ EDia_ep (ExactlyTwoHeadsP ∧ EdgeExist)"
    using notEdia_back[OF N2_and_edge_False notEdia_False] .
  (* 4) Extract poss_notN2 *)
  have poss_notN2: "EDia_ep (¬ ExactlyTwoHeadsP)"
  proof -
    have imp1:
      "(¬ ExactlyTwoHeadsP ∧ EdgeExist) ⟶ (¬ ExactlyTwoHeadsP)"
      by blast
    show ?thesis
      using EDia_ep_forward0[OF notEdia_back imp1 poss_notN2_and_edge] .
  qed
  (* 5) (notN2) is stronger than N2, contradicting candidacy *)
  have strong:
    "stronger_edge (¬ ExactlyTwoHeadsP) ExactlyTwoHeadsP"
    unfolding stronger_edge_def
    using poss_notN2_and_edge not_possN2_and_edge by blast

  have no_stronger:
    "¬ stronger_edge (¬ ExactlyTwoHeadsP) ExactlyTwoHeadsP"
    using CandN2 poss_notN2
    unfolding MaxNT_candidate_N2_def by blast

  show False using strong no_stronger by blast
qed


section ‹17. Actuality and Forcing: World-Lifted Existence of H\_opt q(@{text "∃"}q. H\_opt q) and the N=3 Conclusion›

subsection ‹17.1 Forcing the triune case ``N3''›
text ‹
  We work with four structural cases for ultimate heads:

    N1\_exact   -- exactly one absolute head
    N2\_exact   -- exactly two independent heads
    N3         -- triune mutual-support package
    N4plus     -- four-or-more essentially independent heads

  Key point (clean logic):

  Existence trigger (DN).
    We assume (@{text "¬"}@{text "¬"})(@{text "∃"}x. H\_opt x).
    Since Isabelle/HOL is classical, this yields @{text "∃"}x. H\_opt x.
    Philosophical reading: the ground cannot ``evaporate''; we are not allowed to
    settle into the degenerate option @{text "¬"}@{text "∃"}x. H\_opt x.

  Conditional exhaustiveness.
    The case split is not asserted unconditionally.
    We assume only the conditional form:
      (@{text "∃"}x. H\_opt x)  @{text "⟶"} (N1\_exact @{text "∨"} N2\_exact @{text "∨"} N3 @{text "∨"} N4plus).
    So the disjunction is activated *only after* existence is obtained.

  Elimination (forcing).
    Once the disjunction is available, ruling out ``N1\_exact'', ``N2\_exact'',
    and ``N4plus'' leaves ``N3'' as the unique remaining live case.

  Therefore DN is not decorative: it is the engine that activates the exhaustiveness,
  i.e. it licenses the disjunction by guaranteeing existence.
›

text ‹
  Case-label packaging for the forcing step (Section 17).

  In this section, we treat the ``N=1 exact'' and ``N=2 exact'' cases as
  the corresponding MaxNT-candidate propositions used in the epistemic
  exclusion blocks (Sections 15.2 and 16.6).

  This keeps the forcing logic uniform: the disjunction is over boolean
  case-labels, and the exclusions are exactly the proved negations of
  those labels.
›
definition N1_exact :: bool where
  "N1_exact ≡ MaxNT_candidate ExactlyOneHeadP"

definition N2_exact :: bool where
  "N2_exact ≡ MaxNT_candidate_N2 ExactlyTwoHeadsP"
(* N>=4 case-label: reuse the already-defined ep-level predicate *)
definition N4plus :: bool where
  "N4plus ≡
     (∃a b c d.
        H_opt_ep a ∧ H_opt_ep b ∧ H_opt_ep c ∧ H_opt_ep d ∧
        EDia_ep a  ∧ EDia_ep b  ∧ EDia_ep c  ∧ EDia_ep d  ∧
        ¬ (a ≈⇩NT b) ∧ ¬ (a ≈⇩NT c) ∧ ¬ (a ≈⇩NT d) ∧
        ¬ (b ≈⇩NT c) ∧ ¬ (b ≈⇩NT d) ∧ ¬ (c ≈⇩NT d))"

lemma noN1:
  assumes poss_edge: "EDia_ep EdgeExist"
      and notEdia_back:
            "⋀P Q. (P ⟶ Q) ⟹ ¬ EDia_ep Q ⟹ ¬ EDia_ep P"
      and notEdia_False: "¬ EDia_ep False"
  shows "¬ N1_exact"
  unfolding N1_exact_def
  using N1_fails_MaxNT_final[OF poss_edge notEdia_back notEdia_False] .

lemma noN2:
  assumes poss_edge: "EDia_ep EdgeExist"
      and notEdia_back:
            "⋀P Q. (P ⟶ Q) ⟹ ¬ EDia_ep Q ⟹ ¬ EDia_ep P"
      and notEdia_False: "¬ EDia_ep False"
  shows "¬ N2_exact"
  unfolding N2_exact_def
  using N2_fails_MaxNT_final[OF poss_edge notEdia_back notEdia_False] .

lemma noN4:
  assumes noN4ep: "¬ N4plus"
  shows "¬ N4plus"
  using noN4ep by (simp add: N4plus_def)

lemma force_N3_from_exhaust_and_exclusions:
  assumes Exhaust: "N1_exact ∨ N2_exact ∨ N3 ∨ N4plus"
    and noN1: "¬ N1_exact"
    and noN2: "¬ N2_exact"
    and noN4: "¬ N4plus"
  shows N3
proof -
  have "N3 ∨ N1_exact ∨ N2_exact ∨ N4plus"
    using Exhaust by blast
  thus N3
    using noN1 noN2 noN4 by blast
qed

text ‹
  Clean forced-N3 lemma (DN actually used):

  DN ensures existence:
      (@{text "¬"}@{text "¬"})(@{text "∃"}x. H\_opt x)  implies (@{text "∃"}x. H\_opt x).

  Exhaust\_if\_exists provides the 4-way case split *conditional on existence*:
      (@{text "∃"}x. H\_opt x)  @{text "⟶"} (N1\_exact @{text "∨"} N2\_exact @{text "∨"} N3 @{text "∨"} N4plus).

  With ``N1\_exact'', ``N2\_exact'', ``N4plus'' excluded,
        the only remaining case is ``N3''.

  This makes the dependency explicit:
    without DN you cannot fire Exhaust\_if\_exists, hence you cannot conclude N3.
›
lemma N3_forced_clean:
  assumes DN: "¬¬ (∃x. H_opt x)"
      and Exhaust_if_exists:
            "(∃x. H_opt x) ⟶ (N1_exact ∨ N2_exact ∨ N3 ∨ N4plus)"
      and noN1: "¬ N1_exact"
      and noN2: "¬ N2_exact"
      and noN4: "¬ N4plus"
  shows N3
proof -
  have Ex: "∃x. H_opt x"
    using DN by blast

  have Exhaust: "N1_exact ∨ N2_exact ∨ N3 ∨ N4plus"
    using Exhaust_if_exists Ex by blast

  show N3
    using force_N3_from_exhaust_and_exclusions[OF Exhaust noN1 noN2 noN4] .
qed

subsection ‹17.2  Actuality at the distinguished U-world-point (our-world)›
text ‹
  Recap.
    We already proved ``N3'' purely in the U-layer (Section 13.3 / 17.1),
    i.e. there exist three optimal heads a b c such that the fully symmetric
    ``pair @{text "⟶"} third'' closure holds uniformly at every U-point e
    (see N3\_def). No modal axioms and no extra metaphysical axioms were used.

  Goal (17.2).
    Instantiate that uniform closure at the distinguished point e0 and
    package it as a single internal statement TriuneGod\_e0.
    This uses only @{term Supports}, @{term H_opt}, @{term e0}, and the theorem @{term N3}
    (no Ref / EDia\_ep / Val / @{text "w⇩0"}, and no modal axioms).

  World-reading (methodological, not an axiom).
    We do not add ``U = our world'' as an axiom inside the U-layer (that would be circular).
    Rather, we adopt it as an external interpretive identification—i.e. the usual way
    we interpret a formal system as describing (or modeling) facts about reality.
    Likewise, HOL's basic principles are trusted precisely because they are built from
    highly evident rules; interpreting them as applicable to our reasoning about reality
    is a methodological stance, not an extra postulate inside the object theory.
›

lemma TriuneGod_e0_pair_closure_from_N3:
  assumes N3H: N3
  shows "∃a b c.
          H_opt a ∧ H_opt b ∧ H_opt c ∧
          ((Supports e0 b ∧ Supports e0 c) ⟶ Supports e0 a) ∧
          ((Supports e0 c ∧ Supports e0 a) ⟶ Supports e0 b) ∧
          ((Supports e0 a ∧ Supports e0 b) ⟶ Supports e0 c)"
proof -
  obtain a b c where
    Ha: "H_opt a" and Hb: "H_opt b" and Hc: "H_opt c"
    and Sbc: "∀e. (Supports e b ∧ Supports e c) ⟶ Supports e a"
    and Sca: "∀e. (Supports e c ∧ Supports e a) ⟶ Supports e b"
    and Sab: "∀e. (Supports e a ∧ Supports e b) ⟶ Supports e c"
    using N3H unfolding N3_def by blast
  show ?thesis using Ha Hb Hc Sbc Sca Sab by blast
qed

definition TriuneGod_e0 :: bool where
  "TriuneGod_e0 ≡
     (∃a b c.
        H_opt a ∧ H_opt b ∧ H_opt c ∧
        ((Supports e0 b ∧ Supports e0 c) ⟶ Supports e0 a) ∧
        ((Supports e0 c ∧ Supports e0 a) ⟶ Supports e0 b) ∧
        ((Supports e0 a ∧ Supports e0 b) ⟶ Supports e0 c))"

lemma TriuneGod_e0_holds_from_N3:
  assumes N3H: N3
  shows "TriuneGod_e0"
  unfolding TriuneGod_e0_def
  using TriuneGod_e0_pair_closure_from_N3[OF N3H] by blast
text ‹
  Final philosophical summary.

    (1) Methodological identification (not an axiom).
    We treat the Isabelle U-layer (Supports / H\_opt / the distinguished @{term e0})
    as a formal description of our actual world. This is not added as an axiom
    inside the U-layer (that would be circular); rather, it is an interpretive stance
    taken when reading mathematics.

    This identification is of the same kind as the standard interpretive practice of mathematics:
    results proved from axioms are read as applicable to reality, without re-encoding that applicability
    as an additional axiom inside the object theory.

        Analogy: arithmetic facts such as ``1+1=2'' are proved internally from axioms,
        yet we naturally read them as truths about ordinary counting in reality.
        In doing so, we treat the underlying axioms/rules as applicable to our reasoning
        and to the description of the world.

        Likewise, HOL's basic commitments are accepted precisely as highly evident principles;
        interpreting them as applicable to reality is therefore not an arbitrary stipulation,
        but a methodologically justified interpretation.

    (2) Internal theorem.
        Within that very U-structure, @{term N3} is already proved (Section 17.1),
        axiom-free at the U-layer (no modal axioms, no extra metaphysical postulates).

    (3) Actuality at @{term e0}.
        Since @{term N3} quantifies @{text "∀"}e, we specialize it to @{term e0},
        obtaining @{term TriuneGod_e0}: at our world-point, the ``pair @{text "⟶"} third''
        closure holds for some three optimal heads.

    (4) Consequence.
        Given (1)–(3), the ultimate ground of our world is coherently forced to be triune:
        rival patterns (pure one-head, strict two-head, or 4+-head fragmentation) are excluded
        by the same U-internal constraints that yielded @{term N3}.

  Short reading:
    If you accept Isabelle/U as your descriptive logic of reality, then—without adding any
    extra metaphysical axiom—the only stable ultimate ground compatible with the framework
    is triune.
›


subsection ‹17.3 Ontology argument- world-lift of existence ›

text ‹
  (1) DN trigger: @{text "¬"}@{text "¬"}(@{text "∃"}x. H\_opt x) @{text "⟶"} (@{text "∃"}x. H\_opt x) (E1)
  Isabelle/HOL is classical, so double-negation elimination holds.
›
lemma DN_exists_Hopt:
  assumes DN: "¬¬ (∃x. H_opt x)"
  shows "∃x. H_opt x"
  using DN by blast

text ‹
  (2) Reading ``God exists'' as U-layer existence of an H\_opt witness (E1').
      Moral note: this only asserts the existence of an ‹H_opt› witness in the U-layer,
      and does not assume any further ethical or theological properties.
›
definition GodExists_U :: bool
  where "GodExists_U ≡ (∃x. H_opt x)"

lemma GodExists_U_from_DN:
  assumes DN: "¬¬ (∃x. H_opt x)"
  shows "GodExists_U"
proof -
  from DN have "∃x. H_opt x" by blast
  thus "GodExists_U" by (simp add: GodExists_U_def)
qed

text ‹
  (3) World-lift by identification: we record the interpretive move
      ``our world follows the U-layer logic'' as a definitional identification.
      No new axioms are introduced; we simply mirror the U-claim at the world level.
›
definition GodExists_world :: bool
  where "GodExists_world ≡ GodExists_U"

lemma GodExists_world_from_U:
  assumes "GodExists_U"
  shows   "GodExists_world"
  using assms by (simp add: GodExists_world_def)

lemma GodExists_U_iff_world:
  "GodExists_U ⟷ GodExists_world"
  by (simp add: GodExists_world_def)
text ‹
  Usage sketch:
    have DN: ``@{text "¬"}@{text "¬"}(@{text "∃"}x. H\_opt x)'' by (* your existing U-layer consistency proof *)
    hence ``GodExists\_U''     by (rule GodExists\_U\_from\_DN)
    hence ``GodExists\_world'' by (rule GodExists\_world\_from\_U)
›


section ‹18. Disjunctive-causal collapse on booleans›
lemma disjunctive_causation_collapse:
  assumes "(A ∨ B) ⟶ C" "(A ∨ C) ⟶ B" "(B ∨ C) ⟶ A"
  shows "(A ⟷ C) ∧ (B ⟷ C) ∧ (A ⟷ B)"
proof -
  have AC1: "A ⟹ C" using assms(1) by (meson disjI1)
  have AC2: "C ⟹ A" using assms(3) by (meson disjI2)
  have AC:  "A ⟷ C" using AC1 AC2 by blast
  have BC1: "B ⟹ C" using assms(1) by (meson disjI2)
  have BC2: "C ⟹ B" using assms(2) by (meson disjI2)
  have BC:  "B ⟷ C" using BC1 BC2 by blast
  have AB:  "A ⟷ B" using AC BC by blast
  show ?thesis using AC BC AB by blast
qed

lemma no_disjunctive_trinity:
  assumes "(A ∨ B) ⟶ C" "(A ∨ C) ⟶ B" "(B ∨ C) ⟶ A"
      and "¬ (A ⟷ B) ∨ ¬ (B ⟷ C) ∨ ¬ (A ⟷ C)"
  shows False
  using disjunctive_causation_collapse[OF assms(1-3)] assms(4) by blast


section ‹19. Boolean ``Trinity'' as pure concurrency›

definition Trinity :: "bool ⇒ bool ⇒ bool ⇒ bool" where
  "Trinity Φ Ω ψ ≡ Φ ∧ Ω ∧ ψ"

lemma Trinity_equiv_from_T_and_S_strong:
  assumes T: "Trinity Φ Ω ψ ⟶ R"
      and S: "¬ (Trinity Φ Ω ψ) ⟶ ¬ R"
  shows "Trinity Φ Ω ψ ⟷ R"  "R ⟶ Φ"  "R ⟶ Ω"  "R ⟶ ψ"
proof -
  have "R ⟶ Trinity Φ Ω ψ" using S by (metis)
  hence R_imp: "R ⟶ (Φ ∧ Ω ∧ ψ)" by (simp add: Trinity_def)
  from this show "R ⟶ Φ" "R ⟶ Ω" "R ⟶ ψ" by (simp_all add: Trinity_def)
  show "Trinity Φ Ω ψ ⟷ R" using T ‹R ⟶ Trinity Φ Ω ψ› by blast
qed

lemma singleton_cause_forces_equiv:
  fixes p q :: bool
  assumes "p ⟶ q" and "q ⟶ p"
  shows "p ⟷ q"
  using assms by blast


section ‹20. Packaging (T)+(S): The Trinity provides the possibility condition for created truths(R)›

lemma Trinity_imp_Phi  [simp]: "Trinity Φ Ω ψ ⟹ Φ"
  by (simp add: Trinity_def)

lemma Trinity_imp_Omega [simp]: "Trinity Φ Ω ψ ⟹ Ω"
  by (simp add: Trinity_def)

lemma Trinity_imp_psi  [simp]: "Trinity Φ Ω ψ ⟹ ψ"
  by (simp add: Trinity_def)

lemma Trinity_TS_package:
  assumes T: "Trinity Φ Ω ψ ⟶ ◇ R"
      and S: "¬ (Trinity Φ Ω ψ) ⟶ ¬ R"
  shows "R ⟶ Φ"
        "R ⟶ Ω"
        "R ⟶ ψ"
        "Trinity Φ Ω ψ ⟶ ◇ R"
proof -
  have RT: "R ⟶ Trinity Φ Ω ψ" using S by metis

  show "R ⟶ Φ" using RT
    by (auto simp: Trinity_def)

  show "R ⟶ Ω" using RT
    by (auto simp: Trinity_def)

  show "R ⟶ ψ" using RT
    by (auto simp: Trinity_def)

  show "Trinity Φ Ω ψ ⟶ ◇ R" using T .
qed


section ‹21. Relative Certainty and Ontological Grounding (definition-only)›
text ‹
  We capture the ``R @{text "→"} S \& not (S @{text "→"} R)'' certainty comparison on the U-layer
  via the strict support order of arguments. No axioms are added:
  everything remains definition-only and kernel-verified.

  *Recall.* The relations ``@{text "≼"}'' (relative certainty), ``@{text "≈"}'' (equivalence),
  and ``<U'' (strict relative certainty) were already defined in
  **Section 4 (U-layer: Relative Certainty)**.
  In this section we do not redefine them; we only introduce a
  convenient alias ``RelCert'' and related lemmas, all of which are
  conservative and definitional.
›


subsection ‹21.1 Relative certainty on the U-layer›
text ‹``R is strictly less certain than S'' is rendered as a strict inclusion
  of U-supports for their arguments. Equivalently, (Arg R) <U (Arg S).›

lemma RelCert_iff_lt:
  "RelCert R S ⟷ ((Arg R) ≼ (Arg S) ∧ ¬ ((Arg S) ≼ (Arg R)))"
  by (simp add: RelCert_def LtU_def)

lemma RelCert_implies_le:
  "RelCert R S ⟹ (Arg R) ≼ (Arg S)"
  by (simp add: RelCert_def LtU_def)


subsection ‹21.2 Pointwise and possibility/current-truth monotonicity›

lemma RelCert_pointwise:
  assumes RC: "RelCert R S"
      and SR: "Supports e R"
  shows "Supports e S"
proof -
  (* 1. From RelCert, get the support inclusion *)
  have le: "(Arg R) ≼ (Arg S)"
    using RC by (simp add: RelCert_def LtU_def)
  (* 2. Unfold Supports to obtain e ⊢ Arg R *)
  have eR: "e ⊢ Arg R"
    using SR by (simp add: Supports_def)
  (* 3. Pointwise monotonicity along ≼ *)
  have "e ⊢ Arg S"
    using le eR by (rule le_pointwise)
  (* 4. Fold back to Supports *)
  thus "Supports e S"
    by (simp add: Supports_def)
qed

lemma RelCert_EDia_mono:
  assumes "RelCert R S" and "EDia R"
  shows   "EDia S"
proof -
  obtain e where "Supports e R"
    using assms(2) by (auto simp: EDia_def)
  hence "Supports e S"
    using RelCert_pointwise[OF assms(1)] by blast
  thus "EDia S" by (auto simp: EDia_def)
qed

lemma RelCert_TrueNow_mono:
  assumes "RelCert R S" and "TrueNow R"
  shows   "TrueNow S"
  using RelCert_pointwise[OF assms(1)]
  using assms(2) by (simp add: TrueNow_def)


subsection ‹21.3 TSupp / PSupp monotonicity under ``Relative Certainty''›

lemma RelCert_TSupp_mono:
  assumes "RelCert R S"
  shows   "TSupp (Arg R) ⊆ TSupp (Arg S)"
  using TSupp_mono RelCert_implies_le[OF assms] by blast

lemma RelCert_PSupp_mono:
  assumes "RelCert R S"
  shows   "PSupp (Arg R) ⊆ PSupp (Arg S)"
  using PSupp_mono RelCert_implies_le[OF assms] by blast


subsection ‹21.4 Ontological Grounding: a definitional alias›
text ‹We introduce a thin alias ``Ground'' to record the intended philosophical
  reading: if S is strictly more certain than R (in the RelCert sense),
  then S is an ontological ground for R. This is a pure definition (no axiom).›
definition Ground :: "bool ⇒ bool ⇒ bool" where
  "Ground S R ≡ RelCert R S"

lemma RelCert_implies_Ground: "RelCert R S ⟹ Ground S R"
  by (simp add: Ground_def)

lemma Ground_iff_RelCert: "Ground S R ⟷ RelCert R S"
  by (simp add: Ground_def)


subsection ‹21.5 Model-side view (optional, inside FullIdBridge)›

context FullIdBridge
begin

lemma RelCert_subset_in_model:
  assumes "RelCert R S"
  shows   "Arg0 R ⊆ Arg0 S"
  using LeU_iff_subset RelCert_implies_le[OF assms] by blast

end


section ‹22. Ontological\_Origin\_Truth(OOT) characterization (axiom-free, U-layer only)›

definition Ontological_Origin_Truth :: "bool ⇒ bool" where
  "Ontological_Origin_Truth q ≡
      (∀ζ∈PDom. (Arg ζ) ≼ (Arg q))
    ∧ (∀ζ∈PDom. ¬ ((Arg q) ≺ (Arg ζ)))"

lemma Hopt_dominates_PDom_all:
  assumes HQ:  "H_opt q"
      and PHq: "PH (Arg q)"
  shows "∀ζ∈PDom. (Arg ζ) ≼ (Arg q)"
proof (intro ballI)
  fix ζ assume Zin: "ζ ∈ PDom"
  from PHq show "(Arg ζ) ≼ (Arg q)"
    using Zin by (auto simp: PH_def PDom_def)
qed

lemma Hopt_is_Ontological_Origin_Truth:
  assumes HQ:  "H_opt q"
      and PHq: "PH (Arg q)"
  shows "Ontological_Origin_Truth q"
proof -
  have dom: "∀ζ∈PDom. (Arg ζ) ≼ (Arg q)"
    using Hopt_dominates_PDom_all[OF HQ PHq] .

  have Headq: "Head q"
    using HQ by (simp add: H_opt_def MaxNT_def)
  hence HN: "H_negU_strict q"
    by (simp add: Head_def)

  have noabove: "∀ζ∈PDom. ¬ ((Arg q) ≺ (Arg ζ))"
  proof (intro ballI)
    fix ζ assume Zin: "ζ ∈ PDom"
    show "¬ ((Arg q) ≺ (Arg ζ))"
    proof (cases "ζ = q")
      case True
      then show ?thesis by (simp add: LtU_def)
    next
      case False
      from HN Zin False show ?thesis
        by (simp add: H_negU_strict_def)
    qed
  qed

  show ?thesis
    unfolding Ontological_Origin_Truth_def
    using dom noabove by auto
qed

corollary Ontological_Origin_Truth_covers:
  assumes "Ontological_Origin_Truth q" and "ζ ∈ PDom"
  shows   "(Arg ζ) ≼ (Arg q)"
  using assms unfolding Ontological_Origin_Truth_def by auto

corollary Ontological_Origin_Truth_no_strict_superior:
  assumes "Ontological_Origin_Truth q" and "ζ ∈ PDom"
  shows   "¬ ((Arg q) ≺ (Arg ζ))"
  using assms unfolding Ontological_Origin_Truth_def by auto


subsection ‹22.1  Why Tautology(True) cannot be an Ontologic\_Origin\_truth (anti-coverage witness)›
text‹
  The ``bad point'' clause functions as an anti-coverage witness against the Tautology.
  It says that there exist some @{text "ζ"} in PDom and some support-point e such that
  e supports @{text "ζ"}, while e does not support Arg True. Therefore Arg @{text "ζ"} cannot be
  below Arg True in the support order. This blocks the universal coverage clause
  required for Ontological\_Origin\_Truth True, and thus prevents the Tautology
  from qualifying as an ontological origin truth.
›

lemma anti_coverage_point_for_True:
  assumes "Supports e ζ" and "¬ (e ⊢ Arg True)"
  shows   "¬ ((Arg ζ) ≼ (Arg True))"
  using assms by (auto simp: LeU_def SuppU_def Supports_def)

lemma True_not_Ontological_Origin_Truth_if_point_counterexample:
  assumes Z: "ζ ∈ PDom" and S: "Supports e ζ" and N: "¬ (e ⊢ Arg True)"
  shows   "¬ Ontological_Origin_Truth True"

proof
  assume CT: "Ontological_Origin_Truth True"
  (* pull the coverage conjunct for this ζ ∈ PDom *)
  have cov: "(Arg ζ) ≼ (Arg True)"
    using Ontological_Origin_Truth_covers[OF CT Z] .
  (* but the pointwise witness forbids that *)
  have "¬ ((Arg ζ) ≼ (Arg True))"
    using anti_coverage_point_for_True[OF S N] .
  thus False using cov by contradiction
qed

lemma True_not_Ontological_Origin_Truth_if_exists_bad_point:
  assumes "∃ζ∈PDom. ∃e. Supports e ζ ∧ ¬ (e ⊢ Arg True)"
  shows   "¬ Ontological_Origin_Truth True"
proof -
  obtain ζ e where Z: "ζ ∈ PDom" and S: "Supports e ζ" and N: "¬ (e ⊢ Arg True)"
    using assms by blast
  show ?thesis
    by (rule True_not_Ontological_Origin_Truth_if_point_counterexample[OF Z S N])
qed

text ‹Model-side construction of a ``bad point'' inside the FullIdBridge locale.›
context FullIdBridge
begin

lemma bad_point_exists_for_True:
  assumes "∃w ζ. Val w ζ ∧ ¬ Val w True"
  shows   "∃ζ∈PDom. ∃e. Supports e ζ ∧ ¬ (e ⊢ Arg True)"
proof -
  obtain w ζ where Vζ: "Val w ζ" and nT: "¬ Val w True"
    using assms by blast
  define e where "e = iw w"
  have Sζ: "Supports e ζ"
    using Vζ by (simp add: Supports_def bridge e_def)
  have nTrue_at_e: "¬ (e ⊢ Arg True)"
    using nT by (simp add: bridge e_def)
 
  have Zin: "ζ ∈ PDom"
    using Sζ by (auto simp: PDom_def EDia_def)

  show ?thesis
  proof (intro bexI[of _ ζ] exI[of _ e])
    show "ζ ∈ PDom" by (rule Zin)
    show "Supports e ζ ∧ ¬ (e ⊢ Arg True)"
      by (simp add: Sζ nTrue_at_e)
  qed
qed

end


subsection ‹22.2  Non-triviality package: Ontological\_Origin\_Truths are never the tautology›
text ‹
  We establish that any H\_opt witness (which also satisfies PH) is an
  Ontological Origin Truth and is distinct from the Tautology.
›

lemma Hopt_witness_is_nontrivial_Ontological_Origin_Truth:
  assumes HQ:  "H_opt q"
      and PHq: "PH (Arg q)"
      and Bad: "∃ζ∈PDom. ∃e. Supports e ζ ∧ ¬ (e ⊢ Arg True)"
  shows "Ontological_Origin_Truth q ∧ q ≠ True"
proof -
  have Ctq: "Ontological_Origin_Truth q"
    by (rule Hopt_is_Ontological_Origin_Truth[OF HQ PHq])

  have nq: "q ≠ True"
  proof
    assume qt: "q = True"
    have CtT: "Ontological_Origin_Truth True" using Ctq qt by simp
    have notCTT: "¬ Ontological_Origin_Truth True"
      by (rule True_not_Ontological_Origin_Truth_if_exists_bad_point[OF Bad])
    from notCTT CtT show False by contradiction
  qed

  show ?thesis using Ctq nq by blast
qed

text ‹Existential headline (abstract form, needs a ``bad point'' assumption).›
theorem Ontological_Origin_Truth_nontrivial_existence_from_Hopt_existence:
  assumes Hex: "∃x. H_opt x ∧ PH (Arg x)"
      and Bad: "∃ζ∈PDom. ∃e. Supports e ζ ∧ ¬ (e ⊢ Arg True)"
  shows "∃q. Ontological_Origin_Truth q ∧ q ≠ True"
proof -
  obtain q where HQ: "H_opt q" and PHq: "PH (Arg q)"
    using Hex by blast
 
  have "Ontological_Origin_Truth q ∧ q ≠ True"
    using Hopt_witness_is_nontrivial_Ontological_Origin_Truth[OF HQ PHq Bad] by blast
   
  thus ?thesis by blast
qed


text ‹Tripled version (abstract form, same ``bad point'' assumption).›
theorem Hopt3_gives_three_nontrivial_Ontological_Origin_Truths:
  assumes H3:  "Hopt3 a b c"
      and PHa: "PH (Arg a)"
      and PHb: "PH (Arg b)"
      and PHc: "PH (Arg c)"
      and Bad: "∃ζ∈PDom. ∃e. Supports e ζ ∧ ¬ (e ⊢ Arg True)"
  shows "Ontological_Origin_Truth a ∧ a ≠ True"
    and "Ontological_Origin_Truth b ∧ b ≠ True"
    and "Ontological_Origin_Truth c ∧ c ≠ True"
proof -
  from H3 have Ha: "H_opt a" and Hb: "H_opt b" and Hc: "H_opt c"
    by (auto simp: Hopt3_def)

  have A: "Ontological_Origin_Truth a ∧ a ≠ True"
    by (rule Hopt_witness_is_nontrivial_Ontological_Origin_Truth[OF Ha PHa Bad])
  have B: "Ontological_Origin_Truth b ∧ b ≠ True"
    by (rule Hopt_witness_is_nontrivial_Ontological_Origin_Truth[OF Hb PHb Bad])
  have C: "Ontological_Origin_Truth c ∧ c ≠ True"
    by (rule Hopt_witness_is_nontrivial_Ontological_Origin_Truth[OF Hc PHc Bad])

  show "Ontological_Origin_Truth a ∧ a ≠ True" by (rule A)
  show "Ontological_Origin_Truth b ∧ b ≠ True" by (rule B)
  show "Ontological_Origin_Truth c ∧ c ≠ True" by (rule C)
qed

text ‹Model-side discharge of the ``bad point'' assumption inside FullIdBridge.›
context FullIdBridge
begin

corollary Hopt_witness_is_nontrivial_Ontological_Origin_Truth_model:
  assumes HQ:  "H_opt q"
      and PHq: "PH (Arg q)"
      and Ex:  "∃w ζ. Val w ζ ∧ ¬ Val w True"
  shows "Ontological_Origin_Truth q ∧ q ≠ True"
proof -
  have Bad: "∃ζ∈PDom. ∃e. Supports e ζ ∧ ¬ (e ⊢ Arg True)"
    using bad_point_exists_for_True[OF Ex] .
  show ?thesis
    by (rule Hopt_witness_is_nontrivial_Ontological_Origin_Truth[OF HQ PHq Bad])
qed

corollary Ontological_Origin_Truth_nontrivial_existence_from_model:
  assumes Hex: "∃x. H_opt x ∧ PH (Arg x)"
      and Ex:  "∃w ζ. Val w ζ ∧ ¬ Val w True"
  shows "∃q. Ontological_Origin_Truth q ∧ q ≠ True"
proof -
  obtain q where HQ: "H_opt q" and PHq: "PH (Arg q)"
    using Hex by blast

  have "Ontological_Origin_Truth q ∧ q ≠ True"
    using Hopt_witness_is_nontrivial_Ontological_Origin_Truth_model[OF HQ PHq Ex] .
  thus ?thesis by blast
qed

corollary Hopt3_gives_three_nontrivial_Ontological_Origin_Truths_model:
  assumes H3: "Hopt3 a b c"
      and PHs: "PH (Arg a)" "PH (Arg b)" "PH (Arg c)"
      and Ex: "∃w ζ. Val w ζ ∧ ¬ Val w True"
  shows "Ontological_Origin_Truth a ∧ a ≠ True"
    and  "Ontological_Origin_Truth b ∧ b ≠ True"
    and  "Ontological_Origin_Truth c ∧ c ≠ True"
proof -
  have Bad: "∃ζ∈PDom. ∃e. Supports e ζ ∧ ¬ (e ⊢ Arg True)"
    using bad_point_exists_for_True[OF Ex] .
   
  show "Ontological_Origin_Truth a ∧ a ≠ True"
    using Hopt3_gives_three_nontrivial_Ontological_Origin_Truths(1)[OF H3 PHs(1) PHs(2) PHs(3) Bad] .
   
  show "Ontological_Origin_Truth b ∧ b ≠ True"
    using Hopt3_gives_three_nontrivial_Ontological_Origin_Truths(2)[OF H3 PHs(1) PHs(2) PHs(3) Bad] .
   
  show "Ontological_Origin_Truth c ∧ c ≠ True"
    using Hopt3_gives_three_nontrivial_Ontological_Origin_Truths(3)[OF H3 PHs(1) PHs(2) PHs(3) Bad] .
qed

end


section ‹23. No collapse, and why Trinity (not a singleton) can be the origin›

lemma collapse_if_biimp_of_possibility:
  assumes T: "Trinity Φ Ω ψ ⟶ ◇ R"
      and B: "◇ R ⟶ Trinity Φ Ω ψ"
  shows "◇ R ⟷ Trinity Φ Ω ψ"
  using T B by blast

lemma noncollapse_if_not_back:
  assumes T: "Trinity Φ Ω ψ ⟶ ◇ R"
      and nB: "¬ (◇ R ⟶ Trinity Φ Ω ψ)"
  shows "¬ (◇ R ⟷ Trinity Φ Ω ψ)"
  using T nB by blast

lemma single_cause_collapse_if_back:
  assumes cause: "Φ ⟶ R" and ret: "R ⟶ Φ"
  shows "R ⟷ Φ"
  using cause ret by blast

lemma single_cause_possibility_collapse_if_back:
  assumes cause: "Φ ⟶ ◇ R" and ret: "◇ R ⟶ Φ"
  shows "◇ R ⟷ Φ"
  using cause ret by blast

section ‹24. Trinity truthmaking pattern: (T) + (S)›
text‹
  Philosophical background.

  This section isolates a minimal ``truthmaking'' pattern for contingent reality.
  The structure is intentionally weak and two-sided:

    (T) If the triune ground holds, then R is at least possible.
    (S) If the triune ground fails, then R fails.

  Thus the Trinity is not modeled here as a brute forcing principle
  that immediately yields R, but as a condition that opens the space of R
  while still allowing contingency. In this sense, the section is designed
  to preserve the distinction between enabling and forcing.

  The contrapositive of (S) yields a weak upward dependence:
  if R holds, then the triune structure must hold.
  But (T) itself gives only Trinity @{text "⟶"} @{text "◇"}R, not Trinity @{text "⟶"} R.
  Hence the framework blocks collapse from possibility into actuality.

  Importantly, this section is not part of the indispensable proof-core
  of either the ontological argument or the Trinity-necessity derivation.
  Those results are established independently elsewhere. The present section
  is instead an auxiliary interpretive-diagnostic layer showing how a derived
  triune ground can be related to contingent reality without forcing it.

  The final theorem records the system-level point in classical form:
  whether Trinity actually implies R is left contingent rather than built in
  by the truthmaking pattern itself. The purpose of this section is therefore
  diagnostic and anti-collapse: it shows how a triune ground may underwrite
  contingent reality without erasing contingency.›

locale Trinity_Truthmaking =
  fixes Φ Ω ψ R :: bool
  assumes T: "Trinity Φ Ω ψ ⟶ ◇ R"
      and S: "¬ (Trinity Φ Ω ψ) ⟶ ¬ R"
begin

lemma S_contrapositive: "R ⟶ Trinity Φ Ω ψ" using S by (metis)

lemma R_implies_each:
  shows "R ⟶ Φ" and "R ⟶ Ω" and "R ⟶ ψ"
  using S_contrapositive
  by (auto simp: Trinity_def)

lemma T_weak_truthmaking: "Trinity Φ Ω ψ ⟶ ◇ R" using T .
end

theorem Contingency_Preserved:
  assumes "Trinity Φ Ω ψ ⟶ ◇ R"
  shows "(Trinity Φ Ω ψ ⟶ R) ∨ ¬ (Trinity Φ Ω ψ ⟶ R)"
  by blast (* System-level guarantee that contingency is preserved. *)


section ‹25. The Unity of the Trinity - Ordinal/Cardinal transcendence›
text‹
  This section gives a small ordinal/cardinal diagnostic for the unity of the Trinity.
  The question is whether a triune relational pattern can be faithfully embedded
  into a simple linear three-step order.

  We model a finite ordinal chain with three points (O1, O2, O3), equip it with
  a meet-like operation CAP, and ask whether the three divine persons can be mapped
  bijectively into this linear structure while preserving the triune ``pair implies third''
  pattern.

  The result is negative: no such embedding exists.
  The reason is structural. In a linear chain, CAP behaves like a minimum,
  so pairwise joint structure always collapses downward into a lower point.
  But the triune pattern requires a symmetric and irreducible relational form in which
  each pair stands in a directed relation to the third. That demand cannot be realized
  inside a merely linear ordinal hierarchy.

  Hence the unity of the Trinity is not representable as a simple ordinal ranking
  or as a one-dimensional cardinal ladder. The triune structure has a mode of unity
  that exceeds linear order: it is not a serial progression of ranks, but a mutually
  irreducible relational whole.

  The later oneness lemma then complements this result from the opposite direction:
  although the triune pattern cannot be embedded into a linear three-chain,
  the essence-image of the three persons may still collapse to one at the level of unity.
  Thus plurality of persons and unity of essence are not modeled as contradiction,
  but as two formally distinct dimensions.›

datatype ord3 = O1 | O2 | O3

primrec cap :: "ord3 ⇒ ord3 ⇒ ord3" where
  "cap O1 y = O1"
| "cap O2 y = (case y of O1 ⇒ O1 | O2 ⇒ O2 | O3 ⇒ O2)"
| "cap O3 y = (case y of O1 ⇒ O1 | O2 ⇒ O2 | O3 ⇒ O3)"

notation cap (infixl "CAP" 70)

primrec ltO :: "ord3 ⇒ ord3 ⇒ bool" where
  "ltO O1 y = (case y of O1 ⇒ False | O2 ⇒ True  | O3 ⇒ True)"
| "ltO O2 y = (case y of O1 ⇒ False | O2 ⇒ False | O3 ⇒ True)"
| "ltO O3 y = False"

notation ltO (infix "<o" 50)

lemma ltO_right_O1[simp]: "((x::ord3) <o O1) = False"
  by (cases x) simp_all

datatype person = F | S | G
definition Persons :: "person set" where "Persons = {F,S,G}"

definition O123    :: "ord3 set"   where "O123 = {O1,O2,O3}"

definition preserves_trinity_on_ord3 :: "(person ⇒ ord3) ⇒ bool" where
  "preserves_trinity_on_ord3 f ⟷
     bij_betw f Persons O123 ∧
     ((f F CAP f S) <o f G) ∧
     ((f F CAP f G) <o f S) ∧
     ((f S CAP f G) <o f F)"

lemma no_ordinal_embedding_for_trinity:
  "¬ (∃f. preserves_trinity_on_ord3 f)"
proof
  assume "∃f. preserves_trinity_on_ord3 f"
  then obtain f where B:
    "bij_betw f Persons O123"
    "(f F CAP f S) <o f G"
    "(f F CAP f G) <o f S"
    "(f S CAP f G) <o f F"
    unfolding preserves_trinity_on_ord3_def by blast

  have FF_not_O1: "f F ≠ O1"
  proof
    assume "f F = O1" hence "(f S CAP f G) <o O1" using B(4) by simp
    thus False by simp
  qed
  have FS_not_O1: "f S ≠ O1"
  proof
    assume "f S = O1" hence "(f F CAP f G) <o O1" using B(3) by simp
    thus False by simp
  qed
  have FG_not_O1: "f G ≠ O1"
  proof
    assume "f G = O1" hence "(f F CAP f S) <o O1" using B(2) by simp
    thus False by simp
  qed

  have O1_in_image: "O1 ∈ f ` Persons"
    using B(1) unfolding bij_betw_def Persons_def O123_def by auto

  have notin: "O1 ∉ f ` Persons"
  proof -
    have "O1 ≠ f F" using FF_not_O1 by simp
    moreover have "O1 ≠ f S" using FS_not_O1 by simp
    moreover have "O1 ≠ f G" using FG_not_O1 by simp
    ultimately show ?thesis by (simp add: Persons_def)
  qed
  from notin O1_in_image show False by contradiction
qed
(* Assumption note (already above in this file):
   datatype person = F | S | G
   definition Persons :: "person set" where "Persons = {F,S,G}"
*)
paragraph ‹Remark (Why no 3-ordinal embedding)›
text ‹Two independent obstacles explain the non-embedding into the linear 3-chain 0<1<2.
The TriSupport pair @{text "→"} third (meet-like) symmetry cannot be realized on a linear chain
with meet = min; symmetry would force each image to be maximal, a contradiction. ›
(* ---------- TriOneness : robust Eq-collapse lemma ---------- *)
lemma oneness_global:
  fixes essence :: "person ⇒ 'E"
  assumes FS: "essence F = essence S"
      and SG: "essence S = essence G"
  shows "card (essence ` Persons) = 1"
proof -
  have eq: "essence ` Persons = {essence F}"
  proof (intro subset_antisym)
    show "essence ` Persons ⊆ {essence F}"
    proof
      fix x assume "x ∈ essence ` Persons"
      then obtain p where pP: "p ∈ Persons" and x: "x = essence p" by auto
      from pP have "p = F ∨ p = S ∨ p = G" by (auto simp: Persons_def)
     have "x = essence F"
  using x FS SG pP by (cases p) (auto simp: Persons_def)
      thus "x ∈ {essence F}" by simp
    qed
    show "{essence F} ⊆ essence ` Persons"
      by (auto simp: Persons_def)
  qed
  show ?thesis by (simp add: eq)
qed
(* --- H-principle (extended): if PH holds, it supports both "possible" and "actually true" cases --- *)
lemma H_principle_from_PH_true:
  assumes "PH (Arg Q)" and "TrueNow ζ"
  shows "(Arg ζ) ≼ (Arg Q)"
  using assms by (simp add: PH_def)

lemma H_principle_from_PH_possible:
  assumes "PH (Arg Q)" and "EDia ζ"
  shows "(Arg ζ) ≼ (Arg Q)"
  using assms by (simp add: PH_def)

lemma H_principle_full_from_PH:
  assumes "PH (Arg Q)"
  shows "∀ζ. (TrueNow ζ ∨ EDia ζ) ⟶ (Arg ζ) ≼ (Arg Q)"
  using assms by (simp add: PH_def)

lemma PH_no_strict_superior_pair:
  assumes "PH (Arg Q)" and "PH (Arg R)"
  shows "¬ ((Arg Q) ≺⇧P (Arg R)) ∧ ¬ ((Arg R) ≺⇧P (Arg Q))"
  using PH_no_strict_superior assms by blast


section ‹26. Uniqueness of the Trinity (MaxCov-level)›
text ‹
   Core idea:
    pick one triple (A,B,C) of MaxCov points with pairwise non-@{text "≈"}
    use the ``no 4 MaxCov points can be pairwise non-@{text "≈"}'' exclusion (Excl4)
      to show every MaxCov X must fall into one of the three @{text "≈"}-classes
    hence the union of the three @{text "≈"}-classes is independent of the chosen triple
›

locale Trinity_Uniqueness_MaxCov =
  fixes MaxCov :: "U ⇒ bool"
  assumes SYM:   "⋀p q. p ≈ q ⟹ q ≈ p"
      and TRANS: "⋀p q r. p ≈ q ⟹ q ≈ r ⟹ p ≈ r"
      and Excl4:
        "⋀a b c d.
           ⟦ MaxCov a; MaxCov b; MaxCov c; MaxCov d;
             ¬(a ≈ b); ¬(a ≈ c); ¬(b ≈ c);
             ¬(a ≈ d); ¬(b ≈ d); ¬(c ≈ d) ⟧ ⟹ False"
begin
(* ------------------------------------------------------------- *)
(* 26.0  A "Top-3" triple at the MaxCov-level                      *)
(* ------------------------------------------------------------- *)
definition TrinityTop3_mc :: "U ⇒ U ⇒ U ⇒ bool" where
  "TrinityTop3_mc A B C ⟷
     MaxCov A ∧ MaxCov B ∧ MaxCov C ∧
     ¬(A ≈ B) ∧ ¬(A ≈ C) ∧ ¬(B ≈ C)"

definition Top3Classes :: "U ⇒ U ⇒ U ⇒ U set" where
  "Top3Classes A B C ≡ {x. x ≈ A ∨ x ≈ B ∨ x ≈ C}"

lemma not_EqU_sym:
  assumes H: "¬(x ≈ y)"
  shows "¬(y ≈ x)"
proof
  assume YX: "y ≈ x"
  hence XY: "x ≈ y" using SYM by blast
  show False using H XY by contradiction
qed
(* ------------------------------------------------------------- *)
(* 26.1  Any MaxCov point falls into the Top-3 classes             *)
(* ------------------------------------------------------------- *)
lemma MaxCov_must_fall_into_Top3Classes:
  assumes T:  "TrinityTop3_mc A B C"
      and MX: "MaxCov X"
  shows "X ≈ A ∨ X ≈ B ∨ X ≈ C"
proof (rule classical)
  assume H: "¬(X ≈ A ∨ X ≈ B ∨ X ≈ C)"
  have XA: "¬(X ≈ A)" and XB: "¬(X ≈ B)" and XC: "¬(X ≈ C)"
    using H by auto

  have MA: "MaxCov A" and MB: "MaxCov B" and MC: "MaxCov C"
    using T by (simp_all add: TrinityTop3_mc_def)
  have AB: "¬(A ≈ B)" and AC: "¬(A ≈ C)" and BC: "¬(B ≈ C)"
    using T by (simp_all add: TrinityTop3_mc_def)

  have AX: "¬(A ≈ X)" using XA by (rule not_EqU_sym)
  have BX: "¬(B ≈ X)" using XB by (rule not_EqU_sym)
  have CX: "¬(C ≈ X)" using XC by (rule not_EqU_sym)

  have False
    using Excl4[OF MA MB MC MX AB AC BC AX BX CX] .
  thus "X ≈ A ∨ X ≈ B ∨ X ≈ C" by blast
qed
(* ------------------------------------------------------------- *)
(* 26.2  The Top-3 union of ≈-classes is unique             *)
(* ------------------------------------------------------------- *)
lemma Top3Classes_unique:
  assumes T1: "TrinityTop3_mc A B C"
      and T2: "TrinityTop3_mc A' B' C'"
  shows "Top3Classes A B C = Top3Classes A' B' C'"
proof (rule set_eqI, rule iffI)
  fix x
  (* 1. Left to Right: x ∈ Top3Classes A B C ⟹ x ∈ Top3Classes A' B' C' *)
  assume hx: "x ∈ Top3Classes A B C"
  hence hx0: "x ≈ A ∨ x ≈ B ∨ x ≈ C" by (simp add: Top3Classes_def)

  from hx0 show "x ∈ Top3Classes A' B' C'"
  proof (elim disjE)
    assume xA: "x ≈ A"
    have MA: "MaxCov A" using T1 unfolding TrinityTop3_mc_def by simp
    have "A ≈ A' ∨ A ≈ B' ∨ A ≈ C'"
      using MaxCov_must_fall_into_Top3Classes[OF T2 MA] .
    thus ?thesis using xA TRANS unfolding Top3Classes_def by blast
  next
    assume xB: "x ≈ B"
    have MB: "MaxCov B" using T1 unfolding TrinityTop3_mc_def by simp
    have "B ≈ A' ∨ B ≈ B' ∨ B ≈ C'"
      using MaxCov_must_fall_into_Top3Classes[OF T2 MB] .
    thus ?thesis using xB TRANS unfolding Top3Classes_def by blast
  next
    assume xC: "x ≈ C"
    have MC: "MaxCov C" using T1 unfolding TrinityTop3_mc_def by simp
    have "C ≈ A' ∨ C ≈ B' ∨ C ≈ C'"
      using MaxCov_must_fall_into_Top3Classes[OF T2 MC] .
    thus ?thesis using xC TRANS unfolding Top3Classes_def by blast
  qed

next
  fix x
  (* 2. Right to Left: x ∈ Top3Classes A' B' C' ⟹ x ∈ Top3Classes A B C *)
  assume hx': "x ∈ Top3Classes A' B' C'"
  hence hx0': "x ≈ A' ∨ x ≈ B' ∨ x ≈ C'" by (simp add: Top3Classes_def)

  from hx0' show "x ∈ Top3Classes A B C"
  proof (elim disjE)
    assume xA': "x ≈ A'"
    have MA': "MaxCov A'" using T2 unfolding TrinityTop3_mc_def by simp
    have "A' ≈ A ∨ A' ≈ B ∨ A' ≈ C"
      using MaxCov_must_fall_into_Top3Classes[OF T1 MA'] .
    thus ?thesis using xA' TRANS unfolding Top3Classes_def by blast
  next
    assume xB': "x ≈ B'"
    have MB': "MaxCov B'" using T2 unfolding TrinityTop3_mc_def by simp
    have "B' ≈ A ∨ B' ≈ B ∨ B' ≈ C"
      using MaxCov_must_fall_into_Top3Classes[OF T1 MB'] .
    thus ?thesis using xB' TRANS unfolding Top3Classes_def by blast
  next
    assume xC': "x ≈ C'"
    have MC': "MaxCov C'" using T2 unfolding TrinityTop3_mc_def by simp
    have "C' ≈ A ∨ C' ≈ B ∨ C' ≈ C"
      using MaxCov_must_fall_into_Top3Classes[OF T1 MC'] .
    thus ?thesis using xC' TRANS unfolding Top3Classes_def by blast
  qed
qed
(* ------------------------------------------------------------- *)
(* 26.3  Convenience corollary                                    *)
(* ------------------------------------------------------------- *)
corollary Top3Classes_unique_any_point:
  assumes T1: "TrinityTop3_mc A B C"
      and T2: "TrinityTop3_mc A' B' C'"
  shows "∀x. x ∈ Top3Classes A B C ⟷ x ∈ Top3Classes A' B' C'"
  using Top3Classes_unique[OF T1 T2] by blast

end
(* ========================================================= *)
(*   WRAPPERS (explicitly labeled, still the same math)
    - "God finality" on PDom (from H_opt)
    - "Trinity actuality" N3 (from Hopt3)                          *)
(* ========================================================= *)
section ‹27. Wrappers: ``God finality'' and ``Trinity actuality''›

text ‹``God finality'' (order-theoretic necessity within PDom): if H\_opt q, then nothing in PDom
  is strictly superior to Arg q. This is just a named wrapper of ‹argument\_finality\_PDom›.›
lemma God_finality:
  assumes "H_opt q"
  shows "∀ζ∈PDom. ¬ ((Arg q) ≺ (Arg ζ))"
  using argument_finality_PDom[OF assms] .

text ‹``Trinity actuality'': from ‹Hopt3 a b c› (three H\_opt possibles), we get the N3 pattern
  with no axiom. This is a named wrapper of ‹OnlyN3_from_Hopt3_unboxed›.›
lemma Trinity_actuality:
  assumes H3: "Hopt3 a b c"
      and MCI: "⋀e X Y. Supports e X ⟹ Supports e Y ⟹ Supports e (X ∧ Y)"
  shows N3
  by (rule OnlyN3_from_Hopt3_unboxed[OF H3 MCI])


section ‹28. Final Locale Audit: Discharging Core locale assupmtions ›
text ‹
  This section provides the formal certification of the entire logical architecture.
  We establish a minimal analytic environment and mechanically discharge:
  1) The ``No-Superfluous''(NS), ES, Cov, MCL, MCR constraint via Band Collapse.
  2) The ``Excl4'' constraint for the Uniqueness of the Trinity.
›

locale Final_NS_Audit =
  fixes Ω Ψ Φ :: bool
  ― ‹Minimal boolean grammar assumptions (analytic truths)›
  assumes MCL: "⋀e A B. Makes e (A ∧ B) ⟹ Makes e A"
      and MCR: "⋀e A B. Makes e (A ∧ B) ⟹ Makes e B"
      and MCI: "⋀e A B. Makes e A ⟹ Makes e B ⟹ Makes e (A ∧ B)"
  ― ‹Core existence and ontological coverage assumptions›
  assumes ES:  "EDia_ep (Ω ∧ Ψ)"
      and Cov: "Arg (Ω ∧ Ψ) ≼ Arg Φ"
  ― ‹H-principle projection›
      and Core_to_Y_rule: "⋀Y. H_opt_ep Y ⟹ Arg (Ω ∧ Ψ) ≼ Arg Y"
begin

 
subsection‹28.1  Discharging NS(No-Superfluous), ES, Cov, MCL, MCR ›

  sublocale Trinity_NS_Audit: Band_Collapse_Superfluous Ω Ψ Φ
  proof
    show "EDia_ep (Ω ∧ Ψ)" by (rule ES)
    show "Arg (Ω ∧ Ψ) ≼ Arg Φ" by (rule Cov)
    show "⋀e A B. Makes e (A ∧ B) ⟹ Makes e A" by (rule MCL)
    show "⋀e A B. Makes e (A ∧ B) ⟹ Makes e B" by (rule MCR)
   
    show "((Arg (Ω ∧ Ψ)) ≼ Arg Φ) ⟹
          (∀Y. H_opt_ep Y ⟶ EDia_ep Y ⟶
               Arg ((Ω ∧ Ψ) ∧ Y) ≼ Arg Φ ⟶
               Arg ((Ω ∧ Ψ) ∧ Y) ≈ Arg (Ω ∧ Ψ))"
    proof -
      assume "Arg (Ω ∧ Ψ) ≼ Arg Φ"
      show "∀Y. H_opt_ep Y ⟶ EDia_ep Y ⟶ Arg ((Ω ∧ Ψ) ∧ Y) ≼ Arg Φ ⟶ Arg ((Ω ∧ Ψ) ∧ Y) ≈ Arg (Ω ∧ Ψ)"
      proof (intro allI impI)
        fix Y assume HY: "H_opt_ep Y" and EY: "EDia_ep Y" and Band: "Arg ((Ω ∧ Ψ) ∧ Y) ≼ Arg Φ"
        have CTY: "Arg (Ω ∧ Ψ) ≼ Arg Y" by (rule Core_to_Y_rule[OF HY])
        show "Arg ((Ω ∧ Ψ) ∧ Y) ≈ Arg (Ω ∧ Ψ)"
          using core_conj_equiv_basic [OF ES HY EY CTY MCL MCI] by assumption
      qed
    qed
  qed


subsection‹28.2 Discharge the Trinity\_Uniqueness\_MaxCov Locale ›

  sublocale Trinity_Uniqueness_Certified: Trinity_Uniqueness_MaxCov "λu. ∃Y. u = Arg ((Ω ∧ Ψ) ∧ Y) ∧ H_opt_ep Y ∧ EDia_ep Y"
  proof
    show "⋀p q. p ≈ q ⟹ q ≈ p" by (rule EqU_sym)
    show "⋀p q r. p ≈ q ⟹ q ≈ r ⟹ p ≈ r" by (rule EqU_trans)

    show "⋀a b c d.
         ⟦∃Y. a = Arg ((Ω ∧ Ψ) ∧ Y) ∧ H_opt_ep Y ∧ EDia_ep Y;
          ∃Y. b = Arg ((Ω ∧ Ψ) ∧ Y) ∧ H_opt_ep Y ∧ EDia_ep Y;
          ∃Y. c = Arg ((Ω ∧ Ψ) ∧ Y) ∧ H_opt_ep Y ∧ EDia_ep Y;
          ∃Y. d = Arg ((Ω ∧ Ψ) ∧ Y) ∧ H_opt_ep Y ∧ EDia_ep Y;
          ¬ a ≈ b; ¬ a ≈ c; ¬ b ≈ c; ¬ a ≈ d; ¬ b ≈ d; ¬ c ≈ d⟧ ⟹ False"
    proof -
      fix a b c d
      assume H_a: "∃Y. a = Arg ((Ω ∧ Ψ) ∧ Y) ∧ H_opt_ep Y ∧ EDia_ep Y"
         and H_b: "∃Y. b = Arg ((Ω ∧ Ψ) ∧ Y) ∧ H_opt_ep Y ∧ EDia_ep Y"
         and H_c: "∃Y. c = Arg ((Ω ∧ Ψ) ∧ Y) ∧ H_opt_ep Y ∧ EDia_ep Y"
         and H_d: "∃Y. d = Arg ((Ω ∧ Ψ) ∧ Y) ∧ H_opt_ep Y ∧ EDia_ep Y"
         and N_ab: "¬ a ≈ b" and N_ac: "¬ a ≈ c" and N_bc: "¬ b ≈ c"
         and N_ad: "¬ a ≈ d" and N_bd: "¬ b ≈ d" and N_cd: "¬ c ≈ d"

      obtain Y1 where A: "a = Arg ((Ω ∧ Ψ) ∧ Y1)" "H_opt_ep Y1" "EDia_ep Y1" using H_a by blast
      obtain Y2 where B: "b = Arg ((Ω ∧ Ψ) ∧ Y2)" "H_opt_ep Y2" "EDia_ep Y2" using H_b by blast
      obtain Y3 where C: "c = Arg ((Ω ∧ Ψ) ∧ Y3)" "H_opt_ep Y3" "EDia_ep Y3" using H_c by blast
      obtain Y4 where D: "d = Arg ((Ω ∧ Ψ) ∧ Y4)" "H_opt_ep Y4" "EDia_ep Y4" using H_d by blast
      ― ‹Explicitly map the inequalities to the Arg structure›
      have neqs: "¬ (Arg ((Ω ∧ Ψ) ∧ Y1) ≈ Arg ((Ω ∧ Ψ) ∧ Y2)) ∧
                  ¬ (Arg ((Ω ∧ Ψ) ∧ Y1) ≈ Arg ((Ω ∧ Ψ) ∧ Y3)) ∧
                  ¬ (Arg ((Ω ∧ Ψ) ∧ Y1) ≈ Arg ((Ω ∧ Ψ) ∧ Y4)) ∧
                  ¬ (Arg ((Ω ∧ Ψ) ∧ Y2) ≈ Arg ((Ω ∧ Ψ) ∧ Y3)) ∧
                  ¬ (Arg ((Ω ∧ Ψ) ∧ Y2) ≈ Arg ((Ω ∧ Ψ) ∧ Y4)) ∧
                  ¬ (Arg ((Ω ∧ Ψ) ∧ Y3) ≈ Arg ((Ω ∧ Ψ) ∧ Y4))"
        using A(1) B(1) C(1) D(1) N_ab N_ac N_bc N_ad N_bd N_cd by simp
      ― ‹Summon the Band Collapse theorem from Part 1. It forces the exact opposite of our neqs›
      have col: "¬ (¬ (Arg ((Ω ∧ Ψ) ∧ Y1) ≈ Arg ((Ω ∧ Ψ) ∧ Y2)) ∧
                    ¬ (Arg ((Ω ∧ Ψ) ∧ Y1) ≈ Arg ((Ω ∧ Ψ) ∧ Y3)) ∧
                    ¬ (Arg ((Ω ∧ Ψ) ∧ Y1) ≈ Arg ((Ω ∧ Ψ) ∧ Y4)) ∧
                    ¬ (Arg ((Ω ∧ Ψ) ∧ Y2) ≈ Arg ((Ω ∧ Ψ) ∧ Y3)) ∧
                    ¬ (Arg ((Ω ∧ Ψ) ∧ Y2) ≈ Arg ((Ω ∧ Ψ) ∧ Y4)) ∧
                    ¬ (Arg ((Ω ∧ Ψ) ∧ Y3) ≈ Arg ((Ω ∧ Ψ) ∧ Y4)))"
        by (rule Trinity_NS_Audit.no_four_distinct_classes_in_band_pre132 [OF A(2) A(3) B(2) B(3) C(2) C(3) D(2) D(3)])
           ― ‹Contradiction achieved›
      show False using neqs col by contradiction
    qed
  qed

end

end