Theory Research_Results

theory Research_Results
  imports Second_Way_Reconstructions
begin

section ‹Exact Binary Foundation Classification›

text ‹
  The central binary vocabulary admits an exact classification theorem.  Under
  carrier coverage, meaning that the selected target set is a subset of C, the
  two apparently different foundation notions coincide because the set of all
  independent members is itself a foundation set whenever local foundation
  holds.  This is stronger than merely recording the implication from a
  designated global witness to local first members.
›

lemma integer_predecessor_not_local_foundation:
  "¬ local_foundation_on UNIV integer_predecessor_cause UNIV"
proof
  assume local:
    "local_foundation_on UNIV integer_predecessor_cause UNIV"
  have grounded_zero:
      "grounded_in UNIV integer_predecessor_cause (0 :: int)"
    using integer_predecessor_has_incoming[of "0 :: int"]
    by (auto simp: grounded_in_def)
  obtain f where first:
      "first_member_in UNIV integer_predecessor_cause f (0 :: int)"
    using local grounded_zero
    by (auto simp: local_foundation_on_def)
  have independent:
      "independent_in UNIV integer_predecessor_cause f"
    using first by (rule first_member_inD)
  obtain y where "integer_predecessor_cause y f"
    using integer_predecessor_has_incoming[of f] by blast
  then show False
    using independent by (auto simp: independent_in_def)
qed

theorem binary_foundation_lattice:
  assumes "R ⊆ C"
  shows "(well_founded_on C D ⟷ chain_terminating_on C D) ∧
   (well_founded_on C D ⟶ acyclic_on C D) ∧
   (local_foundation_on C D R ⟷
      global_foundation_on C D R) ∧
   (well_founded_on C D ⟶ local_foundation_on C D R)"
  using well_founded_iff_chain_terminating
    well_founded_implies_acyclic
    local_foundation_iff_global_foundation[OF assms]
    well_founded_implies_local_foundation by blast

theorem finite_binary_foundation_lattice:
  assumes "finite C" and "R ⊆ C"
  shows
    "(well_founded_on C D ⟷ acyclic_on C D) ∧
     (well_founded_on C D ⟷ chain_terminating_on C D) ∧
     (local_foundation_on C D R ⟷
        global_foundation_on C D R)"
  using finite_well_founded_iff_acyclic_on[OF assms(1)]
    well_founded_iff_chain_terminating
    local_foundation_iff_global_foundation[OF assms(2)] by blast

theorem finite_acyclic_implies_foundation:
  assumes "finite C" and "R ⊆ C" and "acyclic_on C D"
  shows "local_foundation_on C D R ∧
    global_foundation_on C D R"
proof -
  have well_founded:
      "well_founded_on C D"
    using finite_well_founded_iff_acyclic_on[OF assms(1)] assms(3)
    by blast
  have local:
      "local_foundation_on C D R"
    using well_founded_implies_local_foundation[OF well_founded] .
  have global:
      "global_foundation_on C D R"
    using local_foundation_implies_global_foundation[OF local assms(2)] .
  show ?thesis
    using local global by blast
qed

theorem finite_foundation_not_acyclic_rooted_cycle:
  "finite ({0, 1, 2} :: nat set) ∧
   local_foundation_on {0, 1, 2} rooted_cycle_dependency {0, 1, 2} ∧
   global_foundation_on {0, 1, 2} rooted_cycle_dependency {0, 1, 2} ∧
   ¬ acyclic_on {0, 1, 2} rooted_cycle_dependency"
  using local_foundation_not_acyclic_rooted_cycle by simp

theorem binary_foundation_separation_matrix:
  "acyclic_on UNIV integer_predecessor_cause ∧
   ¬ local_foundation_on UNIV integer_predecessor_cause UNIV ∧
   local_foundation_on UNIV pedestal_dependency UNIV ∧
   global_foundation_on UNIV pedestal_dependency UNIV ∧
   ¬ well_founded_on UNIV pedestal_dependency ∧
   local_foundation_on {0, 1, 2} rooted_cycle_dependency {0, 1, 2} ∧
   global_foundation_on {0, 1, 2} rooted_cycle_dependency {0, 1, 2} ∧
   ¬ acyclic_on {0, 1, 2} rooted_cycle_dependency ∧
   local_foundation_on {0, 1, 2} paired_dependency {2} ∧
   ¬ full_foundation_on {0, 1, 2} paired_dependency
     paired_full_grounding {2}"
  using integer_predecessor_acyclic_on
    integer_predecessor_not_local_foundation
    foundation_without_well_foundedness_pedestal
    local_foundation_not_acyclic_rooted_cycle
    partial_full_grounding_diverge by blast

