Mac Lane coherence verification (pentagon, triangle, hexagon), Joyal-Street-Verity traced monoidal axioms, feedback analysis, symmetric structure.
check_coherenceVerify Mac Lane coherence for a monoidal structure. Checks the pentagon identity (associator consistency for four-fold tensors), triangle identity (unit coherence), and hexagon identity (braiding cohe...
trace_computationModel bounded iteration via the categorical trace operator Tr(f). Given a function description and initial input, simulate the trace by iterating f with feedback for a bounded number of steps (fuel). ...
verify_traced_axiomsCheck the Joyal-Street-Verity axioms for a traced monoidal category: vanishing (trace of identity on I is identity), yanking (trace of the braid is identity), sliding (pre/post-composition slides thro...
feedback_analysisAnalyze a computation graph with feedback loops. Identifies all feedback cycles, computes trace depth (nesting of feedback), and checks for convergence via contractive mapping analysis. Returns cycle ...
symmetric_structureVerify symmetric monoidal category structure. Checks that the braiding is an involution (swap . swap = identity), naturality holds (braiding commutes with morphisms), and classifies the structure as s...
thm_pentagonThe pentagon identity for the fork/race/fold monoidal category: for four objects A,B,C,D, the two associator paths from `((A×B)×C)×D` to `A×(B×(C×D))` are equal. This is the first generator of Mac Lan...
thm_triangleThe triangle identity: the path `(A×I)×B → A×(I×B) → A×B` via associator + left unitor equals the direct right unitor path. Second generator of Mac Lane coherence. [LEDGER: THM-TRIANGLE]
thm_hexagonThe hexagon identity for braiding: two paths from `(A×B)×C` to `B×(A×C)` via associator + braiding agree. Third generator of symmetric monoidal coherence. [LEDGER: THM-HEXAGON]
thm_monoidal_categoryBundle: `GHom` with `gcomp`, `tensorHom`, `PUnit`, associators, unitors forms a monoidal category. All structural roundtrips (associator, unitor) are identity, pentagon and triangle hold. [LEDGER: THM...
thm_symmetric_monoidalAdding `braid` to the monoidal category makes it symmetric monoidal. Braid is involutive and satisfies the hexagon identity. [LEDGER: THM-SYMMETRIC-MONOIDAL]
thm_coherenceMac Lane coherence: every well-typed diagram of structural morphisms in the fork/race/fold category commutes. Follows from pentagon + triangle + hexagon generators by Mac Lane's coherence theorem (196...
thm_trace_vanishingTrace vanishing: when feedback type is monoidal unit PUnit, the trace reduces to the function itself. Trivial feedback disappears: `Tr_I(f) = f`. [LEDGER: THM-TRACE-VANISHING]
thm_trace_yankingTrace yanking: `Tr(braid) = id`. The trace of the swap morphism is identity — pulling a straight string through a loop leaves it straight. Uses `braid_involutive` from MonoidalCoherence. [LEDGER: THM-...
thm_trace_slidingTrace sliding: `Tr(f ∘ (id⊗g)) = Tr((id⊗g) ∘ f)`. Sliding a morphism around the feedback loop preserves the trace. Naturality of the feedback wire (Joyal-Street-Verity, 1996). [LEDGER: THM-TRACE-SLIDI...
thm_trace_superposingTrace superposing: `Tr(f) ⊗ g = Tr(f ⊗ g)`. Feedback on one component does not interfere with parallel computation. [LEDGER: THM-TRACE-SUPERPOSING]
thm_traced_monoidalBundle: the fork/race/fold category with trace satisfies all Joyal-Street-Verity axioms (vanishing, yanking, sliding, superposing). Extends the symmetric monoidal category to a traced monoidal categor...
thm_trace_iterationThe trace operator models bounded iteration: `Tr(f)(a)` produces the same result as `traceIter(f, a, fuel)` for any fuel. Connects the categorical trace to computational iteration. [LEDGER: THM-TRACE-...
thm_insufficient_dataWhen the deficit is positive (Bule > 0), the answer is not yet computable. "INSUFFICIENT DATA FOR MEANINGFUL ANSWER" is the state where more rejections are needed before convergence. Deficit positive ...
thm_data_accumulatesThe deficit decreases monotonically as data accumulates. Each observation round reduces the deficit. The deficit never increases. Delegates to `future_deficit_monotone [LEDGER: THM-DATA-ACCUMULATES]
thm_answer_eventually_computableAfter exactly d rounds (the initial deficit), the deficit reaches zero. The complement distribution has converged. The answer is computable. Multivac's final moment. Delegates to `future_deficit_event...
thm_heat_death_maximum_voidAt maximum void (every choice rejected every round), every choice has weight exactly 1. Heat death is the state where the void boundary is full. Delegates to `buleyean_min_uncertainty [LEDGER: THM-HEA...
thm_sliver_survives_heat_deathEven at maximum void (heat death), every choice retains weight >= 1. The sliver is irreducible: no choice can reach weight zero. The +1 in the weight formula is structural. Delegates to `buleyean_posi...
thm_let_there_be_lightA converged complement distribution (Bule = 0) is a valid Bayesian prior for a new Buleyean space. Different rejection counts produce different weights. The prior is informative, not uniform. The conv...
thm_entropy_reversalThe void boundary grows monotonically (entropy increases). The complement distribution concentrates monotonically (entropy decreases). Non-rejected choices gain weight after each rejection round. Entr...
thm_no_data_no_answerA system with zero observations (empty void boundary) produces uniform weights -- maximum entropy, zero information, no meaningful answer. Delegates to `fold_without_evidence_is_coinflip [LEDGER: THM-...
thm_trajectory_deterministicThe entire future trajectory of the deficit is known: futureDeficit d k = d - min(k, d). No randomness, no breakthroughs. The convergence round is d. Delegates to `future_deficit_deterministic [LEDGER...
thm_last_questionComplete Last Question theorem: deficit monotonically decreasing, answer eventually computable at round d, every choice survives heat death (weight >= 1), no choice reaches zero, no data means no answ...
thm_utm_universal_forkThe Universal Turing Machine is the maximally general fork: totalPrograms = haltingPrograms + nonHalting. Every computable process is a path in the universal fork. Execution partitions programs into h...
thm_execution_is_foldProgram execution is a fold operation: haltingPrograms + nonHalting = totalPrograms. Every program goes to exactly one set. The fold is total: no program escapes classification [LEDGER: THM-EXECUTION-...
thm_halting_survivors_boundedThe number of halting programs is strictly less than the total. Not every program halts. The void of non-termination is nonempty [LEDGER: THM-HALTING-SURVIVORS-BOUNDED]
thm_omega_positivityThe halting probability is positive: at least one program halts. Omega > 0. The void boundary of program space does not absorb everything [LEDGER: THM-OMEGA-POSITIVITY]
thm_omega_strict_subuniversalityOmega < 1: not every program halts. The fold is nontrivial -- it vents at least one path. The non-halting void is nonempty [LEDGER: THM-OMEGA-STRICT-SUBUNIVERSALITY]
thm_finite_approximation_monotoneExtending the program enumeration can only increase (or maintain) the halting count. The finite approximation to Omega is monotonically non-decreasing as more programs are enumerated [LEDGER: THM-FINI...
thm_omega_approximation_boundedAny finite prefix of the enumeration undercounts (or exactly counts) the true halting set. The finite Omega is a lower bound on the limit [LEDGER: THM-OMEGA-APPROXIMATION-BOUNDED]
thm_halting_as_fold_deficitThe number of non-halting programs is the fold deficit: the topological cost of execution. Analogous to classicalDeficit in quantum search and protocolTopologicalDeficit in transport multiplexing [LED...
thm_omega_is_buleyean_complementOmega (the halting probability) corresponds to the Buleyean complement weight of the halting set. Programs that halt have low rejection count (survived). Programs that don't halt have high rejection c...
thm_chaitin_solomonoff_bridgeChaitin's Omega and Solomonoff's Universal Prior share the same void boundary structure. Both partition the same program space. Both are strictly between 0 and 1. The non-halting deficit is positive. ...
thm_uncomputability_is_infinite_voidThe uncomputability of Omega is the statement that the void boundary of all programs is not finitely constructible. The finite approximation is monotone, bounded, and positive at every stage. Buleyean...
thm_chaitin_omega_masterComplete Chaitin-Omega theorem: UTM is universal fork, execution is fold, halting is bounded, Omega is positive, Omega is subuniversal, void is nonempty, Chaitin-Solomonoff bridge holds. Chaitin's Ome...
thm_arrow_from_trilemmaArrow's impossibility theorem follows from the failure trilemma [LEDGER: THM-ARROW-FROM-TRILEMMA]
thm_arrow_any_twoAny two of three social choice desiderata, but not three [LEDGER: THM-ARROW-ANY-TWO]
thm_godel_buleyean_positivityGodel incompleteness as Buleyean positivity: unprovable statements are the void boundary [LEDGER: THM-GODEL-BULEYEAN-POSITIVITY]
thm_godel_void_nonemptyGodel: void nonempty or inconsistent [LEDGER: THM-GODEL-VOID-NONEMPTY]
thm_chaitin_void_limitChaitin omega as the void limit [LEDGER: THM-CHAITIN-VOID-LIMIT]
thm_consciousness_void_relativityConsciousness as internal zero-deficit perspective on irreversibility [LEDGER: THM-CONSCIOUSNESS-VOID-RELATIVITY]
thm_qualia_complementsQualia are complement distributions [LEDGER: THM-QUALIA-COMPLEMENTS]
thm_thermo_traced_monoidalTraced monoidal semantics coupled to thermodynamics: trace = coarsening (projection away feedback component), non-trivial feedback generates strictly positive Landauer heat, iterated traces increase c...
From "Being Irreversible" by Taylor William Buley.
LEDGER sections: Monoidal Coherence & Traced Structure
Read the paper at Wallington Lab