Dependencies

\(\textsf{liarCost}(\text{Classical}) = 0 = \textsf{classicalLiar.cost}\).

\(\textsf{liarCost}(\text{Fuzzy}) = 1 = \textsf{fuzzyLiar.cost}\).

Enumerate all ancestor sources up to depth \(n\) via DFS, returning a flat list. This is the hypercomputer in function form: the infinite tree of all possible pasts is present as the limit of \(\mathsf{ancestorsUpTo}\ t\ n\) as \(n \to \infty \). No single data structure holds the whole tree; instead the recursion is explicit in the partial function, and every finite approximation is immediately available. “Instant lookup” = calling this function with any depth \(n\).

Maps logic types to Cayley-Dickson construction steps.

A proof-carrying audit trail \(\langle source,\ target,\ proof \rangle \) showing that a tree reaches its equilibrium.

Issues a CortexCertificate for any tree \(t\), certifying that \(t \to \mathsf{rightComb}(t.\mathsf{size})\). This is the quench witness in the Witness-Skeptic game.

A finite chain of contraction steps from an ancestor to a target. \(\mathsf{Chain.tip}\ t\) is the empty chain (the present moment without a reconstructed past). \(\mathsf{Chain.link}\ h\ r\) prepends a contraction step.

The Liar wrapped in Classical logic. Cost \(\Phi = 0\) (at equilibrium). Proven using \(\mathsf{contracts\_ to\_ rightComb}\): the symmetric tree contracts to \(\mathsf{rightComb}(3)\) in finitely many steps.

\(\mathsf{compose} : \mathsf{Decision\ gates} \to \mathsf{Gate} \to \mathsf{Decision\ (g :: gates)}\). The return type is strictly richer than the input type: a gate is added to the type-level history.

The primitive non-associative rewrite rule: \((a \bullet b) \bullet c \to a \bullet (b \bullet c)\). This is the coupling signature for choice resolution, lifted through subtrees.

The reflexive-transitive closure of contracts_one. Represents an audit trail of choice resolutions with monotonic provenance.

A Decision is the refinement type from the specification: \(\mathsf{Decision\ gates} = \{ d : \mathsf{EMLTree} \mid \forall g \in \mathsf{gates},\ g.\mathsf{check}\ d \} \). The type parameter \(\mathsf{gates}\) IS the channel: downstream functions know statically which gates the datum has passed.

For a target tree \(\mathsf{target}\), a \(\mathsf{Decomposition}\) pairs a \(\mathsf{source}\) with a proof \(\mathsf{contracts\_ to}\ \mathsf{source}\ \mathsf{target}\). This is the ontological unit of de-composition: an outcome together with a specific prior configuration that could have produced it.

The type of binary trees representing configurations in the Tamari lattice. A tree is either a Leaf (empty configuration) or a Node \(t_1\ t_2\) (composition of two sub-configurations).

The sum of \(\Phi \) costs across all layers of the Liar tower.

The Liar wrapped in Fuzzy logic. The fixed point \(\neg 0.5 = 0.5\) gives pentagonator distance \(\Phi = 1\) (CD step 1). Proven via the generic liarWrapper.

A Gate is a binary decision predicate indexed by a logic modality: \(\mathsf{Gate} = (\mathsf{name} : \mathsf{String}) \times (\mathsf{modality} : \mathsf{LogicType}) \times (\mathsf{check} : \mathsf{EMLTree} \to \mathsf{Prop})\). Every logic type gives rise to a Gate via \(\mathsf{ofLogicType}\), and every tree passes any such gate (by 26).

The cost \(\Phi (\text{Grandfather}, \text{lt})\), equal to \(\textsf{cdStep}(\text{lt})\).

The Grandfather Paradox stated as a Problem of class \(\mathsf{temporalDecision}\). Its tree is a left-comb chain of size 4, encoding the 4-step time-travel causal loop: traveler exists \(\to \) travels back \(\to \) grandfather killed \(\to \) traveler never born (contradiction). The normal form is \(\mathsf{rightComb}(4)\).

The Grandfather tower: one layer per suitable logic.

For any logic lt, constructs the WrappedProblem with \(\textsf{cost} = \textsf{cdStep}(\textsf{lt})\). Resolves the temporal causal loop via \(\mathsf{contracts\_ to\_ rightComb}\).

