Lean verification registry · Authored proofs · The Logos Architecture
Written formal sequents verified
Axiom-free: true · 1 checked theorem statements.
Lean establishes the listed formal statements and dependencies. The exact authored source, Ground, known premise meanings, application validation and empirical evidence remain separately typed. No unencoded section is certified by a neighboring theorem.
Original source author: Maclain Hunter. Machine formalization: Replit Agent. No original wording was rewritten.
Source registered: 2026-10-03T01:29:49.835Z (not original authorship).
Formalized: 2026-10-03T10:37:05.082Z.
Checked: 2026-10-03T10:41:12.501Z.
Independent timestamp: 2026-10-03T10:42:55.000Z.
Authored source SHA-256: 1777fd11e570cd38f3ff96ea507523cb5866cb1250be230d3405ebdfe0421079
Lean source · Verification JSON · Exact archived source JSON · Compiler report · Current authored source page · Signed release and verification instructions
Lean (version 4.7.0, commit v4.7.0, Release) exitCode=0 'HunterAuthored.inference_1' does not depend on any axioms
{P, P -> Q, (P & Q) -> R, S, S -> T, (S & T) -> U} |= U
Exact source sequent under finite two-valued propositional semantics. Source proposition meanings and Logic/Logos/God Ground are preserved separately; this checks the inference, not unencoded prose.
Proof of the PSR by Maclain Hunter
Definition of the PSR:
The Principle of Sufficient Reason (PSR) is a rational principle stating that everything that exists or occurs must have an ultimate Reason (Explanation; Cause; Logos). Formulated by Leibniz, it asserts that there are no "brute facts" (or illogical logical truths) in reality without contradiction. It means that for any given fact or Truth, there is Logos backing it and a sufficient explanation for why it is the way it is and not otherwise, falling back on non-contradiction as the universal bedrock of why P is P and P is not “not P”.
Premises:
P: Assume the PSR is not a logical rule/principle, but a mere assertion or invalid.
Q: If sufficient Reason (Logos; Coherence) isn’t needed for Coherence (Logic; Reason) then there is no PSR and Coherence doesn’t have to (sufficiently) be Coherence to be Coherence which leads to contradiction, supporting the PSR.
R: P is refuted by Q and combine to proof for the contradiction supporting the PSR as a logical rule even derivable/confirmed by way of its denial.
S: The claim that I need reasoning/proof to back the PSR presupposes the PSR and doesn’t hold of a rule such as the PSR doesn’t hold. The very request for proof of the PSR (to support it) is a concession of the PSR that suggests proof/reasoning (or Reason; or Coherence) is called for.
T: If the PSR were not a logical rule (universally applicable to systems of Logic, statements of fact, positions denying concepts exist such as atheism, etc.) then there wouldn’t be a need for proof of logical rules in general, since no other common logical rule or substantively/substantially different logical rule suggests Logic and logical claims must meet a burden of proof and a Standard of reasoning.
U: Given T and denial of the PSR, the PSR could arbitrarily without sufficient Reason be established as a logical rule still - displaying its tautological self-support (and the support gained from even denial) that true logical rules like the LNC and True Logic (Logos; the One God) enjoy.
Formal Proof:
{P, P -> Q, (P & Q) -> R, S, S -> T, (S & T) -> U} |= U
Conclusion: U
Elaboration:
The PSR (which requires alignment with Logic in the sense of consistency not an arbitrary number of finite reasons, though a number of finite reasons can help establish logical consistency) is logically mandated and genuine logical rule, as demonstrated given {P, Q, R, S, T, U}.
The PSR can be understood as an (also) “elenctic” mode of Logos, Logic, and the LNC, where the LNC wards any “Reason without alignment with Reason/reasoning” and the PSR is the Law that comes from the LNC as Law applying in that “possessive mode” of Logic - where Reason is either possessed or it’s not and it needs to be possessed to not be lacked.
Brute fact is not logical as it doesn’t have explanation (or Logic backing it), making it self-refuting. Beyond that it is refuted positively by Logos providing Universal Logic and an ultimate/foundational and non-contradictory explanation for all logically conceivable concepts. That steals every opportunity away from brute fact (which is itself explainable as an incoherent notion that arises from the limited logical grasp of the contingent and finite mind and its poor reasoning or laziness in explaining Reality and isn’t even itself a brute fact) to be the ultimate and only Ground of fundamental nature of something.
Even brute fact’s ultimate Ground is Logos, and even brute fact’s fundamental nature is “incoherence within Logos/Logic” not actual brute fact (sans Logos and incoherence).
The PSR notoriously, to atheists chagrin and to the dismay of even certain “irrational theists”, requires not only “a universal cause” (a god of arbitrary kind) for the Cosmos, the Logos based Universe (or Order Based Reality; or Ordered Reality), but that the Universal Cause or “True God” (referring to: the genuine Source of Existence; the Genuine Moral Standard; the logically true Ultimate Reality) is 100% coherent with and logically equivalent to Reason/Logic (the Logos at the Foundation of the Cosmos; the God of Reason) itself.
An incoherent notion of any concept including the Universal Cause (or God) does not satisfy Logic (or Logos) and gain the rational support required to meet the bar of the PSR.
Truth Table Analysis:
TTTTTT⎪T TTT TTT TT T TTT TTT TT T
TTTTTF⎪T TTT TTT TT T TTT TTT FF F
TTTTFT⎪T TTT TTT TT T TFF TFF TT T
TTTTFF⎪T TTT TTT TT T TFF TFF TF F
TTTFTT⎪T TTT TTT TT F FTT FFT TT T
TTTFTF⎪T TTT TTT TT F FTT FFT TF F
TTTFFT⎪T TTT TTT TT F FTF FFF TT T
TTTFFF⎪T TTT TTT TT F FTF FFF TF F
TTFTTT⎪T TTT TTT FF T TTT TTT TT T
TTFTTF⎪T TTT TTT FF T TTT TTT FF F
TTFTFT⎪T TTT TTT FF T TFF TFF TT T
TTFTFF⎪T TTT TTT FF T TFF TFF TF F
TTFFTT⎪T TTT TTT FF F FTT FFT TT T
TTFFTF⎪T TTT TTT FF F FTT FFT TF F
TTFFFT⎪T TTT TTT FF F FTF FFF TT T
TTFFFF⎪T TTT TTT FF F FTF FFF TF F
TFTTTT⎪T TFF TFF TT T TTT TTT TT T
TFTTTF⎪T TFF TFF TT T TTT TTT FF F
TFTTFT⎪T TFF TFF TT T TFF TFF TT T
TFTTFF⎪T TFF TFF TT T TFF TFF TF F
TFTFTT⎪T TFF TFF TT F FTT FFT TT T
TFTFTF⎪T TFF TFF TT F FTT FFT TF F
TFTFFT⎪T TFF TFF TT F FTF FFF TT T
TFTFFF⎪T TFF TFF TT F FTF FFF TF F
TFFTTT⎪T TFF TFF TF T TTT TTT TT T
TFFTTF⎪T TFF TFF TF T TTT TTT FF F
TFFTFT⎪T TFF TFF TF T TFF TFF TT T
TFFTFF⎪T TFF TFF TF T TFF TFF TF F
TFFFTT⎪T TFF TFF TF F FTT FFT TT T
TFFFTF⎪T TFF TFF TF F FTT FFT TF F
TFFFFT⎪T TFF TFF TF F FTF FFF TT T
TFFFFF⎪T TFF TFF TF F FTF FFF TF F
FTTTTT⎪F FTT FFT TT T TTT TTT TT T
FTTTTF⎪F FTT FFT TT T TTT TTT FF F
FTTTFT⎪F FTT FFT TT T TFF TFF TT T
FTTTFF⎪F FTT FFT TT T TFF TFF TF F
FTTFTT⎪F FTT FFT TT F FTT FFT TT T
FTTFTF⎪F FTT FFT TT F FTT FFT TF F
FTTFFT⎪F FTT FFT TT F FTF FFF TT T
FTTFFF⎪F FTT FFT TT F FTF FFF TF F
FTFTTT⎪F FTT FFT TF T TTT TTT TT T
FTFTTF⎪F FTT FFT TF T TTT TTT FF F
FTFTFT⎪F FTT FFT TF T TFF TFF TT T
FTFTFF⎪F FTT FFT TF T TFF TFF TF F
FTFFTT⎪F FTT FFT TF F FTT FFT TT T
FTFFTF⎪F FTT FFT TF F FTT FFT TF F
FTFFFT⎪F FTT FFT TF F FTF FFF TT T
FTFFFF⎪F FTT FFT TF F FTF FFF TF F
FFTTTT⎪F FTF FFF TT T TTT TTT TT T
FFTTTF⎪F FTF FFF TT T TTT TTT FF F
FFTTFT⎪F FTF FFF TT T TFF TFF TT T
FFTTFF⎪F FTF FFF TT T TFF TFF TF F
FFTFTT⎪F FTF FFF TT F FTT FFT TT T
FFTFTF⎪F FTF FFF TT F FTT FFT TF F
FFTFFT⎪F FTF FFF TT F FTF FFF TT T
FFTFFF⎪F FTF FFF TT F FTF FFF TF F
FFFTTT⎪F FTF FFF TF T TTT TTT TT T
FFFTTF⎪F FTF FFF TF T TTT TTT FF F
FFFTFT⎪F FTF FFF TF T TFF TFF TT T
FFFTFF⎪F FTF FFF TF T TFF TFF TF F
FFFFTT⎪F FTF FFF TF F FTT FFT TT T
FFFFTF⎪F FTF FFF TF F FTT FFT TF F
FFFFFT⎪F FTF FFF TF F FTF FFF TT T
FFFFFF⎪F FTF FFF TF F FTF FFF TF F
(Valid)
QED