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:30:02.013Z (not original authorship).
Formalized: 2026-10-03T10:37:05.082Z.
Checked: 2026-10-03T10:39:03.028Z.
Independent timestamp: 2026-10-03T10:42:55.000Z.
Authored source SHA-256: 980062ee1ccd709709aaede382742fefe25a971c740911484895ee7e30be0f72
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, R -> 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.
Knowing Logic and Proof by Maclain Hunter
Premises:
P: Logic is lawfully defined by non-contradiction of Logic (universally), and all logical “rules” plural are forms and subsets of non-contradiction of the Logos (of Universal Logic), like the LEM is logical non-contradiction applied to binary Truth values.
Q: The semantics of P elaborate on logical rules and how they actually cohere under Logos as the Singular/Ultimate Law. This is a demonstration of knowledge of Logic that can be validly referred to (here in Q).
R: It is absurd that I would explain Logic (as in P) and to explicitly point of that I had (as in Q) while I don’t know Logic. This valid explanation and argument that I am giving this explanation is by definition “proof” or an argument pointing with Reason and reasoning to the Truth and Reality (see OED definition of proof, it is similar).
S: R suggests I know what proof is and how it is defined by the dictionary (in English) and Logic (logically). Logical proof fully coherent with Logic is logically equivalent to Logic and Coherence and cannot be “not Logic” or “not coherent” without contradiction. This proof stands as Logic sans demonstrated incoherence.
Formal Argument:
{P, P -> Q, Q -> R, R -> S} |= (P & Q) -> (R & S)
Ergo:
The proof above uses valid structure and self-referential semantics to show I know validly what proof and Logic (as defined by Coherence and Lawful Order as the Rule of Logic and the Rule logical rules must themselves align with) are.
To refute me you would have to find contradiction and apply the Lawful Order of Logical Non-Contradiction (or Logos) I am describing which would be mere elenctic support for my position that Logic is about non-contradiction of Lawful Order.
The formal entailment is truth-functionally valid; the semantic premises identify the performed reasoning as an instance of knowledge of Logic and proof. Thus the formal validity and the reflexive semantic content jointly constitute the claimed demonstration.
Truth Table Analysis:
TTTT⎪T TTT TTT TTT TTT T TTT
TTTF⎪T TTT TTT TFF TTT F TFF
TTFT⎪T TTT TFF FTT TTT F FFT
TTFF⎪T TTT TFF FTF TTT F FFF
TFTT⎪T TFF FTT TTT TFF T TTT
TFTF⎪T TFF FTT TFF TFF T TFF
TFFT⎪T TFF FTF FTT TFF T FFT
TFFF⎪T TFF FTF FTF TFF T FFF
FTTT⎪F FTT TTT TTT FFT T TTT
FTTF⎪F FTT TTT TFF FFT T TFF
FTFT⎪F FTT TFF FTT FFT T FFT
FTFF⎪F FTT TFF FTF FFT T FFF
FFTT⎪F FTF FTT TTT FFF T TTT
FFTF⎪F FTF FTT TFF FFF T TFF
FFFT⎪F FTF FTF FTT FFF T FFT
FFFF⎪F FTF FTF FTF FFF T FFF
(Valid)
QED