An idempotent resolution for a type \(\alpha \) consists of:

• \(\mathsf{step} : \alpha \to \alpha \), a regularization step that is idempotent (\(\mathsf{step} \circ \mathsf{step} = \mathsf{step}\)).

• \(\mathsf{limit} : \alpha \to \alpha \), the limiting configuration reachable in one step from any image of \(\mathsf{step}\) (\(\mathsf{limit} = \mathsf{step} \circ \mathsf{limit}\)).

The canonical example is rightCombResolution, where \(\mathsf{step}(t) = \mathsf{rightComb}(t.\mathsf{size})\): every tree is mapped to its right-comb normal form in one step, and applying the step again does nothing because a right-comb is already in normal form.

The institutional closure pipeline composes four layers:

1. Temporal normalization — linearize the event timeline via \(\mathsf{LogicContraction\ Temporal\ =\ contracts\_ to}\).

2. Fuzzy grading — evaluate each event’s impact through graded membership (Sorites-like gradation).

3. Deontic update — revise norms from accumulated blame, using \(\mathsf{LogicContraction\ Deontic}\).

4. Self-recognition — the monadic bind that identifies the output norm as the institution’s own (fixed point).

The pipeline is a monadic computation \(\mathsf{LogicM\ Event \to LogicM\ Norm}\) using the shared \(\mathsf{LogicM}\) backbone, with logic-specific normalization at each layer.

The mirror image of \(\mathsf{rightComb}\): \(\mathsf{leftComb}(0) = \mathsf{Leaf}\) and \(\mathsf{leftComb}(n+1) = \mathsf{Node}(\mathsf{leftComb}(n),\ \mathsf{Leaf})\). Unlike \(\mathsf{rightComb}\), this is not the equilibrium attractor — it represents a fully left-associative configuration.

The cost \(\Phi (\text{Liar}, \text{lt})\) to resolve the Liar under logic lt. Conjectured to equal the Cayley–Dickson step.

The Liar Paradox stated as a Problem of class \(\mathsf{selfReference}\). Its tree is the size-3 symmetric tree \(\mathsf{Node}(\mathsf{Node}(\mathsf{Leaf},\ \mathsf{Leaf}),\ \mathsf{Node}(\mathsf{Leaf},\ \mathsf{Leaf}))\) for most logics, except ManyValued which uses a size-2 left-comb encoding the three-valued disjunction \(\mathsf{True} \lor \mathsf{False} \lor \mathsf{Undefined}\). All logics target \(\mathsf{rightComb}(3)\) as the normal form.

A four-layer prototype tower alternating Classical and Fuzzy wrappers. Demonstrates the stacked collapse pattern; the full tower with Quantum, Intuitionistic, Fuzzy, and Classical layers is not yet populated because non-Classical LogicContractions are missing.

For any logic lt, constructs the WrappedProblem with \(\textsf{cost} = \textsf{liarCost}(\text{lt})\). Fills all 12 mail slots.

The free monad over binary trees: \(\mathsf{LogicM}\ \alpha \) is a tree whose leaves carry values of type \(\alpha \) and whose internal nodes represent non-associative composition of computations.

• \(\mathsf{pure}\ a\) = a leaf containing \(a\) (a completed computation)

• \(\mathsf{node}\ l\ r\) = deferred composition of two sub-computations

• \(\mathsf{bind}\) = substitution: replace every leaf with a new tree

This is self-contained by definition (recursive structure IS self-reference) and extensible (interpreters fold over \(\mathsf{LogicM}\ \alpha \) to produce any target monad).

A LogicPipeline is a sequence of logic types to run as gates. Running it on a tree produces a Decision tagged with all of them. The institutional closure is a pipeline with gates Temporal, Fuzzy, Deontic.

For each logic type \(\mathsf{lt}\), the \(\mathsf{LogicMonad}\ \mathsf{lt}\ \alpha \) structure wraps a \(\mathsf{LogicM}\ \alpha \) and normalizes it via \(\mathsf{LogicContraction}\ \mathsf{lt}\). The normalization cost is \(\mathsf{cdStep}\ \mathsf{lt}\).

