R20 — interoceptive tripwires (observes the harness as a whole)
PERCEIVE
BELIEVE
EVALUATE
SELECT
ACT
CTAU-TOKEN → R5: C-τ (absent from the Lean)
R1 → R17: μ (named in the Lean, not imported)
R1 → R3: μ (named in the Lean, not imported)
R1 → R3a: μ (imported in the Lean)
R1 → R4: μ (imported in the Lean)
R13 → CTAU-CLASS: T (one side has no Lean module)
R13 → CTAU-TOKEN: T (imported in the Lean)
R13 → R4: T (imported in the Lean)
R14 → R6: τ (imported in the Lean)
R16 → R1: u (imported in the Lean)
R16 → R2: world (named in the Lean, not imported), u (imported in the Lean)
R17 → R6: E (imported in the Lean)
R17 → SCAN: a-conc (imported in the Lean)
R19 → R5: C (named in the Lean, not imported), U-t (named in the Lean, not imported)
R2 → R1: o (imported in the Lean)
R2 → R17: o (named in the Lean, not imported)
R2 → R3: o (imported in the Lean)
R2 → R3a: o (imported in the Lean)
R2 → R4: interp (imported in the Lean)
R2 → R6: interp (imported in the Lean)
R2 → R7: ref-label (absent from the Lean), o (imported in the Lean)
R2 → R8: o (imported in the Lean)
R2 → SCAN: o (absent from the Lean)
R3 → R1: s-next (imported in the Lean)
R3a → R3: ε (imported in the Lean)
R3a → R7: ε (absent from the Lean)
R4 → R1: A (absent from the Lean), B (absent from the Lean)
R4 → R2: A (absent from the Lean), B (absent from the Lean)
R4 → R3: A (absent from the Lean), B (absent from the Lean)
R4 → R3a: A (absent from the Lean), B (absent from the Lean)
R4 → R5: Q-o-π (absent from the Lean), A (named in the Lean, not imported)
R4 → R7: A (named in the Lean, not imported)
R4 → R8: A (absent from the Lean)
R5 → R6: G (imported in the Lean)
R6 → R16: Q-π (imported in the Lean), π (imported in the Lean)
R6 → R17: π (imported in the Lean)
R6 → R4: r (imported in the Lean), π (imported in the Lean)
R6 → R8: π (imported in the Lean)
R7 → R17: wc (named in the Lean, not imported)
R7 → R3: Π (absent from the Lean)
R7 → R4: rates (imported in the Lean)
R8 → R3: F-π (absent from the Lean)
R8 → R6: F-π (imported in the Lean)
CTAU-CLASS
Class C_tau
CTAU-TOKEN
Token C_tau
R1
Belief state
R13
Temporal policy depth
R14
Commitment temperature
R16
Grounded enactment
R17
Structure learning
R19
Mission preference
R2
Structured observation
R3
Belief update
R3a
Prediction-error projection
R4
Forward model
R5
Expected free energy core
R6
Candidate action space
R7
Evidence-channel precision
R8
Present-fit mismatch
SCAN
Scan observation model
R10
Scheduled entrypoint
R11
Hierarchical shared budget
R12
Two-layer calibration
R15
Hierarchy and timescale
R9
No self-certification
An arrow is a term one node defines and another uses:
imported in the Lean
named in the Lean, not imported
absent from the Lean
no Lean module at this node