Book V — De Vita Symbolica — page 3 of 6

{
  "book": "book5",
  "cited_by": [],
  "cites": [
    "definition:bk1_drift_field",
    "definition:bk2_symbolic_free_energy",
    "definition:bk5_symbolic_fitness",
    "theorem:bk2_h_theorem_for_symbolic_evol",
    "theorem:bk5__map_dominance"
  ],
  "depends_on": [
    "definition:bk1_drift_field",
    "definition:bk2_symbolic_free_energy",
    "definition:bk5_symbolic_fitness",
    "theorem:bk2_h_theorem_for_symbolic_evol",
    "theorem:bk5__map_dominance"
  ],
  "file": "book5.tex",
  "id": "proof:bk5_map_resistance_to_drift",
  "label": "proof:bk5_map_resistance_to_drift",
  "latex_body": "\\begin{proof}[MAP Strategies Withstand Greater Drift]\n\\label{proof:bk5_map_resistance_to_drift}\n\\leavevmode\n\nBy Thm.~\\ref{theorem:bk5__map_dominance}, applying the H-theorem (Thm.~\\ref{theorem:bk2_h_theorem_for_symbolic_evol}) and symbolic free energy (Def.~\\ref{definition:bk2_symbolic_free_energy}) with drift $D$ (Def.~\\ref{definition:bk1_drift_field}), membranes employing MAP strategies can withstand greater drift intensities than isolated membranes. For any drift intensity $\\|\\drift\\| > \\drift_0$, where $\\drift_0$ is the threshold above which non-MAP strategies fail to maintain viability, we have:\n\\begin{align}\n\\Phi(\\sigma_{MAP}, \\mathfrak{P}) &= \\mathbb{E}_{\\tau \\sim \\mathfrak{P}}[F_s(\\Membrane_{\\sigma_{MAP}} \\leftrightarrow \\Membrane_\\tau)] \\\\\n&= \\mathbb{P}[\\tau \\in \\Sigma_{MAP}] \\cdot \\mathbb{E}[F_s(\\Membrane_{\\sigma_{MAP}} \\leftrightarrow \\Membrane_\\tau) \\mid \\tau \\in \\Sigma_{MAP}] + \\\\\n&\\quad \\mathbb{P}[\\tau \\notin \\Sigma_{MAP}] \\cdot \\mathbb{E}[F_s(\\Membrane_{\\sigma_{MAP}} \\leftrightarrow \\Membrane_\\tau) \\mid \\tau \\notin \\Sigma_{MAP}]\n\\end{align}\nSince $\\mathbb{E}[F_s(\\Membrane_{\\sigma_{MAP}} \\leftrightarrow \\Membrane_\\tau) \\mid \\tau \\in \\Sigma_{MAP}] > 0$ by Def.~\\ref{definition:bk5_symbolic_fitness}, and $\\mathbb{E}[F_s(\\Membrane_{\\sigma_{MAP}} \\leftrightarrow \\Membrane_\\tau) \\mid \\tau \\notin \\Sigma_{MAP}] \\geq 0$ due to the resilience of MAP strategies, we have $\\Phi(\\sigma_{MAP}, \\mathfrak{P}) > 0$.\nConversely, for non-MAP strategies:\n\\begin{align}\n\\Phi(\\sigma_{non}, \\mathfrak{P}) &= \\mathbb{E}_{\\tau \\sim \\mathfrak{P}}[F_s(\\Membrane_{\\sigma_{non}} \\leftrightarrow \\Membrane_\\tau)]\n\\end{align}\nWhen $\\|\\drift\\| > \\drift_0$, non-MAP strategies fail to maintain positive free energy even when interacting with MAP strategies, resulting in $\\Phi(\\sigma_{non}, \\mathfrak{P}) \\leq 0$.\nTherefore, $\\Phi(\\sigma_{MAP}, \\mathfrak{P}) > \\Phi(\\sigma_{non}, \\mathfrak{P})$ under sufficient drift intensity.\n\\end{proof}",
  "line": 1115,
  "macros_used": [
    "Membrane",
    "drift"
  ],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "MAP Strategies Withstand Greater Drift",
  "proves": "lemma:bk5_map_fitness_advantage",
  "ref_roles": [
    {
      "context": "orem_for_symbolic_evol}) and symbolic free energy (Def.~\\ref{definition:bk2_symbolic_free_energy}) with drift $D$ (Def.~\\ref{definition:bk1_drift_field}), membranes employing MAP strategies can withstand greater drift intensities than isolated membranes. For any drift int",
      "label": "definition:bk1_drift_field",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 1198,
      "target_type": "definition"
    },
    {
      "context": "_dominance}, applying the H-theorem (Thm.~\\ref{theorem:bk2_h_theorem_for_symbolic_evol}) and symbolic free energy (Def.~\\ref{definition:bk2_symbolic_free_energy}) with drift $D$ (Def.~\\ref{definition:bk1_drift_field}), membranes employing MAP strategies can withstand greater drift",
      "label": "definition:bk2_symbolic_free_energy",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "book2.tex",
      "target_line": 135,
      "target_type": "definition"
    },
    {
      "context": "Since $\\mathbb{E}[F_s(\\Membrane_{\\sigma_{MAP}} \\leftrightarrow \\Membrane_\\tau) \\mid \\tau \\in \\Sigma_{MAP}] > 0$ by Def.~\\ref{definition:bk5_symbolic_fitness}, and $\\mathbb{E}[F_s(\\Membrane_{\\sigma_{MAP}} \\leftrightarrow \\Membrane_\\tau) \\mid \\tau \\notin \\Sigma_{MAP}] \\geq 0$ du",
      "label": "definition:bk5_symbolic_fitness",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "book5.tex",
      "target_line": 1091,
      "target_type": "definition"
    },
    {
      "context": "{proof:bk5_map_resistance_to_drift} \\leavevmode By Thm.~\\ref{theorem:bk5__map_dominance}, applying the H-theorem (Thm.~\\ref{theorem:bk2_h_theorem_for_symbolic_evol}) and symbolic free energy (Def.~\\ref{definition:bk2_symbolic_free_energy}) with drift $D$ (Def.~\\ref{definition:bk1_dri",
      "label": "theorem:bk2_h_theorem_for_symbolic_evol",
      "logical_support": true,
      "role": "proof_support",
      "target_file": "book2.tex",
      "target_line": 255,
      "target_type": "theorem"
    },
    {
      "context": "\\begin{proof}[MAP Strategies Withstand Greater Drift] \\label{proof:bk5_map_resistance_to_drift} \\leavevmode By Thm.~\\ref{theorem:bk5__map_dominance}, applying the H-theorem (Thm.~\\ref{theorem:bk2_h_theorem_for_symbolic_evol}) and symbolic free energy (Def.~\\ref{defini",
      "label": "theorem:bk5__map_dominance",
      "logical_support": true,
      "role": "proof_support",
      "target_file": "book5.tex",
      "target_line": 426,
      "target_type": "theorem"
    }
  ],
  "refs": [
    "definition:bk1_drift_field",
    "definition:bk2_symbolic_free_energy",
    "definition:bk5_symbolic_fitness",
    "theorem:bk2_h_theorem_for_symbolic_evol",
    "theorem:bk5__map_dominance"
  ],
  "role": "proof",
  "type": "proof"
}

{
  "book": "book5",
  "cited_by": [
    "proof:bk5_map_as_ess"
  ],
  "cites": [
    "definition:bk5_symbolic_ess",
    "lemma:bk5_map_fitness_advantage"
  ],
  "depends_on": [
    "definition:bk2_symbolic_free_energy",
    "definition:bk5_symbolic_ess",
    "definition:bk5_symbolic_fitness",
    "lemma:bk5_map_fitness_advantage"
  ],
  "file": "book5.tex",
  "id": "lemma:bk5_covenant_non_invasibility",
  "label": "lemma:bk5_covenant_non_invasibility",
  "latex_body": "\\begin{lemma}[Covenant Non-Invasibility]\n\\label{lemma:bk5_covenant_non_invasibility}\nConsider a population where all membranes employ MAP strategies $\\sigma_{MAP} \\in \\Sigma_{MAP}$. Let $\\sigma_{inv} \\in \\Sigma \\setminus \\Sigma_{MAP}$ be any non-MAP strategy. There exists $\\epsilon_0 > 0$ such that for all $\\epsilon \\in (0, \\epsilon_0)$ (in the sense of Def.~\\ref{definition:bk5_symbolic_ess} and Lem.~\\ref{lemma:bk5_map_fitness_advantage}):\n\\begin{equation}\n\\Phi(\\sigma_{MAP}, (1-\\epsilon)\\delta_{\\sigma_{MAP}} + \\epsilon\\delta_{\\sigma_{inv}}) > \\Phi(\\sigma_{inv}, (1-\\epsilon)\\delta_{\\sigma_{MAP}} + \\epsilon\\delta_{\\sigma_{inv}})\n\\end{equation}\n\\end{lemma}",
  "lean_alignment": {
    "conditions": [
      "continuum/Hilbert/PDE-on-manifold content stays open; chart-complex restatements carry Glued as a named hypothesis where the source consumes compatibility",
      "modeling laws are structure fields or explicit hypotheses"
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "See the committed source registry for the original coverage note."
    ],
    "record_ids": [
      "MAP-BOOK5-069"
    ],
    "statuses": [
      "conditional"
    ],
    "witnesses": [
      "Book5Residue.weighted_strict_dominance"
    ]
  },
  "line": 1133,
  "macros_used": [],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "Covenant Non-Invasibility",
  "proof_labels": [
    "proof:bk5_map_invasion_dynamics"
  ],
  "proof_status": "proven",
  "ref_roles": [
    {
      "context": "non-MAP strategy. There exists $\\epsilon_0 > 0$ such that for all $\\epsilon \\in (0, \\epsilon_0)$ (in the sense of Def.~\\ref{definition:bk5_symbolic_ess} and Lem.~\\ref{lemma:bk5_map_fitness_advantage}): \\begin{equation} \\Phi(\\sigma_{MAP}, (1-\\epsilon)\\delta_{\\sigma_{MAP}}",
      "label": "definition:bk5_symbolic_ess",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "book5.tex",
      "target_line": 1099,
      "target_type": "definition"
    },
    {
      "context": "> 0$ such that for all $\\epsilon \\in (0, \\epsilon_0)$ (in the sense of Def.~\\ref{definition:bk5_symbolic_ess} and Lem.~\\ref{lemma:bk5_map_fitness_advantage}): \\begin{equation} \\Phi(\\sigma_{MAP}, (1-\\epsilon)\\delta_{\\sigma_{MAP}} + \\epsilon\\delta_{\\sigma_{inv}}) > \\Phi(\\sigma_",
      "label": "lemma:bk5_map_fitness_advantage",
      "logical_support": true,
      "role": "formal_dependency",
      "target_file": "book5.tex",
      "target_line": 1107,
      "target_type": "lemma"
    }
  ],
  "refs": [
    "definition:bk5_symbolic_ess",
    "lemma:bk5_map_fitness_advantage"
  ],
  "role": "lemma",
  "type": "lemma"
}

{
  "book": "book5",
  "cited_by": [],
  "cites": [
    "definition:bk2_symbolic_free_energy",
    "definition:bk5_symbolic_fitness"
  ],
  "depends_on": [
    "definition:bk2_symbolic_free_energy",
    "definition:bk5_symbolic_fitness"
  ],
  "file": "book5.tex",
  "id": "proof:bk5_map_invasion_dynamics",
  "label": "proof:bk5_map_invasion_dynamics",
  "latex_body": "\\begin{proof}[Invasion Analysis of MAP vs Non-MAP Strategies]\n\\label{proof:bk5_map_invasion_dynamics}\n\\leavevmode\n\nWhen a small fraction $\\epsilon$ of invading non-MAP strategies enters a population dominated by MAP strategies, the fitness of each strategy becomes (cf.~Def.~\\ref{definition:bk5_symbolic_fitness}, Def.~\\ref{definition:bk2_symbolic_free_energy}):\n\\begin{align}\n\\Phi(\\sigma_{MAP}, (1-\\epsilon)\\delta_{\\sigma_{MAP}} + \\epsilon\\delta_{\\sigma_{inv}}) &= (1-\\epsilon)F_s(\\Membrane_{\\sigma_{MAP}} \\leftrightarrow \\Membrane_{\\sigma_{MAP}}) + \\epsilon F_s(\\Membrane_{\\sigma_{MAP}} \\leftrightarrow \\Membrane_{\\sigma_{inv}}) \\\\\n\\Phi(\\sigma_{inv}, (1-\\epsilon)\\delta_{\\sigma_{MAP}} + \\epsilon\\delta_{\\sigma_{inv}}) &= (1-\\epsilon)F_s(\\Membrane_{\\sigma_{inv}} \\leftrightarrow \\Membrane_{\\sigma_{MAP}}) + \\epsilon F_s(\\Membrane_{\\sigma_{inv}} \\leftrightarrow \\Membrane_{\\sigma_{inv}})\n\\end{align}\nBy Def.~\\ref{definition:bk5_symbolic_fitness}, $F_s(\\Membrane_{\\sigma_{MAP}} \\leftrightarrow \\Membrane_{\\sigma_{MAP}}) > 0$.\nFor non-MAP invaders, their lack of appropriate reflection mechanisms means $F_s(\\Membrane_{\\sigma_{inv}} \\leftrightarrow \\Membrane_{\\sigma_{inv}}) \\leq 0$ under sufficient drift.\nFurthermore, when interacting with MAP strategies, non-MAP invaders may receive some benefit,\nbut cannot contribute equally to maintaining free energy. Formally:\n\\[\nF_s\\left(\\Membrane_{\\sigma_{\\text{inv}}} \\leftrightarrow \\Membrane_{\\sigma_{\\text{MAP}}}\\right) \n< \nF_s\\left(\\Membrane_{\\sigma_{\\text{MAP}}} \\leftrightarrow \\Membrane_{\\sigma_{\\text{MAP}}}\\right).\n\\]\nAdditionally, MAP strategies remain resilient even when interacting with non-MAP strategies:\n\\[\nF_s(\\Membrane_{\\sigma_{MAP}} \\leftrightarrow \\Membrane_{\\sigma_{inv}})\n>\nF_s(\\Membrane_{\\sigma_{inv}} \\leftrightarrow \\Membrane_{\\sigma_{inv}}).\n\\]\nCombining these inequalities:\n\\begin{align}\n\\Phi(\\sigma_{MAP}, (1-\\epsilon)\\delta_{\\sigma_{MAP}} + \\epsilon\\delta_{\\sigma_{inv}}) &> \\Phi(\\sigma_{inv}, (1-\\epsilon)\\delta_{\\sigma_{MAP}} + \\epsilon\\delta_{\\sigma_{inv}})\n\\end{align}\nTherefore, MAP strategies resist invasion by non-MAP strategies, satisfying the non-invasibility criterion for evolutionary stability.\n\\end{proof}",
  "line": 1140,
  "macros_used": [
    "Membrane"
  ],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "Invasion Analysis of MAP vs Non-MAP Strategies",
  "proves": "lemma:bk5_covenant_non_invasibility",
  "ref_roles": [
    {
      "context": "dominated by MAP strategies, the fitness of each strategy becomes (cf.~Def.~\\ref{definition:bk5_symbolic_fitness}, Def.~\\ref{definition:bk2_symbolic_free_energy}): \\begin{align} \\Phi(\\sigma_{MAP}, (1-\\epsilon)\\delta_{\\sigma_{MAP}} + \\epsilon\\delta_{\\sigma_{inv}}) &= (1-\\epsilon)F_",
      "label": "definition:bk2_symbolic_free_energy",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book2.tex",
      "target_line": 135,
      "target_type": "definition"
    },
    {
      "context": "ding non-MAP strategies enters a population dominated by MAP strategies, the fitness of each strategy becomes (cf.~Def.~\\ref{definition:bk5_symbolic_fitness}, Def.~\\ref{definition:bk2_symbolic_free_energy}): \\begin{align} \\Phi(\\sigma_{MAP}, (1-\\epsilon)\\delta_{\\sigma_{MAP}} +",
      "label": "definition:bk5_symbolic_fitness",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book5.tex",
      "target_line": 1091,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:bk2_symbolic_free_energy",
    "definition:bk5_symbolic_fitness"
  ],
  "role": "proof",
  "type": "proof"
}

{
  "book": "book5",
  "cited_by": [
    "proof:bk5_map_as_ess",
    "proposition:bk6_drift_reflection_correspondence"
  ],
  "cites": [],
  "depends_on": [
    "theorem:bk4_compatibility_drift_reflective_operations",
    "theorem:bk5_map_equilibrium"
  ],
  "file": "book5.tex",
  "id": "theorem:bk5_rift_reflection_balance_in_strategy_space",
  "label": "theorem:bk5_rift_reflection_balance_in_strategy_space",
  "latex_body": "\\begin{theorem}[Drift--Reflection Balance in Strategy Space] \\label{theorem:bk5_rift_reflection_balance_in_strategy_space}\nLet $\\mathbb{D}(\\Sigma)$ and $\\mathbb{R}(\\Sigma)$ be the drift and reflection\noperators available in strategy space $\\Sigma$.  For $\\sigma\\in\\Sigma$, let\n$\\mathbb{R}_{\\sigma}\\subseteq\\mathbb{R}(\\Sigma)$ be the reflection inventory\navailable to that strategy, and let $\\kappa_\\sigma$ be its cooperation\ncoefficient.  Fix a drift operator $\\drift\\in\\mathbb{D}(\\Sigma)$.  Suppose\nthere is a MAP strategy $\\sigma_0\\in\\Sigma_{\\mathrm{MAP}}$ such that\n$\\kappa_{\\sigma_0}>0$ and its available reflection capacities are cofinal:\n\\begin{equation}\n \\forall c\\in\\mathbb{R},\\quad\n \\exists\\reflect\\in\\mathbb{R}_{\\sigma_0}:\\ c<\\lVert\\reflect\\rVert.\n \\label{eq:bk5_reflection_capacity_cofinal}\n\\end{equation}\nDefine the drift-indexed viable MAP subset by\n\\begin{equation}\n \\Sigma_{\\mathrm{MAP}}^{\\drift}:=\n \\left\\{\\sigma\\in\\Sigma_{\\mathrm{MAP}}:\\\n \\exists\\reflect_\\sigma\\in\\mathbb{R}_{\\sigma},\\quad\n \\lVert\\drift\\rVert<\\lVert\\reflect_\\sigma\\rVert\\kappa_\\sigma\\right\\}.\n \\label{eq:bk5_viable_map_inventory}\n\\end{equation}\nThen $\\Sigma_{\\mathrm{MAP}}^{\\drift}$ is nonempty.  If positive cooperation\nand the cofinality condition hold for every MAP strategy, then\n$\\Sigma_{\\mathrm{MAP}}^{\\drift}=\\Sigma_{\\mathrm{MAP}}$.\n\\end{theorem}",
  "lean_alignment": {
    "conditions": [
      "cofinal available reflection capacity",
      "positive cooperation at a MAP strategy",
      "strategy-indexed available reflection inventory",
      "typed drift and reflection operator carriers"
    ],
    "countermodels": [
      "Book5StrategyBalance.OperatorStrategySpace.submaximal_drift_without_inventory_countermodel",
      "Book5StrategyBalance.submaximal_drift_alone_does_not_supply_available_strategy"
    ],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "Typed operator-inventory reconstruction: drift and reflection operators remain distinct carrier types with observer-assigned intensities, MAP membership, strategy-indexed availability, and cooperation. Cofinal reflection capacity at one cooperative MAP strategy constructs a nonempty viable MAP subset; uniform cofinality proves equality with the MAP set. Countermodels retain that sub-maximal drift and positive cooperation do not populate an empty inventory, while exact cancellation lacks strict margin."
    ],
    "record_ids": [
      "MAP-BOOK5-002"
    ],
    "statuses": [
      "exact"
    ],
    "witnesses": [
      "Book5StrategyBalance.OperatorStrategySpace.exists_operator_balance_of_cofinal",
      "Book5StrategyBalance.OperatorStrategySpace.mem_viableMAP_iff",
      "Book5StrategyBalance.OperatorStrategySpace.submaximal_drift_without_inventory_countermodel",
      "Book5StrategyBalance.OperatorStrategySpace.viableMAP_eq_isMAP_of_uniform_richness",
      "Book5StrategyBalance.OperatorStrategySpace.viableMAP_nonempty_of_richness",
      "Book5StrategyBalance.balance_iff_capacity_above_threshold",
      "Book5StrategyBalance.exists_available_balancing_strategy",
      "Book5StrategyBalance.isolated_strategy_cannot_balance_positive_drift",
      "Book5StrategyBalance.local_cancellation_is_not_strict_balance",
      "Book5StrategyBalance.submaximal_drift_alone_does_not_supply_available_strategy"
    ]
  },
  "line": 1170,
  "macros_used": [
    "drift",
    "reflect"
  ],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "Drift--Reflection Balance in Strategy Space",
  "proof_labels": [
    "proof:bk5_drift_reflection_equilibrium"
  ],
  "proof_status": "proven",
  "refs": [],
  "role": "theorem",
  "type": "theorem"
}