This is the minimal monad for each logic: it does the least work (pure substitution) and then normalizes using that logic’s contraction dynamics. The self-reference property of the free monad (bind = substitution) means every logic monad shares the same core recursion — they differ only in how they normalize.

The pluralistic logic monad transcends identity: the monad structure (pure, bind, the laws) is invariant under change of logic. Only the normalization differs. This means the “eternal” layer (pure functional composition) is common to all logics; the “endless” layer (iteration, normalization cost) is what distinguishes them.

Classification of logic types as Substructural, Extension, Alternative, Generalization, or Classical.

A type family of contraction relations indexed by LogicType. For Classical logic this is the Tamari contraction from EMLRegistry.

The normal form for each logic type. For Classical logic this is rightComb.

A type family assigning EML trees to each logic type. Currently uniform; extensible to logic-specific tree types.

An inductive type enumerating 13 reasoning paradigms.

Each handles specific classes of paradoxes as boundary conditions rather than errors.

Cross-logic contraction allowing reasoning that spans multiple logic types via intra-logic contraction, inter-logic translation, and transitivity.

A Problem of class \(\mathsf{metaParadox}\) constructed from any existing Problem and LogicType whose proof is missing.

A witness of a contraction path through the Tamari lattice: \(\mathsf{Path}\ s\ t\) is an inductive sequence of \(\mathsf{contracts\_ one}\) steps from \(s\) to \(t\).

• \(\mathsf{nil}\) — the trivial path (reflexivity).

• \(\mathsf{cons}\ h\_ one\ p\) — prepend a single contraction step to an existing path.

Concatenates two compatible paths: \(\mathsf{append} : \mathsf{Path}\ s\ t \to \mathsf{Path}\ t\ u \to \mathsf{Path}\ s\ u\).

The number of contraction steps in a path: \(\mathsf{length}(\mathsf{nil}) = 0\), \(\mathsf{length}(\mathsf{cons}\ h\_ one\ p) = 1 + \mathsf{length}(p)\).

The immediate predecessor sources of a target tree \(\mathsf{predecessors}(t) = \mathsf{reverse\_ one}(t)\). Soundness is maintained as a separate theorem \(\mathsf{predecessors\_ sound}\): if \(s \in \mathsf{predecessors}(t)\) then \(\mathsf{contracts\_ one}\ s\ t\).

A structure parameterized by a problem class, a name, a list of suitable logics, a tree family \(\mathsf{LogicType} \to \mathsf{EMLTree}\) (the paradox as encoded in each logic), and a normal form family \(\mathsf{LogicType} \to \mathsf{EMLTree}\) (the resolution target for each logic).

An inductive type enumerating 12 paradox classes, each with a native logic type: self-reference (ManyValued), vagueness (Fuzzy), inconsistent definition (Paraconsistent), temporal decision (Temporal), deontic (Deontic), epistemic (Epistemic), quantum superposition (Quantum), constructive (Intuitionistic), relevance (Relevance), empty reference (Free), infinity (Infinitary), modality (Modal).

An injective mapping from router indices to EML trees. This is the cortex-registry interface where neural computation meets formal grammar.

Generates all immediate predecessors of a tree under \(\mathsf{contracts\_ one}\). For a target tree \(t\), \(\mathsf{reverse\_ one}(t)\) is a list of all \(s\) such that \(s \to t\) in one step. Three structural cases:

• \(\mathsf{Leaf}\) has no predecessors.

• \(\mathsf{Node}\ l\ (\mathsf{Node}\ r_1\ r_2)\): the rotation target plus predecessors from reversing the left and right subtrees.

• \(\mathsf{Node}\ l\ r\) (right child not a Node): predecessors from reversing the left and right subtrees only.

This is the core de-composition primitive: given an outcome, what could have immediately preceded it?

The minimum element of the Tamari lattice — the equilibrium attractor. Defined as \(\mathsf{rightComb}(0) = \mathsf{Leaf}\) and \(\mathsf{rightComb}(n+1) = \mathsf{Node}(\mathsf{Leaf},\ \mathsf{rightComb}(n))\).

A bounded natural number \(\mathsf{Fin}(n)\) serving as a neural binding address.

The cost \(\Phi (\text{Russell}, \text{lt})\), equal to \(\textsf{cdStep}(\text{lt})\).