lemma integer_predecessor_is_essentially_ordered_grounded:
  "essentially_ordered_series UNIV integer_predecessor_cause
    (λx. grounded_in UNIV integer_predecessor_cause x) (0 :: int)"
proof -
  have incoming:
      "∀x. grounded_in UNIV integer_predecessor_cause x"
    using integer_predecessor_has_incoming
    by (auto simp: grounded_in_def)
  show ?thesis
    unfolding essentially_ordered_series_def
    using incoming by auto
qed

section ‹Auxiliary Local Causal-Efficacy Stress Test›

text ‹
  As an auxiliary stress test rather than a full semantics of derivative
  causal efficacy, we introduce a small structural efficacy interface.
  @{term "H x p"} says
  that entity @{term x} possesses causal power @{term p}; @{term "E x p a"}
  says that it exercises that power toward effect @{term a}.  A locally
  borrowed exercise requires an immediate cause @{term x} of @{term a}, and
  requires the exercised power to be possessed by an earlier supporter of
  @{term x}.  This is deliberately local: it expresses transmission at each
  step without postulating a global well-foundedness or foundation principle.
›

definition locally_borrowed_power_on ::
  "'a set ⇒ ('a ⇒ 'a ⇒ bool) ⇒
   ('a ⇒ 'p ⇒ bool) ⇒
   ('a ⇒ 'p ⇒ 'a ⇒ bool) ⇒
   'a set ⇒ bool"
where
  "locally_borrowed_power_on C D H E R ⟷
     (∀a ∈ R. grounded_in C D a ⟶
       (∃x p y. x ∈ C ∧ D x a ∧ H x p ∧ E x p a ∧
          y ∈ C ∧ D y x ∧ H y p))"

lemma integer_regress_has_local_borrowed_power:
  "locally_borrowed_power_on UNIV integer_predecessor_cause
    (λ(_ :: int) (_ :: unit). True)
    (λ(_ :: int) (_ :: unit) (_ :: int). True) UNIV"
proof -
  show ?thesis
    unfolding locally_borrowed_power_on_def
  proof (intro ballI impI)
    fix a :: int
    assume "a ∈ (UNIV :: int set)"
      and "grounded_in UNIV integer_predecessor_cause a"
    show "∃x p y. x ∈ (UNIV :: int set) ∧
        integer_predecessor_cause x a ∧
        (λ(_ :: int) (_ :: unit). True) x p ∧
        (λ(_ :: int) (_ :: unit) (_ :: int). True) x p a ∧
        y ∈ (UNIV :: int set) ∧
        integer_predecessor_cause y x ∧
        (λ(_ :: int) (_ :: unit). True) y p"
      by (intro exI[of _ "a - 1"] exI[of _ "()"] exI[of _ "a - 2"])
        (simp add: integer_predecessor_cause_def)
  qed
qed

theorem essential_ordering_local_efficacy_countermodel:
  "acyclic_on UNIV integer_predecessor_cause ∧
   locally_borrowed_power_on UNIV integer_predecessor_cause
     (λ(_ :: int) (_ :: unit). True)
     (λ(_ :: int) (_ :: unit) (_ :: int). True) UNIV ∧
   essentially_ordered_series UNIV integer_predecessor_cause
     (λx. grounded_in UNIV integer_predecessor_cause x) (0 :: int) ∧
   ¬ local_foundation_on UNIV integer_predecessor_cause UNIV"
  using integer_predecessor_acyclic_on
    integer_regress_has_local_borrowed_power
    integer_predecessor_is_essentially_ordered_grounded
    integer_predecessor_not_local_foundation by blast

text ‹
  Thus the formalized local support/transmission condition leaves an infinite
  descending regress possible.  Any theorem excluding this model must add a
  genuinely global principle such as well-foundedness, local/global foundation,
  or an equivalent termination condition.  This is a result about the precise
  interface formalized here, not a claim about every possible metaphysical
  theory of causal efficacy.
›

end