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-02T21:46:58.577Z (not original authorship).
Formalized: 2026-10-03T10:37:05.082Z.
Checked: 2026-10-03T10:41:03.195Z.
Independent timestamp: 2026-10-03T10:42:55.000Z.
Authored source SHA-256: e58e12ad28490c9367345c3f942f6f0579372963042a03fefaff15b38ce0d5ff
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.inference_2' does not depend on any axioms
{PS, PS -> DT, DT & EOC, PS -> PRN} |= ((DT & EOC) -> PRN) <-> PS
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.
{P, P -> Q, Q & R, P -> S} |= ((P & Q) -> R) <-> 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.
Proof of Established Certainty by Maclain Hunter
Premises:
P: Truth can be demonstrated with 100% certainty (rationally) though deductive logical proof. This can be represented by DT (standing for “Deductive Truth”)
Q: In the context I am sharing this proof I have shown deductive logical proof to support my claims, thus I can be 100% certain. If the context changes then the level of certainty may change but where proof is present my certainty is complete. This can be encoded as PS (ie - proof shown).
R: If A) I were uncertain then B) would contradict my certainty expressed confidently here in written (even “empirically observable”) form. This can be encoded as EOC (ie - empirically observable certainty).
S: Since proof supports my rational certainty it is not blind acceptance, it is rationally justified. For my level of certainty to change it would take superior logical proof (SP) that refutes and/or logically supersedes the proof(s) at hand - not merely assertions or disbelief without superseding proof and Coherence. This can be encoded as PRN (ie - proper refutation necessary).
T: The premises {P, Q, R, S} and the symbolic representations encoded within them have relationship that include the expression:
{PS, PS -> DT, DT & EOC, PS -> PRN} |= ((DT & EOC) -> PRN) <-> PS
Formal Reasoning:
{P, P -> Q, Q & R, P -> S} |= ((P & Q) -> R) <-> S
Truth Table Analysis:
PQRS⎪P P→Q Q&R P→S╞((Q&R)→S)↔P
TTTT⎪T TT TT TT TT T T
TTTF⎪T TT TT TF TT F T
TTFT⎪T TT TF TT TF T T
TTFF⎪T TT TF TF TF F T
TFTT⎪T TF FT TT FT T T
TFTF⎪T TF FT TF FT F T
TFFT⎪T TF FF TT FF T T
TFFF⎪T TF FF TF FF F T
FTTT⎪F FT TT FT TT T F
FTTF⎪F FT TT FF TT F F
FTFT⎪F FT TF FT TF T F
FTFF⎪F FT TF FF TF F F
FFTT⎪F FF FT FT FT T F
FFTF⎪F FF FT FF FT F F
FFFT⎪F FF FF FT FF T F
FFFF⎪F FF FF FF FF F F
(Valid)
Q.E.D.