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:52.110Z (not original authorship).
Formalized: 2026-10-03T10:37:05.082Z.
Checked: 2026-10-03T10:41:25.314Z.
Independent timestamp: 2026-10-03T10:42:55.000Z.
Authored source SHA-256: f800f0482b9d8a4fb1e71f63f37aa16f40b9a61f66db811f64f5d96982588c61
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 -> R, P -> (Q <-> R), S, S -> T, T -> ((P & Q) & R)} |= P <-> (Q <-> R)
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.
Reason’s Reasoning by Maclain Hunter
Premises:
P: Logos (Reason) and non-contradiction of Logic.
Q: Coherent engagement with/between Reason and reasoning (including Reason and Reason’s own reasoning in the absolute sense; including “neosis neoseos” ala Aristotle).
R: Reasoning without contradiction, engaging Logic/Logos (by Logos or contingent minds).
S: Assume different permutations of {P, Q, R} being true or false. Only P, Q, and R all being true ends in the Coherence of Reason, reasoning, and coherent engagement. If P is True but Q and R are false, or any similar combination, the incoherence tautologically arises between Reason, reasoning, and rational engagement - which is untenable.
T: Premise S and its reductio show that P, Q, and R must be true, not for merely the sake of this proof or a personal belief, but for the general and transcendental Coherence of Reason, reasoning, and rational engagement.
Proof:
{P, P -> Q, P -> R, P -> (Q <-> R), S, S -> T, T -> ((P & Q) & R)} |= P <-> (Q <-> R)
Conclusion: {P, Q, R, S, T}:
The reasoning of Reason is mandatory for non-contradiction as much as coherent reasoning by contingent minds is mandatory for non-contradiction and for rational engagement with Reason. This aligns well with Aristotle’s notion of “neosis neoseos”.
Truth Table Analysis:
TTTTT⎪T TTT TTT TT TTT T TTT TT TTT TT TT TTT
TTTTF⎪T TTT TTT TT TTT T TFF FT TTT TT TT TTT
TTTFT⎪T TTT TTT TT TTT F FTT TT TTT TT TT TTT
TTTFF⎪T TTT TTT TT TTT F FTF FT TTT TT TT TTT
TTFTT⎪T TTT TFF TF TFF T TTT TF TTT FF TF TFF
TTFTF⎪T TTT TFF TF TFF T TFF FT TTT FF TF TFF
TTFFT⎪T TTT TFF TF TFF F FTT TF TTT FF TF TFF
TTFFF⎪T TTT TFF TF TFF F FTF FT TTT FF TF TFF
TFTTT⎪T TFF TTT TF FFT T TTT TF TFF FT TF FFT
TFTTF⎪T TFF TTT TF FFT T TFF FT TFF FT TF FFT
TFTFT⎪T TFF TTT TF FFT F FTT TF TFF FT TF FFT
TFTFF⎪T TFF TTT TF FFT F FTF FT TFF FT TF FFT
TFFTT⎪T TFF TFF TT FTF T TTT TF TFF FF TT FTF
TFFTF⎪T TFF TFF TT FTF T TFF FT TFF FF TT FTF
TFFFT⎪T TFF TFF TT FTF F FTT TF TFF FF TT FTF
TFFFF⎪T TFF TFF TT FTF F FTF FT TFF FF TT FTF
FTTTT⎪F FTT FTT FT TTT T TTT TF FFT FT FF TTT
FTTTF⎪F FTT FTT FT TTT T TFF FT FFT FT FF TTT
FTTFT⎪F FTT FTT FT TTT F FTT TF FFT FT FF TTT
FTTFF⎪F FTT FTT FT TTT F FTF FT FFT FT FF TTT
FTFTT⎪F FTT FTF FT TFF T TTT TF FFT FF FT TFF
FTFTF⎪F FTT FTF FT TFF T TFF FT FFT FF FT TFF
FTFFT⎪F FTT FTF FT TFF F FTT TF FFT FF FT TFF
FTFFF⎪F FTT FTF FT TFF F FTF FT FFT FF FT TFF
FFTTT⎪F FTF FTT FT FFT T TTT TF FFF FT FT FFT
FFTTF⎪F FTF FTT FT FFT T TFF FT FFF FT FT FFT
FFTFT⎪F FTF FTT FT FFT F FTT TF FFF FT FT FFT
FFTFF⎪F FTF FTT FT FFT F FTF FT FFF FT FT FFT
FFFTT⎪F FTF FTF FT FTF T TTT TF FFF FF FF FTF
FFFTF⎪F FTF FTF FT FTF T TFF FT FFF FF FF FTF
FFFFT⎪F FTF FTF FT FTF F FTT TF FFF FF FF FTF
FFFFF⎪F FTF FTF FT FTF F FTF FT FFF FF FF FTF
(VALID)
QED