Russell’s Paradox stated as a Problem of class \(\mathsf{inconsistentDef}\). Its tree is a left-comb chain of size 3, encoding the three levels of set-theoretic diagonalization: elements \(\to \) self-membership predicate \(\to \) the set of all sets not containing themselves. The normal form is \(\mathsf{rightComb}(3)\).

Disclaimer: This formalization is deliberately incomplete with respect to the infinity/eternity axis. The “cheat” of setting cost \(= \textsf{cdStep}\) captures only the Cayley–Dickson property-loss dimension, not the regularization dimension (endless \(\to \) eternity \(\to \) actual \(\infty \to \) boundlessness). Future work must pin this axis down properly; here we procrastinate it using the same wrapper pattern as Liar/Sorites/Grandfather.

The Russell tower: one layer per suitable logic.

For any logic lt, constructs the WrappedProblem with \(\textsf{cost} = \textsf{cdStep}(\textsf{lt})\). Resolves set-theoretic diagonalization via \(\mathsf{contracts\_ to\_ rightComb}\).

The number of internal nodes in a tree, used as the lattice index \(n\) in \(T_n\).

The cost \(\Phi (\text{Sorites}, \text{lt})\), equal to \(\textsf{cdStep}(\text{lt})\).

The Sorites (Heap) Paradox stated as a Problem of class \(\mathsf{vagueness}\). Its tree is a left-comb chain of size 5, encoding the inductive threshold: “If \(n\) grains form a heap, then \(n-1\) grains form a heap.” The normal form is \(\mathsf{rightComb}(5)\).

The Sorites tower: one layer per suitable logic, analogous to the Liar tower.

For any logic lt, constructs the WrappedProblem with \(\textsf{cost} = \textsf{cdStep}(\textsf{lt})\). Follows the same pattern as the generic Liar wrapper, using \(\mathsf{contracts\_ to\_ rightComb}\).

Divides logic types into associative and non-associative sectors of the split-octonion algebra.

A sequence of logic-wrapped problems, each collapsing the previous layer’s output. Implements the nested wrapper pattern from Lumo section B:

Each layer’s logic type is tracked via a dependent pair \(\Sigma lt,\ \mathsf{WrappedProblem}\ p\ lt\). The total cost is the sum of per-layer costs.

A structure specifying forward and backward maps between logic types with soundness and completeness proofs.

The Very Big Box is the product of idempotent resolutions over all populated problem classes:

The canonical veryBigBox assigns rightCombResolution to each coordinate.

A \(\mathsf{viewDFS}\) is a single lineage (DFS) extracted from the ancestor space by always following the first predecessor. Returns a \(\mathsf{Chain}\) that may end at any depth. This is the narrative self in formal type: committed to a single thread, but honest about termination.

The WfCA collapse rule: pairs a Problem with a LogicType. Records the tree (problem as interpreted in this logic), target (normal form), cost (pentagonator distance \(\Phi \)), and proof (contraction path). A problem’s superposition of possible resolutions collapses to the definite outcome given by the logic type’s contraction rule.

If \(t \to t'\) then \(\mathsf{Node}(t,\ r) \to \mathsf{Node}(t',\ r)\). Choice resolution in the left subtree propagates to the whole composition.

If \(r \to r'\) then \(\mathsf{Node}(l,\ r) \to \mathsf{Node}(l,\ r')\). Choice resolution in the right subtree propagates to the whole composition.

For any \(a, b : \mathbb {N}\),

The equilibrium attractor is closed under non-associative composition.

Contraction paths preserve tree size, establishing that the Tamari lattice \(T_n\) is graded by node count \(n\).

Rotation rewrites the tree depth but does not change the number of internal nodes.

If \(s \to t\) and \(t \to u\) then \(s \to u\). Audit trails concatenate monotonically.

\(\mathsf{selfRecognize} \circ \mathsf{closure} = \mathsf{closure}\): self-recognition is a fixed point. Once the pipeline has produced a norm, further recognition does not change it.

For any tree \(t : \mathsf{EMLTree}\),

Every configuration has a valid evolution path to the equilibrium attractor indexed by its size.

