.. _e7he-overview-expert:

****************************************************
e7He --- Overview for Experts
****************************************************

e7He is a coinductive model of moral development, formalized as a
perpetual hero journey through seven stages. The model encodes three
fundamental epistemic distortions --- oversimplification (BA),
overcomplication (ASH), and overreach (MOL) --- as bits in a 3-bit
binary word. The seven stages correspond to the seven non-zero
elements of {0,1}^3, visited in counting order (001 through 111).
The resulting structure proposes a combinatorially complete
inoculation protocol: a hero who traverses all seven stages has
faced every non-trivial BA-ASH-MOL combination exactly once.

The model sits atop two inherited systems: PET (a modal-mereological
theology) and JUB (a Jubilee-cycle socioeconomic extension of PET).
e7He adds coalgebraic structure, dynamical systems formalism, and
game-theoretic mechanism design to model the individual agent's
journey within the PET/JUB framework.

This overview is written for readers with graduate-level familiarity
in formal logic, dynamical systems, or game theory. For an accessible
introduction, see :doc:`overview-beginner`.


1. Axiomatic Summary
======================

14 axioms in two groups. The 7 prerequisite axioms (m0) define the
framework; the 7 stage axioms (m1--m7) define the journey segments.
Each axiom below uses BEST Names (see :doc:`symbols`). Full
definitions with math blocks are in :ref:`e7he-axioms`.

**m0 Prerequisites:**

- **m0.ax1 (Uniqueness):**
  :math:`\forall h: \text{profile}(h) \text{ unique}`

- **m0.ax2 (FATE):**
  :math:`\text{FATE}(h, t_0^k) = \text{state}(h, t_0^k)`; hero
  journey requires :math:`\text{accepts}(h, \text{FATE})`

- **m0.ax3 (GOAL):**
  :math:`\forall h: \exists\,\text{GOAL}(h) \in D_{\text{inno}}`
  with positive entropy; pursuing GOAL contributes positively to
  :math:`d\,\text{Ie}_W/dt` and is locally optimal for h's
  comparative advantage

- **m0.ax4 (Cycle):**
  :math:`\text{FATE} \xrightarrow{s_1 \ldots s_7} \text{DESTINY}`;
  DESTINY provisional

- **m0.ax5 (Reset):**
  :math:`\text{FATE}(k{+}1) := \text{DESTINY}(k) \oplus \text{rest}(k)`;
  self-assessment = NOT-OK

- **m0.ax6 (Irrelevance):**
  :math:`\text{stops} \wedge \text{low influence} \rightarrow
  \text{Ie stagnates}`

- **m0.ax7 (Supervillain):**
  :math:`\text{stops} \wedge \text{high influence} \rightarrow
  \text{scope stagnates, friendly-fire}`

**Stage axioms (m1--m7):**

Each stage axiom has the general form
:math:`\text{step}(\mu_{k-1}) = (\mathcal{J}_k, \mu_k)` where the
journey segment :math:`\mathcal{J}_k` carries a BABL pattern
:math:`b(m_k) = k` in binary. The stage axioms, with their BABL
encodings, are:

- **m1 (ACD -- 001 = BA):** accepts complexity, commits to journey
- **m2 (TTT -- 010 = ASH):** skills increase, endurance tested
- **m3 (GAT -- 011 = ASH+BA):** holds advantage, not captured by it
- **m4 (MYM -- 100 = MOL):** midpoint bifurcation; false-self-died
  (ZION) or CWA adopted (BABL)
- **m5 (LUC -- 101 = MOL+BA):** received without entitlement, shared
  without grasping
- **m6 (RES -- 110 = MOL+ASH):** gift alive in others' hands, no
  institutional capture
- **m7 (FRE -- 111 = MOL+ASH+BA):** full BABL resisted, rest, open
  to next call (ZION); or insights weaponized, Machiavelli-Prince
  (BABL)


2. Theorem Summary
=====================