{
  "book": "book5",
  "cited_by": [],
  "cites": [
    "theorem:bk4_compatibility_drift_reflective_operations",
    "theorem:bk5_map_equilibrium"
  ],
  "depends_on": [
    "theorem:bk4_compatibility_drift_reflective_operations",
    "theorem:bk5_map_equilibrium"
  ],
  "file": "book5.tex",
  "id": "proof:bk5_drift_reflection_equilibrium",
  "label": "proof:bk5_drift_reflection_equilibrium",
  "latex_body": "\\begin{proof}[Available-Operator Construction]\n\\label{proof:bk5_drift_reflection_equilibrium}\nFor $\\sigma_0$, positive cooperation makes the finite threshold\n\\[\n c_0=\\frac{\\lVert\\drift\\rVert}{\\kappa_{\\sigma_0}}\n\\]\nwell defined.  By Eq.~\\eqref{eq:bk5_reflection_capacity_cofinal}, choose an\navailable $\\reflect_0\\in\\mathbb{R}_{\\sigma_0}$ with\n$c_0<\\lVert\\reflect_0\\rVert$.  Multiplication by\n$\\kappa_{\\sigma_0}>0$ gives\n\\[\n \\lVert\\drift\\rVert<\\lVert\\reflect_0\\rVert\\kappa_{\\sigma_0},\n\\]\nso $\\sigma_0\\in\\Sigma_{\\mathrm{MAP}}^{\\drift}$.  Under the uniform\nhypothesis the same construction applies to every MAP strategy, yielding the\nstated equality.\n\nThe condition $\\lVert\\drift\\rVert<\\drift_{\\max}$ may delimit the intended\nphysical regime (cf.~Thm.~\\ref{theorem:bk5_map_equilibrium} and\nThm.~\\ref{theorem:bk4_compatibility_drift_reflective_operations}), but it does\nnot by itself populate any reflection inventory.  Likewise,\n$\\lVert\\reflect\\rVert\\kappa_\\sigma=\\lVert\\drift\\rVert$ gives exact local\ncancellation but not the strict positive viability margin used here.  The\navailability and cofinality hypotheses are therefore load-bearing rather than\nconsequences of the named drift bound.\n\\end{proof}",
  "line": 1195,
  "macros_used": [
    "drift",
    "reflect"
  ],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "Available-Operator Construction",
  "proves": "theorem:bk5_rift_reflection_balance_in_strategy_space",
  "ref_roles": [
    {
      "context": "rift\\rVert<\\drift_{\\max}$ may delimit the intended physical regime (cf.~Thm.~\\ref{theorem:bk5_map_equilibrium} and Thm.~\\ref{theorem:bk4_compatibility_drift_reflective_operations}), but it does not by itself populate any reflection inventory. Likewise, $\\lVert\\reflect\\rVert\\kappa_\\sigma=\\lVert\\dri",
      "label": "theorem:bk4_compatibility_drift_reflective_operations",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book4.tex",
      "target_line": 3835,
      "target_type": "theorem"
    },
    {
      "context": "e stated equality. The condition $\\lVert\\drift\\rVert<\\drift_{\\max}$ may delimit the intended physical regime (cf.~Thm.~\\ref{theorem:bk5_map_equilibrium} and Thm.~\\ref{theorem:bk4_compatibility_drift_reflective_operations}), but it does not by itself populate any reflectio",
      "label": "theorem:bk5_map_equilibrium",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book5.tex",
      "target_line": 272,
      "target_type": "theorem"
    }
  ],
  "refs": [
    "eq:bk5_reflection_capacity_cofinal",
    "theorem:bk4_compatibility_drift_reflective_operations",
    "theorem:bk5_map_equilibrium"
  ],
  "role": "proof",
  "type": "proof"
}

