Lean verification registry · Authored proofs · The Logos Architecture
Written formal sequents verified
Axiom-free: true · 2 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-02T16:57:39.572Z (not original authorship).
Formalized: 2026-10-03T10:37:05.082Z.
Checked: 2026-10-03T10:39:30.100Z.
Independent timestamp: 2026-10-03T10:42:55.000Z.
Authored source SHA-256: 4f40a117323e4933b097560d59f89e8ad14c6c2e53b3134d6dc0e896447ca08c
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 'HunterAuthored.source_identity_rule' does not depend on any axioms
{P, P → Q, Q → R, 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.
Logic is Logic
The explicitly named Identity rule, over every type and element. The remaining prose is not replaced by this witness.
Logic, Ethics, and Epistemology by Maclain Hunter:
Premises:
P: Logic is Logic (a tautology) and, as the self-supporting Foundation of Logical Concepts (the Logos - the Highest Order of Logic - the Natural Order of the Cosmos) encompasses and entails all epistemology and ethics.
Q: To assume otherwise (ie - “~P”) leads to paradox and contradiction where neither epistemology nor ethics are logically coherent and valid concepts (or “logical concepts”).
R: That assumption in premise Q is an absurdity that we must maintain Logic as God and as the Supreme Entity to avoid.
Formal Argument:
{P, P → Q, Q → R, R} |= P <-> (Q & R)
Conclusion: {P, Q, R}: If Logic does not encompass all such notions, and even any concept you can think of, then contradiction arises.
Truth Table Analysis:
valid
↓ ↓ ↓ ↓ ↓
PQR⎪P P→Q Q→R R╞P↔(Q&R)
――――――――――――――――――――――――
TTT⎪T TTT TTT T TT TTT
TTF⎪T TTT TFF F TF TFF
TFT⎪T TFF FTT T TF FFT
TFF⎪T TFF FTF F TF FFF
FTT⎪F FTT TTT T FF TTT
FTF⎪F FTT TFF F FT TFF
FFT⎪F FTF FTT T FT FFT
FFF⎪F FTF FTF F FT FFF
Q.E.D.