7 theorems with a dependency graph. Full statements are in
:ref:`e7he-theorems`.

**th1 (Anti-BABL Inoculation Completeness):**
:math:`\text{completes-cycle}(h) \rightarrow \forall b \in
\mathcal{B} \setminus \{000\}: \text{babl-resisted}(h, m_k)`.
Follows directly from the binary counting encoding: stages 1--7
exhaust :math:`\mathcal{B} \setminus \{000\}`. Depends on sp1.

**th2 (Supervillain Theorem):**
Stopping on the ridge with high influence leads to BABL drift.
The ridge is conditionally stable: GOAL pursuit supplies directional
force; removing it exposes perpendicular OSCR instabilities. Needs
full Lyapunov formalization (deferred; sketch uses
:math:`V(h,t) = -\text{Ie} + \lambda \cdot \text{OSCR\_exposure}`).
Structural theorem.

**th3 (Scope Expansion / Anti-Livelock):**
:math:`\text{completes-cycle} \wedge \text{babl-resisted} \wedge
\text{rest-adequate} \wedge \text{goal-pursued} \rightarrow
\text{Ie}(t_f^k) > \text{Ie}(t_0^k)`.
Integral form:
:math:`\int_{t_0^k}^{t_f^k} (I_{\text{pursuit}} +
I_{\text{serendipity}} - I_{\text{decay}})\,dt > 0`.
Condition-to-term mapping: goal-pursued maps to
:math:`I_{\text{pursuit}} > 0` (from m0.ax3); babl-resisted maps
to :math:`I_{\text{serendipity}} \geq 0` (serendipity channel open);
rest-adequate maps to :math:`I_{\text{decay}}` bounded
(consolidation controls decay). Derivable from th1 + m0.ax3 + m7.

**th4 (Coinductive Productivity):**
The coalgebra is productive: every milestone produces a non-trivial
journey segment and a next milestone. The process never terminates.
Follows from m0.ax5 (perpetual reset). Rest is a journey segment
with outgoing transitions, not a terminal state.

**th5 (Bifurcation Asymmetry):**
:math:`P(\text{BABL self-destructs} \mid t \to \infty) = 1`; ZION
can replace BABL if :math:`\exists\,h^*` with
:math:`\text{sufficiently-convincing-case}(h^*)`. CTMC argument
with absorbing state for BABL self-destruction. Structural theorem.

**th6 (Commitment Trichotomy / Frying Pan Theorem):**
Three cases partition the h* commitment space:

- *Case 1 (No Volunteer):*
  :math:`\neg\exists\,h: \text{irrevocable-NOT-OK}(h) \rightarrow
  \text{game}(H) = \text{PD} \rightarrow \text{OK dominant}
  \rightarrow \text{BABL}`
- *Case 2 (Dishonest Volunteer):*
  :math:`\text{claims-irrevocable-NOT-OK}(h') \wedge
  \neg\text{genuine}(h') \rightarrow \text{transparency-test}`:
  HELD (fraud detected, system strengthened) or BREACH (fraud
  undetected, maximum damage)
- *Case 3 (Genuine Volunteer):*
  :math:`\text{genuine-NOT-OK}(h^*) \wedge
  \text{irrevocable}(\text{commitment}) \wedge
  \text{transparent}(h^*) \rightarrow \text{game}(H) =
  \text{Assurance} \wedge (\text{NOT-OK}, \text{Cooperate}) =
  \text{Nash eq.}`

Derives from Schelling (1960) commitment theory + Spence (1973)
signaling. Irrevocable NOT-OK eliminates OK from h*'s strategy set;
transparency makes commitment assessable; PD transforms to
Assurance Game. Depends on m0.ax5 (NOT-OK reset).

**th7 (Succession Robustness / Mortality Theorem):**
The system survives h*'s death iff h*'s contribution has been
externalized into personnel-independent infrastructure: (a) documented
transparency requirements, (b) published mathematical theory,
(c) demonstrated precedent, (d) testing protocol for successors.
Depends on th6 (Commitment Trichotomy).