\(\mathsf{decide}\) runs the institutional closure on \(\mathsf{LogicM\ Event}\) and produces a Decision whose datum passes all closure gates. The channel is the type: \(\mathsf{Decision\ (closurePipeline.gates)}\).

\(\textsf{grandfatherCost}(\text{lt}) \le \textsf{cdStep}(\text{lt})\) for every logic type.

\(\mathsf{size}(\mathsf{leftComb}\ n) = n\).

\(\textsf{liarCost}(\text{lt}) \le \textsf{cdStep}(\text{lt})\) for every logic type. For Classical and Fuzzy the bound is tight (equality).

For any logic type \(lt\) and tree \(t\), \(\mathsf{LogicContraction}\ lt\ t\ (\mathsf{LogicNormalForm}\ lt\ t.\mathsf{size})\). Proven for all 13 logic types via \(\mathsf{contracts\_ to\_ rightComb}\).

The free monad \(\mathsf{LogicM}\) satisfies the three monad laws:

• \(\mathsf{pure}\ a \gg \! \! = f = f a\) (left identity)

• \(m \gg \! \! = \mathsf{pure} = m\) (right identity)

• \((m \gg \! \! = f) \gg \! \! = g = m \gg \! \! = (\lambda x.\ f x \gg \! \! = g)\) (associativity)

Proof by structural induction on the tree.

The forgetful functor from \(\mathsf{LogicMonad}\ \mathsf{lt}\) to \(\mathsf{LogicM}\) is an isomorphism of monads for any \(\mathsf{lt}\). Only the normalization (LogicContraction) changes between logics.

For \(n \ge 2\), the target \(\mathsf{rightComb}\ n\) has at least two distinct Decompositions with different sources:

This is the core ontological result: the past is underdetermined by the present. The same outcome (rightComb \(n\)) admits multiple evidential histories (rightComb \(n\) itself and leftComb \(n\), among others).

\(\mathsf{closure} \circ \mathsf{temporalNormalize} = \mathsf{closure}\): the normalization pipeline is a projection. Re-processing an already- normalized history yields the same norm.

There exist two distinct paths between the same source-target pair in \(T_3\):

Explicitly, \(\mathsf{leftComb}\ 3 \to \mathsf{rightComb}\ 3\) has two distinct maximal chains in the Tamari lattice:

• \(((ab)c)d \to (a(bc))d \to a((bc)d) \to a(b(cd))\) (3 steps)

• \(((ab)c)d \to (ab)(cd) \to a(b(cd))\) (2 steps)

This proves that intent is not uniquely determined by outcome — multiple reasoning chains can connect the same evidence to the same verdict.

For any path \(p : \mathsf{Path}\ s\ t\), we have \(\mathsf{contracts\_ to}\ s\ t\). The path provides constructive evidence for the existence of a contraction sequence.

For any tree and any gate in the closure pipeline, \(\mathsf{soundness}\) guarantees the gate check holds. This is the compile-time contract: the type signature IS the channel.

If \(\mathsf{contracts\_ one}\ s\ t\) then \(s \in \mathsf{reverse\_ one}(t)\). Every valid immediate predecessor is generated.

If \(s \in \mathsf{reverse\_ one}(t)\) then \(\mathsf{contracts\_ one}\ s\ t\). Every generated predecessor is a valid immediate prior configuration.

Applying rightComb normal form to a tree that is already a rightComb is the identity:

Boundlessness is not a structure we build, but a property we recognize.

The step function of rightCombResolution is already its own fixed point:

This is the terminal regularization: applying boundary-response again changes nothing. Not because there is nothing more to say, but because saying more is already captured by the first application.

For \(n \ge 2\), \(\mathsf{rightComb}\ n \neq \mathsf{leftComb}\ n\). The two canonical trees of size \(n\) are distinct in the Tamari lattice.

\(\mathsf{size}(\mathsf{rightComb}\ n) = n\).

\(\mathsf{size}(\mathsf{rightComb}\ n) = n\) for all \(n : \mathbb {N}\).

\(\textsf{russellsCost}(\text{lt}) \le \textsf{cdStep}(\text{lt})\) for every logic type.

\(\textsf{soritesCost}(\text{lt}) \le \textsf{cdStep}(\text{lt})\) for every logic type.