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:37:25.622Z (not original authorship).
Formalized: 2026-10-03T10:37:05.082Z.
Checked: 2026-10-03T10:37:12.319Z.
Independent timestamp: 2026-10-03T10:42:55.000Z.
Authored source SHA-256: 182a4ad2b271db6d8daaa393f8878f9b94c1d90bb7c23c086e54b88450ed69f1
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, Q -> R, ((P & Q) & R) -> S} |= S
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.
Absolute Logic in Universal Contingency by Maclain Hunter
Premises:
P: Assume universal contingency and nothing that is logically Absolute (or God in that sense of the Absolute or God of Reason, personal or not).
Q: Logic remains something that even while logically contingent (or assumed to be such) cannot both stay Logic and diverge from Logic, as say an incoherent human can stay human while diverging from Logic.
R: Logic is logically valid contingent upon Logic, while other concepts do not without fallacy or incoherence get to “deviate from Logic validly” and be contingent upon only themselves (as Logic could be valid while deviant from all other concepts and needs only alignment with itself for validity under assumed universal contingency - which means “even when we start without assuming Logic as Absolute”.
S: Given {P, Q, R} Logic is logically Absolute (and God in that sense of the thing that all else relies on to exist logically while it relies only on itself for existence) without that being a presupposition and even when the assumption of the opposite is our presupposed starting point.
Proof:
{P, P -> Q, Q -> R, ((P & Q) & R) -> S} |= S
Truth Table:
PQRS⎪P P→Q Q→R ((P&Q)&R)→S╞S
TTTT⎪T TTT TTT TTT TT TT T
TTTF⎪T TTT TTT TTT TT FF F
TTFT⎪T TTT TFF TTT FF TT T
TTFF⎪T TTT TFF TTT FF TF F
TFTT⎪T TFF FTT TFF FT TT T
TFTF⎪T TFF FTT TFF FT TF F
TFFT⎪T TFF FTF TFF FF TT T
TFFF⎪T TFF FTF TFF FF TF F
FTTT⎪F FTT TTT FFT FT TT T
FTTF⎪F FTT TTT FFT FT TF F
FTFT⎪F FTT TFF FFT FF TT T
FTFF⎪F FTT TFF FFT FF TF F
FFTT⎪F FTF FTT FFF FT TT T
FFTF⎪F FTF FTT FFF FT TF F
FFFT⎪F FTF FTF FFF FF TT T
FFFF⎪F FTF FTF FFF FF TF F
Formal Validity: Valid.
Semantic Content: Sound.
Overall Validity and Soundness: Valid and Sound.
QED