**Dependency graph:**

::

  sp1 --> th1 --> th3 <-- m0.ax3, m7
  m0.ax5 --> th4
  m0.ax5 --> th6 --> th7
  th2: structural (needs Lyapunov)
  th5: structural (needs CTMC)


3. Structural Properties
==========================

Three structural properties underpin the axioms and theorems. See
:ref:`e7he-sp1`, :ref:`e7he-sp2`, :ref:`e7he-sp3`.

**sp1 (Binary Completeness):**
The encoding :math:`b(m_k) = k` in binary is a bijection
:math:`\{m_1, \ldots, m_7\} \to \mathcal{B} \setminus \{000\}`.
This is the unique standard ordering that satisfies three criteria:
(i) Hamming-3 midpoint at m3-to-m4 (sp2); (ii) progressive BABL
escalation (BA/ASH only in stages 1--3, MOL introduced at stage 4);
(iii) minimal description length (counting from 1 with no arbitrary
permutation). Gray code would distribute bit-flips uniformly across
transitions but would not produce the Hamming-3 midpoint
concentration.

**sp2 (Midpoint Maximality):**
The transition :math:`m_3 \to m_4` (011 to 100) has Hamming
distance 3 --- all bits flip. This is the maximal Hamming distance
between consecutive stages in counting order. It marks the
qualitative shift from pre-MOL (stages 1--3) to MOL-inclusive
(stages 4--7). The departure from m3 to m4 does not feel radical
from inside the journey: by stage 4, accumulated BA and ASH
normalization makes MOL's overreach seem like a small step.

**sp3 (Lognormal Influence Distribution):**
:math:`|\text{bif}(h,s,t)| \sim \text{Lognormal}(\mu,\sigma)`.
This is the null hypothesis for multiplicative influence systems
(central limit theorem applied to products). Most agents contribute
small effects; few contribute large effects; h* contributes the
maximal effect. The lognormal assumption is motivated by standard
statistical theory for multiplicative systems but has not been
empirically tested against h* influence distributions.


4. Formal Disciplines
=======================

e7He draws on multiple formal disciplines. The base logic is
inherited; the extensions are model-specific. All 12 WisdomBase
disciplines were loaded during the TEMPER rounds. See
:doc:`logics` for the full mapping.

**Inherited from PET/JUB:**

- S5 modal logic (necessity/possibility with equivalence-class
  accessibility)
- Classical Extensional Mereology (part-whole, God-World containment)
- First-order predicate calculus (quantification over agents, cycles,
  stages, time)

**Added by e7He:**

- *Coalgebra and coinduction* --- th4 (step function productivity),
  perpetual-cycle formalization, bisimulation for journey equivalence
- *Dynamical systems theory* --- th2 (ridge conditional stability,
  Lyapunov sketch), th3 (Ie evolution equation), th5 (attractor
  analysis)
- *Game theory and mechanism design* --- th6 (Schelling commitment,
  Spence signaling, PD-to-Assurance transformation, Nash equilibrium
  at (NOT-OK, Cooperate))
- *Information theory* --- m0.ax3 (entropy condition on GOAL), sp3
  (lognormal influence distribution)
- *Stochastic processes* --- th5 (CTMC with absorbing state for BABL
  self-destruction)

The 10 Iron Maiden tests collectively cover all 12 WisdomBase
disciplines, ensuring that each formal claim is subjected to the
relevant discipline's standard of rigor during adversarial review.


5. Known Weaknesses and Open Problems
========================================

The following gaps are acknowledged and tracked in the model's AA
(Any Aims) register.