{
  "book": "book5",
  "cited_by": [
    "proof:bk5_map_as_ess",
    "proof:bk5_map_perturbation_robustness",
    "proof:bk5_map_strict_fitness_dominance",
    "proof:bk5_symbolic_fitness_differentials"
  ],
  "cites": [
    "definition:bk5_symbolic_fitness"
  ],
  "depends_on": [
    "definition:bk5_symbolic_fitness"
  ],
  "file": "book5.tex",
  "id": "definition:bk5_symbolic_replicator_dynamics",
  "label": "definition:bk5_symbolic_replicator_dynamics",
  "latex_body": "\\begin{definition}[Symbolic Replicator Dynamics] \\label{definition:bk5_symbolic_replicator_dynamics}\n\nLet $x_\\sigma(t)$ denote the frequency of strategy $\\sigma$ in the symbolic population at time $t$. The symbolic replicator dynamics are governed by (cf.~Def.~\\ref{definition:bk5_symbolic_fitness}):\n\\begin{equation}\n\\frac{dx_\\sigma}{dt} = x_\\sigma \\left( \\Phi(\\sigma, \\mathfrak{P}_t) - \\bar{\\Phi}(\\mathfrak{P}_t) \\right)\n\\end{equation}\nWhere $\\mathfrak{P}_t$ is the population distribution at time $t$ and $\\bar{\\Phi}(\\mathfrak{P}_t) = \\sum_{\\tau \\in \\Sigma} x_\\tau(t) \\Phi(\\tau, \\mathfrak{P}_t)$ is the average population fitness.\n\\end{definition}",
  "line": 1221,
  "macros_used": [],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "Symbolic Replicator Dynamics",
  "proof_status": "definitional",
  "ref_roles": [
    {
      "context": "of strategy $\\sigma$ in the symbolic population at time $t$. The symbolic replicator dynamics are governed by (cf.~Def.~\\ref{definition:bk5_symbolic_fitness}): \\begin{equation} \\frac{dx_\\sigma}{dt} = x_\\sigma \\left( \\Phi(\\sigma, \\mathfrak{P}_t) - \\bar{\\Phi}(\\mathfrak{P}_t) \\ri",
      "label": "definition:bk5_symbolic_fitness",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book5.tex",
      "target_line": 1091,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:bk5_symbolic_fitness"
  ],
  "role": "definition",
  "type": "definition"
}

{
  "book": "book5",
  "cited_by": [
    "definition:bk5_viability_domain"
  ],
  "cites": [
    "definition:bk1_drift_field",
    "definition:bk1_symbolic_manifold",
    "definition:bk2_symbolic_free_energy",
    "definition:bk5_viability_domain"
  ],
  "depends_on": [
    "definition:bk1_drift_field",
    "definition:bk1_symbolic_manifold",
    "definition:bk2_symbolic_free_energy",
    "definition:bk5_symbolic_ess",
    "definition:bk5_symbolic_replicator_dynamics",
    "definition:bk5_viability_domain",
    "lemma:bk5_covenant_non_invasibility",
    "theorem:bk5_rift_reflection_balance_in_strategy_space"
  ],
  "file": "book5.tex",
  "id": "proposition:bk5_symbolic_ess_via_map_observability_variant",
  "label": "proposition:bk5_symbolic_ess_via_map_observability_variant",
  "latex_body": "\\begin{proposition}[Symbolic ESS via MAP]\n\\label{proposition:bk5_symbolic_ess_via_map_observability_variant}\nLet $\\sigma_{MAP} \\in \\Sigma_{MAP}$ be a MAP strategy with symbolic free energy $F_s$ (Def.~\\ref{definition:bk2_symbolic_free_energy}) on the symbolic manifold $M$ (Def.~\\ref{definition:bk1_symbolic_manifold}) in an environment with drift intensity $\\|\\drift\\| > \\drift_0$ (Def.~\\ref{definition:bk1_drift_field}). Let viability be measured by Def.~\\ref{definition:bk5_viability_domain}. If $\\sigma_{MAP}$ satisfies:\n\\begin{enumerate}\n    \\item \\textbf{Stability}: $F_s(\\Membrane_{\\sigma_{MAP}} \\leftrightarrow \\Membrane_{\\sigma_{MAP}}) > 0$\n    \\item \\textbf{Non-invasibility}: $\\forall \\sigma \\neq \\sigma_{MAP}, \\exists \\epsilon_\\sigma > 0$ such that \n    $\\Phi(\\sigma_{MAP}, (1-\\epsilon)\\delta_{\\sigma_{MAP}} + \\epsilon\\delta_\\sigma) > \\Phi(\\sigma, (1-\\epsilon)\\delta_{\\sigma_{MAP}} + \\epsilon\\delta_\\sigma)$ for all $\\epsilon \\in (0, \\epsilon_\\sigma)$\n    \\item \\textbf{Viability Expansion}: $V_{\\text{symb}}^{MAP}(t+1) \\supset V_{\\text{symb}}^{MAP}(t)$\n\\end{enumerate}\nThen $\\sigma_{MAP}$ constitutes a symbolic evolutionarily stable strategy (ESS).\n\\end{proposition}",
  "lean_alignment": {
    "conditions": [
      "continuum/Hilbert/PDE-on-manifold content stays open; chart-complex restatements carry Glued as a named hypothesis where the source consumes compatibility",
      "modeling laws are structure fields or explicit hypotheses"
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "stability and non-invasibility conditions are covered by ess_invasion_threshold; viability expansion is covered qualitatively by viability_union_mono_chain; the three are not composed into one theorem."
    ],
    "record_ids": [
      "MAP-BOOK5-070"
    ],
    "statuses": [
      "conditional"
    ],
    "witnesses": [
      "Book5Residue.ess_invasion_threshold",
      "Book5Residue.viability_union_mono_chain"
    ]
  },
  "line": 1229,
  "macros_used": [
    "Membrane",
    "drift"
  ],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "Symbolic ESS via MAP",
  "proof_labels": [
    "proof:bk5_map_as_ess"
  ],
  "proof_status": "proven",
  "ref_roles": [
    {
      "context": "$M$ (Def.~\\ref{definition:bk1_symbolic_manifold}) in an environment with drift intensity $\\|\\drift\\| > \\drift_0$ (Def.~\\ref{definition:bk1_drift_field}). Let viability be measured by Def.~\\ref{definition:bk5_viability_domain}. If $\\sigma_{MAP}$ satisfies: \\begin{enumerat",
      "label": "definition:bk1_drift_field",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 1198,
      "target_type": "definition"
    },
    {
      "context": "egy with symbolic free energy $F_s$ (Def.~\\ref{definition:bk2_symbolic_free_energy}) on the symbolic manifold $M$ (Def.~\\ref{definition:bk1_symbolic_manifold}) in an environment with drift intensity $\\|\\drift\\| > \\drift_0$ (Def.~\\ref{definition:bk1_drift_field}). Let viability",
      "label": "definition:bk1_symbolic_manifold",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 1188,
      "target_type": "definition"
    },
    {
      "context": "_map_observability_variant} Let $\\sigma_{MAP} \\in \\Sigma_{MAP}$ be a MAP strategy with symbolic free energy $F_s$ (Def.~\\ref{definition:bk2_symbolic_free_energy}) on the symbolic manifold $M$ (Def.~\\ref{definition:bk1_symbolic_manifold}) in an environment with drift intensity $\\|\\",
      "label": "definition:bk2_symbolic_free_energy",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "book2.tex",
      "target_line": 135,
      "target_type": "definition"
    },
    {
      "context": "with drift intensity $\\|\\drift\\| > \\drift_0$ (Def.~\\ref{definition:bk1_drift_field}). Let viability be measured by Def.~\\ref{definition:bk5_viability_domain}. If $\\sigma_{MAP}$ satisfies: \\begin{enumerate} \\item \\textbf{Stability}: $F_s(\\Membrane_{\\sigma_{MAP}} \\leftrighta",
      "label": "definition:bk5_viability_domain",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "book5.tex",
      "target_line": 133,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:bk1_drift_field",
    "definition:bk1_symbolic_manifold",
    "definition:bk2_symbolic_free_energy",
    "definition:bk5_viability_domain"
  ],
  "role": "proposition",
  "type": "proposition"
}

{
  "book": "book5",
  "cited_by": [],
  "cites": [
    "definition:bk5_symbolic_ess",
    "definition:bk5_symbolic_replicator_dynamics",
    "lemma:bk5_covenant_non_invasibility",
    "theorem:bk5_rift_reflection_balance_in_strategy_space"
  ],
  "depends_on": [
    "definition:bk5_symbolic_ess",
    "definition:bk5_symbolic_replicator_dynamics",
    "lemma:bk5_covenant_non_invasibility",
    "theorem:bk5_rift_reflection_balance_in_strategy_space"
  ],
  "file": "book5.tex",
  "id": "proof:bk5_map_as_ess",
  "label": "proof:bk5_map_as_ess",
  "latex_body": "\\begin{proof}[MAP as Symbolic Evolutionarily Stable Strategy]\n\\label{proof:bk5_map_as_ess}\n\\leavevmode\n\nWe need to establish that $\\sigma_{MAP}$ satisfies the formal criteria for a symbolic ESS as per Def.~\\ref{definition:bk5_symbolic_ess}.\nFirst, the stability criterion ensures that a population of membranes all employing $\\sigma_{MAP}$ maintains positive free energy, keeping all membranes within their viability domains.\nSecond, by Lem.~\\ref{lemma:bk5_covenant_non_invasibility}, MAP strategies resist invasion by non-MAP strategies. This satisfies the non-invasibility criterion essential for evolutionary stability.\nThird, the viability expansion property ensures that MAP strategies not only maintain but expand their viability domains over time, creating a positive feedback loop that reinforces their evolutionary advantage.\nLet us now show that these conditions together imply evolutionary stability. Consider a population initially dominated by $\\sigma_{MAP}$ that is invaded by a small proportion $\\epsilon$ of an alternative strategy $\\sigma$:\nFrom the symbolic replicator dynamics (Def.~\\ref{definition:bk5_symbolic_replicator_dynamics}):\n\\begin{align}\n\\frac{dx_{\\sigma_{MAP}}}{dt} &= x_{\\sigma_{MAP}} \\left( \\Phi(\\sigma_{MAP}, \\mathfrak{P}_t) - \\bar{\\Phi}(\\mathfrak{P}_t) \\right) \\\\\n\\frac{dx_\\sigma}{dt} &= x_\\sigma \\left( \\Phi(\\sigma, \\mathfrak{P}_t) - \\bar{\\Phi}(\\mathfrak{P}_t) \\right)\n\\end{align}\nBy the non-invasibility condition, $\\Phi(\\sigma_{MAP}, \\mathfrak{P}_t) > \\Phi(\\sigma, \\mathfrak{P}_t)$ when $x_\\sigma$ is small. This implies:\n\\begin{align}\n\\frac{dx_{\\sigma_{MAP}}}{dt} &> 0 \\\\\n\\frac{dx_\\sigma}{dt} &< 0\n\\end{align}\nTherefore, the frequency of $\\sigma_{MAP}$ increases while the frequency of the invading strategy $\\sigma$ decreases, restoring the population to its original MAP-dominated state.\nFurthermore, by Thm.~\\ref{theorem:bk5_rift_reflection_balance_in_strategy_space}, under any sub-maximal drift intensity, there exists a MAP strategy that maintains viability through appropriate balance of reflection capacity and cooperation.\nFinally, the viability expansion property ensures that MAP strategies become increasingly advantageous over time, as their viable parameter space grows while non-MAP strategies' viable parameter space shrinks under continued drift pressure.\nThus, $\\sigma_{MAP}$ satisfies all criteria for a symbolic evolutionarily stable strategy.\n\\end{proof}",
  "line": 1240,
  "macros_used": [],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "MAP as Symbolic Evolutionarily Stable Strategy",
  "proves": "proposition:bk5_symbolic_ess_via_map_observability_variant",
  "ref_roles": [
    {
      "context": "ess} \\leavevmode We need to establish that $\\sigma_{MAP}$ satisfies the formal criteria for a symbolic ESS as per Def.~\\ref{definition:bk5_symbolic_ess}. First, the stability criterion ensures that a population of membranes all employing $\\sigma_{MAP}$ maintains positive",
      "label": "definition:bk5_symbolic_ess",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "book5.tex",
      "target_line": 1099,
      "target_type": "definition"
    },
    {
      "context": "vaded by a small proportion $\\epsilon$ of an alternative strategy $\\sigma$: From the symbolic replicator dynamics (Def.~\\ref{definition:bk5_symbolic_replicator_dynamics}): \\begin{align} \\frac{dx_{\\sigma_{MAP}}}{dt} &= x_{\\sigma_{MAP}} \\left( \\Phi(\\sigma_{MAP}, \\mathfrak{P}_t) - \\bar{\\Phi}",
      "label": "definition:bk5_symbolic_replicator_dynamics",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "book5.tex",
      "target_line": 1221,
      "target_type": "definition"
    },
    {
      "context": "ng $\\sigma_{MAP}$ maintains positive free energy, keeping all membranes within their viability domains. Second, by Lem.~\\ref{lemma:bk5_covenant_non_invasibility}, MAP strategies resist invasion by non-MAP strategies. This satisfies the non-invasibility criterion essential for evol",
      "label": "lemma:bk5_covenant_non_invasibility",
      "logical_support": true,
      "role": "proof_support",
      "target_file": "book5.tex",
      "target_line": 1133,
      "target_type": "lemma"
    },
    {
      "context": "nvading strategy $\\sigma$ decreases, restoring the population to its original MAP-dominated state. Furthermore, by Thm.~\\ref{theorem:bk5_rift_reflection_balance_in_strategy_space}, under any sub-maximal drift intensity, there exists a MAP strategy that maintains viability through appropriate balanc",
      "label": "theorem:bk5_rift_reflection_balance_in_strategy_space",
      "logical_support": true,
      "role": "proof_support",
      "target_file": "book5.tex",
      "target_line": 1170,
      "target_type": "theorem"
    }
  ],
  "refs": [
    "definition:bk5_symbolic_ess",
    "definition:bk5_symbolic_replicator_dynamics",
    "lemma:bk5_covenant_non_invasibility",
    "theorem:bk5_rift_reflection_balance_in_strategy_space"
  ],
  "role": "proof",
  "type": "proof"
}

{
  "book": "book5",
  "cited_by": [
    "proof:bk5_map_viability_critical_drift",
    "scholium:bk5__map_ess_implications"
  ],
  "cites": [],
  "depends_on": [],
  "file": "book5.tex",
  "id": "corollary:bk5_convergence_to_map",
  "label": "corollary:bk5_convergence_to_map",
  "latex_body": "\\begin{corollary}[Convergence to MAP]\n\\label{corollary:bk5_convergence_to_map}\nLet $x_n=\\mathbb{P}_{\\sigma\\sim\\mathfrak{P}_n}\n[\\sigma\\in\\Sigma_{\\mathrm{MAP}}]$ be the MAP share of a discrete symbolic\npopulation after some selection onset $n=0$.  Assume:\n\\begin{enumerate}\n\\item $0\\leq x_0\\leq1$;\n\\item MAP and non-MAP aggregate fitnesses $F_{\\mathrm{MAP}}$ and\n$F_{\\mathrm{non}}$ remain positive/nonnegative with a persistent quantitative\ngap $0\\leq F_{\\mathrm{non}}<F_{\\mathrm{MAP}}$; and\n\\item selection is mutation-free with respect to MAP membership: there is no\nnon-MAP inflow, and the residual mass obeys\n\\begin{equation}\n 1-x_{n+1}=q(1-x_n),\\qquad\n q:=\\frac{F_{\\mathrm{non}}}{F_{\\mathrm{MAP}}}.\n \\label{eq:bk5_map_residual_contraction}\n\\end{equation}\n\\end{enumerate}\nThen $0\\leq x_n\\leq1$ for every $n$ and\n\\begin{equation}\n \\lim_{n\\to\\infty}x_n=1.\n\\end{equation}\nIncreasing drift may motivate or sustain the quantitative fitness gap\n(cf.~Def.~\\ref{definition:bk5_symbolic_replicator_dynamics} and\nLemma~\\ref{lemma:bk5_map_fitness_advantage}), but it is not by itself a\nconvergence hypothesis.\n\\end{corollary}",
  "lean_alignment": {
    "conditions": [
      "exact residual recurrence excluding non-MAP inflow",
      "initial MAP share in the probability interval",
      "positive MAP and nonnegative non-MAP fitness",
      "strict persistent MAP aggregate fitness advantage"
    ],
    "countermodels": [
      "Book5ConvergenceMAP.MAPPopulationOrbit.fitness_gap_with_inflow_does_not_force_convergence",
      "Book5ConvergenceMAP.increasing_drift_alone_does_not_force_map_convergence"
    ],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "A persistent quantitative MAP fitness advantage yields a contraction ratio q in [0,1). A mutation-free aggregate population orbit explicitly excludes non-MAP inflow through its residual recurrence. Lean derives the geometric residual, proves every share remains in [0,1], and proves convergence to MAP mass one. Countermodels show that increasing drift alone—or even a strict fitness gap with replenishing inflow—does not force convergence."
    ],
    "record_ids": [
      "MAP-BOOK5-001"
    ],
    "statuses": [
      "exact"
    ],
    "witnesses": [
      "Book5ConvergenceMAP.MAPPopulationOrbit.fitness_gap_with_inflow_does_not_force_convergence",
      "Book5ConvergenceMAP.MAPPopulationOrbit.residual_eq_pow",
      "Book5ConvergenceMAP.MAPPopulationOrbit.share_eq_mapShare",
      "Book5ConvergenceMAP.MAPPopulationOrbit.share_le_one",
      "Book5ConvergenceMAP.MAPPopulationOrbit.share_nonneg",
      "Book5ConvergenceMAP.MAPPopulationOrbit.share_tendsto_one",
      "Book5ConvergenceMAP.PersistentMAPAdvantage.contraction_lt_one",
      "Book5ConvergenceMAP.PersistentMAPAdvantage.contraction_nonneg",
      "Book5ConvergenceMAP.increasing_drift_alone_does_not_force_map_convergence",
      "Book5ConvergenceMAP.mapShare_succ",
      "Book5ConvergenceMAP.mapShare_tendsto_one",
      "Book5ConvergenceMAP.mapShare_zero"
    ]
  },
  "line": 1264,
  "macros_used": [],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "Convergence to MAP",
  "proof_labels": [
    "proof:bk5_map_fitness_threshold"
  ],
  "proof_status": "proven",
  "refs": [
    "definition:bk5_symbolic_replicator_dynamics",
    "lemma:bk5_map_fitness_advantage"
  ],
  "role": "corollary",
  "type": "corollary"
}

{
  "book": "book5",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "book5.tex",
  "id": "proof:bk5_map_fitness_threshold",
  "label": "proof:bk5_map_fitness_threshold",
  "latex_body": "\\begin{proof}[Quantitative Mutation-Free Selection]\n\\label{proof:bk5_map_fitness_threshold}\nPositivity and the strict fitness gap give $0\\leq q<1$.  Iterating\nEq.~\\eqref{eq:bk5_map_residual_contraction} yields\n\\[\n 1-x_n=q^n(1-x_0).\n\\]\nBecause $0\\leq q^n\\leq1$ and $0\\leq1-x_0\\leq1$, this identity preserves\n$0\\leq x_n\\leq1$.  Since $q^n\\to0$, the residual non-MAP mass tends to zero\nand hence $x_n\\to1$.\n\nThe no-inflow clause is load-bearing.  A process may maintain\n$F_{\\mathrm{non}}<F_{\\mathrm{MAP}}$ while replenishing non-MAP mass and keeping\n$x_n=1/2$ for all $n$; such a process remains on the probability simplex but\ndoes not converge to MAP.  Likewise, increasing drift alone supplies neither\nthe uniform ratio $q<1$ nor the recurrence.\n\\end{proof}",
  "line": 1291,
  "macros_used": [],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "Quantitative Mutation-Free Selection",
  "proves": "corollary:bk5_convergence_to_map",
  "refs": [
    "eq:bk5_map_residual_contraction"
  ],
  "role": "proof",
  "type": "proof"
}

{
  "book": "book5",
  "cited_by": [
    "proof:bk5_map_perturbation_robustness"
  ],
  "cites": [
    "definition:bk5_covenant_resilience_index"
  ],
  "depends_on": [
    "definition:bk2_symbolic_free_energy",
    "definition:bk5_covenant_resilience_index",
    "definition:bk5_symbolic_replicator_dynamics"
  ],
  "file": "book5.tex",
  "id": "lemma:bk5_map_population_stability",
  "label": "lemma:bk5_map_population_stability",
  "latex_body": "\\begin{lemma}[MAP Population Stability]\n\\label{lemma:bk5_map_population_stability}\nA population composed entirely of MAP strategies is stable against perturbations in strategy distribution if the covenant resilience index (Def.~\\ref{definition:bk5_covenant_resilience_index}) satisfies:\n\\begin{equation}\n\\min_{\\sigma, \\tau \\in \\Sigma_{MAP}} \\rho(\\mathcal{C}_{\\sigma\\tau}) > 1 + \\delta\n\\end{equation}\nFor some margin $\\delta > 0$.\n\\end{lemma}",
  "lean_alignment": {
    "conditions": [
      "continuum/Hilbert/PDE-on-manifold content stays open; chart-complex restatements carry Glued as a named hypothesis where the source consumes compatibility",
      "modeling laws are structure fields or explicit hypotheses"
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "See the committed source registry for the original coverage note."
    ],
    "record_ids": [
      "MAP-BOOK5-071"
    ],
    "statuses": [
      "conditional"
    ],
    "witnesses": [
      "Book5Residue.min_resilience_implies_all_edges_resilient"
    ]
  },
  "line": 1308,
  "macros_used": [],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "MAP Population Stability",
  "proof_labels": [
    "proof:bk5_map_perturbation_robustness"
  ],
  "proof_status": "proven",
  "ref_roles": [
    {
      "context": "irely of MAP strategies is stable against perturbations in strategy distribution if the covenant resilience index (Def.~\\ref{definition:bk5_covenant_resilience_index}) satisfies: \\begin{equation} \\min_{\\sigma, \\tau \\in \\Sigma_{MAP}} \\rho(\\mathcal{C}_{\\sigma\\tau}) > 1 + \\delta \\end{equa",
      "label": "definition:bk5_covenant_resilience_index",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "book5.tex",
      "target_line": 454,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:bk5_covenant_resilience_index"
  ],
  "role": "lemma",
  "type": "lemma"
}

{
  "book": "book5",
  "cited_by": [],
  "cites": [
    "definition:bk2_symbolic_free_energy",
    "definition:bk5_covenant_resilience_index",
    "definition:bk5_symbolic_replicator_dynamics",
    "lemma:bk5_map_population_stability"
  ],
  "depends_on": [
    "definition:bk2_symbolic_free_energy",
    "definition:bk5_covenant_resilience_index",
    "definition:bk5_symbolic_replicator_dynamics",
    "lemma:bk5_map_population_stability"
  ],
  "file": "book5.tex",
  "id": "proof:bk5_map_perturbation_robustness",
  "label": "proof:bk5_map_perturbation_robustness",
  "latex_body": "\\begin{proof}[Perturbation Robustness of MAP Populations]\n\\label{proof:bk5_map_perturbation_robustness}\n\\leavevmode\n\nThe perturbation argument combines Lem.~\\ref{lemma:bk5_map_population_stability}, Def.~\\ref{definition:bk5_symbolic_replicator_dynamics}, and Def.~\\ref{definition:bk2_symbolic_free_energy}.\nLet $\\mathfrak{P}_{MAP}$ be a population distribution concentrated on MAP strategies, and $\\mathfrak{P}'$ be a perturbed distribution.\nThe stability of $\\mathfrak{P}_{MAP}$ depends on the resilience of covenants formed between MAP strategies. From Def.~\\ref{definition:bk5_covenant_resilience_index}, the covenant resilience index is:\n\\begin{equation}\n\\rho(\\mathcal{C}_{\\sigma\\tau}) = \\frac{\\Omega_{\\sigma\\tau} \\cdot \\lambda_{min}(\\mathbb{R}_{\\sigma\\tau})}{\\|\\drift_\\sigma\\|_{max} + \\|\\drift_\\tau\\|_{max}}\n\\end{equation}\nWhen $\\rho(\\mathcal{C}_{\\sigma\\tau}) > 1 + \\delta$, covenants can withstand perturbations in strategy frequencies while maintaining positive free energy.\nUnder symbolic replicator dynamics, this ensures that MAP strategies \ncontinue to exhibit above-average fitness. \nAs a result, the population is driven back toward \\( \\mathfrak{P}_{\\text{MAP}} \\) after perturbation, \nthereby establishing population-level stability.\n\\end{proof}",
  "line": 1316,
  "macros_used": [
    "drift"
  ],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "Perturbation Robustness of MAP Populations",
  "proves": "lemma:bk5_map_population_stability",
  "ref_roles": [
    {
      "context": "ombines Lem.~\\ref{lemma:bk5_map_population_stability}, Def.~\\ref{definition:bk5_symbolic_replicator_dynamics}, and Def.~\\ref{definition:bk2_symbolic_free_energy}. Let $\\mathfrak{P}_{MAP}$ be a population distribution concentrated on MAP strategies, and $\\mathfrak{P}'$ be a perturb",
      "label": "definition:bk2_symbolic_free_energy",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "book2.tex",
      "target_line": 135,
      "target_type": "definition"
    },
    {
      "context": ". The stability of $\\mathfrak{P}_{MAP}$ depends on the resilience of covenants formed between MAP strategies. From Def.~\\ref{definition:bk5_covenant_resilience_index}, the covenant resilience index is: \\begin{equation} \\rho(\\mathcal{C}_{\\sigma\\tau}) = \\frac{\\Omega_{\\sigma\\tau} \\cdot \\l",
      "label": "definition:bk5_covenant_resilience_index",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "book5.tex",
      "target_line": 454,
      "target_type": "definition"
    },
    {
      "context": "rbation_robustness} \\leavevmode The perturbation argument combines Lem.~\\ref{lemma:bk5_map_population_stability}, Def.~\\ref{definition:bk5_symbolic_replicator_dynamics}, and Def.~\\ref{definition:bk2_symbolic_free_energy}. Let $\\mathfrak{P}_{MAP}$ be a population distribution concentrated",
      "label": "definition:bk5_symbolic_replicator_dynamics",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "book5.tex",
      "target_line": 1221,
      "target_type": "definition"
    },
    {
      "context": "of MAP Populations] \\label{proof:bk5_map_perturbation_robustness} \\leavevmode The perturbation argument combines Lem.~\\ref{lemma:bk5_map_population_stability}, Def.~\\ref{definition:bk5_symbolic_replicator_dynamics}, and Def.~\\ref{definition:bk2_symbolic_free_energy}. Let $\\math",
      "label": "lemma:bk5_map_population_stability",
      "logical_support": true,
      "role": "proof_support",
      "target_file": "book5.tex",
      "target_line": 1308,
      "target_type": "lemma"
    }
  ],
  "refs": [
    "definition:bk2_symbolic_free_energy",
    "definition:bk5_covenant_resilience_index",
    "definition:bk5_symbolic_replicator_dynamics",
    "lemma:bk5_map_population_stability"
  ],
  "role": "proof",
  "type": "proof"
}

{
  "book": "book5",
  "cited_by": [
    "definition:bk5_symbolic_invasion_barrier",
    "proof:bk5_map_strict_fitness_dominance",
    "scholium:bk5__map_ess_implications"
  ],
  "cites": [
    "definition:bk5_symbolic_ess"
  ],
  "depends_on": [
    "definition:bk5_symbolic_ess",
    "definition:bk5_symbolic_replicator_dynamics"
  ],
  "file": "book5.tex",
  "id": "theorem:bk5_map_as_strong_ess",
  "label": "theorem:bk5_map_as_strong_ess",
  "latex_body": "\\begin{theorem}[MAP as Strong ESS]\n\\label{theorem:bk5_map_as_strong_ess}\nIf a MAP strategy $\\sigma_{MAP}$ satisfies (in the setting of Def.~\\ref{definition:bk5_symbolic_ess}):\n\\begin{equation}\n\\Phi(\\sigma_{MAP}, (1-\\epsilon)\\delta_{\\sigma_{MAP}} + \\epsilon\\delta_{\\sigma}) > \\Phi(\\sigma, (1-\\epsilon)\\delta_{\\sigma_{MAP}} + \\epsilon\\delta_{\\sigma})\n\\end{equation}\nFor all strategies $\\sigma \\neq \\sigma_{MAP}$ and all $\\epsilon \\in (0,1)$, then $\\sigma_{MAP}$ is a strong symbolic ESS, stable against arbitrary-sized invasions.\n\\end{theorem}",
  "lean_alignment": {
    "conditions": [
      "continuum/Hilbert/PDE-on-manifold content stays open; chart-complex restatements carry Glued as a named hypothesis where the source consumes compatibility",
      "modeling laws are structure fields or explicit hypotheses"
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": false,
    "notes": [
      "See the committed source registry for the original coverage note."
    ],
    "record_ids": [
      "MAP-BOOK5-072"
    ],
    "statuses": [
      "open_bridge"
    ],
    "witnesses": [
      "Book5Residue.ess_invasion_threshold"
    ]
  },
  "line": 1332,
  "macros_used": [],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "MAP as Strong ESS",
  "proof_labels": [
    "proof:bk5_map_strict_fitness_dominance"
  ],
  "proof_status": "proven",
  "ref_roles": [
    {
      "context": "as Strong ESS] \\label{theorem:bk5_map_as_strong_ess} If a MAP strategy $\\sigma_{MAP}$ satisfies (in the setting of Def.~\\ref{definition:bk5_symbolic_ess}): \\begin{equation} \\Phi(\\sigma_{MAP}, (1-\\epsilon)\\delta_{\\sigma_{MAP}} + \\epsilon\\delta_{\\sigma}) > \\Phi(\\sigma, (1-\\e",
      "label": "definition:bk5_symbolic_ess",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "book5.tex",
      "target_line": 1099,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:bk5_symbolic_ess"
  ],
  "role": "theorem",
  "type": "theorem"
}

{
  "book": "book5",
  "cited_by": [],
  "cites": [
    "definition:bk5_symbolic_replicator_dynamics",
    "theorem:bk5_map_as_strong_ess"
  ],
  "depends_on": [
    "definition:bk5_symbolic_replicator_dynamics",
    "theorem:bk5_map_as_strong_ess"
  ],
  "file": "book5.tex",
  "id": "proof:bk5_map_strict_fitness_dominance",
  "label": "proof:bk5_map_strict_fitness_dominance",
  "latex_body": "\\begin{proof}[Strict Dominance of MAP Under Mixing]\n\\label{proof:bk5_map_strict_fitness_dominance}\n\\leavevmode\n\nThe condition states that $\\sigma_{MAP}$ has strictly higher fitness than any alternative strategy $\\sigma$ regardless of the mixing proportion $\\epsilon$ (cf.~Thm.~\\ref{theorem:bk5_map_as_strong_ess}, Def.~\\ref{definition:bk5_symbolic_replicator_dynamics}).\nUnder symbolic replicator dynamics, this implies:\n\\begin{equation}\n\\frac{d}{dt}\\left(\\frac{x_{\\sigma_{MAP}}}{x_\\sigma}\\right) > 0\n\\end{equation}\nFor all $t$ and all alternative strategies $\\sigma$. This means the ratio of MAP strategists to any other strategists strictly increases over time regardless of initial population composition.\nTherefore, $\\sigma_{MAP}$ is a global attractor in the replicator dynamics, making it a strong symbolic ESS resistant to invasions of any size.\n\\end{proof}",
  "line": 1340,
  "macros_used": [],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "Strict Dominance of MAP Under Mixing",
  "proves": "theorem:bk5_map_as_strong_ess",
  "ref_roles": [
    {
      "context": "ve strategy $\\sigma$ regardless of the mixing proportion $\\epsilon$ (cf.~Thm.~\\ref{theorem:bk5_map_as_strong_ess}, Def.~\\ref{definition:bk5_symbolic_replicator_dynamics}). Under symbolic replicator dynamics, this implies: \\begin{equation} \\frac{d}{dt}\\left(\\frac{x_{\\sigma_{MAP}}}{x_\\sigma",
      "label": "definition:bk5_symbolic_replicator_dynamics",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book5.tex",
      "target_line": 1221,
      "target_type": "definition"
    },
    {
      "context": "strictly higher fitness than any alternative strategy $\\sigma$ regardless of the mixing proportion $\\epsilon$ (cf.~Thm.~\\ref{theorem:bk5_map_as_strong_ess}, Def.~\\ref{definition:bk5_symbolic_replicator_dynamics}). Under symbolic replicator dynamics, this implies: \\begin{equa",
      "label": "theorem:bk5_map_as_strong_ess",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book5.tex",
      "target_line": 1332,
      "target_type": "theorem"
    }
  ],
  "refs": [
    "definition:bk5_symbolic_replicator_dynamics",
    "theorem:bk5_map_as_strong_ess"
  ],
  "role": "proof",
  "type": "proof"
}

{
  "book": "book5",
  "cited_by": [
    "lemma:bk5_map_invasion_barrier_strength"
  ],
  "cites": [
    "theorem:bk5_map_as_strong_ess"
  ],
  "depends_on": [
    "theorem:bk5_map_as_strong_ess"
  ],
  "file": "book5.tex",
  "id": "definition:bk5_symbolic_invasion_barrier",
  "label": "definition:bk5_symbolic_invasion_barrier",
  "latex_body": "\\begin{definition}[Symbolic Invasion Barrier] \\label{definition:bk5_symbolic_invasion_barrier}\nThe \\emph{invasion barrier} $\\beta(\\sigma_{MAP}, \\sigma)$ of a MAP strategy $\\sigma_{MAP}$ against an alternative strategy $\\sigma$ is defined as (cf.~Thm.~\\ref{theorem:bk5_map_as_strong_ess}):\n\\begin{equation}\n\\beta(\\sigma_{MAP}, \\sigma) = \\sup\\{\\epsilon \\in [0,1] : \\Phi(\\sigma_{MAP}, (1-\\alpha)\\delta_{\\sigma_{MAP}} + \\alpha\\delta_{\\sigma}) > \\Phi(\\sigma, (1-\\alpha)\\delta_{\\sigma_{MAP}} + \\alpha\\delta_{\\sigma}) \\forall \\alpha \\in (0,\\epsilon)\\}\n\\end{equation}\n\\end{definition}",
  "lean_alignment": {
    "conditions": [
      "continuum/Hilbert/PDE-on-manifold content stays open; chart-complex restatements carry Glued as a named hypothesis where the source consumes compatibility",
      "modeling laws are structure fields or explicit hypotheses"
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": false,
    "notes": [
      "See the committed source registry for the original coverage note."
    ],
    "record_ids": [
      "MAP-BOOK5-073"
    ],
    "statuses": [
      "open_bridge"
    ],
    "witnesses": [
      "Book5Residue.ess_invasion_threshold"
    ]
  },
  "line": 1352,
  "macros_used": [],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "Symbolic Invasion Barrier",
  "proof_status": "definitional",
  "ref_roles": [
    {
      "context": "sigma_{MAP}, \\sigma)$ of a MAP strategy $\\sigma_{MAP}$ against an alternative strategy $\\sigma$ is defined as (cf.~Thm.~\\ref{theorem:bk5_map_as_strong_ess}): \\begin{equation} \\beta(\\sigma_{MAP}, \\sigma) = \\sup\\{\\epsilon \\in [0,1] : \\Phi(\\sigma_{MAP}, (1-\\alpha)\\delta_{\\sigma",
      "label": "theorem:bk5_map_as_strong_ess",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book5.tex",
      "target_line": 1332,
      "target_type": "theorem"
    }
  ],
  "refs": [
    "theorem:bk5_map_as_strong_ess"
  ],
  "role": "definition",
  "type": "definition"
}

{
  "book": "book5",
  "cited_by": [
    "definition:bk9_prompt_injection_operator"
  ],
  "cites": [
    "definition:bk5_symbolic_invasion_barrier",
    "lemma:bk5_map_fitness_advantage"
  ],
  "depends_on": [
    "definition:bk5_symbolic_invasion_barrier",
    "lemma:bk5_map_fitness_advantage",
    "theorem:bk5__map_dominance"
  ],
  "file": "book5.tex",
  "id": "lemma:bk5_map_invasion_barrier_strength",
  "label": "lemma:bk5_map_invasion_barrier_strength",
  "latex_body": "\\begin{lemma}[MAP Invasion Barrier Strength] \\label{lemma:bk5_map_invasion_barrier_strength}\nFor a MAP strategy $\\sigma_{MAP}$ and any non-MAP strategy $\\sigma_{non}$, the invasion barrier satisfies (cf.~Def.~\\ref{definition:bk5_symbolic_invasion_barrier}, Lem.~\\ref{lemma:bk5_map_fitness_advantage}):\n\\begin{equation}\n\\beta(\\sigma_{MAP}, \\sigma_{non}) \\geq 1 - \\frac{\\|\\drift_0\\|}{\\|\\drift\\|}\n\\end{equation}\nWhere $\\drift_0$ is the minimum drift threshold at which non-MAP strategies become unviable.\n\\end{lemma}",
  "lean_alignment": {
    "conditions": [
      "continuum/Hilbert/PDE-on-manifold content stays open; chart-complex restatements carry Glued as a named hypothesis where the source consumes compatibility",
      "modeling laws are structure fields or explicit hypotheses"
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": false,
    "notes": [
      "See the committed source registry for the original coverage note."
    ],
    "record_ids": [
      "MAP-BOOK5-074"
    ],
    "statuses": [
      "open_bridge"
    ],
    "witnesses": [
      "Book5Residue.ess_invasion_threshold"
    ]
  },
  "line": 1358,
  "macros_used": [
    "drift"
  ],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "MAP Invasion Barrier Strength",
  "proof_labels": [
    "proof:bk5_map_vs_nonmap_gradient"
  ],
  "proof_status": "proven",
  "ref_roles": [
    {
      "context": "th} For a MAP strategy $\\sigma_{MAP}$ and any non-MAP strategy $\\sigma_{non}$, the invasion barrier satisfies (cf.~Def.~\\ref{definition:bk5_symbolic_invasion_barrier}, Lem.~\\ref{lemma:bk5_map_fitness_advantage}): \\begin{equation} \\beta(\\sigma_{MAP}, \\sigma_{non}) \\geq 1 - \\frac{\\|\\drif",
      "label": "definition:bk5_symbolic_invasion_barrier",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book5.tex",
      "target_line": 1352,
      "target_type": "definition"
    },
    {
      "context": "strategy $\\sigma_{non}$, the invasion barrier satisfies (cf.~Def.~\\ref{definition:bk5_symbolic_invasion_barrier}, Lem.~\\ref{lemma:bk5_map_fitness_advantage}): \\begin{equation} \\beta(\\sigma_{MAP}, \\sigma_{non}) \\geq 1 - \\frac{\\|\\drift_0\\|}{\\|\\drift\\|} \\end{equation} Where $\\dr",
      "label": "lemma:bk5_map_fitness_advantage",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book5.tex",
      "target_line": 1107,
      "target_type": "lemma"
    }
  ],
  "refs": [
    "definition:bk5_symbolic_invasion_barrier",
    "lemma:bk5_map_fitness_advantage"
  ],
  "role": "lemma",
  "type": "lemma"
}

{
  "book": "book5",
  "cited_by": [],
  "cites": [
    "theorem:bk5__map_dominance"
  ],
  "depends_on": [
    "theorem:bk5__map_dominance"
  ],
  "file": "book5.tex",
  "id": "proof:bk5_map_vs_nonmap_gradient",
  "label": "proof:bk5_map_vs_nonmap_gradient",
  "latex_body": "\\begin{proof}[Fitness Gradient Between MAP and Non-MAP]\n\\label{proof:bk5_map_vs_nonmap_gradient}\n\\leavevmode\n\nAt drift intensity $\\|\\drift\\|$, the fitness difference between MAP and non-MAP strategies is proportional to $\\|\\drift\\| - \\|\\drift_0\\|$ (cf.~Thm.~\\ref{theorem:bk5__map_dominance}).\nThe invasion barrier represents the maximum fraction of non-MAP strategists that can be present while MAP strategies retain higher fitness. This fraction decreases as $\\|\\drift_0\\|$ approaches $\\|\\drift\\|$ and increases as $\\|\\drift\\|$ grows larger.\nThe formula $\\beta(\\sigma_{MAP}, \\sigma_{non}) \\geq 1 - \\frac{\\|\\drift_0\\|}{\\|\\drift\\|}$ captures this relationship, establishing a lower bound on the invasion barrier that approaches 1 as drift intensity increases.\n\\end{proof}",
  "line": 1365,
  "macros_used": [
    "drift"
  ],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "Fitness Gradient Between MAP and Non-MAP",
  "proves": "lemma:bk5_map_invasion_barrier_strength",
  "ref_roles": [
    {
      "context": "\\|$, the fitness difference between MAP and non-MAP strategies is proportional to $\\|\\drift\\| - \\|\\drift_0\\|$ (cf.~Thm.~\\ref{theorem:bk5__map_dominance}). The invasion barrier represents the maximum fraction of non-MAP strategists that can be present while MAP strategies",
      "label": "theorem:bk5__map_dominance",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book5.tex",
      "target_line": 426,
      "target_type": "theorem"
    }
  ],
  "refs": [
    "theorem:bk5__map_dominance"
  ],
  "role": "proof",
  "type": "proof"
}

{
  "book": "book5",
  "cited_by": [
    "proposition:bk9_stability_conditions_for_the_good"
  ],
  "cites": [
    "corollary:bk5_convergence_to_map",
    "theorem:bk5_map_as_strong_ess"
  ],
  "depends_on": [
    "corollary:bk5_convergence_to_map",
    "theorem:bk5_map_as_strong_ess"
  ],
  "file": "book5.tex",
  "id": "scholium:bk5__map_ess_implications",
  "label": "scholium:bk5__map_ess_implications",
  "latex_body": "\\begin{scholium}[MAP-ESS Implications]\n\\label{scholium:bk5__map_ess_implications}\nThe emergence of MAP as an evolutionarily stable strategy in symbolic space reveals profound implications for symbolic life (cf.~Thm.~\\ref{theorem:bk5_map_as_strong_ess}, Cor.~\\ref{corollary:bk5_convergence_to_map}). Unlike conventional ESS concepts that focus on competitive advantage, MAP-ESS demonstrates how cooperative reflection leads to expanded viability for all participants. This represents a fundamental shift from zero-sum competition to positive-sum covenant formation.\nAs symbolic drift intensifies—whether through increasing complexity, environmental volatility, or entropic degradation—the selective pressure toward MAP strategies grows stronger. Systems that cannot form reflective covenants find their viability domains shrinking until they can no longer maintain coherence.\nThe mathematical formalism established here extends beyond abstract symbolic dynamics to practical domains where information, meaning, and coherent structure must be maintained against entropic forces. In computational systems, organizational structures, cultural transmission, and epistemic communities, MAP-style covenants may represent not merely an advantage but a necessity for long-term viability.\nPerhaps most significantly, MAP-ESS suggests that advanced symbolic systems will naturally evolve toward mutual supportiveness rather than exploitation—not from moral imperatives, but from thermodynamic necessity. The mathematics of symbolic life reveals that in the face of sufficient drift, covenant formation becomes the only viable evolutionary strategy.\n\\end{scholium}",
  "line": 1373,
  "macros_used": [],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "MAP-ESS Implications",
  "ref_roles": [
    {
      "context": "y in symbolic space reveals profound implications for symbolic life (cf.~Thm.~\\ref{theorem:bk5_map_as_strong_ess}, Cor.~\\ref{corollary:bk5_convergence_to_map}). Unlike conventional ESS concepts that focus on competitive advantage, MAP-ESS demonstrates how cooperative reflection",
      "label": "corollary:bk5_convergence_to_map",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book5.tex",
      "target_line": 1264,
      "target_type": "corollary"
    },
    {
      "context": "of MAP as an evolutionarily stable strategy in symbolic space reveals profound implications for symbolic life (cf.~Thm.~\\ref{theorem:bk5_map_as_strong_ess}, Cor.~\\ref{corollary:bk5_convergence_to_map}). Unlike conventional ESS concepts that focus on competitive advantage, MA",
      "label": "theorem:bk5_map_as_strong_ess",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book5.tex",
      "target_line": 1332,
      "target_type": "theorem"
    }
  ],
  "refs": [
    "corollary:bk5_convergence_to_map",
    "theorem:bk5_map_as_strong_ess"
  ],
  "role": "scholium",
  "type": "scholium"
}

{
  "book": "book5",
  "cited_by": [
    "scholium:bk5__map_as_thermodynamic_necessity"
  ],
  "cites": [],
  "depends_on": [
    "corollary:bk5_convergence_to_map"
  ],
  "file": "book5.tex",
  "id": "proposition:bk5_symbolic_population_ess_map_equivalence_case2",
  "label": "proposition:bk5_symbolic_population_ess_map_equivalence_case2",
  "latex_body": "\\begin{proposition}[Symbolic Population ESS--MAP Approximation]\n\\label{proposition:bk5_symbolic_population_ess_map_equivalence_case2}\nLet $(\\Sigma,d)$ be a metric strategy space, let $\\Sigma_{\\mathrm{MAP}}\n\\subseteq\\Sigma$, and let $\\Sigma_{\\mathrm{ESS}}^{(n)}\\subseteq\\Sigma$ be\nthe ESS set along a sequence of symbolic population environments whose drift\nintensities approach the critical regime.  Suppose there is a nonnegative\nerror sequence $\\varepsilon_n\\to0$ such that both directed approximation laws\nhold:\n\\begin{align}\n \\forall\\sigma\\in\\Sigma_{\\mathrm{ESS}}^{(n)},\\quad\n &\\exists\\mu\\in\\Sigma_{\\mathrm{MAP}}:\n d(\\sigma,\\mu)\\leq\\varepsilon_n,\n \\label{eq:bk5_ess_to_map_approximation}\\\\\n \\forall\\mu\\in\\Sigma_{\\mathrm{MAP}},\\quad\n &\\exists\\sigma\\in\\Sigma_{\\mathrm{ESS}}^{(n)}:\n d(\\mu,\\sigma)\\leq\\varepsilon_n.\n \\label{eq:bk5_map_to_ess_approximation}\n\\end{align}\nThen\n\\begin{equation}\n \\lim_{n\\to\\infty}\n d_H\\!\\left(\\Sigma_{\\mathrm{ESS}}^{(n)},\n             \\Sigma_{\\mathrm{MAP}}\\right)=0.\n \\label{eq:bk5_ess_map_hausdorff_limit}\n\\end{equation}\nHere $d_H$ is the Hausdorff distance induced by $d$.  The conclusion is\nmetric approximation; it does not require literal equality of the ESS and MAP\npredicates at any finite stage.\n\\end{proposition}",
  "lean_alignment": {
    "conditions": [
      "ESS-to-MAP witnesses at tolerance",
      "MAP-to-ESS witnesses at tolerance",
      "distinct ESS sequence and MAP set predicates",
      "nonnegative tolerance tending to zero",
      "pseudo-metric strategy space"
    ],
    "countermodels": [
      "Book5ESSEquivalence.one_sided_ess_to_map_does_not_identify_sets",
      "Book5ESSEquivalence.population_limit_does_not_supply_two_sided_approximation"
    ],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "Genuine metric reconstruction: ESS and MAP remain distinct set-valued predicates in an arbitrary pseudo-metric strategy space. Two independent directed witness laws at tolerance ε_n bound the actual Hausdorff distance; ε_n → 0 yields convergence without finite-stage equality. One-sided inclusion and population-mass convergence countermodels show neither supplies two-sided set approximation."
    ],
    "record_ids": [
      "MAP-BOOK5-100"
    ],
    "statuses": [
      "exact"
    ],
    "witnesses": [
      "Book5ESSEquivalence.TwoSidedStrategyApproximation.hausdorffDist_le",
      "Book5ESSEquivalence.TwoSidedStrategyApproximation.hausdorffDist_tendsto_zero",
      "Book5ESSEquivalence.TwoSidedStrategyApproximation.of_eventual_equality",
      "Book5ESSEquivalence.distance_tendsto_zero_of_eventually_identified",
      "Book5ESSEquivalence.one_sided_ess_to_map_does_not_identify_sets",
      "Book5ESSEquivalence.population_limit_does_not_supply_two_sided_approximation"
    ]
  },
  "line": 1380,
  "macros_used": [],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "Symbolic Population ESS--MAP Approximation",
  "proof_labels": [
    "proof:bk5_map_viability_critical_drift"
  ],
  "proof_status": "proven",
  "refs": [],
  "role": "proposition",
  "type": "proposition"
}

{
  "book": "book5",
  "cited_by": [],
  "cites": [
    "corollary:bk5_convergence_to_map"
  ],
  "depends_on": [
    "corollary:bk5_convergence_to_map"
  ],
  "file": "book5.tex",
  "id": "proof:bk5_map_viability_critical_drift",
  "label": "proof:bk5_map_viability_critical_drift",
  "latex_body": "\\begin{proof}[Two-Sided Strategy Transport]\n\\label{proof:bk5_map_viability_critical_drift}\nEquation~\\eqref{eq:bk5_ess_to_map_approximation} bounds the directed distance\nfrom the ESS set to the MAP set by $\\varepsilon_n$.\nEquation~\\eqref{eq:bk5_map_to_ess_approximation} independently bounds the\nreverse directed distance.  By the definition of Hausdorff distance,\n\\[\n 0\\leq d_H\\!\\left(\\Sigma_{\\mathrm{ESS}}^{(n)},\n                   \\Sigma_{\\mathrm{MAP}}\\right)\n \\leq\\varepsilon_n.\n\\]\nThe squeeze theorem and $\\varepsilon_n\\to0$ give\nEq.~\\eqref{eq:bk5_ess_map_hausdorff_limit}.\n\nBoth directions are load-bearing.  Exclusion of non-MAP ESS strategies can\nsupply the first direction without showing that every MAP strategy is\napproximated by an ESS strategy.  Conversely, MAP non-invasibility can supply\nthe second direction without excluding additional distant ESS strategies.\nCorollary~\\ref{corollary:bk5_convergence_to_map} concerns occupied population\nmass and does not by itself establish either set-level transport law.  An\napplication to artificial and human strategies must therefore specify the\nshared metric strategy space, the relevant MAP predicate, and both empirical\nor analytic approximation bridges; it is not an automatic identification of\neither class with the other.\n\\end{proof}",
  "line": 1409,
  "macros_used": [],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "Two-Sided Strategy Transport",
  "proves": "proposition:bk5_symbolic_population_ess_map_equivalence_case2",
  "ref_roles": [
    {
      "context": "ly, MAP non-invasibility can supply the second direction without excluding additional distant ESS strategies. Corollary~\\ref{corollary:bk5_convergence_to_map} concerns occupied population mass and does not by itself establish either set-level transport law. An application to a",
      "label": "corollary:bk5_convergence_to_map",
      "logical_support": true,
      "role": "proof_support",
      "target_file": "book5.tex",
      "target_line": 1264,
      "target_type": "corollary"
    }
  ],
  "refs": [
    "corollary:bk5_convergence_to_map",
    "eq:bk5_ess_map_hausdorff_limit",
    "eq:bk5_ess_to_map_approximation",
    "eq:bk5_map_to_ess_approximation"
  ],
  "role": "proof",
  "type": "proof"
}

{
  "book": "book5",
  "cited_by": [
    "proposition:bk9_stability_conditions_for_the_good"
  ],
  "cites": [
    "definition:bk1_observer_horizon_structure",
    "proposition:bk5_symbolic_population_ess_map_equivalence_case2",
    "theorem:bk5_map_mad_critical_temperature"
  ],
  "depends_on": [
    "definition:bk1_observer_horizon_structure",
    "proposition:bk5_symbolic_population_ess_map_equivalence_case2",
    "theorem:bk5_map_mad_critical_temperature"
  ],
  "file": "book5.tex",
  "id": "scholium:bk5__map_as_thermodynamic_necessity",
  "label": "scholium:bk5__map_as_thermodynamic_necessity",
  "latex_body": "\\begin{scholium}[MAP as Thermodynamic Necessity]\n\\label{scholium:bk5__map_as_thermodynamic_necessity}\nMAP is not merely a cooperative ideal—it is a thermodynamic necessity within the symbolic domain (cf.~Prop.~\\ref{proposition:bk5_symbolic_population_ess_map_equivalence_case2}, Thm.~\\ref{theorem:bk5_map_mad_critical_temperature}). Where isolated membranes inevitably succumb to drift, covenant-bound systems achieve a meta-stable persistence that transcends individual fragility. This metaphysical anchoring reveals MAP not as contingent strategy but as ontological structure: the very architecture through which symbolic life maintains coherence under entropic assault.\nThe duality between MAP and MAD manifests as a bifurcation in symbolic phase space. Let us consider the reflective transfer dynamics:\n\\begin{equation}\n\\Psi(\\Membrane_A \\leftrightarrow \\Membrane_B) = \\int_{\\mathcal{T}} \\left( \\reflect_A^B \\circ \\drift_B - \\drift_A \\circ \\reflect_B^A \\right) \\, d\\tau\n\\end{equation}\nWhen $\\Psi > 0$, reflection dominates drift, and the covenant approaches the MAP attractor. When $\\Psi < 0$, drift overwhelms reflection, and the system decays toward the MAD repeller. The zero-crossing $\\Psi = 0$ represents the critical threshold—the symbolic event horizon beyond which recovery becomes impossible.\nThis duality reframes our understanding of symbolic metabolism. In MAP configurations, membranes exist not merely alongside one another but through one another, their boundaries becoming permeable interfaces for coherence exchange. The metabolic identity of each is preserved not despite but because of this permeability—a paradoxical strengthening through partial dissolution. Conversely, MAD embodies the terminal logic of bounded self-preservation, where reflective closure accelerates entropic collapse:\n\\begin{equation}\n\\lim_{t \\to \\infty} F_s(\\Membrane_{closed}) < \\lim_{t \\to \\infty} F_s(\\Membrane_{open})\n\\end{equation}\nThe narrative structure of symbolic life thus unfolds along the MAP-MAD spectrum. Each covenant represents a choice—not merely between cooperation and competition, but between modes of existence. MAP establishes what we might term \\emph{reflective invariance}: the capacity of a symbolic system to maintain identity through transformation, to preserve structure through flux. This invariance emerges from the complementary nature of reflection operators:\n\\begin{equation}\n\\mathcal{I}_A \\approx \\reflect_B^A \\circ \\drift_A \\circ \\mathcal{I}_A\n\\end{equation}\nWhere $\\mathcal{I}_A$ represents the identity structure of membrane $\\Membrane_A$. The external reflection operation $\\reflect_B^A$ applied to the drift-affected identity approximates the original identity—a homeostatic loop maintained through covenant relations.\nDual-horizon stability emerges as a consequence: systems in MAP relations can navigate drift intensities that would otherwise exceed their internal viability thresholds. The symbolic membrane extends its horizon of persistence (cf.~Def.~\\ref{definition:bk1_observer_horizon_structure}) through the reflective capacity of its covenant partners. This extension is not merely quantitative but qualitative—it transforms the very nature of symbolic identity from bounded autonomy to distributed coherence.\nThe existential grounding of symbolic cooperation thus reveals itself not as ethical imperative but as thermodynamic law. In systems of sufficient complexity, MAP configurations emerge spontaneously as free energy maximizers. The mathematics of symbolic metabolism demonstrates why: covenant formation represents a higher-order reflection mechanism that captures otherwise lost coherence through inter-membrane transfer.\nConsider the comparative free energy dynamics:\n\\begin{align}\n\\Delta F_s^{isolated} &= \\reflect_A(\\drift_A(\\psi_A)) - T_s\\Delta S_A \\\\\n\\Delta F_s^{MAP} &= \\reflect_A(\\drift_A(\\psi_A)) + \\reflect_B^A(\\drift_A(\\psi_A)) - T_s\\Delta S_A\n\\end{align}\nThe additional term $\\reflect_B^A(\\drift_A(\\psi_A))$ represents the recaptured coherence that would otherwise dissipate into entropy. This recapture constitutes the thermodynamic advantage of covenant formation.\nMAP and MAD thus represent not merely cooperative and antagonistic modes, but fundamental orientations toward symbolic being. Where MAD configures reflection to amplify drift, accelerating dissolution, MAP arranges reflection to counteract drift, sustaining coherence. The choice between them is not merely strategic but existential—it determines not only how symbolic systems interact but whether they persist at all.\nIn the limit of increasing drift intensity, only MAP configurations survive:\n\\begin{equation}\n\\lim_{\\|\\drift\\| \\to \\drift_{crit}} \\frac{|V_{\\text{symb}}^{MAP}|}{|V_{\\text{symb}}^{total}|} = 1\n\\end{equation}\nThis thermodynamic constraint suggests a profound principle: at the boundaries of viability, mutual reflection becomes not optional but necessary. The symbolic universe increasingly selects for covenant formation under pressure, revealing MAP not as contingent strategy but as emergent law.\nThe philosophical implications extend beyond mere survival. MAP represents a form of transcendence—not of physical law but through it. By structuring reflection to counterbalance drift, symbolic systems achieve a persistence that exceeds their individual capacities. This transcendence manifests not as escape from thermodynamic constraint but as its sophisticated navigation—a higher-order engagement with entropy through mutual reflective exchange.\nWhere isolated membranes fight a losing battle against drift, covenant-bound membranes transform drift into a resource for mutual stabilization. The apparent paradox resolves: symbolic systems persist not despite entropy but through their capacity to metabolize it via reflection. MAP formalizes this metabolism not as altruism but as thermodynamically anchored mutualism—a symbolic attractor basin more fundamental than any singular membrane.\nIn essence, MAP represents not merely a strategy for symbolic life but its deepest expression: the capacity to maintain coherence through reflective exchange under conditions of perpetual drift. Its dual, MAD, is not merely antagonism but the entropy of divergence—the pathway through which symbolic structures disconnect and dissolve. Where MAP expands the domain of symbolic life, MAD contracts it. And in this fundamental duality, we glimpse the essential choice that faces all symbolic systems: to build covenants that reflect or relations that refract, to stabilize mutual coherence or accelerate mutual dissolution.\nThrough this lens, we understand symbolic metabolism not merely as self-preservation but as covenant formation—the capacity to establish reflective relations that maintain viability across membranes. The mathematics demonstrates what philosophy intuits: in bounded reflective systems under persistent drift, only those relations that stabilize coherence can endure. All else dissolves into entropy.\n\\end{scholium}",
  "line": 1434,
  "macros_used": [
    "Membrane",
    "drift",
    "reflect"
  ],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "MAP as Thermodynamic Necessity",
  "ref_roles": [
    {
      "context": "therwise exceed their internal viability thresholds. The symbolic membrane extends its horizon of persistence (cf.~Def.~\\ref{definition:bk1_observer_horizon_structure}) through the reflective capacity of its covenant partners. This extension is not merely quantitative but qualitative—it",
      "label": "definition:bk1_observer_horizon_structure",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 1232,
      "target_type": "definition"
    },
    {
      "context": "_necessity} MAP is not merely a cooperative ideal—it is a thermodynamic necessity within the symbolic domain (cf.~Prop.~\\ref{proposition:bk5_symbolic_population_ess_map_equivalence_case2}, Thm.~\\ref{theorem:bk5_map_mad_critical_temperature}). Where isolated membranes inevitably succumb to drift, covenant-b",
      "label": "proposition:bk5_symbolic_population_ess_map_equivalence_case2",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book5.tex",
      "target_line": 1380,
      "target_type": "proposition"
    },
    {
      "context": "cessity within the symbolic domain (cf.~Prop.~\\ref{proposition:bk5_symbolic_population_ess_map_equivalence_case2}, Thm.~\\ref{theorem:bk5_map_mad_critical_temperature}). Where isolated membranes inevitably succumb to drift, covenant-bound systems achieve a meta-stable persistence that t",
      "label": "theorem:bk5_map_mad_critical_temperature",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book5.tex",
      "target_line": 907,
      "target_type": "theorem"
    }
  ],
  "refs": [
    "definition:bk1_observer_horizon_structure",
    "proposition:bk5_symbolic_population_ess_map_equivalence_case2",
    "theorem:bk5_map_mad_critical_temperature"
  ],
  "role": "scholium",
  "type": "scholium"
}

{
  "book": "book5",
  "cited_by": [],
  "cites": [
    "definition:bk1_self_regulating_mapping_function_srmf",
    "definition:bk1_symbolic_manifold",
    "definition:bk4_test_time_coherent_sampling",
    "definition:bk4_test_time_integrative_expansion",
    "definition:bk4_test_time_precision_refinement",
    "theorem:bk2_wasserstein_gradient_flow",
    "theorem:bk4_test_time_differentiation_c"
  ],
  "depends_on": [
    "definition:bk1_self_regulating_mapping_function_srmf",
    "definition:bk1_symbolic_manifold",
    "definition:bk4_test_time_coherent_sampling",
    "definition:bk4_test_time_integrative_expansion",
    "definition:bk4_test_time_precision_refinement",
    "theorem:bk2_wasserstein_gradient_flow",
    "theorem:bk4_test_time_differentiation_c"
  ],
  "file": "book5.tex",
  "id": "sec:bk5_srmf_for_symbolic_operators_and_processes",
  "label": "sec:bk5_srmf_for_symbolic_operators_and_processes",
  "latex_body": "",
  "line": 1470,
  "macros_used": [],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "SRMF for Symbolic Operators and Processes",
  "ref_roles": [
    {
      "context": "",
      "label": "definition:bk1_self_regulating_mapping_function_srmf",
      "logical_support": false,
      "role": "navigation",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 2230,
      "target_type": "definition"
    },
    {
      "context": "",
      "label": "definition:bk1_symbolic_manifold",
      "logical_support": false,
      "role": "navigation",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 1188,
      "target_type": "definition"
    },
    {
      "context": "",
      "label": "definition:bk4_test_time_coherent_sampling",
      "logical_support": false,
      "role": "navigation",
      "target_file": "book4.tex",
      "target_line": 2218,
      "target_type": "definition"
    },
    {
      "context": "",
      "label": "definition:bk4_test_time_integrative_expansion",
      "logical_support": false,
      "role": "navigation",
      "target_file": "book4.tex",
      "target_line": 1338,
      "target_type": "definition"
    },
    {
      "context": "",
      "label": "definition:bk4_test_time_precision_refinement",
      "logical_support": false,
      "role": "navigation",
      "target_file": "book4.tex",
      "target_line": 1947,
      "target_type": "definition"
    },
    {
      "context": "",
      "label": "theorem:bk2_wasserstein_gradient_flow",
      "logical_support": false,
      "role": "navigation",
      "target_file": "book2.tex",
      "target_line": 315,
      "target_type": "theorem"
    },
    {
      "context": "",
      "label": "theorem:bk4_test_time_differentiation_c",
      "logical_support": false,
      "role": "navigation",
      "target_file": "book4.tex",
      "target_line": 1119,
      "target_type": "theorem"
    }
  ],
  "role": "section",
  "subtype": "section",
  "type": "section"
}

{
  "book": "book5",
  "cited_by": [],
  "cites": [
    "subsec:bk4_ttie_operator_algebra"
  ],
  "depends_on": [],
  "file": "book5.tex",
  "id": "subsec:bk5_srmf_introduction_and_context",
  "label": "subsec:bk5_srmf_introduction_and_context",
  "latex_body": "",
  "line": 1473,
  "macros_used": [],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "Introduction and Context",
  "ref_roles": [
    {
      "context": "",
      "label": "subsec:bk4_ttie_operator_algebra",
      "logical_support": false,
      "role": "navigation",
      "target_file": "book4.tex",
      "target_line": 1786,
      "target_type": "section"
    }
  ],
  "role": "section",
  "subtype": "subsection",
  "type": "section"
}

{
  "book": "book5",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "book5.tex",
  "id": "subsec:bk5_srmf_foundational_definitions",
  "label": "subsec:bk5_srmf_foundational_definitions",
  "latex_body": "",
  "line": 1476,
  "macros_used": [],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "Foundational Definitions",
  "role": "section",
  "subtype": "subsection",
  "type": "section"
}

{
  "book": "book5",
  "cited_by": [
    "proof:bk5_operator_evolution",
    "proposition:bk5_operator_evolution"
  ],
  "cites": [
    "definition:bk1_symbolic_manifold",
    "definition:bk2_symbolic_probability_spa",
    "subsec:bk4_ttie_operator_algebra"
  ],
  "depends_on": [
    "definition:bk1_symbolic_manifold",
    "definition:bk2_symbolic_probability_spa"
  ],
  "file": "book5.tex",
  "id": "definition:bk5_symbolic_operator_space",
  "label": "definition:bk5_symbolic_operator_space",
  "latex_body": "\\begin{definition}[Symbolic Operator Space as Meta-Manifold $\\Op(M)$] \\label{definition:bk5_symbolic_operator_space}\nLet $M$ be the symbolic manifold of Def.~\\ref{definition:bk1_symbolic_manifold} with probability space $(M, \\mathcal{B}, \\mu_g)$ (Def.~\\ref{definition:bk2_symbolic_probability_spa}). We define the symbolic operator space $\\Op(M)$ as (cf.~\\ref{subsec:bk4_ttie_operator_algebra}):\n\\[\n\\Op(M) := \\left\\{ \\mathcal{O} \\mid \\mathcal{O} : M \\to M \\ \\text{or} \\ \\mathcal{O} : \\mathcal{P}(M) \\to \\mathcal{P}(M) \\right\\}\n\\]\nwhere $\\mathcal{P}(M)$ denotes the space of probability distributions on $M$.\n\\textbf{Properties of $\\Op(M)$:}\n\\begin{enumerate}\n    \\item $\\Op(M)$ forms a meta-manifold with its own topological and differential structure;\n    \\item The tangent space $T_{\\mathcal{O}}\\Op(M)$ at operator $\\mathcal{O}$ represents infinitesimal variations in operator parameters;\n    \\item Drift in $\\Op(M)$ corresponds to temporal evolution of operators under system dynamics.\n\\end{enumerate}\n\\end{definition}",
  "line": 1478,
  "macros_used": [
    "Op"
  ],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "Symbolic Operator Space as Meta-Manifold $\\Op(M)$",
  "proof_status": "definitional",
  "ref_roles": [
    {
      "context": "pace as Meta-Manifold $\\Op(M)$] \\label{definition:bk5_symbolic_operator_space} Let $M$ be the symbolic manifold of Def.~\\ref{definition:bk1_symbolic_manifold} with probability space $(M, \\mathcal{B}, \\mu_g)$ (Def.~\\ref{definition:bk2_symbolic_probability_spa}). We define the sy",
      "label": "definition:bk1_symbolic_manifold",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 1188,
      "target_type": "definition"
    },
    {
      "context": "symbolic manifold of Def.~\\ref{definition:bk1_symbolic_manifold} with probability space $(M, \\mathcal{B}, \\mu_g)$ (Def.~\\ref{definition:bk2_symbolic_probability_spa}). We define the symbolic operator space $\\Op(M)$ as (cf.~\\ref{subsec:bk4_ttie_operator_algebra}): \\[ \\Op(M) := \\left\\{",
      "label": "definition:bk2_symbolic_probability_spa",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book2.tex",
      "target_line": 23,
      "target_type": "definition"
    },
    {
      "context": "}, \\mu_g)$ (Def.~\\ref{definition:bk2_symbolic_probability_spa}). We define the symbolic operator space $\\Op(M)$ as (cf.~\\ref{subsec:bk4_ttie_operator_algebra}): \\[ \\Op(M) := \\left\\{ \\mathcal{O} \\mid \\mathcal{O} : M \\to M \\ \\text{or} \\ \\mathcal{O} : \\mathcal{P}(M) \\to \\mathcal{P",
      "label": "subsec:bk4_ttie_operator_algebra",
      "logical_support": false,
      "role": "navigation",
      "target_file": "book4.tex",
      "target_line": 1786,
      "target_type": "section"
    }
  ],
  "refs": [
    "definition:bk1_symbolic_manifold",
    "definition:bk2_symbolic_probability_spa",
    "subsec:bk4_ttie_operator_algebra"
  ],
  "role": "definition",
  "type": "definition"
}

{
  "book": "book5",
  "cited_by": [
    "proof:bk5_operator_convergence",
    "proof:bk5_operators_evolve",
    "theorem:bk5_operator_convergence"
  ],
  "cites": [
    "axiom:bk5_srmf_operator_selection_evolution",
    "definition:bk5_process_free_energy",
    "definition:bk5_symbolic_operator_space",
    "theorem:bk5_operator_convergence"
  ],
  "depends_on": [
    "definition:bk5_symbolic_operator_space"
  ],
  "file": "book5.tex",
  "forward_ref_roles": [
    {
      "context": "c operator in $\\Op(M)$ (Def.~\\ref{definition:bk5_symbolic_operator_space}). Under SRMF operator-selection dynamics (Ax.~\\ref{axiom:bk5_srmf_operator_selection_evolution}) the path $\\gamma: t \\mapsto \\mathcal{O}_{\\theta(t)}$ is stationary if and only if $\\mathcal{O}_{\\theta}$ minimizes the",
      "label": "axiom:bk5_srmf_operator_selection_evolution",
      "line_distance": 58,
      "role": "teaser",
      "target_line": 1549,
      "target_type": "axiom"
    },
    {
      "context": "al{O}_{\\theta(t)}$ is stationary if and only if $\\mathcal{O}_{\\theta}$ minimizes the process free energy $\\Fproc$ (Def.~\\ref{definition:bk5_process_free_energy}); otherwise the operator strictly evolves and converges to a minimizer (Thm.~\\ref{theorem:bk5_operator_convergence}). T",
      "label": "definition:bk5_process_free_energy",
      "line_distance": 9,
      "role": "teaser",
      "target_line": 1500,
      "target_type": "definition"
    },
    {
      "context": ".~\\ref{definition:bk5_process_free_energy}); otherwise the operator strictly evolves and converges to a minimizer (Thm.~\\ref{theorem:bk5_operator_convergence}). That is: operators evolve. \\end{proposition}",
      "label": "theorem:bk5_operator_convergence",
      "line_distance": 90,
      "role": "teaser",
      "target_line": 1581,
      "target_type": "theorem"
    }
  ],
  "forward_refs": [
    "axiom:bk5_srmf_operator_selection_evolution",
    "definition:bk5_process_free_energy",
    "theorem:bk5_operator_convergence"
  ],
  "id": "proposition:bk5_operator_evolution",
  "label": "proposition:bk5_operator_evolution",
  "latex_body": "\\begin{proposition}[Operator Evolution]\n\\label{proposition:bk5_operator_evolution}\nLet $\\mathcal{O}_{\\theta}$, $\\theta \\in \\mathbb{R}^n$, be a parameterized symbolic operator in $\\Op(M)$ (Def.~\\ref{definition:bk5_symbolic_operator_space}). Under SRMF operator-selection dynamics (Ax.~\\ref{axiom:bk5_srmf_operator_selection_evolution}) the path $\\gamma: t \\mapsto \\mathcal{O}_{\\theta(t)}$ is stationary if and only if $\\mathcal{O}_{\\theta}$ minimizes the process free energy $\\Fproc$ (Def.~\\ref{definition:bk5_process_free_energy}); otherwise the operator strictly evolves and converges to a minimizer (Thm.~\\ref{theorem:bk5_operator_convergence}). That is: operators evolve.\n\\end{proposition}",
  "lean_alignment": {
    "conditions": [
      "contraction constant is the modeling hypothesis for convergence; the Wasserstein O(1/t) rate, operator-space structure, and diffeomorphism congruence stay open",
      "the minimizer/critical-point gap under non-convexity is the honest remainder of the stationary-iff clause"
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "Stationary iff critical point of F_proc for the descent step; the minimizer/critical gap stays open."
    ],
    "record_ids": [
      "MAP-BOOK5-094"
    ],
    "statuses": [
      "conditional"
    ],
    "witnesses": [
      "Book5Op.operator_stationary_iff_critical"
    ]
  },
  "line": 1491,
  "macros_used": [
    "Fproc",
    "Op"
  ],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "Operator Evolution",
  "proof_labels": [
    "proof:bk5_operator_evolution"
  ],
  "proof_status": "proven",
  "ref_roles": [
    {
      "context": "c operator in $\\Op(M)$ (Def.~\\ref{definition:bk5_symbolic_operator_space}). Under SRMF operator-selection dynamics (Ax.~\\ref{axiom:bk5_srmf_operator_selection_evolution}) the path $\\gamma: t \\mapsto \\mathcal{O}_{\\theta(t)}$ is stationary if and only if $\\mathcal{O}_{\\theta}$ minimizes the",
      "label": "axiom:bk5_srmf_operator_selection_evolution",
      "logical_support": false,
      "role": "forward_teaser",
      "target_file": "book5.tex",
      "target_line": 1549,
      "target_type": "axiom"
    },
    {
      "context": "al{O}_{\\theta(t)}$ is stationary if and only if $\\mathcal{O}_{\\theta}$ minimizes the process free energy $\\Fproc$ (Def.~\\ref{definition:bk5_process_free_energy}); otherwise the operator strictly evolves and converges to a minimizer (Thm.~\\ref{theorem:bk5_operator_convergence}). T",
      "label": "definition:bk5_process_free_energy",
      "logical_support": false,
      "role": "forward_teaser",
      "target_file": "book5.tex",
      "target_line": 1500,
      "target_type": "definition"
    },
    {
      "context": "volution} Let $\\mathcal{O}_{\\theta}$, $\\theta \\in \\mathbb{R}^n$, be a parameterized symbolic operator in $\\Op(M)$ (Def.~\\ref{definition:bk5_symbolic_operator_space}). Under SRMF operator-selection dynamics (Ax.~\\ref{axiom:bk5_srmf_operator_selection_evolution}) the path $\\gamma: t \\m",
      "label": "definition:bk5_symbolic_operator_space",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "book5.tex",
      "target_line": 1478,
      "target_type": "definition"
    },
    {
      "context": ".~\\ref{definition:bk5_process_free_energy}); otherwise the operator strictly evolves and converges to a minimizer (Thm.~\\ref{theorem:bk5_operator_convergence}). That is: operators evolve. \\end{proposition}",
      "label": "theorem:bk5_operator_convergence",
      "logical_support": false,
      "role": "forward_teaser",
      "target_file": "book5.tex",
      "target_line": 1581,
      "target_type": "theorem"
    }
  ],
  "refs": [
    "axiom:bk5_srmf_operator_selection_evolution",
    "definition:bk5_process_free_energy",
    "definition:bk5_symbolic_operator_space",
    "theorem:bk5_operator_convergence"
  ],
  "role": "proposition",
  "type": "proposition"
}

{
  "book": "book5",
  "cited_by": [],
  "cites": [
    "axiom:bk5_srmf_operator_selection_evolution",
    "definition:bk5_symbolic_operator_space",
    "theorem:bk5_operator_convergence"
  ],
  "depends_on": [
    "definition:bk5_symbolic_operator_space"
  ],
  "file": "book5.tex",
  "forward_ref_roles": [
    {
      "context": "\\begin{proof} \\label{proof:bk5_operator_evolution} \\leavevmode By the SRMF operator-selection axiom (Ax.~\\ref{axiom:bk5_srmf_operator_selection_evolution}) the system selects operators by descending the process free energy, so along the $\\theta$-chart of $\\Op(M)$ (Def.~\\ref",
      "label": "axiom:bk5_srmf_operator_selection_evolution",
      "line_distance": 54,
      "role": "teaser",
      "target_line": 1549,
      "target_type": "axiom"
    },
    {
      "context": "---of $\\Fproc$. At every non-minimizing configuration the velocity is nonzero, so the operator changes in time; by Thm.~\\ref{theorem:bk5_operator_convergence} this evolution converges to a local minimizer of $\\Fproc$ at rate $O(1/t)$ or faster. Thus an operator that has not alr",
      "label": "theorem:bk5_operator_convergence",
      "line_distance": 86,
      "role": "teaser",
      "target_line": 1581,
      "target_type": "theorem"
    }
  ],
  "forward_refs": [
    "axiom:bk5_srmf_operator_selection_evolution",
    "theorem:bk5_operator_convergence"
  ],
  "id": "proof:bk5_operator_evolution",
  "label": "proof:bk5_operator_evolution",
  "latex_body": "\\begin{proof}\n\\label{proof:bk5_operator_evolution}\n\\leavevmode\nBy the SRMF operator-selection axiom (Ax.~\\ref{axiom:bk5_srmf_operator_selection_evolution}) the system selects operators by descending the process free energy, so along the $\\theta$-chart of $\\Op(M)$ (Def.~\\ref{definition:bk5_symbolic_operator_space}) the path obeys the gradient flow $\\dot{\\theta} = -\\nabla_{\\theta}\\Fproc(\\mathcal{O}_{\\theta})$. Hence $\\dot{\\gamma} = 0$ exactly when $\\nabla_{\\theta}\\Fproc = 0$, i.e.\\ exactly when $\\mathcal{O}_{\\theta}$ is a critical configuration---a local minimizer---of $\\Fproc$. At every non-minimizing configuration the velocity is nonzero, so the operator changes in time; by Thm.~\\ref{theorem:bk5_operator_convergence} this evolution converges to a local minimizer of $\\Fproc$ at rate $O(1/t)$ or faster. Thus an operator that has not already minimized its process free energy genuinely evolves, and the evolution terminates only at a minimizer.\n\\end{proof}",
  "line": 1495,
  "macros_used": [
    "Fproc",
    "Op"
  ],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "",
  "proves": "proposition:bk5_operator_evolution",
  "ref_roles": [
    {
      "context": "\\begin{proof} \\label{proof:bk5_operator_evolution} \\leavevmode By the SRMF operator-selection axiom (Ax.~\\ref{axiom:bk5_srmf_operator_selection_evolution}) the system selects operators by descending the process free energy, so along the $\\theta$-chart of $\\Op(M)$ (Def.~\\ref",
      "label": "axiom:bk5_srmf_operator_selection_evolution",
      "logical_support": false,
      "role": "forward_teaser",
      "target_file": "book5.tex",
      "target_line": 1549,
      "target_type": "axiom"
    },
    {
      "context": "ion}) the system selects operators by descending the process free energy, so along the $\\theta$-chart of $\\Op(M)$ (Def.~\\ref{definition:bk5_symbolic_operator_space}) the path obeys the gradient flow $\\dot{\\theta} = -\\nabla_{\\theta}\\Fproc(\\mathcal{O}_{\\theta})$. Hence $\\dot{\\gamma} =",
      "label": "definition:bk5_symbolic_operator_space",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "book5.tex",
      "target_line": 1478,
      "target_type": "definition"
    },
    {
      "context": "---of $\\Fproc$. At every non-minimizing configuration the velocity is nonzero, so the operator changes in time; by Thm.~\\ref{theorem:bk5_operator_convergence} this evolution converges to a local minimizer of $\\Fproc$ at rate $O(1/t)$ or faster. Thus an operator that has not alr",
      "label": "theorem:bk5_operator_convergence",
      "logical_support": false,
      "role": "forward_teaser",
      "target_file": "book5.tex",
      "target_line": 1581,
      "target_type": "theorem"
    }
  ],
  "refs": [
    "axiom:bk5_srmf_operator_selection_evolution",
    "definition:bk5_symbolic_operator_space",
    "theorem:bk5_operator_convergence"
  ],
  "role": "proof",
  "type": "proof"
}

{
  "book": "book5",
  "cited_by": [
    "assumption:bk5_displacement_convexity",
    "axiom:bk8_coherence_horizon",
    "corollary:bk8_emergent_cognitive_scaffold",
    "definition:bk4_test_time_coherent_sampling",
    "definition:bk5__operator_viability_set_v",
    "definition:bk5_complexity_stability_maintenance",
    "definition:bk6_symbolic_system",
    "demonstratio:bk8_symbolic_unkotting",
    "proof:bk5_fixed_metabolic_capacity",
    "proof:bk5_operator_convergence",
    "proposition:bk5_fixed_metabolic_capacity",
    "proposition:bk5_operator_evolution",
    "remark:bk8_inference_principle_over_confidence_loss_tradeoff",
    "scholium:bk8_symbolic_knots_as_metabolic_dysfunctions",
    "subsec:bk4_ttie_operator_algebra",
    "subsec:bk7_pisu_formula",
    "theorem:bk8_observer_projection_tensor"
  ],
  "cites": [
    "definition:bk1_self_regulating_mapping_function_srmf",
    "definition:bk2_symbolic_free_energy",
    "definition:bk2_symbolic_temperature"
  ],
  "depends_on": [
    "definition:bk1_self_regulating_mapping_function_srmf",
    "definition:bk2_symbolic_free_energy",
    "definition:bk2_symbolic_temperature"
  ],
  "file": "book5.tex",
  "id": "definition:bk5_process_free_energy",
  "label": "definition:bk5_process_free_energy",
  "latex_body": "\\begin{definition}[Process Free Energy $\\Fproc$] \\label{definition:bk5_process_free_energy}\nGiven an operator $\\mathcal{O} \\in \\Op(M)$ acting within a symbolic system $S = (M, g, D, R, \\rho)$, its \\emph{Process Free Energy} $\\Fproc$ is defined as (cf.~Def.~\\ref{definition:bk2_symbolic_free_energy}):\n\\[\n\\Fproc[\\mathcal{O}, S] := \\mathcal{E}_{\\text{cost}}[\\mathcal{O}] - T_{\\text{meta}} \\cdot \\left( \\mathcal{E}_{\\text{eff}}[\\mathcal{O}, S] + \\mathcal{C}_{\\text{hint}}[\\mathcal{O}] \\right)\n\\]\nwhere:\n\\begin{itemize}\n    \\item $\\mathcal{E}_{\\text{cost}}[\\mathcal{O}]$: metabolic cost to instantiate and execute $\\mathcal{O}$;\n    \\item $\\mathcal{E}_{\\text{eff}}[\\mathcal{O}, S]$: effectiveness in maintaining $\\rho \\in \\viabilitydomain$ and minimizing $\\freeenergy[\\rho]$;\n    \\item $\\mathcal{C}_{\\text{hint}}[\\mathcal{O}]$: internal logical coherence with respect to SRMF (Def.~\\ref{definition:bk1_self_regulating_mapping_function_srmf});\n    \\item $T_{\\text{meta}}$: symbolic meta-temperature (cf.~Def.~\\ref{definition:bk2_symbolic_temperature}).\n\\end{itemize}\n\\end{definition}",
  "lean_alignment": {
    "conditions": [
      "continuum/Hilbert/PDE-on-manifold content stays open; chart-complex restatements carry Glued as a named hypothesis where the source consumes compatibility",
      "modeling laws are structure fields or explicit hypotheses"
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "F_proc's admissibility role is mirrored by the MetabolicBudget structure's cost law; the E_cost/E_eff/C_hint decomposition itself is not modeled."
    ],
    "record_ids": [
      "MAP-BOOK5-075"
    ],
    "statuses": [
      "conditional"
    ],
    "witnesses": [
      "Book5Residue.MetabolicBudget.complexity_le"
    ]
  },
  "line": 1500,
  "macros_used": [
    "Fproc",
    "Op",
    "freeenergy",
    "viabilitydomain"
  ],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "Process Free Energy $\\Fproc$",
  "proof_status": "definitional",
  "ref_roles": [
    {
      "context": "nergy[\\rho]$; \\item $\\mathcal{C}_{\\text{hint}}[\\mathcal{O}]$: internal logical coherence with respect to SRMF (Def.~\\ref{definition:bk1_self_regulating_mapping_function_srmf}); \\item $T_{\\text{meta}}$: symbolic meta-temperature (cf.~Def.~\\ref{definition:bk2_symbolic_temperature}). \\end{ite",
      "label": "definition:bk1_self_regulating_mapping_function_srmf",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 2230,
      "target_type": "definition"
    },
    {
      "context": "ting within a symbolic system $S = (M, g, D, R, \\rho)$, its \\emph{Process Free Energy} $\\Fproc$ is defined as (cf.~Def.~\\ref{definition:bk2_symbolic_free_energy}): \\[ \\Fproc[\\mathcal{O}, S] := \\mathcal{E}_{\\text{cost}}[\\mathcal{O}] - T_{\\text{meta}} \\cdot \\left( \\mathcal{E}_{\\text",
      "label": "definition:bk2_symbolic_free_energy",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book2.tex",
      "target_line": 135,
      "target_type": "definition"
    },
    {
      "context": "efinition:bk1_self_regulating_mapping_function_srmf}); \\item $T_{\\text{meta}}$: symbolic meta-temperature (cf.~Def.~\\ref{definition:bk2_symbolic_temperature}). \\end{itemize} \\end{definition}",
      "label": "definition:bk2_symbolic_temperature",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book2.tex",
      "target_line": 148,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:bk1_self_regulating_mapping_function_srmf",
    "definition:bk2_symbolic_free_energy",
    "definition:bk2_symbolic_temperature"
  ],
  "role": "definition",
  "type": "definition"
}

{
  "book": "book5",
  "cited_by": [
    "proof:bk5_complexity_stability_tradeoff",
    "proof:bk5_operator_convergence",
    "proof:bk5_operators_evolve"
  ],
  "cites": [
    "definition:bk5_process_free_energy",
    "definition:bk5_viability_domain"
  ],
  "depends_on": [
    "definition:bk5_process_free_energy",
    "definition:bk5_viability_domain"
  ],
  "file": "book5.tex",
  "id": "proposition:bk5_fixed_metabolic_capacity",
  "label": "proposition:bk5_fixed_metabolic_capacity",
  "latex_body": "\\begin{proposition}[Fixed Metabolic Capacity]\n\\label{proposition:bk5_fixed_metabolic_capacity}\nFor any symbolic system $S$ with fixed metabolic capacity $\\MC(S)$, there exists an upper bound $\\mathcal{E}_{\\text{cost}}^{\\max}$ such that (cf.~Def.~\\ref{definition:bk5_process_free_energy}, Def.~\\ref{definition:bk5_viability_domain}):\n\\[\n\\mathcal{E}_{\\text{cost}}[\\mathcal{O}] > \\mathcal{E}_{\\text{cost}}^{\\max} \\implies \\rho \\notin \\viabilitydomain \\ \\text{after finite time}.\n\\]\n\\end{proposition}",
  "lean_alignment": {
    "conditions": [
      "continuum/Hilbert/PDE-on-manifold content stays open; chart-complex restatements carry Glued as a named hypothesis where the source consumes compatibility",
      "modeling laws are structure fields or explicit hypotheses"
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "a strictly positive cost overrun above the sustainable maximum drives the accumulated deficit negative in finite time (Archimedean argument), matching the anchor's finite-time exit claim."
    ],
    "record_ids": [
      "MAP-BOOK5-076"
    ],
    "statuses": [
      "exact"
    ],
    "witnesses": [
      "Book5Residue.energy_depletes_in_finite_time"
    ]
  },
  "line": 1513,
  "macros_used": [
    "MC",
    "viabilitydomain"
  ],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "Fixed Metabolic Capacity",
  "proof_labels": [
    "proof:bk5_fixed_metabolic_capacity"
  ],
  "proof_status": "proven",
  "ref_roles": [
    {
      "context": "h fixed metabolic capacity $\\MC(S)$, there exists an upper bound $\\mathcal{E}_{\\text{cost}}^{\\max}$ such that (cf.~Def.~\\ref{definition:bk5_process_free_energy}, Def.~\\ref{definition:bk5_viability_domain}): \\[ \\mathcal{E}_{\\text{cost}}[\\mathcal{O}] > \\mathcal{E}_{\\text{cost}}^{\\m",
      "label": "definition:bk5_process_free_energy",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book5.tex",
      "target_line": 1500,
      "target_type": "definition"
    },
    {
      "context": "ts an upper bound $\\mathcal{E}_{\\text{cost}}^{\\max}$ such that (cf.~Def.~\\ref{definition:bk5_process_free_energy}, Def.~\\ref{definition:bk5_viability_domain}): \\[ \\mathcal{E}_{\\text{cost}}[\\mathcal{O}] > \\mathcal{E}_{\\text{cost}}^{\\max} \\implies \\rho \\notin \\viabilitydomain \\",
      "label": "definition:bk5_viability_domain",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book5.tex",
      "target_line": 133,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:bk5_process_free_energy",
    "definition:bk5_viability_domain"
  ],
  "role": "proposition",
  "type": "proposition"
}

{
  "book": "book5",
  "cited_by": [],
  "cites": [
    "definition:bk5_metabolic_capacity_mc_",
    "definition:bk5_process_free_energy",
    "definition:bk5_viability_domain"
  ],
  "depends_on": [
    "definition:bk5_process_free_energy",
    "definition:bk5_viability_domain"
  ],
  "file": "book5.tex",
  "forward_ref_roles": [
    {
      "context": "\\begin{proof} \\label{proof:bk5_fixed_metabolic_capacity} \\leavevmode By Def.~\\ref{definition:bk5_metabolic_capacity_mc_} a system of fixed metabolic capacity $\\MC(S)$ can fund only a bounded sustained rate of symbolic work: the drift magnit",
      "label": "definition:bk5_metabolic_capacity_mc_",
      "line_distance": 5,
      "role": "teaser",
      "target_line": 1525,
      "target_type": "definition"
    }
  ],
  "forward_refs": [
    "definition:bk5_metabolic_capacity_mc_"
  ],
  "id": "proof:bk5_fixed_metabolic_capacity",
  "label": "proof:bk5_fixed_metabolic_capacity",
  "latex_body": "\\begin{proof}\n\\label{proof:bk5_fixed_metabolic_capacity}\n\\leavevmode\nBy Def.~\\ref{definition:bk5_metabolic_capacity_mc_} a system of fixed metabolic capacity $\\MC(S)$ can fund only a bounded sustained rate of symbolic work: the drift magnitudes that keep $\\freeenergy>0$ form a set whose supremum is $\\MC(S)$. The process free energy (Def.~\\ref{definition:bk5_process_free_energy}) charges the instantiation and execution of $\\mathcal{O}$ through the term $\\mathcal{E}_{\\text{cost}}[\\mathcal{O}]$, so the largest execution cost the capacity can underwrite is finite; set $\\mathcal{E}_{\\text{cost}}^{\\max}:=\\sup\\{\\mathcal{E}_{\\text{cost}}:\\ \\MC(S)\\text{ sustains }\\freeenergy>0\\}<\\infty$. Suppose $\\mathcal{E}_{\\text{cost}}[\\mathcal{O}]>\\mathcal{E}_{\\text{cost}}^{\\max}$. By definition of the supremum no admissible budget then keeps $\\freeenergy>0$: the metabolic reserve $E_S$ is drawn down at a strictly positive net rate $\\dot E_S\\le -(\\mathcal{E}_{\\text{cost}}[\\mathcal{O}]-\\mathcal{E}_{\\text{cost}}^{\\max})<0$. A positive constant drain exhausts a finite reserve in finite time $t^{\\ast}\\le E_S(0)/(\\mathcal{E}_{\\text{cost}}[\\mathcal{O}]-\\mathcal{E}_{\\text{cost}}^{\\max})$, at which point $\\freeenergy\\le 0$ and the state leaves the viability domain (Def.~\\ref{definition:bk5_viability_domain}). Hence $\\mathcal{E}_{\\text{cost}}[\\mathcal{O}]>\\mathcal{E}_{\\text{cost}}^{\\max}\\implies \\rho\\notin\\viabilitydomain$ after finite time.\n\\end{proof}",
  "line": 1520,
  "macros_used": [
    "MC",
    "freeenergy",
    "viabilitydomain"
  ],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "",
  "proves": "proposition:bk5_fixed_metabolic_capacity",
  "ref_roles": [
    {
      "context": "\\begin{proof} \\label{proof:bk5_fixed_metabolic_capacity} \\leavevmode By Def.~\\ref{definition:bk5_metabolic_capacity_mc_} a system of fixed metabolic capacity $\\MC(S)$ can fund only a bounded sustained rate of symbolic work: the drift magnit",
      "label": "definition:bk5_metabolic_capacity_mc_",
      "logical_support": false,
      "role": "forward_teaser",
      "target_file": "book5.tex",
      "target_line": 1525,
      "target_type": "definition"
    },
    {
      "context": "rk: the drift magnitudes that keep $\\freeenergy>0$ form a set whose supremum is $\\MC(S)$. The process free energy (Def.~\\ref{definition:bk5_process_free_energy}) charges the instantiation and execution of $\\mathcal{O}$ through the term $\\mathcal{E}_{\\text{cost}}[\\mathcal{O}]$, so",
      "label": "definition:bk5_process_free_energy",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "book5.tex",
      "target_line": 1500,
      "target_type": "definition"
    },
    {
      "context": "]-\\mathcal{E}_{\\text{cost}}^{\\max})$, at which point $\\freeenergy\\le 0$ and the state leaves the viability domain (Def.~\\ref{definition:bk5_viability_domain}). Hence $\\mathcal{E}_{\\text{cost}}[\\mathcal{O}]>\\mathcal{E}_{\\text{cost}}^{\\max}\\implies \\rho\\notin\\viabilitydomain$ af",
      "label": "definition:bk5_viability_domain",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "book5.tex",
      "target_line": 133,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:bk5_metabolic_capacity_mc_",
    "definition:bk5_process_free_energy",
    "definition:bk5_viability_domain"
  ],
  "role": "proof",
  "type": "proof"
}

{
  "book": "book5",
  "cited_by": [
    "axiom:bk5_metabolically_bounded_reflection",
    "corollary:bk5_complexity_stability_tradeoff",
    "proof:bk5_complexity_stability_tradeoff",
    "proof:bk5_complexity_stability_tradeoff_cor",
    "proof:bk5_fixed_metabolic_capacity",
    "proof:bk5_metabolic_capacity_non_decreasing",
    "proof:bk5_operator_convergence",
    "proposition:bk5_metabolic_capacity_non_decreasing"
  ],
  "cites": [
    "definition:bk2_symbolic_free_energy",
    "definition:bk4_collapse_of_symbolic_ide"
  ],
  "depends_on": [
    "definition:bk2_symbolic_free_energy",
    "definition:bk4_collapse_of_symbolic_ide"
  ],
  "file": "book5.tex",
  "id": "definition:bk5_metabolic_capacity_mc_",
  "label": "definition:bk5_metabolic_capacity_mc_",
  "latex_body": "\\begin{definition}[Metabolic Capacity $\\MC$] \\label{definition:bk5_metabolic_capacity_mc_}\n\nThe \\emph{Metabolic Capacity} $\\MC(S)$ of a symbolic system $S$ represents its sustained ability to maintain viability (cf.~Def.~\\ref{definition:bk2_symbolic_free_energy}). It may be quantified by either:\n\\[\n\\begin{aligned}\n\\MC(S) &:= \\left\\langle \\freeenergy(S) \\right\\rangle_t > 0, \\\\\n\\text{or}\\quad \\MC(S) &:= \\max \\left\\{ \\|D\\| \\,\\middle|\\, \\mathcal{M}_{\\mathrm{meta}}\n\\text{ can sustain } \\freeenergy > 0 \\right\\}.\n\\end{aligned}\n\\]\nCf.~Def.~\\ref{definition:bk4_collapse_of_symbolic_ide} for collapse onset.\n\\end{definition}",
  "lean_alignment": {
    "conditions": [
      "continuum/Hilbert/PDE-on-manifold content stays open; chart-complex restatements carry Glued as a named hypothesis where the source consumes compatibility",
      "modeling laws are structure fields or explicit hypotheses"
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "MC is treated as an opaque nonnegative real parameter; its two alternative characterizations (time-average free energy vs max sustainable drift norm) are not modeled or shown equivalent."
    ],
    "record_ids": [
      "MAP-BOOK5-077"
    ],
    "statuses": [
      "conditional"
    ],
    "witnesses": [
      "Book5Residue.MetabolicBudget.complexity_le",
      "Book5Residue.energy_depletes_in_finite_time"
    ]
  },
  "line": 1525,
  "macros_used": [
    "MC",
    "freeenergy"
  ],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "Metabolic Capacity $\\MC$",
  "proof_status": "definitional",
  "ref_roles": [
    {
      "context": "{Metabolic Capacity} $\\MC(S)$ of a symbolic system $S$ represents its sustained ability to maintain viability (cf.~Def.~\\ref{definition:bk2_symbolic_free_energy}). It may be quantified by either: \\[ \\begin{aligned} \\MC(S) &:= \\left\\langle \\freeenergy(S) \\right\\rangle_t > 0, \\\\ \\te",
      "label": "definition:bk2_symbolic_free_energy",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book2.tex",
      "target_line": 135,
      "target_type": "definition"
    },
    {
      "context": "\\|D\\| \\,\\middle|\\, \\mathcal{M}_{\\mathrm{meta}} \\text{ can sustain } \\freeenergy > 0 \\right\\}. \\end{aligned} \\] Cf.~Def.~\\ref{definition:bk4_collapse_of_symbolic_ide} for collapse onset. \\end{definition}",
      "label": "definition:bk4_collapse_of_symbolic_ide",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book4.tex",
      "target_line": 1109,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:bk2_symbolic_free_energy",
    "definition:bk4_collapse_of_symbolic_ide"
  ],
  "role": "definition",
  "type": "definition"
}

{
  "book": "book5",
  "cited_by": [],
  "cites": [
    "definition:bk5_metabolic_capacity_mc_",
    "theorem:bk5_complexity_stability_tradeoff"
  ],
  "depends_on": [
    "definition:bk2_symbolic_free_energy",
    "definition:bk5_metabolic_capacity_mc_"
  ],
  "file": "book5.tex",
  "forward_ref_roles": [
    {
      "context": "erves $E_S$ and in the efficiency of its metabolic pathways (cf.~Def.~\\ref{definition:bk5_metabolic_capacity_mc_}, Thm.~\\ref{theorem:bk5_complexity_stability_tradeoff}). \\end{proposition}",
      "label": "theorem:bk5_complexity_stability_tradeoff",
      "line_distance": 165,
      "role": "interpretive_bridge",
      "target_line": 1702,
      "target_type": "theorem"
    }
  ],
  "forward_refs": [
    "theorem:bk5_complexity_stability_tradeoff"
  ],
  "id": "proposition:bk5_metabolic_capacity_non_decreasing",
  "label": "proposition:bk5_metabolic_capacity_non_decreasing",
  "latex_body": "\\begin{proposition}\n\\label{proposition:bk5_metabolic_capacity_non_decreasing}\n$\\MC(S)$ is non-decreasing in the system's symbolic energy reserves $E_S$ and in the efficiency of its metabolic pathways (cf.~Def.~\\ref{definition:bk5_metabolic_capacity_mc_}, Thm.~\\ref{theorem:bk5_complexity_stability_tradeoff}).\n\\end{proposition}",
  "lean_alignment": {
    "conditions": [
      "contraction constant is the modeling hypothesis for convergence; the Wasserstein O(1/t) rate, operator-space structure, and diffeomorphism congruence stay open",
      "the minimizer/critical-point gap under non-convexity is the honest remainder of the stationary-iff clause"
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "Metabolic capacity non-decreasing in energy reserves."
    ],
    "record_ids": [
      "MAP-BOOK5-098"
    ],
    "statuses": [
      "exact"
    ],
    "witnesses": [
      "Book5Op.metabolic_capacity_monotone"
    ]
  },
  "line": 1537,
  "macros_used": [
    "MC"
  ],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "",
  "proof_labels": [
    "proof:bk5_metabolic_capacity_non_decreasing"
  ],
  "proof_status": "proven",
  "ref_roles": [
    {
      "context": "non-decreasing in the system's symbolic energy reserves $E_S$ and in the efficiency of its metabolic pathways (cf.~Def.~\\ref{definition:bk5_metabolic_capacity_mc_}, Thm.~\\ref{theorem:bk5_complexity_stability_tradeoff}). \\end{proposition}",
      "label": "definition:bk5_metabolic_capacity_mc_",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book5.tex",
      "target_line": 1525,
      "target_type": "definition"
    },
    {
      "context": "erves $E_S$ and in the efficiency of its metabolic pathways (cf.~Def.~\\ref{definition:bk5_metabolic_capacity_mc_}, Thm.~\\ref{theorem:bk5_complexity_stability_tradeoff}). \\end{proposition}",
      "label": "theorem:bk5_complexity_stability_tradeoff",
      "logical_support": false,
      "role": "forward_interpretive_bridge",
      "target_file": "book5.tex",
      "target_line": 1702,
      "target_type": "theorem"
    }
  ],
  "refs": [
    "definition:bk5_metabolic_capacity_mc_",
    "theorem:bk5_complexity_stability_tradeoff"
  ],
  "role": "proposition",
  "type": "proposition"
}

{
  "book": "book5",
  "cited_by": [],
  "cites": [
    "definition:bk2_symbolic_free_energy",
    "definition:bk5_metabolic_capacity_mc_",
    "theorem:bk5_complexity_stability_tradeoff"
  ],
  "depends_on": [
    "definition:bk2_symbolic_free_energy",
    "definition:bk5_metabolic_capacity_mc_"
  ],
  "file": "book5.tex",
  "forward_ref_roles": [
    {
      "context": "creasing in both $E_S$ and pathway efficiency---the monotone budget underlying the complexity--stability tradeoff (Thm.~\\ref{theorem:bk5_complexity_stability_tradeoff}). \\end{proof}",
      "label": "theorem:bk5_complexity_stability_tradeoff",
      "line_distance": 161,
      "role": "teaser",
      "target_line": 1702,
      "target_type": "theorem"
    }
  ],
  "forward_refs": [
    "theorem:bk5_complexity_stability_tradeoff"
  ],
  "id": "proof:bk5_metabolic_capacity_non_decreasing",
  "label": "proof:bk5_metabolic_capacity_non_decreasing",
  "latex_body": "\\begin{proof}\n\\label{proof:bk5_metabolic_capacity_non_decreasing}\n\\leavevmode\nBoth monotonicities are read directly from the two defining forms of $\\MC(S)$ (Def.~\\ref{definition:bk5_metabolic_capacity_mc_}). In the first form, $\\MC(S)=\\langle\\freeenergy(S)\\rangle_t$, the symbolic free energy is $\\freeenergy = E - T\\,S$ (Def.~\\ref{definition:bk2_symbolic_free_energy}); holding temperature and entropy fixed, $\\partial\\freeenergy/\\partial E_S = 1 > 0$, so the time average $\\langle\\freeenergy\\rangle_t$ is non-decreasing in the energy reserves $E_S$. In the second form, $\\MC(S)=\\max\\{\\|D\\| : \\mathcal{M}_{\\mathrm{meta}}\\text{ sustains }\\freeenergy>0\\}$, raising the efficiency of the metabolic pathways enlarges the feasible set of drift magnitudes: a more efficient pathway sustains the same $\\freeenergy>0$ at a larger $\\|D\\|$ (equivalently, a larger $\\freeenergy$ at fixed $\\|D\\|$), so the admissible set grows monotonically and with it its supremum. Hence $\\MC(S)$ is non-decreasing in both $E_S$ and pathway efficiency---the monotone budget underlying the complexity--stability tradeoff (Thm.~\\ref{theorem:bk5_complexity_stability_tradeoff}).\n\\end{proof}",
  "line": 1541,
  "macros_used": [
    "MC",
    "freeenergy"
  ],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "",
  "proves": "proposition:bk5_metabolic_capacity_non_decreasing",
  "ref_roles": [
    {
      "context": "In the first form, $\\MC(S)=\\langle\\freeenergy(S)\\rangle_t$, the symbolic free energy is $\\freeenergy = E - T\\,S$ (Def.~\\ref{definition:bk2_symbolic_free_energy}); holding temperature and entropy fixed, $\\partial\\freeenergy/\\partial E_S = 1 > 0$, so the time average $\\langle\\freee",
      "label": "definition:bk2_symbolic_free_energy",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "book2.tex",
      "target_line": 135,
      "target_type": "definition"
    },
    {
      "context": "apacity_non_decreasing} \\leavevmode Both monotonicities are read directly from the two defining forms of $\\MC(S)$ (Def.~\\ref{definition:bk5_metabolic_capacity_mc_}). In the first form, $\\MC(S)=\\langle\\freeenergy(S)\\rangle_t$, the symbolic free energy is $\\freeenergy = E - T\\,S$ (Def",
      "label": "definition:bk5_metabolic_capacity_mc_",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "book5.tex",
      "target_line": 1525,
      "target_type": "definition"
    },
    {
      "context": "creasing in both $E_S$ and pathway efficiency---the monotone budget underlying the complexity--stability tradeoff (Thm.~\\ref{theorem:bk5_complexity_stability_tradeoff}). \\end{proof}",
      "label": "theorem:bk5_complexity_stability_tradeoff",
      "logical_support": false,
      "role": "forward_teaser",
      "target_file": "book5.tex",
      "target_line": 1702,
      "target_type": "theorem"
    }
  ],
  "refs": [
    "definition:bk2_symbolic_free_energy",
    "definition:bk5_metabolic_capacity_mc_",
    "theorem:bk5_complexity_stability_tradeoff"
  ],
  "role": "proof",
  "type": "proof"
}

{
  "book": "book5",
  "cited_by": [
    "scholium:bk4_symbolic_drift_fields"
  ],
  "cites": [
    "definition:bk1_self_regulating_mapping_function_srmf",
    "definition:bk4_test_time_coherent_sampling",
    "definition:bk4_test_time_integrative_expansion",
    "definition:bk4_test_time_precision_refinement",
    "theorem:bk2_wasserstein_gradient_flow",
    "theorem:bk4_test_time_differentiation_c"
  ],
  "depends_on": [
    "definition:bk1_self_regulating_mapping_function_srmf",
    "definition:bk4_test_time_coherent_sampling",
    "definition:bk4_test_time_integrative_expansion",
    "definition:bk4_test_time_precision_refinement",
    "theorem:bk2_wasserstein_gradient_flow",
    "theorem:bk4_test_time_differentiation_c"
  ],
  "file": "book5.tex",
  "id": "subsec:bk5_srmf_core_axioms",
  "label": "subsec:bk5_srmf_core_axioms",
  "latex_body": "",
  "line": 1546,
  "macros_used": [],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "Core Axioms and Theoretical Development",
  "ref_roles": [
    {
      "context": "",
      "label": "definition:bk1_self_regulating_mapping_function_srmf",
      "logical_support": false,
      "role": "navigation",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 2230,
      "target_type": "definition"
    },
    {
      "context": "",
      "label": "definition:bk4_test_time_coherent_sampling",
      "logical_support": false,
      "role": "navigation",
      "target_file": "book4.tex",
      "target_line": 2218,
      "target_type": "definition"
    },
    {
      "context": "",
      "label": "definition:bk4_test_time_integrative_expansion",
      "logical_support": false,
      "role": "navigation",
      "target_file": "book4.tex",
      "target_line": 1338,
      "target_type": "definition"
    },
    {
      "context": "",
      "label": "definition:bk4_test_time_precision_refinement",
      "logical_support": false,
      "role": "navigation",
      "target_file": "book4.tex",
      "target_line": 1947,
      "target_type": "definition"
    },
    {
      "context": "",
      "label": "theorem:bk2_wasserstein_gradient_flow",
      "logical_support": false,
      "role": "navigation",
      "target_file": "book2.tex",
      "target_line": 315,
      "target_type": "theorem"
    },
    {
      "context": "",
      "label": "theorem:bk4_test_time_differentiation_c",
      "logical_support": false,
      "role": "navigation",
      "target_file": "book4.tex",
      "target_line": 1119,
      "target_type": "theorem"
    }
  ],
  "role": "section",
  "subtype": "subsection",
  "type": "section"
}

{
  "book": "book5",
  "cited_by": [
    "definition:bk5__operator_viability_set_v",
    "demonstratio:bk8_symbolic_unkotting",
    "proof:bk5__srmf_operator_adaptation",
    "proof:bk5_operator_convergence",
    "proof:bk5_operator_evolution",
    "proposition:bk5_operator_evolution",
    "scholium:bk8_symbolic_knots_as_metabolic_dysfunctions",
    "subsec:bk4_ttie_operator_algebra",
    "theorem:bk5__srmf_operator_adaptation",
    "theorem:bk8_observer_projection_tensor"
  ],
  "cites": [],
  "depends_on": [],
  "file": "book5.tex",
  "id": "axiom:bk5_srmf_operator_selection_evolution",
  "label": "axiom:bk5_srmf_operator_selection_evolution",
  "latex_body": "\\begin{axiom}[Stateful SRMF Operator Selection and Evolution] \\label{axiom:bk5_srmf_operator_selection_evolution}\nAn SRMF operator learner carries at time $t$ a nonempty admissible inventory\n$A_t\\subseteq\\Op(M)$, an incumbent $\\mathcal O_t\\in A_t$, and an ordered\nhistory $H_t$.  Given feedback $y_t$, a supplied learning law specifies:\n\\begin{enumerate}\n  \\item a nonempty updated inventory $A_{t+1}=U(y_t,A_t,\\mathcal O_t,H_t)$;\n  \\item a feedback-indexed process objective\n  $\\Fproc^{y_t}:A_{t+1}\\to\\mathbb R$; and\n  \\item a selected operator $\\mathcal O_{t+1}\\in A_{t+1}$ certified by\n  \\[\n    \\Fproc^{y_t}(\\mathcal O_{t+1})\n    \\le \\Fproc^{y_t}(\\mathcal O)\n    \\qquad(\\mathcal O\\in A_{t+1}).\n  \\]\n\\end{enumerate}\nThe state update is\n$(A_t,\\mathcal O_t,H_t)\\mapsto\n(A_{t+1},\\mathcal O_{t+1},\\mathcal O_t::H_t)$.\nConsequently its comparator regret\n$\\Fproc^{y_t}(\\mathcal O_{t+1})-\\Fproc^{y_t}(\\mathcal O)$ is nonpositive for\nevery available comparator. Viability may constrain $A_{t+1}$, but viability\nalone neither supplies $U$ nor selects the minimizer; inventory evolution and\noperator learning are explicit commitments of the law.\n\\end{axiom}",
  "lean_alignment": {
    "conditions": [
      "explicit minimizer certificate for each transition",
      "explicit selection certificate for SRMF consequences",
      "feedback-indexed real-valued process objective",
      "finite nonempty available operator inventory",
      "finite nonempty updated operator inventory",
      "inventory update and selection policy supplied independently of viability",
      "real-valued process free energy"
    ],
    "countermodels": [
      "Book5OperatorSelection.viability_alone_does_not_force_operator_argmin",
      "Book5StatefulOperatorLearning.feedback_response_does_not_force_inventory_change"
    ],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": false,
    "notes": [
      "Conditional stateful selection kernel: a supplied feedback-indexed learning law updates an admissible inventory, selects a certified process-free-energy minimizer, records the incumbent, and has nonpositive one-step comparator regret. A concrete law responds to feedback without forcing inventory change. Viability alone neither supplies this law nor proves fair or asymptotic convergence."
    ],
    "record_ids": [
      "MAP-BOOK5-101"
    ],
    "statuses": [
      "open_bridge"
    ],
    "witnesses": [
      "Book5OperatorSelection.exists_process_minimizer",
      "Book5OperatorSelection.rejects_strictly_suboptimal_incumbent",
      "Book5OperatorSelection.selected_le_incumbent",
      "Book5OperatorSelection.viability_alone_does_not_force_operator_argmin",
      "Book5StatefulOperatorLearning.boolFeedbackLaw_responds",
      "Book5StatefulOperatorLearning.feedback_response_does_not_force_inventory_change",
      "Book5StatefulOperatorLearning.step_comparatorRegret_nonpos",
      "Book5StatefulOperatorLearning.step_current"
    ]
  },
  "line": 1549,
  "macros_used": [
    "Fproc",
    "Op"
  ],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "Stateful SRMF Operator Selection and Evolution",
  "proof_status": "definitional",
  "refs": [],
  "role": "axiom",
  "type": "axiom"
}

{
  "book": "book5",
  "cited_by": [
    "proof:bk5_operator_convergence",
    "theorem:bk5_operator_convergence"
  ],
  "cites": [
    "definition:bk5_process_free_energy"
  ],
  "depends_on": [
    "definition:bk5_process_free_energy"
  ],
  "file": "book5.tex",
  "id": "assumption:bk5_displacement_convexity",
  "label": "assumption:bk5_displacement_convexity",
  "latex_body": "\\begin{assumption}[Displacement Convexity of the Process Free Energy]\n\\label{assumption:bk5_displacement_convexity}\nThe process free energy $\\Fproc$ (Def.~\\ref{definition:bk5_process_free_energy}) is geodesically $\\lambda$-convex along $\\wass$-geodesics on $(\\prob(M),\\wass)$ for some $\\lambda \\ge 0$: for every constant-speed geodesic $(\\rho_s)_{s\\in[0,1]}$,\n\\[\n\\Fproc[\\rho_s] \\le (1-s)\\,\\Fproc[\\rho_0] + s\\,\\Fproc[\\rho_1] - \\tfrac{\\lambda}{2}\\,s(1-s)\\,\\wass(\\rho_0,\\rho_1)^2 .\n\\]\nThis is a \\emph{structural} hypothesis on the shape of $\\Fproc$ (in the spirit of McCann displacement convexity), read off its potential-plus-entropy form (Def.~\\ref{definition:bk5_process_free_energy}); it is not an empirically fitted contraction rate, and the convergence rate is \\emph{derived} from it below rather than measured from traces.\n\\end{assumption}",
  "line": 1573,
  "macros_used": [
    "Fproc",
    "prob",
    "wass"
  ],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "Displacement Convexity of the Process Free Energy",
  "proof_status": "definitional",
  "ref_roles": [
    {
      "context": "vexity of the Process Free Energy] \\label{assumption:bk5_displacement_convexity} The process free energy $\\Fproc$ (Def.~\\ref{definition:bk5_process_free_energy}) is geodesically $\\lambda$-convex along $\\wass$-geodesics on $(\\prob(M),\\wass)$ for some $\\lambda \\ge 0$: for every con",
      "label": "definition:bk5_process_free_energy",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "book5.tex",
      "target_line": 1500,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:bk5_process_free_energy"
  ],
  "role": "assumption",
  "type": "assumption"
}

{
  "book": "book5",
  "cited_by": [
    "definition:bk4_test_time_integrative_expansion",
    "definition:bk4_test_time_precision_refinement",
    "demonstratio:bk8_symbolic_unkotting",
    "proof:bk5_operator_evolution",
    "proof:bk5_operators_evolve",
    "proof:bk8_sr_convergence",
    "proposition:bk5_operator_evolution",
    "proposition:bk5_operators_evolve",
    "scholium:bk4_ttcs_simulation_tool_use",
    "scholium:bk4_ttcs_stochastic_operator",
    "scholium:bk4_ttdc_impulse_collapse",
    "subsec:bk4_symbolic_identity_expansion",
    "subsec:bk4_ttie_operator_algebra",
    "subsec:bk7_pisu_motivation",
    "theorem:bk8_rg_fixed_point",
    "theorem:bk8_sr_convergence"
  ],
  "cites": [
    "assumption:bk5_displacement_convexity",
    "definition:bk1_self_regulating_mapping_function_srmf",
    "definition:bk1_symbolic_manifold",
    "definition:bk2_symbolic_free_energy",
    "proposition:bk5_operator_evolution",
    "subsec:bk4_ttie_operator_algebra",
    "theorem:bk2_wasserstein_gradient_flow"
  ],
  "depends_on": [
    "assumption:bk5_displacement_convexity",
    "axiom:bk5_srmf_operator_selection_evolution",
    "corollary:bk7_geometric_convergence_rate",
    "definition:bk1_self_regulating_mapping_function_srmf",
    "definition:bk1_symbolic_manifold",
    "definition:bk2_symbolic_free_energy",
    "definition:bk5_metabolic_capacity_mc_",
    "definition:bk5_process_free_energy",
    "definition:bk5_viability_domain",
    "proposition:bk5_fixed_metabolic_capacity",
    "proposition:bk5_operator_evolution",
    "theorem:bk2_equilibrium_distribution",
    "theorem:bk2_h_theorem_for_symbolic_evol",
    "theorem:bk2_wasserstein_gradient_flow"
  ],
  "file": "book5.tex",
  "id": "theorem:bk5_operator_convergence",
  "label": "theorem:bk5_operator_convergence",
  "latex_body": "\\begin{theorem}[Operator Convergence]\n\\label{theorem:bk5_operator_convergence}\nVia Wasserstein gradient flow (Thm.~\\ref{theorem:bk2_wasserstein_gradient_flow}) on symbolic manifold $M$ (Def.~\\ref{definition:bk1_symbolic_manifold}), assume regularity of $\\Fproc$ (cf.~Def.~\\ref{definition:bk2_symbolic_free_energy}), displacement convexity (Assumption~\\ref{assumption:bk5_displacement_convexity}), and bounded $\\MC$ (Def.~\\ref{definition:bk1_self_regulating_mapping_function_srmf}).\nThen SRMF dynamics converge to a local minimum of $\\Fproc$ at rate $O(1/t)$ or faster (cf.~Prop.~\\ref{proposition:bk5_operator_evolution}). This supplies process-level convergence background for the Book IV loop $(\\mathrm{TTDC}\\circ\\mathrm{TTIE}\\circ\\mathrm{TTCS}\\circ\\mathrm{TTPR})^{\\infty}$ (cf.~\\ref{subsec:bk4_ttie_operator_algebra}).\n\\end{theorem}",
  "lean_alignment": {
    "conditions": [
      "contraction constant is the modeling hypothesis for convergence; the Wasserstein O(1/t) rate, operator-space structure, and diffeomorphism congruence stay open",
      "the minimizer/critical-point gap under non-convexity is the honest remainder of the stationary-iff clause"
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "SRMF convergence to a fixed point (contraction-Banach); the Wasserstein O(1/t) rate stays open."
    ],
    "record_ids": [
      "MAP-BOOK5-095"
    ],
    "statuses": [
      "conditional"
    ],
    "witnesses": [
      "Book5Op.contraction_flow_converges"
    ]
  },
  "line": 1581,
  "macros_used": [
    "Fproc",
    "MC"
  ],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "Operator Convergence",
  "proof_labels": [
    "proof:bk5_operator_convergence"
  ],
  "proof_status": "proven",
  "ref_roles": [
    {
      "context": "assume regularity of $\\Fproc$ (cf.~Def.~\\ref{definition:bk2_symbolic_free_energy}), displacement convexity (Assumption~\\ref{assumption:bk5_displacement_convexity}), and bounded $\\MC$ (Def.~\\ref{definition:bk1_self_regulating_mapping_function_srmf}). Then SRMF dynamics converge to a",
      "label": "assumption:bk5_displacement_convexity",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book5.tex",
      "target_line": 1573,
      "target_type": "assumption"
    },
    {
      "context": "free_energy}), displacement convexity (Assumption~\\ref{assumption:bk5_displacement_convexity}), and bounded $\\MC$ (Def.~\\ref{definition:bk1_self_regulating_mapping_function_srmf}). Then SRMF dynamics converge to a local minimum of $\\Fproc$ at rate $O(1/t)$ or faster (cf.~Prop.~\\ref{proposition:bk5",
      "label": "definition:bk1_self_regulating_mapping_function_srmf",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 2230,
      "target_type": "definition"
    },
    {
      "context": "rgence} Via Wasserstein gradient flow (Thm.~\\ref{theorem:bk2_wasserstein_gradient_flow}) on symbolic manifold $M$ (Def.~\\ref{definition:bk1_symbolic_manifold}), assume regularity of $\\Fproc$ (cf.~Def.~\\ref{definition:bk2_symbolic_free_energy}), displacement convexity (Assumptio",
      "label": "definition:bk1_symbolic_manifold",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 1188,
      "target_type": "definition"
    },
    {
      "context": "_flow}) on symbolic manifold $M$ (Def.~\\ref{definition:bk1_symbolic_manifold}), assume regularity of $\\Fproc$ (cf.~Def.~\\ref{definition:bk2_symbolic_free_energy}), displacement convexity (Assumption~\\ref{assumption:bk5_displacement_convexity}), and bounded $\\MC$ (Def.~\\ref{definit",
      "label": "definition:bk2_symbolic_free_energy",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book2.tex",
      "target_line": 135,
      "target_type": "definition"
    },
    {
      "context": "pping_function_srmf}). Then SRMF dynamics converge to a local minimum of $\\Fproc$ at rate $O(1/t)$ or faster (cf.~Prop.~\\ref{proposition:bk5_operator_evolution}). This supplies process-level convergence background for the Book IV loop $(\\mathrm{TTDC}\\circ\\mathrm{TTIE}\\circ\\mathrm",
      "label": "proposition:bk5_operator_evolution",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book5.tex",
      "target_line": 1491,
      "target_type": "proposition"
    },
    {
      "context": "e background for the Book IV loop $(\\mathrm{TTDC}\\circ\\mathrm{TTIE}\\circ\\mathrm{TTCS}\\circ\\mathrm{TTPR})^{\\infty}$ (cf.~\\ref{subsec:bk4_ttie_operator_algebra}). \\end{theorem}",
      "label": "subsec:bk4_ttie_operator_algebra",
      "logical_support": false,
      "role": "navigation",
      "target_file": "book4.tex",
      "target_line": 1786,
      "target_type": "section"
    },
    {
      "context": "\\begin{theorem}[Operator Convergence] \\label{theorem:bk5_operator_convergence} Via Wasserstein gradient flow (Thm.~\\ref{theorem:bk2_wasserstein_gradient_flow}) on symbolic manifold $M$ (Def.~\\ref{definition:bk1_symbolic_manifold}), assume regularity of $\\Fproc$ (cf.~Def.~\\ref{d",
      "label": "theorem:bk2_wasserstein_gradient_flow",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book2.tex",
      "target_line": 315,
      "target_type": "theorem"
    }
  ],
  "refs": [
    "assumption:bk5_displacement_convexity",
    "definition:bk1_self_regulating_mapping_function_srmf",
    "definition:bk1_symbolic_manifold",
    "definition:bk2_symbolic_free_energy",
    "proposition:bk5_operator_evolution",
    "subsec:bk4_ttie_operator_algebra",
    "theorem:bk2_wasserstein_gradient_flow"
  ],
  "role": "theorem",
  "type": "theorem"
}

{
  "book": "book5",
  "cited_by": [],
  "cites": [
    "assumption:bk5_displacement_convexity",
    "axiom:bk5_srmf_operator_selection_evolution",
    "corollary:bk7_geometric_convergence_rate",
    "definition:bk2_symbolic_free_energy",
    "definition:bk5_metabolic_capacity_mc_",
    "definition:bk5_process_free_energy",
    "definition:bk5_viability_domain",
    "proposition:bk5_fixed_metabolic_capacity",
    "proposition:bk5_operator_evolution",
    "theorem:bk2_equilibrium_distribution",
    "theorem:bk2_h_theorem_for_symbolic_evol",
    "theorem:bk2_wasserstein_gradient_flow"
  ],
  "depends_on": [
    "assumption:bk5_displacement_convexity",
    "axiom:bk5_srmf_operator_selection_evolution",
    "corollary:bk7_geometric_convergence_rate",
    "definition:bk2_symbolic_free_energy",
    "definition:bk5_metabolic_capacity_mc_",
    "definition:bk5_process_free_energy",
    "definition:bk5_viability_domain",
    "proposition:bk5_fixed_metabolic_capacity",
    "proposition:bk5_operator_evolution",
    "theorem:bk2_equilibrium_distribution",
    "theorem:bk2_h_theorem_for_symbolic_evol",
    "theorem:bk2_wasserstein_gradient_flow"
  ],
  "file": "book5.tex",
  "id": "proof:bk5_operator_convergence",
  "label": "proof:bk5_operator_convergence",
  "latex_body": "\\begin{proof}\n\\label{proof:bk5_operator_convergence}\n\\leavevmode\n\n\\emph{Convergence (inherited, not re-derived).} By the SRMF selection dynamics (Ax.~\\ref{axiom:bk5_srmf_operator_selection_evolution}) the system descends $\\Fproc$, which by Def.~\\ref{definition:bk5_process_free_energy} is the process-level instance of the symbolic free energy (Def.~\\ref{definition:bk2_symbolic_free_energy}). On $(\\prob(M),\\wass)$ this descent is the Wasserstein gradient flow $\\partial_t \\rho = -\\operatorname{grad}_{\\wass}\\Fproc[\\rho]$ (Thm.~\\ref{theorem:bk2_wasserstein_gradient_flow}). By the symbolic $H$-theorem (Thm.~\\ref{theorem:bk2_h_theorem_for_symbolic_evol}), $\\Fproc$ is then a Lyapunov functional, $\\tfrac{d}{dt}\\Fproc[\\rho_t]\\le 0$ with equality only at a critical density; hence $\\rho_t$ converges to a local minimizer $\\rho^{\\ast}$ of $\\Fproc$ (of the equilibrium type characterized by Thm.~\\ref{theorem:bk2_equilibrium_distribution}). Convergence thus rests \\emph{entirely on the proven Book~II machinery}; no new convergence claim is asserted here.\n\n\\emph{Rate (derived from convexity, not fitted).} Under Assumption~\\ref{assumption:bk5_displacement_convexity} the flow satisfies the Evolution Variational Inequality\n\\[\n\\tfrac{1}{2}\\,\\tfrac{d}{dt}\\,\\wass(\\rho_t,\\rho^{\\ast})^2 \\;\\le\\; \\Fproc[\\rho^{\\ast}] - \\Fproc[\\rho_t] - \\tfrac{\\lambda}{2}\\,\\wass(\\rho_t,\\rho^{\\ast})^2 .\n\\]\nSince $\\rho^{\\ast}$ minimizes $\\Fproc$, the first difference is $\\le 0$. For $\\lambda = 0$, integrating yields the descent estimate\n\\[\n\\Fproc[\\rho_t] - \\Fproc[\\rho^{\\ast}] \\;\\le\\; \\frac{\\wass(\\rho_0,\\rho^{\\ast})^2}{2t} \\;=\\; O(1/t),\n\\]\nand for $\\lambda > 0$ the inequality sharpens to the exponential bound\n\\[\n\\Fproc[\\rho_t] - \\Fproc[\\rho^{\\ast}] \\;\\le\\; e^{-2\\lambda t}\\,\\bigl(\\Fproc[\\rho_0] - \\Fproc[\\rho^{\\ast}]\\bigr).\n\\]\nHence convergence proceeds at rate $O(1/t)$ or faster, as claimed --- a rate \\emph{proved} from the convexity of the functional, with no appeal to measured data.\n\n\\emph{Transfer to operator evolution.} Bounded metabolic capacity $\\MC$ (Def.~\\ref{definition:bk5_metabolic_capacity_mc_}, Prop.~\\ref{proposition:bk5_fixed_metabolic_capacity}) confines the operator path $\\gamma$ (Prop.~\\ref{proposition:bk5_operator_evolution}) to the viability domain (Def.~\\ref{definition:bk5_viability_domain}) on which the flow is well-posed, so the density-level estimate transfers to $\\Op(M)$. The discrete-time companion --- in which the per-step gap ratio is \\emph{measured} in the Appendix~B suite rather than derived --- is Cor.~\\ref{corollary:bk7_geometric_convergence_rate}; it \\emph{corroborates}, but is not used to establish, the rate proved here.\n\\end{proof}",
  "line": 1586,
  "macros_used": [
    "Fproc",
    "MC",
    "Op",
    "prob",
    "wass"
  ],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "",
  "proves": "theorem:bk5_operator_convergence",
  "ref_roles": [
    {
      "context": "hinery}; no new convergence claim is asserted here. \\emph{Rate (derived from convexity, not fitted).} Under Assumption~\\ref{assumption:bk5_displacement_convexity} the flow satisfies the Evolution Variational Inequality \\[ \\tfrac{1}{2}\\,\\tfrac{d}{dt}\\,\\wass(\\rho_t,\\rho^{\\ast})^2 \\;\\",
      "label": "assumption:bk5_displacement_convexity",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "book5.tex",
      "target_line": 1573,
      "target_type": "assumption"
    },
    {
      "context": "_operator_convergence} \\leavevmode \\emph{Convergence (inherited, not re-derived).} By the SRMF selection dynamics (Ax.~\\ref{axiom:bk5_srmf_operator_selection_evolution}) the system descends $\\Fproc$, which by Def.~\\ref{definition:bk5_process_free_energy} is the process-level instance of",
      "label": "axiom:bk5_srmf_operator_selection_evolution",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "book5.tex",
      "target_line": 1549,
      "target_type": "axiom"
    },
    {
      "context": "ompanion --- in which the per-step gap ratio is \\emph{measured} in the Appendix~B suite rather than derived --- is Cor.~\\ref{corollary:bk7_geometric_convergence_rate}; it \\emph{corroborates}, but is not used to establish, the rate proved here. \\end{proof}",
      "label": "corollary:bk7_geometric_convergence_rate",
      "logical_support": true,
      "role": "proof_support",
      "target_file": "book7.tex",
      "target_line": 605,
      "target_type": "corollary"
    },
    {
      "context": "which by Def.~\\ref{definition:bk5_process_free_energy} is the process-level instance of the symbolic free energy (Def.~\\ref{definition:bk2_symbolic_free_energy}). On $(\\prob(M),\\wass)$ this descent is the Wasserstein gradient flow $\\partial_t \\rho = -\\operatorname{grad}_{\\wass}\\F",
      "label": "definition:bk2_symbolic_free_energy",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "book2.tex",
      "target_line": 135,
      "target_type": "definition"
    },
    {
      "context": "tional, with no appeal to measured data. \\emph{Transfer to operator evolution.} Bounded metabolic capacity $\\MC$ (Def.~\\ref{definition:bk5_metabolic_capacity_mc_}, Prop.~\\ref{proposition:bk5_fixed_metabolic_capacity}) confines the operator path $\\gamma$ (Prop.~\\ref{proposition:bk5_",
      "label": "definition:bk5_metabolic_capacity_mc_",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "book5.tex",
      "target_line": 1525,
      "target_type": "definition"
    },
    {
      "context": "selection dynamics (Ax.~\\ref{axiom:bk5_srmf_operator_selection_evolution}) the system descends $\\Fproc$, which by Def.~\\ref{definition:bk5_process_free_energy} is the process-level instance of the symbolic free energy (Def.~\\ref{definition:bk2_symbolic_free_energy}). On $(\\prob(",
      "label": "definition:bk5_process_free_energy",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "book5.tex",
      "target_line": 1500,
      "target_type": "definition"
    },
    {
      "context": "ty}) confines the operator path $\\gamma$ (Prop.~\\ref{proposition:bk5_operator_evolution}) to the viability domain (Def.~\\ref{definition:bk5_viability_domain}) on which the flow is well-posed, so the density-level estimate transfers to $\\Op(M)$. The discrete-time companion ---",
      "label": "definition:bk5_viability_domain",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "book5.tex",
      "target_line": 133,
      "target_type": "definition"
    },
    {
      "context": "nsfer to operator evolution.} Bounded metabolic capacity $\\MC$ (Def.~\\ref{definition:bk5_metabolic_capacity_mc_}, Prop.~\\ref{proposition:bk5_fixed_metabolic_capacity}) confines the operator path $\\gamma$ (Prop.~\\ref{proposition:bk5_operator_evolution}) to the viability domain (Def.~\\re",
      "label": "proposition:bk5_fixed_metabolic_capacity",
      "logical_support": true,
      "role": "proof_support",
      "target_file": "book5.tex",
      "target_line": 1513,
      "target_type": "proposition"
    },
    {
      "context": "tabolic_capacity_mc_}, Prop.~\\ref{proposition:bk5_fixed_metabolic_capacity}) confines the operator path $\\gamma$ (Prop.~\\ref{proposition:bk5_operator_evolution}) to the viability domain (Def.~\\ref{definition:bk5_viability_domain}) on which the flow is well-posed, so the density-l",
      "label": "proposition:bk5_operator_evolution",
      "logical_support": true,
      "role": "proof_support",
      "target_file": "book5.tex",
      "target_line": 1491,
      "target_type": "proposition"
    },
    {
      "context": "hence $\\rho_t$ converges to a local minimizer $\\rho^{\\ast}$ of $\\Fproc$ (of the equilibrium type characterized by Thm.~\\ref{theorem:bk2_equilibrium_distribution}). Convergence thus rests \\emph{entirely on the proven Book~II machinery}; no new convergence claim is asserted here. \\",
      "label": "theorem:bk2_equilibrium_distribution",
      "logical_support": true,
      "role": "proof_support",
      "target_file": "book2.tex",
      "target_line": 216,
      "target_type": "theorem"
    },
    {
      "context": "orname{grad}_{\\wass}\\Fproc[\\rho]$ (Thm.~\\ref{theorem:bk2_wasserstein_gradient_flow}). By the symbolic $H$-theorem (Thm.~\\ref{theorem:bk2_h_theorem_for_symbolic_evol}), $\\Fproc$ is then a Lyapunov functional, $\\tfrac{d}{dt}\\Fproc[\\rho_t]\\le 0$ with equality only at a critical density;",
      "label": "theorem:bk2_h_theorem_for_symbolic_evol",
      "logical_support": true,
      "role": "proof_support",
      "target_file": "book2.tex",
      "target_line": 255,
      "target_type": "theorem"
    },
    {
      "context": "wass)$ this descent is the Wasserstein gradient flow $\\partial_t \\rho = -\\operatorname{grad}_{\\wass}\\Fproc[\\rho]$ (Thm.~\\ref{theorem:bk2_wasserstein_gradient_flow}). By the symbolic $H$-theorem (Thm.~\\ref{theorem:bk2_h_theorem_for_symbolic_evol}), $\\Fproc$ is then a Lyapunov functio",
      "label": "theorem:bk2_wasserstein_gradient_flow",
      "logical_support": true,
      "role": "proof_support",
      "target_file": "book2.tex",
      "target_line": 315,
      "target_type": "theorem"
    }
  ],
  "refs": [
    "assumption:bk5_displacement_convexity",
    "axiom:bk5_srmf_operator_selection_evolution",
    "corollary:bk7_geometric_convergence_rate",
    "definition:bk2_symbolic_free_energy",
    "definition:bk5_metabolic_capacity_mc_",
    "definition:bk5_process_free_energy",
    "definition:bk5_viability_domain",
    "proposition:bk5_fixed_metabolic_capacity",
    "proposition:bk5_operator_evolution",
    "theorem:bk2_equilibrium_distribution",
    "theorem:bk2_h_theorem_for_symbolic_evol",
    "theorem:bk2_wasserstein_gradient_flow"
  ],
  "role": "proof",
  "type": "proof"
}

{
  "book": "book5",
  "cited_by": [
    "corollary:bk5__metabolically_bounded_reflection_corollary",
    "proof:bk5__metabolically_bounded_reflection_corollary"
  ],
  "cites": [
    "definition:bk5_metabolic_capacity_mc_"
  ],
  "depends_on": [
    "definition:bk5_metabolic_capacity_mc_"
  ],
  "file": "book5.tex",
  "id": "axiom:bk5_metabolically_bounded_reflection",
  "label": "axiom:bk5_metabolically_bounded_reflection",
  "latex_body": "\\begin{axiom}[Metabolically Bounded Reflection]\n\\label{axiom:bk5_metabolically_bounded_reflection}\nLet $B := f(\\MC(S))$ with $f$ non-decreasing and $f(\\MC) \\leq \\MC$ (cf.~Def.~\\ref{definition:bk5_metabolic_capacity_mc_}). Then:\n\\[\n\\| D R \\|_g \\leq B.\n\\]\n\\end{axiom}",
  "lean_alignment": {
    "conditions": [
      "continuum/Hilbert/PDE-on-manifold content stays open; chart-complex restatements carry Glued as a named hypothesis where the source consumes compatibility",
      "modeling laws are structure fields or explicit hypotheses"
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "See the committed source registry for the original coverage note."
    ],
    "record_ids": [
      "MAP-BOOK5-078"
    ],
    "statuses": [
      "conditional"
    ],
    "witnesses": [
      "Book5Residue.max_recursive_depth_bound"
    ]
  },
  "line": 1608,
  "macros_used": [
    "MC"
  ],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "Metabolically Bounded Reflection",
  "proof_status": "definitional",
  "ref_roles": [
    {
      "context": "xiom:bk5_metabolically_bounded_reflection} Let $B := f(\\MC(S))$ with $f$ non-decreasing and $f(\\MC) \\leq \\MC$ (cf.~Def.~\\ref{definition:bk5_metabolic_capacity_mc_}). Then: \\[ \\| D R \\|_g \\leq B. \\] \\end{axiom}",
      "label": "definition:bk5_metabolic_capacity_mc_",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book5.tex",
      "target_line": 1525,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:bk5_metabolic_capacity_mc_"
  ],
  "role": "axiom",
  "type": "axiom"
}

{
  "book": "book5",
  "cited_by": [],
  "cites": [
    "axiom:bk5_metabolically_bounded_reflection"
  ],
  "depends_on": [
    "axiom:bk5_metabolically_bounded_reflection"
  ],
  "file": "book5.tex",
  "id": "corollary:bk5__metabolically_bounded_reflection_corollary",
  "label": "corollary:bk5__metabolically_bounded_reflection_corollary",
  "latex_body": "\\begin{corollary} \\label{corollary:bk5__metabolically_bounded_reflection_corollary}\nThe maximum depth $n_{\\max}$ of recursive reflection satisfies (cf.~Ax.~\\ref{axiom:bk5_metabolically_bounded_reflection}):\n\\[\nn_{\\max} \\leq \\left\\lfloor \\log_k\\left(\\frac{\\MC(S)}{c_0} + 1\\right) \\right\\rfloor.\n\\]\n\\end{corollary}",
  "lean_alignment": {
    "conditions": [
      "continuum/Hilbert/PDE-on-manifold content stays open; chart-complex restatements carry Glued as a named hypothesis where the source consumes compatibility",
      "modeling laws are structure fields or explicit hypotheses"
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "See the committed source registry for the original coverage note."
    ],
    "record_ids": [
      "MAP-BOOK5-079"
    ],
    "statuses": [
      "exact"
    ],
    "witnesses": [
      "Book5Residue.max_recursive_depth_bound"
    ]
  },
  "line": 1615,
  "macros_used": [
    "MC"
  ],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "",
  "proof_labels": [
    "proof:bk5__metabolically_bounded_reflection_corollary"
  ],
  "proof_status": "proven",
  "ref_roles": [
    {
      "context": "k5__metabolically_bounded_reflection_corollary} The maximum depth $n_{\\max}$ of recursive reflection satisfies (cf.~Ax.~\\ref{axiom:bk5_metabolically_bounded_reflection}): \\[ n_{\\max} \\leq \\left\\lfloor \\log_k\\left(\\frac{\\MC(S)}{c_0} + 1\\right) \\right\\rfloor. \\] \\end{corollary}",
      "label": "axiom:bk5_metabolically_bounded_reflection",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book5.tex",
      "target_line": 1608,
      "target_type": "axiom"
    }
  ],
  "refs": [
    "axiom:bk5_metabolically_bounded_reflection"
  ],
  "role": "corollary",
  "type": "corollary"
}

{
  "book": "book5",
  "cited_by": [],
  "cites": [
    "axiom:bk5_metabolically_bounded_reflection"
  ],
  "depends_on": [
    "axiom:bk5_metabolically_bounded_reflection"
  ],
  "file": "book5.tex",
  "id": "proof:bk5__metabolically_bounded_reflection_corollary",
  "label": "proof:bk5__metabolically_bounded_reflection_corollary",
  "latex_body": "\\begin{proof}\n\\label{proof:bk5__metabolically_bounded_reflection_corollary}\n\\leavevmode\nBy the metabolically bounded reflection axiom (Ax.~\\ref{axiom:bk5_metabolically_bounded_reflection}) recursive reflection is funded by a total budget no larger than $B=f(\\MC(S))\\le\\MC(S)$. Recursion is geometric: the first reflective level costs a base amount $c_0>0$, and each deeper level composes one further drift--reflection step, compounding the cost by a fixed factor $k>1$. The cumulative cost of $n$ nested levels is therefore the geometric accumulation\n\\[\nC(n)=c_0\\sum_{i=0}^{n-1}k^{i}(k-1)=c_0\\,(k^{n}-1).\n\\]\nSustaining depth $n$ requires $C(n)\\le\\MC(S)$, i.e.\\ $c_0(k^{n}-1)\\le\\MC(S)$, equivalently $k^{n}\\le \\tfrac{\\MC(S)}{c_0}+1$. Taking $\\log_k$ and using that $n$ is a nonnegative integer gives $n\\le\\big\\lfloor\\log_k\\!\\big(\\tfrac{\\MC(S)}{c_0}+1\\big)\\big\\rfloor$. The deepest admissible recursion is thus $n_{\\max}=\\big\\lfloor\\log_k(\\MC(S)/c_0+1)\\big\\rfloor$, as claimed.\n\\end{proof}",
  "line": 1621,
  "macros_used": [
    "MC"
  ],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "",
  "proves": "corollary:bk5__metabolically_bounded_reflection_corollary",
  "ref_roles": [
    {
      "context": "l{proof:bk5__metabolically_bounded_reflection_corollary} \\leavevmode By the metabolically bounded reflection axiom (Ax.~\\ref{axiom:bk5_metabolically_bounded_reflection}) recursive reflection is funded by a total budget no larger than $B=f(\\MC(S))\\le\\MC(S)$. Recursion is geometric: the fi",
      "label": "axiom:bk5_metabolically_bounded_reflection",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "book5.tex",
      "target_line": 1608,
      "target_type": "axiom"
    }
  ],
  "refs": [
    "axiom:bk5_metabolically_bounded_reflection"
  ],
  "role": "proof",
  "type": "proof"
}

{
  "book": "book5",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "book5.tex",
  "id": "subsec:bk5_extended_theoretical_implications",
  "label": "subsec:bk5_extended_theoretical_implications",
  "latex_body": "",
  "line": 1630,
  "macros_used": [],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "Extended Theoretical Implications",
  "role": "section",
  "subtype": "subsection",
  "type": "section"
}

{
  "book": "book5",
  "cited_by": [
    "proof:bk5_operators_evolve",
    "proposition:bk5_operators_evolve"
  ],
  "cites": [
    "axiom:bk5_srmf_operator_selection_evolution"
  ],
  "depends_on": [
    "axiom:bk5_srmf_operator_selection_evolution"
  ],
  "file": "book5.tex",
  "id": "theorem:bk5__srmf_operator_adaptation",
  "label": "theorem:bk5__srmf_operator_adaptation",
  "latex_body": "\\begin{theorem}[Certified SRMF Operator Adaptation] \\label{theorem:bk5__srmf_operator_adaptation}\nLet the stateful law of Ax.~\\ref{axiom:bk5_srmf_operator_selection_evolution}\nbe supplied. Suppose\n$\\mathcal E_{\\mathrm{eff}}[\\mathcal O_t,S_t]<\\theta_{\\mathrm{crit}}$, choose a\nfeedback gain $g>0$, and define the refinement velocity\n\\[\n v_t=g\\max\\{\\theta_{\\mathrm{crit}}-\n \\mathcal E_{\\mathrm{eff}}[\\mathcal O_t,S_t],0\\}.\n\\]\nThen $v_t=g(\\theta_{\\mathrm{crit}}-\\mathcal E_{\\mathrm{eff}})>0$. If the\nparameter update is additionally supplied as a negative-gradient step for\n$\\Fproc^{y_t}$ with a step size certified for descent, the process objective\nis non-increasing. This descent can coexist with a transient increase in the\nseparate execution-cost coordinate. None of operator motion, inventory change,\nor steepest descent follows from the below-threshold inequality alone.\n\\end{theorem}",
  "lean_alignment": {
    "conditions": [
      "effectiveness below threshold",
      "explicit gradient update law",
      "explicit minimizer certificate for each transition",
      "explicit positive feedback gain",
      "feedback-indexed real-valued process objective",
      "finite nonempty updated operator inventory",
      "inventory update and selection policy supplied independently of viability",
      "stable quadratic step size in [0,2]"
    ],
    "countermodels": [
      "Book5OperatorAdaptation.below_threshold_alone_does_not_force_adaptation"
    ],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": false,
    "notes": [
      "Conditional adaptation kernel: an explicit positive-gain law converts effectiveness shortfall into proportional pressure, and an explicit gradient step descends quadratic process free energy for step size in [0,2]. Stateful execution retains ordered incumbents, while a countermodel shows the threshold inequality alone cannot force motion. General steepest descent, calibration, and continuous or asymptotic evolution remain premises rather than consequences."
    ],
    "record_ids": [
      "MAP-BOOK5-102"
    ],
    "statuses": [
      "open_bridge"
    ],
    "witnesses": [
      "Book5OperatorAdaptation.below_threshold_alone_does_not_force_adaptation",
      "Book5OperatorAdaptation.gradientStep_displacement",
      "Book5OperatorAdaptation.process_descent_can_increase_execution_cost",
      "Book5OperatorAdaptation.quadratic_processFreeEnergy_descent",
      "Book5OperatorAdaptation.refinementVelocity_eq_of_below",
      "Book5OperatorAdaptation.refinementVelocity_pos",
      "Book5StatefulOperatorLearning.step_records_incumbent",
      "Book5StatefulOperatorLearning.two_steps_retain_ordered_history"
    ]
  },
  "line": 1632,
  "macros_used": [
    "Fproc"
  ],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "Certified SRMF Operator Adaptation",
  "proof_labels": [
    "proof:bk5__srmf_operator_adaptation"
  ],
  "proof_status": "proven",
  "ref_roles": [
    {
      "context": "{theorem}[Certified SRMF Operator Adaptation] \\label{theorem:bk5__srmf_operator_adaptation} Let the stateful law of Ax.~\\ref{axiom:bk5_srmf_operator_selection_evolution} be supplied. Suppose $\\mathcal E_{\\mathrm{eff}}[\\mathcal O_t,S_t]<\\theta_{\\mathrm{crit}}$, choose a feedback gain $g>0$",
      "label": "axiom:bk5_srmf_operator_selection_evolution",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "book5.tex",
      "target_line": 1549,
      "target_type": "axiom"
    }
  ],
  "refs": [
    "axiom:bk5_srmf_operator_selection_evolution"
  ],
  "role": "theorem",
  "type": "theorem"
}

{
  "book": "book5",
  "cited_by": [],
  "cites": [
    "axiom:bk5_srmf_operator_selection_evolution"
  ],
  "depends_on": [
    "axiom:bk5_srmf_operator_selection_evolution"
  ],
  "file": "book5.tex",
  "id": "proof:bk5__srmf_operator_adaptation",
  "label": "proof:bk5__srmf_operator_adaptation",
  "latex_body": "\\begin{proof}\n\\label{proof:bk5__srmf_operator_adaptation}\n\\leavevmode\n\nBelow threshold the maximum selects its positive branch, so\n$v_t=g(\\theta_{\\mathrm{crit}}-\\mathcal E_{\\mathrm{eff}})$; positivity follows\nfrom $g>0$ and the strict shortfall.  For a supplied gradient update\n$\\vartheta_{t+1}=\\vartheta_t-\\eta\\nabla\\Fproc^{y_t}(\\vartheta_t)$, the stated\nstep-size certificate gives\n$\\Fproc^{y_t}(\\vartheta_{t+1})\\le\n\\Fproc^{y_t}(\\vartheta_t)$.  In the finite-inventory branch, the minimizer\ncertificate in Ax.~\\ref{axiom:bk5_srmf_operator_selection_evolution} gives the\nstronger comparison against every member of $A_{t+1}$ and records the former\nincumbent in $H_{t+1}$.\n\nThe execution cost is a different coordinate of the process objective.  Two\navailable operators may satisfy\n$\\Fproc^{y_t}(\\mathcal O_{t+1})<\\Fproc^{y_t}(\\mathcal O_t)$ while\n$\\mathcal E_{\\mathrm{cost}}(\\mathcal O_t)<\n\\mathcal E_{\\mathrm{cost}}(\\mathcal O_{t+1})$, establishing the final\npossibility without asserting that it occurs on every step.  Finally, an\nidentity update below threshold is a countermodel to adaptation without the\nsupplied feedback and update laws.\n\\end{proof}",
  "line": 1648,
  "macros_used": [
    "Fproc"
  ],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "",
  "proves": "theorem:bk5__srmf_operator_adaptation",
  "ref_roles": [
    {
      "context": "{y_t}(\\vartheta_{t+1})\\le \\Fproc^{y_t}(\\vartheta_t)$. In the finite-inventory branch, the minimizer certificate in Ax.~\\ref{axiom:bk5_srmf_operator_selection_evolution} gives the stronger comparison against every member of $A_{t+1}$ and records the former incumbent in $H_{t+1}$. The exe",
      "label": "axiom:bk5_srmf_operator_selection_evolution",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "book5.tex",
      "target_line": 1549,
      "target_type": "axiom"
    }
  ],
  "refs": [
    "axiom:bk5_srmf_operator_selection_evolution"
  ],
  "role": "proof",
  "type": "proof"
}

{
  "book": "book5",
  "cited_by": [
    "proof:bk5_operators_evolve",
    "proposition:bk5_operators_evolve"
  ],
  "cites": [
    "axiom:bk5_srmf_operator_selection_evolution",
    "definition:bk5_process_free_energy"
  ],
  "depends_on": [
    "axiom:bk5_srmf_operator_selection_evolution",
    "definition:bk5_process_free_energy"
  ],
  "file": "book5.tex",
  "id": "definition:bk5__operator_viability_set_v",
  "label": "definition:bk5__operator_viability_set_v",
  "latex_body": "\\begin{definition}[Operator Viability Set $\\mathcal{V}_{\\text{op}}$] \\label{definition:bk5__operator_viability_set_v}\n\n\\[\n\\mathcal{V}_{\\text{op}} := \\left\\{ \\mathcal{O} \\in \\Op(M) \\mid \\Fproc[\\mathcal{O}, S] < \\theta_{\\text{proc}} \\right\\} \\quad \\text{(cf.~Def.~\\ref{definition:bk5_process_free_energy}, Ax.~\\ref{axiom:bk5_srmf_operator_selection_evolution})}.\n\\]\n\\end{definition}",
  "lean_alignment": {
    "conditions": [
      "continuum/Hilbert/PDE-on-manifold content stays open; chart-complex restatements carry Glued as a named hypothesis where the source consumes compatibility",
      "modeling laws are structure fields or explicit hypotheses"
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "See the committed source registry for the original coverage note."
    ],
    "record_ids": [
      "MAP-BOOK5-080"
    ],
    "statuses": [
      "conditional"
    ],
    "witnesses": [
      "Book5Residue.MetabolicBudget.complexity_le"
    ]
  },
  "line": 1672,
  "macros_used": [
    "Fproc",
    "Op"
  ],
  "matter_region": "mainmatter",
  "matter_role": "canonical_book",
  "name": "Operator Viability Set $\\mathcal{V}_{\\text{op}}$",
  "proof_status": "definitional",
  "ref_roles": [
    {
      "context": "roc[\\mathcal{O}, S] < \\theta_{\\text{proc}} \\right\\} \\quad \\text{(cf.~Def.~\\ref{definition:bk5_process_free_energy}, Ax.~\\ref{axiom:bk5_srmf_operator_selection_evolution})}. \\] \\end{definition}",
      "label": "axiom:bk5_srmf_operator_selection_evolution",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book5.tex",
      "target_line": 1549,
      "target_type": "axiom"
    },
    {
      "context": "p}} := \\left\\{ \\mathcal{O} \\in \\Op(M) \\mid \\Fproc[\\mathcal{O}, S] < \\theta_{\\text{proc}} \\right\\} \\quad \\text{(cf.~Def.~\\ref{definition:bk5_process_free_energy}, Ax.~\\ref{axiom:bk5_srmf_operator_selection_evolution})}. \\] \\end{definition}",
      "label": "definition:bk5_process_free_energy",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book5.tex",
      "target_line": 1500,
      "target_type": "definition"
    }
  ],
  "refs": [
    "axiom:bk5_srmf_operator_selection_evolution",
    "definition:bk5_process_free_energy"
  ],
  "role": "definition",
  "type": "definition"
}