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-03T01:30:26.416Z (not original authorship).
Formalized: 2026-10-03T10:37:05.082Z.
Checked: 2026-10-03T10:42:50.879Z.
Independent timestamp: 2026-10-03T10:42:55.000Z.
Authored source SHA-256: c03d1a3f419ddfa9dcca81b4a54ab39effa3229caf4eb612a0417b86d3eed843
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
{P, P → Q, Q → R, R → S, S → T, T → U, U → P, ~(~P & ~Q & ~R & ~S & ~T & ~U)} |= ((P & Q) & (R & S) & T) & U
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, R → S, S → T, T → U, U → P, ~(~P & ~Q & ~R & ~S & ~T & ~U)} |= ((P & Q) & (R & S) & T) & U
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.
Version 1:
{P, P → Q, Q → R, R → S, S → T, T → U, U → P, ~(~P & ~Q & ~R & ~S & ~T & ~U)} |= ((P & Q) & (R & S) & T) & U
P: A self-evident truth is true regardless of any mind's belief or denial.
Q: Well-formed formal logical proofs are self-evident truths.
R: The existence of a self-consistent and complete (even if minimal) set of logical truths is necessary for the existence of a self-evident truth.
S: The Universal Logic is the self-consistent and complete/dynamic set of logical truths.
T: The Universal Logic exists independently of human beliefs and opinions.
U: The Universal Logic is the self-evident truth that underlies all reality.
OR
Version 2:
{P, P → Q, Q → R, R → S, S → T, T → U, U → P, ~(~P & ~Q & ~R & ~S & ~T & ~U)} |= ((P & Q) & (R & S) & T) & U
P: The immanent and self-evident Absolute Truth (coherent with and synonymous with the Logic of the Universe or Logos) is inherently logical (existing logically by default and necessity) and is absolutely true for eternity, beyond/throughout contingent concepts of space and time, regardless of any mind's belief or denial.
Q: Well-formed formal logical proofs are self-evident truths, as Logic is (the ultimate self-evident Truth/Logic).
R: The existence of the self-consistent and complete set of logical truths is logically necessary, and is evidenced by the existence/confirmation of any truths or falsehoods (anything with a logically determined/determinable truth value).
S: The Absolute Truth (Universal Logic - the Natural Order) is the self-evident (tautological) and complete/dynamic Reality and its Logic - the Logical Framework of the Real World.
T: The Universal Logic (Logos - Absolute Truth) exists independently of human beliefs and opinions, and furthermore is evident in all subjectivity and contingent being/life/thought. No thought objective or subjective could occur without Reason (Logos - Universal Logic).
U: The Natural Order (Universal Logic - Absolute Truth) is the self-evident Logical Origin (True God - the Source and Sustainer of the Universe) that underlies Reality and all aspects of Existence (including human existence and inquiry).