**Lyapunov formalization gap (th2).**
The ridge-stability argument rests on a Lyapunov-like function
:math:`V(h,t) = -\text{Ie} + \lambda \cdot \text{OSCR\_exposure}`.
A sketch exists from the FORGE session; a full specification
including basin boundaries, the precise form of the OSCR exposure
term, and conditions under which :math:`\dot{V} < 0` holds remains
outstanding. Without this, th2 is a structural claim with a
plausibility argument, not a derivable theorem.

**CTMC precision gap (th5).**
The claim that BABL self-destructs with probability 1 as
:math:`t \to \infty` uses an absorbing-state CTMC argument. In
practice, BABL regimes are metastable, not truly absorbing: they
can reform after collapse. A quasi-absorbing model (metastable
states with exponentially distributed escape times) would be more
faithful to the dynamics. The qualitative conclusion (BABL regimes
are stochastically self-destructive) likely survives, but the
"probability 1" claim is stronger than the current formalization
warrants.

**Lognormal empirical gap (sp3).**
The lognormal distribution for :math:`|\text{bif}(h,s,t)|` is the
standard null hypothesis for multiplicative systems. It is motivated
but not empirically tested for h* influence distributions. Alternative
heavy-tailed distributions (Pareto, power-law) would produce
qualitatively similar but quantitatively different predictions about
the concentration of influence at the tail.

