Theory Diagnostics_Nitpick
theory Diagnostics_Nitpick
imports Axiom_Free_Ontological_Trinity
begin
section ‹1. Diagnostics Overview›
text ‹This theory gathers lightweight diagnostics for the U-core and packages:
• Purity checks: ensure no backflow from optional bridges/locales into the D-route core.
• Sanity checks: Nitpick is expected to find no counterexample (i.e., @{text "expect = none"}).
• Suspicion checks: Nitpick is expected to find a genuine counterexample (i.e., flags over-strong statements).
• Model checks(Trinity model): Nitpick is expected to produce a genuine Trinity witness model, certifying non-vacuity and concrete realizability of the target configuration.
• Model checks(anti-modal collapse): Nitpick is expected to produce a genuine witness model showing that created truths are not forced into necessity, thereby confirming the absence of modal collapse.
›
section ‹2. Locale / Theorem Introspection (non-proof diagnostics)›
text ‹Quick check that locales are only interpreted where intended (no leakage).›
print_interps FullIdBridge
print_interps Riemann_Toy
text ‹Show hypotheses while printing key equivalences, then turn it back off.›
declare [[show_hyps]]
thm PH_imp_EH PH_imp_TH EH_TH_imp_PH PH_iff_EH_TH
thm EqU_iff_LeU_both
declare [[show_hyps = false]]
section ‹3. Nitpick setup (parameters and unfolds)›
text ‹Global defaults for Nitpick runs in this file (bump if needed).›
nitpick_params [verbose, card = 2-4, card U = 1-3, timeout = 60]
text ‹Unfold core definitions so Nitpick can see the structure.›
declare SuppU_def [nitpick_unfold]
declare LeU_def [nitpick_unfold]
declare EqU_def [nitpick_unfold]
declare Supports_def [nitpick_unfold]
declare EDia_def [nitpick_unfold]
declare TrueNow_def [nitpick_unfold]
declare EH_def [nitpick_unfold]
declare TH_def [nitpick_unfold]
declare PH_def [nitpick_unfold]
declare LtU_def [nitpick_unfold]
declare H_negU_strict_def [nitpick_unfold]
declare H_opt_def [nitpick_unfold]
declare PDom_def [nitpick_unfold]
declare PSupp_def [nitpick_unfold]
section ‹4. Sanity checks (no counterexample expected)›
text ‹1) @{term PH} iff @{text "EH ∧ TH"}.›
lemma Nitpick_PH_iff_EH_TH:
shows "PH q ⟷ (EH q ∧ TH q)"
nitpick [expect = none] oops
text ‹2) @{term Hopt3} implies @{term N3} (unboxed, D-route).›
lemma Nitpick_OnlyN3_from_Hopt3_unboxed:
assumes "Hopt3 a b c"
shows N3
nitpick [expect = none] oops
text ‹3) Global n=1 exclusion (core witness wrapper).›
lemma Nitpick_n1_global_exclusion_core:
assumes "∃a a' b c.
EDia b ∧ EDia c ∧
(Arg b) ≼ (Arg a) ∧ (Arg c) ≼ (Arg a) ∧
(¬ ((Arg b) ≼ (Arg a')) ∨ ¬ ((Arg c) ≼ (Arg a'))) ∧
EH (Arg a')"
shows False
nitpick [expect = none] oops
text ‹4) Global n=1 exclusion (H\_opt wrapper).›
lemma Nitpick_n1_global_exclusion_for_Hopt:
assumes "∃Q b c a'.
H_opt Q ∧ EDia b ∧ EDia c ∧
(¬ ((Arg b) ≼ (Arg a')) ∨ ¬ ((Arg c) ≼ (Arg a'))) ∧
EH (Arg a')"
shows False
nitpick [expect = none] oops
text ‹5) H\_opt finality over @{term PDom}: no strict superior.›
lemma Nitpick_argument_finality_PDom:
assumes "H_opt q"
shows "∀ζ∈PDom. ¬ ((Arg q) ≺ (Arg ζ))"
nitpick [expect = none] oops
text ‹6) Pair collapse at Arg-level from two @{term PH} + possibility.›
lemma Nitpick_PH_pair_collapse_to_EqU:
assumes "PH (Arg Φ)" "PH (Arg Ω)" "EDia Φ" "EDia Ω"
shows "(Arg Φ) ≈ (Arg Ω)"
nitpick [expect = none] oops
section ‹5. Suspicion checks (Nitpick should find genuine counterexamples)›
text ‹Universal entailment / empty entailment are both false.›
lemma entails_universal_suspect: "ALL e u. e ⊢ u"
nitpick [card U=3, timeout=15, expect = genuine] oops
lemma entails_empty_suspect: "~ (EX e u. e ⊢ u)"
nitpick [card U=3, timeout=15, expect = genuine] oops
section ‹6. Strengthened / boundary diagnostics›
text ‹Strict variants: @{term EH_strict} does not imply @{term EH} in general (should be refutable).›
lemma EH_strict_converse_suspect: "ALL q. EH_strict q --> EH q"
nitpick [card U=3, timeout=20, expect = genuine] oops
text ‹But @{term PH_strict} does imply @{term PH} (holds by definitions used here).›
lemma PH_strict_converse_check: "ALL q. PH_strict q --> PH q"
nitpick [card U=3, timeout=20, expect = none] oops
text ‹One-way TSupp-maximality: the converse direction should hold under our setup.›
lemma TH_TSupp_max_converse_check:
"ALL q. ((ALL x. TSupp x ⊆ TSupp q) --> TH q)"
nitpick [card U=3, timeout=20, expect = none] oops
text ‹The following global tautologies should be refutable.›
lemma Hopt_tautology_suspect: "ALL q. H_opt q"
nitpick [card U=3, timeout=20, expect = genuine] oops
lemma Comparable_PDom_on_tautology_suspect: "ALL q. Comparable_PDom_on q"
nitpick [card U=3, timeout=20, expect = genuine] oops
lemma H_negU_strict_tautology_suspect: "ALL q. H_negU_strict q"
nitpick [card U=3, timeout=20, expect = genuine] oops
section ‹7. No modal collapse (Nitpick model test)›
text ‹
We established that the Trinity implies the possibility of R (@{text "◇"}R).
The critical question is whether the Trinity necessitates R (Modal Collapse).
If Nitpick finds a counter-model for the lemma below, we confirm that
Trinity and @{text "¬"}R can co-exist without contradiction, proving that collapse is resolved.
›
lemma Trinity_does_not_necessitate_R:
fixes Φ Ω ψ R :: bool
assumes T_Pattern: "Trinity Φ Ω ψ ⟶ ◇ R"
assumes S_Pattern: "¬ (Trinity Φ Ω ψ) ⟶ ¬ R"
shows "Trinity Φ Ω ψ ⟶ R"
nitpick [expect = genuine, show_all, satisfy]
oops
text ‹
(1) Anti-degeneracy: @{text "◇"} is not trivially True for every proposition.
›
lemma Diamond_is_not_degenerate:
shows "¬ (∀P::bool. ◇ P)"
nitpick [expect = genuine, show_all, satisfy]
oops
text ‹
(2) Non-triviality guard: @{text "◇"}False is not forced (not a theorem).
We test both directions as independence smoke-tests.
›
lemma Dia_False_is_not_a_theorem:
shows "◇ False"
nitpick [expect = genuine, show_all, satisfy]
oops
lemma Not_Dia_False_is_not_a_theorem:
shows "¬ (◇ False)"
nitpick [expect = genuine, show_all, satisfy]
oops
section ‹8. Computational Diagnostics and Trinity Model Existence (Nitpick test)›
text ‹
APPENDIX: The following diagnostic block uses Nitpick to explore the model-theoretic
properties of the theory.
Note on ``oops'': The usage of ``oops'' here does not indicate a proof failure.
Rather, it marks a diagnostic check where Nitpick attempts to find counter-examples.
The absence of counter-examples in these finite scopes supports the consistency
of the Triune Necessity (N=3) as the unique logical equilibrium of the system.
›
typedef U3 = "{0::nat, 1, 2}" by auto
setup_lifting type_definition_U3
definition HeadP_U3 :: "U3 ⇒ bool" where
"HeadP_U3 _ ≡ True"
definition NT_pair_supportU3 :: "U3 ⇒ U3 ⇒ U3 ⇒ bool" where
"NT_pair_supportU3 A B C ≡ (A ≠ B ∧ A ≠ C ∧ B ≠ C)"
definition TrinityModel :: bool where
"TrinityModel ≡ (∃A B C :: U3.
HeadP_U3 A ∧ HeadP_U3 B ∧ HeadP_U3 C ∧
A ≠ B ∧ A ≠ C ∧ B ≠ C ∧
NT_pair_supportU3 A B C ∧
NT_pair_supportU3 B C A ∧
NT_pair_supportU3 C A B)"
lemma "TrinityModel"
nitpick [satisfy, card U3 = 3, expect = genuine]
oops
subsection ‹8.1 Trinity Model existence Nitpick Test - MaxNT›