**Proto-formal predicates.**
Of the 42 specified predicates, approximately 10 remain at the
behavioral-criterion level without full formal semantics. The most
consequential is ``false-self-died`` (#19), which relies on a
negative behavioral test (reversion to BA/ASH patterns under
identity threat). Full operationalization requires empirically
grounded criteria from psychology or behavioral science. This is
tracked as AA-e7He-Predicates-a1.

**th6 + th7 (TEMPER-tested 2026-03-30).**
Both theorems were TEMPER-tested as a pair on 2026-03-30
(dv_ClaOp46Max_OOv1r1). All 10 Iron Maiden tests were applied to
th6, th7, and their interaction. Two KOs were found and repaired:
(1) th6's "irrevocable" was redefined as "effectively irrevocable"
via costly commitment device (Schelling 1960), resolving a
computability concern; (2) th7's "iff (a)-(d)" bootstrap condition
was weakened to monotonic increase, since component (c) is
unavailable at first instantiation. Five OKOs remain open,
documented in the AA register: sincerity semi-decidability,
population-level transition dynamics, cross-generational equilibrium
preservation, multi-h₀ extension, and institutional capture risk.

**Predicate count.**
42 predicates are specified. Some, particularly those governing the
stage axiom milestones (e.g., ``received-without-entitlement``,
``gift-alive-in-others-hands``), remain at behavioral-criterion
granularity. They are assessable by human judgment but not yet
reducible to formal decision procedures.


6. Relationship to Existing Literature
========================================

e7He intersects several established research programs. The model
does not derive from any of them but borrows formalism and, where
indicated, proposes extensions.

**Campbell's monomyth.**
The hero journey stages are structurally parallel to Campbell's
(1949) departure-initiation-return schema. The parallel is
acknowledged but e7He is not derived from Campbell: the binary BABL
encoding and the coinductive perpetual-cycle structure have no
counterpart in the monomyth. Campbell's framework is narrative;
e7He proposes formal testability through the combinatorial
completeness property (sp1).

**Schelling (1960), commitment theory.**
th6 Case 3 uses irrevocable commitment to transform a Prisoner's
Dilemma into an Assurance Game. The mechanism is standard Schelling:
an agent who credibly eliminates a strategy from their own set
changes the game's equilibrium structure. The specific application
--- irrevocable NOT-OK self-assessment as commitment device --- is
novel to e7He.

**Spence (1973), signaling theory.**
th6 Case 3 treats irrevocable NOT-OK as a costly, credible signal.
The cost structure is asymmetric: a genuine agent bears the cost of
perpetual self-scrutiny; a dishonest agent must maintain indefinite
deception under transparency conditions. This asymmetry is the
separating condition.

**Arrow (1951), impossibility theorem.**
m0.ax3 dissolves Arrow's impossibility by operating within a
different framework: local optimality for each agent's comparative
advantage replaces the global total ordering that Arrow's theorem
renders impossible. No social welfare function aggregating all
preferences is required; each agent pursues the GOAL that is locally
optimal given their unique profile (m0.ax1).

**Lyapunov stability theory.**
th2 sketches a Lyapunov-like function for the ridge dynamics: the
hero journey's directional force (GOAL pursuit) supplies conditional
stability, and removing it (stopping) exposes the agent to
perpendicular OSCR instabilities. The connection is structural: a
full Lyapunov proof would require specifying the function's domain,
establishing :math:`\dot{V} < 0` on trajectories, and bounding the
basin of attraction.

**CTMC absorbing states.**
th5 models BABL self-destruction as absorption in a continuous-time
Markov chain. Standard CTMC results guarantee absorption with
probability 1 given irreducibility conditions and at least one
absorbing state. The application to institutional corruption regimes
is novel; the mathematical machinery is not.

**Nash equilibrium.**
th6 Case 3 identifies a unique Pareto-optimal Nash equilibrium at
(NOT-OK, Cooperate) in the Assurance Game. This equilibrium is
subgame perfect under the stated conditions (permanent commitment,
observable behavior) and self-reinforcing (visible cooperation
attracts further cooperation). The equilibrium analysis is standard;
the application to moral self-assessment as a strategic variable is
the model's contribution.


7. Epistemic Status
=====================

All 24 claims (14 axioms, 7 theorems, 3 structural properties)
carry **OOv1** status per the author's assessment. This means:
formulated, extracted from working sessions, and internally checked
for consistency --- but not independently tested by a separate
auditor.

**Testing history:**

- One full FORGE TEMPER cycle: 3 rounds (a1, a2, a3)
- 10 Iron Maiden tests applied to all 24 statements
- The auditor (ClaudeOp46Max) proposed PP (provisionally passed)
  verdicts for 21 of 24 claims; the author holds all at OOv1,
  reflecting the conservative assessment that a single auditor's
  TEMPER round does not yet constitute independent testing
- Dedicated TEMPER round for th6+th7 as a pair (2026-03-30):
  2 KOs found and repaired, 5 OKOs documented. Both theorems
  advanced to OOv1r1.

**What would advance the epistemic status:**

1. *Independent TEMPER round.* A different auditor applying the same
   10 Iron Maiden tests. This is the single most valuable next step.
   The current round used a single AI auditor (ClaudeOp46Max);
   independent human review or a different AI system would provide
   genuine adversarial pressure.

2. *Empirical testing of proto-formal predicates.* Behavioral
   science criteria for the ~10 predicates that currently rely on
   human judgment (especially ``false-self-died``, #19). This
   connects e7He to empirical psychology and makes the model's
   claims about moral development assessable against data.

3. *Formal proofs of derivable theorems.* th1 (Anti-BABL
   Inoculation), th3 (Scope Expansion), and th4 (Coinductive
   Productivity) are claimed to be derivable from the axioms. Writing
   these proofs in a proof assistant (e.g., Agda for the coinductive
   components, Lean for the algebraic components) would either confirm
   the derivations or expose hidden assumptions.

4. *Lyapunov and CTMC formalizations.* th2 and th5 are structural
   theorems with plausibility arguments. Full formalization --- a
   specified Lyapunov function with proven stability conditions for
   th2, and a precise CTMC transition matrix with verified absorption
   properties for th5 --- would either elevate them to derivable
   theorems or reveal that the informal arguments conceal gaps.

The model is a proposal. It proposes structural claims about moral
development, institutional corruption, and the game theory of
transparent commitment. These claims are internally consistent (per
the TEMPER round) and formally expressible (per the axiom/theorem
structure). They are not proven. Treating them as established results
would be precisely the kind of oversimplification (BA) the model
itself identifies as the first and most common epistemic distortion.