sectionchapterappendix

Symbolic Reflexive Validation of Symbolic Dynamics

section:appendix_symbolic_reflexive_validation.tex:3

Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "section:appendix_symbolic_reflexive_validation.tex:3",
  "label": "",
  "latex_body": "",
  "line": 3,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Symbolic Reflexive Validation of Symbolic Dynamics",
  "role": "section",
  "subtype": "chapter",
  "type": "section"
}

sectionsectionappendix

Overview

sec:appB_overview

Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "sec:appB_overview",
  "label": "sec:appB_overview",
  "latex_body": "",
  "line": 4,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Overview",
  "role": "section",
  "subtype": "section",
  "type": "section"
}

sectionsectionappendix

Symbolic Validation Procedure

sec:appB_symbolic_validation_procedure

Reference roles

TargetRoleLogical support
remark:bk7_unnamed_remark_04navigationno
remark:bk7_unnamed_remark_05navigationno
scholium:bk7_popperian_extensionnavigationno
Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [],
  "cites": [
    "remark:bk7_unnamed_remark_04",
    "remark:bk7_unnamed_remark_05",
    "scholium:bk7_popperian_extension"
  ],
  "depends_on": [
    "remark:bk7_unnamed_remark_04",
    "remark:bk7_unnamed_remark_05",
    "scholium:bk7_popperian_extension"
  ],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "sec:appB_symbolic_validation_procedure",
  "label": "sec:appB_symbolic_validation_procedure",
  "latex_body": "",
  "line": 34,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Symbolic Validation Procedure",
  "ref_roles": [
    {
      "context": "",
      "label": "remark:bk7_unnamed_remark_04",
      "logical_support": false,
      "role": "navigation",
      "target_file": "book7.tex",
      "target_line": 1458,
      "target_type": "remark"
    },
    {
      "context": "",
      "label": "remark:bk7_unnamed_remark_05",
      "logical_support": false,
      "role": "navigation",
      "target_file": "book7.tex",
      "target_line": 1490,
      "target_type": "remark"
    },
    {
      "context": "",
      "label": "scholium:bk7_popperian_extension",
      "logical_support": false,
      "role": "navigation",
      "target_file": "book7.tex",
      "target_line": 1462,
      "target_type": "scholium"
    }
  ],
  "role": "section",
  "subtype": "section",
  "type": "section"
}

sectionsubsectionappendix

Symbolic Reflexive Validation

subsec:appB_symbolic_reflexive_validation

Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "subsec:appB_symbolic_reflexive_validation",
  "label": "subsec:appB_symbolic_reflexive_validation",
  "latex_body": "",
  "line": 71,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Symbolic Reflexive Validation",
  "role": "section",
  "subtype": "subsection",
  "type": "section"
}

sectionsectionappendix

Symbolic Operator Simulations

sec:appB_symbolic_operator_simulations

Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "sec:appB_symbolic_operator_simulations",
  "label": "sec:appB_symbolic_operator_simulations",
  "latex_body": "",
  "line": 77,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Symbolic Operator Simulations",
  "role": "section",
  "subtype": "section",
  "type": "section"
}

sectionsectionappendix

Real-World Reflections of Symbolic Law

sec:appB_real_world_reflections

Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "sec:appB_real_world_reflections",
  "label": "sec:appB_real_world_reflections",
  "latex_body": "",
  "line": 85,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Real-World Reflections of Symbolic Law",
  "role": "section",
  "subtype": "section",
  "type": "section"
}

sectionsectionappendix

Structural Correspondence Traces

sec:appB_structural_correspondence

Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "sec:appB_structural_correspondence",
  "label": "sec:appB_structural_correspondence",
  "latex_body": "",
  "line": 88,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Structural Correspondence Traces",
  "role": "section",
  "subtype": "section",
  "type": "section"
}

sectionsectionappendix

Symbolic Smoothness Resolution: Completeness of the Observer Metric and Smooth Emergence of the Symbolic Manifold

sec:appB_symbolic_smoothness_resolution

Reference roles

TargetRoleLogical support
scholium:bk1_resolution_of_continuum_disjunctionnavigationno
Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [
    "sec:appD_preamble_nature_of_appendix"
  ],
  "cites": [
    "scholium:bk1_resolution_of_continuum_disjunction"
  ],
  "depends_on": [
    "scholium:bk1_resolution_of_continuum_disjunction"
  ],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "sec:appB_symbolic_smoothness_resolution",
  "label": "sec:appB_symbolic_smoothness_resolution",
  "latex_body": "",
  "line": 93,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Symbolic Smoothness Resolution: Completeness of the Observer Metric and Smooth Emergence of the Symbolic Manifold",
  "ref_roles": [
    {
      "context": "",
      "label": "scholium:bk1_resolution_of_continuum_disjunction",
      "logical_support": false,
      "role": "navigation",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 2709,
      "target_type": "scholium"
    }
  ],
  "role": "section",
  "subtype": "section",
  "type": "section"
}

sectionsubsectionappendix

B.1 Preliminaries and Topological Foundations

subsec:appB_preliminaries

Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "subsec:appB_preliminaries",
  "label": "subsec:appB_preliminaries",
  "latex_body": "",
  "line": 100,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "B.1 Preliminaries and Topological Foundations",
  "role": "section",
  "subtype": "subsection",
  "type": "section"
}

definitiondefinitionalappendix

Symbolic State Space

definition:appB_symbolic_state_space

Exact LaTeX body

\begin{definition}[Symbolic State Space]
\label{definition:appB_symbolic_state_space}
Let $\mathcal{S}$ denote the space of symbolic configurations with finite symbolic complexity (cf.~\ref{definition:bk1_symbolic_manifold}). For each resolution level $\lambda \in \mathbb{N}$, define:
\[
P_\lambda = \left\{(s, \rho) \in \mathcal{S} \times \text{End}(\mathcal{S}) : \text{complexity}(s) \leq \lambda, \|\rho\|_{\text{op}} \leq \lambda \right\}
\]
The symbolic tower is the directed union $\mathcal{P} = \bigcup_{\lambda} P_\lambda$.
\end{definition}

Reference roles

TargetRoleLogical support
definition:bk1_symbolic_manifoldcf_near_matchyes
Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [
    "definition:appB_symbolic_energy",
    "proof:appB_chart_bounds",
    "proof:appB_metric_completion",
    "proof:appB_resolution_of_smoothness",
    "proof:appB_smooth_atlas"
  ],
  "cites": [
    "definition:bk1_symbolic_manifold"
  ],
  "depends_on": [
    "definition:bk1_symbolic_manifold"
  ],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "definition:appB_symbolic_state_space",
  "label": "definition:appB_symbolic_state_space",
  "latex_body": "\\begin{definition}[Symbolic State Space]\n\\label{definition:appB_symbolic_state_space}\nLet $\\mathcal{S}$ denote the space of symbolic configurations with finite symbolic complexity (cf.~\\ref{definition:bk1_symbolic_manifold}). For each resolution level $\\lambda \\in \\mathbb{N}$, define:\n\\[\nP_\\lambda = \\left\\{(s, \\rho) \\in \\mathcal{S} \\times \\text{End}(\\mathcal{S}) : \\text{complexity}(s) \\leq \\lambda, \\|\\rho\\|_{\\text{op}} \\leq \\lambda \\right\\}\n\\]\nThe symbolic tower is the directed union $\\mathcal{P} = \\bigcup_{\\lambda} P_\\lambda$.\n\\end{definition}",
  "lean_alignment": {
    "conditions": [
      "modeling laws are structure fields or explicit hypotheses; continuum/categorical content is NOT formalized"
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": false,
    "notes": [
      "Only the monotone-nesting content of the level sets P_lambda is modeled, via the InLevel threshold predicate. The underlying space S, End(S), and the operator norm are not modeled."
    ],
    "record_ids": [
      "MAP-SMALLPACK-001"
    ],
    "statuses": [
      "open_bridge"
    ],
    "witnesses": [
      "SmallPack.resolutionLevel_mono"
    ]
  },
  "line": 103,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Symbolic State Space",
  "proof_status": "definitional",
  "ref_roles": [
    {
      "context": "ymbolic_state_space} Let $\\mathcal{S}$ denote the space of symbolic configurations with finite symbolic complexity (cf.~\\ref{definition:bk1_symbolic_manifold}). For each resolution level $\\lambda \\in \\mathbb{N}$, define: \\[ P_\\lambda = \\left\\{(s, \\rho) \\in \\mathcal{S} \\times \\t",
      "label": "definition:bk1_symbolic_manifold",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 1188,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:bk1_symbolic_manifold"
  ],
  "role": "definition",
  "type": "definition"
}

definitiondefinitionalappendix

Observer-Relative Symbolic Metric

definition:appB_observer_metric

Exact LaTeX body

\begin{definition}[Observer-Relative Symbolic Metric]
\label{definition:appB_observer_metric}
For $x = (s_x, \rho_x), y = (s_y, \rho_y) \in \mathcal{P}$, define:
\[
d_{\mathcal{O}}(x,y) = \sup_{t \in [0,1]} \left\| \Phi_{x \to y}(t) - \text{Ad}_{\rho_x^{-1}}(\rho_y) \right\|_{\kappa}
\]
where $\Phi_{x \to y}(t)$ is the SRV flow (cf.~\ref{definition:bk1_symbolic_flow}) and $\text{Ad}_g(h) = g h g^{-1}$; the norm $\|\cdot\|_\kappa$ is induced by the coherence metric (cf.~\ref{definition:bk4_coherence_metric_on_symbolic_manifold}).
\end{definition}

Reference roles

TargetRoleLogical support
definition:bk1_symbolic_flowcf_near_matchyes
definition:bk4_coherence_metric_on_symbolic_manifoldcf_near_matchyes
Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [
    "proof:appB_srv_cauchy",
    "theorem:appB_srv_cauchy"
  ],
  "cites": [
    "definition:bk1_symbolic_flow",
    "definition:bk4_coherence_metric_on_symbolic_manifold"
  ],
  "depends_on": [
    "definition:bk1_symbolic_flow",
    "definition:bk4_coherence_metric_on_symbolic_manifold"
  ],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "definition:appB_observer_metric",
  "label": "definition:appB_observer_metric",
  "latex_body": "\\begin{definition}[Observer-Relative Symbolic Metric]\n\\label{definition:appB_observer_metric}\nFor $x = (s_x, \\rho_x), y = (s_y, \\rho_y) \\in \\mathcal{P}$, define:\n\\[\nd_{\\mathcal{O}}(x,y) = \\sup_{t \\in [0,1]} \\left\\| \\Phi_{x \\to y}(t) - \\text{Ad}_{\\rho_x^{-1}}(\\rho_y) \\right\\|_{\\kappa}\n\\]\nwhere $\\Phi_{x \\to y}(t)$ is the SRV flow (cf.~\\ref{definition:bk1_symbolic_flow}) and $\\text{Ad}_g(h) = g h g^{-1}$; the norm $\\|\\cdot\\|_\\kappa$ is induced by the coherence metric (cf.~\\ref{definition:bk4_coherence_metric_on_symbolic_manifold}).\n\\end{definition}",
  "line": 112,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Observer-Relative Symbolic Metric",
  "proof_status": "definitional",
  "ref_roles": [
    {
      "context": "\\Phi_{x \\to y}(t) - \\text{Ad}_{\\rho_x^{-1}}(\\rho_y) \\right\\|_{\\kappa} \\] where $\\Phi_{x \\to y}(t)$ is the SRV flow (cf.~\\ref{definition:bk1_symbolic_flow}) and $\\text{Ad}_g(h) = g h g^{-1}$; the norm $\\|\\cdot\\|_\\kappa$ is induced by the coherence metric (cf.~\\ref{definition",
      "label": "definition:bk1_symbolic_flow",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 2872,
      "target_type": "definition"
    },
    {
      "context": "_symbolic_flow}) and $\\text{Ad}_g(h) = g h g^{-1}$; the norm $\\|\\cdot\\|_\\kappa$ is induced by the coherence metric (cf.~\\ref{definition:bk4_coherence_metric_on_symbolic_manifold}). \\end{definition}",
      "label": "definition:bk4_coherence_metric_on_symbolic_manifold",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book4.tex",
      "target_line": 2363,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:bk1_symbolic_flow",
    "definition:bk4_coherence_metric_on_symbolic_manifold"
  ],
  "role": "definition",
  "type": "definition"
}

sectionsubsectionappendix

B.2 Energy Contraction and Cauchy Structure

subsec:appB_cauchy

Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "subsec:appB_cauchy",
  "label": "subsec:appB_cauchy",
  "latex_body": "",
  "line": 122,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "B.2 Energy Contraction and Cauchy Structure",
  "role": "section",
  "subtype": "subsection",
  "type": "section"
}

definitiondefinitionalappendix

Symbolic Energy Functional

definition:appB_symbolic_energy

Exact LaTeX body

\begin{definition}[Symbolic Energy Functional]
\label{definition:appB_symbolic_energy}
Given an SRV trajectory $\{x_t\}$ through the symbolic state space (Def.~\ref{definition:appB_symbolic_state_space}), define:
\[
\mathcal{E}_t = H_{\text{symb}}(x_t) + \frac{1}{2}\|\text{drift}_t\|_\kappa^2 + \frac{\epsilon_{\mathcal{O}}}{2}\|\text{refl}_t\|_\kappa^2
\]
\end{definition}

Reference roles

TargetRoleLogical support
definition:appB_symbolic_state_spacedefinition_anchoryes
Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [
    "proof:appB_chart_bounds",
    "proof:appB_energy_contraction"
  ],
  "cites": [
    "definition:appB_symbolic_state_space"
  ],
  "depends_on": [
    "definition:appB_symbolic_state_space"
  ],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "definition:appB_symbolic_energy",
  "label": "definition:appB_symbolic_energy",
  "latex_body": "\\begin{definition}[Symbolic Energy Functional]\n\\label{definition:appB_symbolic_energy}\nGiven an SRV trajectory $\\{x_t\\}$ through the symbolic state space (Def.~\\ref{definition:appB_symbolic_state_space}), define:\n\\[\n\\mathcal{E}_t = H_{\\text{symb}}(x_t) + \\frac{1}{2}\\|\\text{drift}_t\\|_\\kappa^2 + \\frac{\\epsilon_{\\mathcal{O}}}{2}\\|\\text{refl}_t\\|_\\kappa^2\n\\]\n\\end{definition}",
  "lean_alignment": {
    "conditions": [
      "modeling laws are structure fields or explicit hypotheses; continuum/categorical content is NOT formalized"
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "Models the algebraic form H + (1/2)*drift^2 + (epsO/2)*refl^2 directly on reals and proves nonnegativity conditional on H >= 0, epsO >= 0. The kappa-norm and symbolic-manifold structure underlying drift/refl are erased to bare reals."
    ],
    "record_ids": [
      "MAP-SMALLPACK-002"
    ],
    "statuses": [
      "conditional"
    ],
    "witnesses": [
      "SmallPack.symbolicEnergy_nonneg"
    ]
  },
  "line": 125,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Symbolic Energy Functional",
  "proof_status": "definitional",
  "ref_roles": [
    {
      "context": "ional] \\label{definition:appB_symbolic_energy} Given an SRV trajectory $\\{x_t\\}$ through the symbolic state space (Def.~\\ref{definition:appB_symbolic_state_space}), define: \\[ \\mathcal{E}_t = H_{\\text{symb}}(x_t) + \\frac{1}{2}\\|\\text{drift}_t\\|_\\kappa^2 + \\frac{\\epsilon_{\\mathcal{O",
      "label": "definition:appB_symbolic_state_space",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "appendix_symbolic_reflexive_validation.tex",
      "target_line": 103,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:appB_symbolic_state_space"
  ],
  "role": "definition",
  "type": "definition"
}

assumptiondefinitionalappendix

SRV as a Stable Dissipative Descent

assumption:appB_srv_dissipativity

Exact LaTeX body

\begin{assumption}[SRV as a Stable Dissipative Descent]
\label{assumption:appB_srv_dissipativity}
The SRV step (drift then reflective correction; Def.~\ref{definition:bk1_drift_field}, Def.~\ref{definition:bk1_reflection_operator}) is a stable descent iteration on the symbolic Hamiltonian $H_{\text{symb}}$ (Def.~\ref{definition:bk2_symbolic_hamiltonian}): $H_{\text{symb}}$ is bounded below, $L$-smooth and $\mu$-strongly convex on the symbolic state space, the drift increment is a gradient step $\text{drift}_t=\eta\,\nabla H_{\text{symb}}(x_t)$ with stabilizing step size $\eta\in(0,1/L]$, and the reflective correction is non-expansive in $\|\cdot\|_\kappa$. Write $\lambda_{\text{cont}}:=\eta\big(1-\tfrac{L\eta}{2}\big)>0$ for the resulting structural descent modulus. This is a structural well-posedness hypothesis on the SRV map; the contraction ratios observed in the Appendix simulations corroborate but do not define $\lambda_{\text{cont}}$.
\end{assumption}

Reference roles

TargetRoleLogical support
definition:bk1_drift_fielddefinition_anchoryes
definition:bk1_reflection_operatordefinition_anchoryes
definition:bk2_symbolic_hamiltoniandefinition_anchoryes
Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [
    "proof:appB_energy_contraction",
    "proof:appB_srv_cauchy"
  ],
  "cites": [
    "definition:bk1_drift_field",
    "definition:bk1_reflection_operator",
    "definition:bk2_symbolic_hamiltonian"
  ],
  "depends_on": [
    "definition:bk1_drift_field",
    "definition:bk1_reflection_operator",
    "definition:bk2_symbolic_hamiltonian"
  ],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "assumption:appB_srv_dissipativity",
  "label": "assumption:appB_srv_dissipativity",
  "latex_body": "\\begin{assumption}[SRV as a Stable Dissipative Descent]\n\\label{assumption:appB_srv_dissipativity}\nThe SRV step (drift then reflective correction; Def.~\\ref{definition:bk1_drift_field}, Def.~\\ref{definition:bk1_reflection_operator}) is a stable descent iteration on the symbolic Hamiltonian $H_{\\text{symb}}$ (Def.~\\ref{definition:bk2_symbolic_hamiltonian}): $H_{\\text{symb}}$ is bounded below, $L$-smooth and $\\mu$-strongly convex on the symbolic state space, the drift increment is a gradient step $\\text{drift}_t=\\eta\\,\\nabla H_{\\text{symb}}(x_t)$ with stabilizing step size $\\eta\\in(0,1/L]$, and the reflective correction is non-expansive in $\\|\\cdot\\|_\\kappa$. Write $\\lambda_{\\text{cont}}:=\\eta\\big(1-\\tfrac{L\\eta}{2}\\big)>0$ for the resulting structural descent modulus. This is a structural well-posedness hypothesis on the SRV map; the contraction ratios observed in the Appendix simulations corroborate but do not define $\\lambda_{\\text{cont}}$.\n\\end{assumption}",
  "line": 133,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "SRV as a Stable Dissipative Descent",
  "proof_status": "definitional",
  "ref_roles": [
    {
      "context": "ble Dissipative Descent] \\label{assumption:appB_srv_dissipativity} The SRV step (drift then reflective correction; Def.~\\ref{definition:bk1_drift_field}, Def.~\\ref{definition:bk1_reflection_operator}) is a stable descent iteration on the symbolic Hamiltonian $H_{\\text{sym",
      "label": "definition:bk1_drift_field",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 1198,
      "target_type": "definition"
    },
    {
      "context": "ion:appB_srv_dissipativity} The SRV step (drift then reflective correction; Def.~\\ref{definition:bk1_drift_field}, Def.~\\ref{definition:bk1_reflection_operator}) is a stable descent iteration on the symbolic Hamiltonian $H_{\\text{symb}}$ (Def.~\\ref{definition:bk2_symbolic_hamilto",
      "label": "definition:bk1_reflection_operator",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 1209,
      "target_type": "definition"
    },
    {
      "context": "{definition:bk1_reflection_operator}) is a stable descent iteration on the symbolic Hamiltonian $H_{\\text{symb}}$ (Def.~\\ref{definition:bk2_symbolic_hamiltonian}): $H_{\\text{symb}}$ is bounded below, $L$-smooth and $\\mu$-strongly convex on the symbolic state space, the drift incre",
      "label": "definition:bk2_symbolic_hamiltonian",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "book2.tex",
      "target_line": 67,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:bk1_drift_field",
    "definition:bk1_reflection_operator",
    "definition:bk2_symbolic_hamiltonian"
  ],
  "role": "assumption",
  "type": "assumption"
}

lemmaprovenappendix

Energy Contraction Lemma

lemma:appB_energy_contraction

Exact LaTeX body

\begin{lemma}[Energy Contraction Lemma]
\label{lemma:appB_energy_contraction}
Under SRV, we have:
\[
\mathcal{E}_{t+1} - \mathcal{E}_t \leq -\lambda_{\text{cont}} \left( \|\text{drift}_t\|_\kappa^2 + \epsilon_{\mathcal{O}}\|\text{refl}_t\|_\kappa^2 \right)
\]
Here $H_{\text{symb}}$ generalizes the symbolic Hamiltonian (cf.~\ref{definition:bk2_symbolic_hamiltonian}) under SRV dynamics.
\end{lemma}

Reference roles

TargetRoleLogical support
definition:bk2_symbolic_hamiltoniancf_near_matchyes
Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [
    "proof:appB_resolution_of_smoothness",
    "proof:appB_smooth_atlas",
    "proof:appB_srv_cauchy"
  ],
  "cites": [
    "definition:bk2_symbolic_hamiltonian"
  ],
  "depends_on": [
    "assumption:appB_srv_dissipativity",
    "definition:appB_symbolic_energy",
    "definition:bk2_symbolic_hamiltonian"
  ],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "lemma:appB_energy_contraction",
  "label": "lemma:appB_energy_contraction",
  "latex_body": "\\begin{lemma}[Energy Contraction Lemma]\n\\label{lemma:appB_energy_contraction}\nUnder SRV, we have:\n\\[\n\\mathcal{E}_{t+1} - \\mathcal{E}_t \\leq -\\lambda_{\\text{cont}} \\left( \\|\\text{drift}_t\\|_\\kappa^2 + \\epsilon_{\\mathcal{O}}\\|\\text{refl}_t\\|_\\kappa^2 \\right)\n\\]\nHere $H_{\\text{symb}}$ generalizes the symbolic Hamiltonian (cf.~\\ref{definition:bk2_symbolic_hamiltonian}) under SRV dynamics.\n\\end{lemma}",
  "lean_alignment": {
    "conditions": [
      "modeling laws are structure fields or explicit hypotheses; continuum/categorical content is NOT formalized"
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "The per-step contraction law is kept as a structure field on an abstract energy : Nat -> Real sequence; its telescoped/accumulated form over n steps is proved by induction, mirroring Book8's metabolic-sufficiency pattern. H_symb and the underlying SRV dynamics are not modeled."
    ],
    "record_ids": [
      "MAP-SMALLPACK-003"
    ],
    "statuses": [
      "conditional"
    ],
    "witnesses": [
      "SmallPack.symbolicEnergyContraction_accum"
    ]
  },
  "line": 138,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Energy Contraction Lemma",
  "proof_labels": [
    "proof:appB_energy_contraction"
  ],
  "proof_status": "proven",
  "ref_roles": [
    {
      "context": "lon_{\\mathcal{O}}\\|\\text{refl}_t\\|_\\kappa^2 \\right) \\] Here $H_{\\text{symb}}$ generalizes the symbolic Hamiltonian (cf.~\\ref{definition:bk2_symbolic_hamiltonian}) under SRV dynamics. \\end{lemma}",
      "label": "definition:bk2_symbolic_hamiltonian",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book2.tex",
      "target_line": 67,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:bk2_symbolic_hamiltonian"
  ],
  "role": "lemma",
  "type": "lemma"
}

proofappendix

proof:appB_energy_contraction

proof:appB_energy_contraction

Exact LaTeX body

\begin{proof}
\label{proof:appB_energy_contraction}
\leavevmode
By Assumption~\ref{assumption:appB_srv_dissipativity} the drift increment is a gradient step on the $L$-smooth Hamiltonian, $x_t\mapsto x_t-\eta\nabla H_{\text{symb}}(x_t)$ with $\eta\le 1/L$. The standard descent estimate for an $L$-smooth function then gives
\[
H_{\text{symb}}(x_{t+1})-H_{\text{symb}}(x_t)\le -\eta\big(1-\tfrac{L\eta}{2}\big)\,\|\nabla H_{\text{symb}}(x_t)\|_\kappa^2=-\lambda_{\text{cont}}\,\|\text{drift}_t\|_\kappa^2,
\]
where the last equality uses $\text{drift}_t=\eta\nabla H_{\text{symb}}(x_t)$ (the step size is folded into $\lambda_{\text{cont}}$). The reflective correction is non-expansive in $\|\cdot\|_\kappa$, so it cannot increase the reflection channel of the energy and contributes the analogous nonpositive term $-\lambda_{\text{cont}}\,\epsilon_{\mathcal{O}}\|\text{refl}_t\|_\kappa^2$ (Def.~\ref{definition:appB_symbolic_energy}). Summing the drift and reflection channels yields
\[
\mathcal{E}_{t+1}-\mathcal{E}_t\le -\lambda_{\text{cont}}\big(\|\text{drift}_t\|_\kappa^2+\epsilon_{\mathcal{O}}\|\text{refl}_t\|_\kappa^2\big),
\]
the claimed contraction. The modulus $\lambda_{\text{cont}}=\eta(1-L\eta/2)$ is structural, fixed by the smoothness $L$ and step size $\eta$, not measured.
\end{proof}

Reference roles

TargetRoleLogical support
assumption:appB_srv_dissipativitydefinition_anchoryes
definition:appB_symbolic_energydefinition_anchoryes
Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [],
  "cites": [
    "assumption:appB_srv_dissipativity",
    "definition:appB_symbolic_energy"
  ],
  "depends_on": [
    "assumption:appB_srv_dissipativity",
    "definition:appB_symbolic_energy"
  ],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "proof:appB_energy_contraction",
  "label": "proof:appB_energy_contraction",
  "latex_body": "\\begin{proof}\n\\label{proof:appB_energy_contraction}\n\\leavevmode\nBy Assumption~\\ref{assumption:appB_srv_dissipativity} the drift increment is a gradient step on the $L$-smooth Hamiltonian, $x_t\\mapsto x_t-\\eta\\nabla H_{\\text{symb}}(x_t)$ with $\\eta\\le 1/L$. The standard descent estimate for an $L$-smooth function then gives\n\\[\nH_{\\text{symb}}(x_{t+1})-H_{\\text{symb}}(x_t)\\le -\\eta\\big(1-\\tfrac{L\\eta}{2}\\big)\\,\\|\\nabla H_{\\text{symb}}(x_t)\\|_\\kappa^2=-\\lambda_{\\text{cont}}\\,\\|\\text{drift}_t\\|_\\kappa^2,\n\\]\nwhere the last equality uses $\\text{drift}_t=\\eta\\nabla H_{\\text{symb}}(x_t)$ (the step size is folded into $\\lambda_{\\text{cont}}$). The reflective correction is non-expansive in $\\|\\cdot\\|_\\kappa$, so it cannot increase the reflection channel of the energy and contributes the analogous nonpositive term $-\\lambda_{\\text{cont}}\\,\\epsilon_{\\mathcal{O}}\\|\\text{refl}_t\\|_\\kappa^2$ (Def.~\\ref{definition:appB_symbolic_energy}). Summing the drift and reflection channels yields\n\\[\n\\mathcal{E}_{t+1}-\\mathcal{E}_t\\le -\\lambda_{\\text{cont}}\\big(\\|\\text{drift}_t\\|_\\kappa^2+\\epsilon_{\\mathcal{O}}\\|\\text{refl}_t\\|_\\kappa^2\\big),\n\\]\nthe claimed contraction. The modulus $\\lambda_{\\text{cont}}=\\eta(1-L\\eta/2)$ is structural, fixed by the smoothness $L$ and step size $\\eta$, not measured.\n\\end{proof}",
  "line": 146,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "",
  "proves": "lemma:appB_energy_contraction",
  "ref_roles": [
    {
      "context": "\\begin{proof} \\label{proof:appB_energy_contraction} \\leavevmode By Assumption~\\ref{assumption:appB_srv_dissipativity} the drift increment is a gradient step on the $L$-smooth Hamiltonian, $x_t\\mapsto x_t-\\eta\\nabla H_{\\text{symb}}(x_t)$",
      "label": "assumption:appB_srv_dissipativity",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "appendix_symbolic_reflexive_validation.tex",
      "target_line": 133,
      "target_type": "assumption"
    },
    {
      "context": "ributes the analogous nonpositive term $-\\lambda_{\\text{cont}}\\,\\epsilon_{\\mathcal{O}}\\|\\text{refl}_t\\|_\\kappa^2$ (Def.~\\ref{definition:appB_symbolic_energy}). Summing the drift and reflection channels yields \\[ \\mathcal{E}_{t+1}-\\mathcal{E}_t\\le -\\lambda_{\\text{cont}}\\big(\\|\\",
      "label": "definition:appB_symbolic_energy",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "appendix_symbolic_reflexive_validation.tex",
      "target_line": 125,
      "target_type": "definition"
    }
  ],
  "refs": [
    "assumption:appB_srv_dissipativity",
    "definition:appB_symbolic_energy"
  ],
  "role": "proof",
  "type": "proof"
}

theoremprovenappendix

Cauchy Convergence of SRV Trajectories

theorem:appB_srv_cauchy

Exact LaTeX body

\begin{theorem}[Cauchy Convergence of SRV Trajectories]
\label{theorem:appB_srv_cauchy}
All SRV trajectories $\{x_t\}$ are Cauchy in $(\mathcal{P}, d_{\mathcal{O}})$ (cf.~\ref{definition:appB_observer_metric}).
\end{theorem}

Reference roles

TargetRoleLogical support
definition:appB_observer_metriccf_near_matchyes
Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [
    "proof:appB_resolution_of_smoothness"
  ],
  "cites": [
    "definition:appB_observer_metric"
  ],
  "depends_on": [
    "assumption:appB_srv_dissipativity",
    "definition:appB_observer_metric",
    "lemma:appB_energy_contraction"
  ],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "theorem:appB_srv_cauchy",
  "label": "theorem:appB_srv_cauchy",
  "latex_body": "\\begin{theorem}[Cauchy Convergence of SRV Trajectories]\n\\label{theorem:appB_srv_cauchy}\nAll SRV trajectories $\\{x_t\\}$ are Cauchy in $(\\mathcal{P}, d_{\\mathcal{O}})$ (cf.~\\ref{definition:appB_observer_metric}).\n\\end{theorem}",
  "lean_alignment": {
    "conditions": [
      "modeling laws are structure fields or explicit hypotheses; continuum/categorical content is NOT formalized"
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": false,
    "notes": [
      "Does not construct the observer metric d_O or prove literal Cauchy-ness of the trajectory. Instead proves the quantitative content the Cauchy claim depends on: given a lower bound on energy, the cumulative and individual squared-drift terms stay uniformly bounded across all steps. This is a genuinely weaker, honest substitute, not a full proof of the stated theorem."
    ],
    "record_ids": [
      "MAP-SMALLPACK-004"
    ],
    "statuses": [
      "open_bridge"
    ],
    "witnesses": [
      "SmallPack.symbolicEnergyContraction_sum_bounded",
      "SmallPack.symbolicEnergyContraction_term_bounded"
    ]
  },
  "line": 160,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Cauchy Convergence of SRV Trajectories",
  "proof_labels": [
    "proof:appB_srv_cauchy"
  ],
  "proof_status": "proven",
  "ref_roles": [
    {
      "context": "ies] \\label{theorem:appB_srv_cauchy} All SRV trajectories $\\{x_t\\}$ are Cauchy in $(\\mathcal{P}, d_{\\mathcal{O}})$ (cf.~\\ref{definition:appB_observer_metric}). \\end{theorem}",
      "label": "definition:appB_observer_metric",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "appendix_symbolic_reflexive_validation.tex",
      "target_line": 112,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:appB_observer_metric"
  ],
  "role": "theorem",
  "type": "theorem"
}

proofappendix

proof:appB_srv_cauchy

proof:appB_srv_cauchy

Exact LaTeX body

\begin{proof}
\label{proof:appB_srv_cauchy}
\leavevmode
By the Energy Contraction Lemma (Lemma~\ref{lemma:appB_energy_contraction}) the energy is non-increasing and bounded below, hence convergent. By the $\mu$-strong convexity of $H_{\text{symb}}$ (Assumption~\ref{assumption:appB_srv_dissipativity}) the gradient step contracts the Hamiltonian gap linearly,
\[
H_{\text{symb}}(x_t)-H_{\text{symb}}^{\ast}\le (1-\mu\eta)^{t}\big(H_{\text{symb}}(x_0)-H_{\text{symb}}^{\ast}\big),\qquad 1-\mu\eta\in[0,1).
\]
By $L$-smoothness $\|\nabla H_{\text{symb}}(x_t)\|_\kappa\le\sqrt{2L\,(H_{\text{symb}}(x_t)-H_{\text{symb}}^{\ast})}$, so the drift magnitude decays geometrically, $\|\text{drift}_t\|_\kappa=\eta\|\nabla H_{\text{symb}}(x_t)\|_\kappa\le c\,(1-\mu\eta)^{t/2}$, and the non-expansive reflection magnitude is dominated by it. The observer-metric step is controlled by these magnitudes, $d_{\mathcal{O}}(x_t,x_{t+1})\le C\big(\|\text{drift}_t\|_\kappa+\|\text{refl}_t\|_\kappa\big)$ (Def.~\ref{definition:appB_observer_metric}), whence the consecutive-distance tail is summable and vanishing,
\[
\sum_{t\ge N} d_{\mathcal{O}}(x_t,x_{t+1})\le C'\sum_{t\ge N}(1-\mu\eta)^{t/2}=\frac{C'\,(1-\mu\eta)^{N/2}}{1-(1-\mu\eta)^{1/2}}\xrightarrow[N\to\infty]{}0 .
\]
A sequence whose consecutive-distance tails vanish is Cauchy; therefore every SRV trajectory is Cauchy in $(\mathcal{P},d_{\mathcal{O}})$.
\end{proof}

Reference roles

TargetRoleLogical support
assumption:appB_srv_dissipativitydefinition_anchoryes
definition:appB_observer_metricdefinition_anchoryes
lemma:appB_energy_contractionproof_supportyes
Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [],
  "cites": [
    "assumption:appB_srv_dissipativity",
    "definition:appB_observer_metric",
    "lemma:appB_energy_contraction"
  ],
  "depends_on": [
    "assumption:appB_srv_dissipativity",
    "definition:appB_observer_metric",
    "lemma:appB_energy_contraction"
  ],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "proof:appB_srv_cauchy",
  "label": "proof:appB_srv_cauchy",
  "latex_body": "\\begin{proof}\n\\label{proof:appB_srv_cauchy}\n\\leavevmode\nBy the Energy Contraction Lemma (Lemma~\\ref{lemma:appB_energy_contraction}) the energy is non-increasing and bounded below, hence convergent. By the $\\mu$-strong convexity of $H_{\\text{symb}}$ (Assumption~\\ref{assumption:appB_srv_dissipativity}) the gradient step contracts the Hamiltonian gap linearly,\n\\[\nH_{\\text{symb}}(x_t)-H_{\\text{symb}}^{\\ast}\\le (1-\\mu\\eta)^{t}\\big(H_{\\text{symb}}(x_0)-H_{\\text{symb}}^{\\ast}\\big),\\qquad 1-\\mu\\eta\\in[0,1).\n\\]\nBy $L$-smoothness $\\|\\nabla H_{\\text{symb}}(x_t)\\|_\\kappa\\le\\sqrt{2L\\,(H_{\\text{symb}}(x_t)-H_{\\text{symb}}^{\\ast})}$, so the drift magnitude decays geometrically, $\\|\\text{drift}_t\\|_\\kappa=\\eta\\|\\nabla H_{\\text{symb}}(x_t)\\|_\\kappa\\le c\\,(1-\\mu\\eta)^{t/2}$, and the non-expansive reflection magnitude is dominated by it. The observer-metric step is controlled by these magnitudes, $d_{\\mathcal{O}}(x_t,x_{t+1})\\le C\\big(\\|\\text{drift}_t\\|_\\kappa+\\|\\text{refl}_t\\|_\\kappa\\big)$ (Def.~\\ref{definition:appB_observer_metric}), whence the consecutive-distance tail is summable and vanishing,\n\\[\n\\sum_{t\\ge N} d_{\\mathcal{O}}(x_t,x_{t+1})\\le C'\\sum_{t\\ge N}(1-\\mu\\eta)^{t/2}=\\frac{C'\\,(1-\\mu\\eta)^{N/2}}{1-(1-\\mu\\eta)^{1/2}}\\xrightarrow[N\\to\\infty]{}0 .\n\\]\nA sequence whose consecutive-distance tails vanish is Cauchy; therefore every SRV trajectory is Cauchy in $(\\mathcal{P},d_{\\mathcal{O}})$.\n\\end{proof}",
  "line": 164,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "",
  "proves": "theorem:appB_srv_cauchy",
  "ref_roles": [
    {
      "context": "y is non-increasing and bounded below, hence convergent. By the $\\mu$-strong convexity of $H_{\\text{symb}}$ (Assumption~\\ref{assumption:appB_srv_dissipativity}) the gradient step contracts the Hamiltonian gap linearly, \\[ H_{\\text{symb}}(x_t)-H_{\\text{symb}}^{\\ast}\\le (1-\\mu\\eta",
      "label": "assumption:appB_srv_dissipativity",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "appendix_symbolic_reflexive_validation.tex",
      "target_line": 133,
      "target_type": "assumption"
    },
    {
      "context": "these magnitudes, $d_{\\mathcal{O}}(x_t,x_{t+1})\\le C\\big(\\|\\text{drift}_t\\|_\\kappa+\\|\\text{refl}_t\\|_\\kappa\\big)$ (Def.~\\ref{definition:appB_observer_metric}), whence the consecutive-distance tail is summable and vanishing, \\[ \\sum_{t\\ge N} d_{\\mathcal{O}}(x_t,x_{t+1})\\le C'\\s",
      "label": "definition:appB_observer_metric",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "appendix_symbolic_reflexive_validation.tex",
      "target_line": 112,
      "target_type": "definition"
    },
    {
      "context": "\\begin{proof} \\label{proof:appB_srv_cauchy} \\leavevmode By the Energy Contraction Lemma (Lemma~\\ref{lemma:appB_energy_contraction}) the energy is non-increasing and bounded below, hence convergent. By the $\\mu$-strong convexity of $H_{\\text{symb}}$ (",
      "label": "lemma:appB_energy_contraction",
      "logical_support": true,
      "role": "proof_support",
      "target_file": "appendix_symbolic_reflexive_validation.tex",
      "target_line": 138,
      "target_type": "lemma"
    }
  ],
  "refs": [
    "assumption:appB_srv_dissipativity",
    "definition:appB_observer_metric",
    "lemma:appB_energy_contraction"
  ],
  "role": "proof",
  "type": "proof"
}

sectionsubsectionappendix

B.3 Metric Completion and Smooth Atlas

subsec:appB_smooth_completion

Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "subsec:appB_smooth_completion",
  "label": "subsec:appB_smooth_completion",
  "latex_body": "",
  "line": 179,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "B.3 Metric Completion and Smooth Atlas",
  "role": "section",
  "subtype": "subsection",
  "type": "section"
}

theoremprovenappendix

Existence of Metric Completion

theorem:appB_metric_completion

Exact LaTeX body

\begin{theorem}[Existence of Metric Completion]
\label{theorem:appB_metric_completion}
The metric completion $\overline{\mathcal{P}}$ of $(\mathcal{P}, d_{\mathcal{O}})$ exists and is separable.
The symbolic tower $\mathcal{P}$ is equipped with the coherence metric (cf.~\ref{definition:bk4_coherence_metric_on_symbolic_manifold}).
\end{theorem}

Reference roles

TargetRoleLogical support
definition:bk4_coherence_metric_on_symbolic_manifoldcf_near_matchyes
Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [
    "definition:appB_symbolic_chart",
    "proof:appB_resolution_of_smoothness",
    "proof:appB_smooth_atlas",
    "proof:appB_smoothness_emergence",
    "theorem:appB_smooth_atlas",
    "theorem:bk4_fuzzy_symbolic_geometry_theorem"
  ],
  "cites": [
    "definition:bk4_coherence_metric_on_symbolic_manifold"
  ],
  "depends_on": [
    "definition:appB_symbolic_state_space",
    "definition:bk4_coherence_metric_on_symbolic_manifold"
  ],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "theorem:appB_metric_completion",
  "label": "theorem:appB_metric_completion",
  "latex_body": "\\begin{theorem}[Existence of Metric Completion]\n\\label{theorem:appB_metric_completion}\nThe metric completion $\\overline{\\mathcal{P}}$ of $(\\mathcal{P}, d_{\\mathcal{O}})$ exists and is separable.\nThe symbolic tower $\\mathcal{P}$ is equipped with the coherence metric (cf.~\\ref{definition:bk4_coherence_metric_on_symbolic_manifold}).\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": true,
    "notes": [
      "\"the metric completion exists\" is re-read as \"a single global metric consistent with every chart exists\" via single_geometry_iff_glued, given PairCovers and Glued; separability is not modeled."
    ],
    "record_ids": [
      "MAP-SMALLPACK-010"
    ],
    "statuses": [
      "conditional"
    ],
    "witnesses": [
      "Book9B.atlas_consistent_of_glued_and_covers"
    ]
  },
  "line": 182,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Existence of Metric Completion",
  "proof_labels": [
    "proof:appB_metric_completion"
  ],
  "proof_status": "proven",
  "ref_roles": [
    {
      "context": "d_{\\mathcal{O}})$ exists and is separable. The symbolic tower $\\mathcal{P}$ is equipped with the coherence metric (cf.~\\ref{definition:bk4_coherence_metric_on_symbolic_manifold}). \\end{theorem}",
      "label": "definition:bk4_coherence_metric_on_symbolic_manifold",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book4.tex",
      "target_line": 2363,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:bk4_coherence_metric_on_symbolic_manifold"
  ],
  "role": "theorem",
  "type": "theorem"
}

proofappendix

proof:appB_metric_completion

proof:appB_metric_completion

Exact LaTeX body

\begin{proof}
\label{proof:appB_metric_completion}
\leavevmode
Every metric space admits a completion: form the equivalence classes of Cauchy sequences in $(\mathcal{P},d_{\mathcal{O}})$ under $\{x_t\}\sim\{y_t\}\Leftrightarrow d_{\mathcal{O}}(x_t,y_t)\to 0$, with the induced metric $\bar d_{\mathcal{O}}([x],[y])=\lim_t d_{\mathcal{O}}(x_t,y_t)$ (Def.~\ref{definition:bk4_coherence_metric_on_symbolic_manifold} supplies the metric). The resulting space $\overline{\mathcal{P}}$ is complete and contains $\mathcal{P}$ isometrically as a dense subset. For separability, recall the tower is the countable directed union $\mathcal{P}=\bigcup_{\lambda\in\mathbb{N}}P_\lambda$ (Def.~\ref{definition:appB_symbolic_state_space}), and each level $P_\lambda$ is bounded in complexity ($\le\lambda$) and operator norm ($\le\lambda$), hence totally bounded in $d_{\mathcal{O}}$ and therefore separable. A countable union of separable sets is separable, so $\mathcal{P}$ has a countable dense subset $Q$; since $\mathcal{P}$ is dense in $\overline{\mathcal{P}}$, $Q$ is dense in $\overline{\mathcal{P}}$ as well. Thus the completion $\overline{\mathcal{P}}$ exists and is separable.
\end{proof}

Reference roles

TargetRoleLogical support
definition:appB_symbolic_state_spacedefinition_anchoryes
definition:bk4_coherence_metric_on_symbolic_manifolddefinition_anchoryes
Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [],
  "cites": [
    "definition:appB_symbolic_state_space",
    "definition:bk4_coherence_metric_on_symbolic_manifold"
  ],
  "depends_on": [
    "definition:appB_symbolic_state_space",
    "definition:bk4_coherence_metric_on_symbolic_manifold"
  ],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "proof:appB_metric_completion",
  "label": "proof:appB_metric_completion",
  "latex_body": "\\begin{proof}\n\\label{proof:appB_metric_completion}\n\\leavevmode\nEvery metric space admits a completion: form the equivalence classes of Cauchy sequences in $(\\mathcal{P},d_{\\mathcal{O}})$ under $\\{x_t\\}\\sim\\{y_t\\}\\Leftrightarrow d_{\\mathcal{O}}(x_t,y_t)\\to 0$, with the induced metric $\\bar d_{\\mathcal{O}}([x],[y])=\\lim_t d_{\\mathcal{O}}(x_t,y_t)$ (Def.~\\ref{definition:bk4_coherence_metric_on_symbolic_manifold} supplies the metric). The resulting space $\\overline{\\mathcal{P}}$ is complete and contains $\\mathcal{P}$ isometrically as a dense subset. For separability, recall the tower is the countable directed union $\\mathcal{P}=\\bigcup_{\\lambda\\in\\mathbb{N}}P_\\lambda$ (Def.~\\ref{definition:appB_symbolic_state_space}), and each level $P_\\lambda$ is bounded in complexity ($\\le\\lambda$) and operator norm ($\\le\\lambda$), hence totally bounded in $d_{\\mathcal{O}}$ and therefore separable. A countable union of separable sets is separable, so $\\mathcal{P}$ has a countable dense subset $Q$; since $\\mathcal{P}$ is dense in $\\overline{\\mathcal{P}}$, $Q$ is dense in $\\overline{\\mathcal{P}}$ as well. Thus the completion $\\overline{\\mathcal{P}}$ exists and is separable.\n\\end{proof}",
  "line": 187,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "",
  "proves": "theorem:appB_metric_completion",
  "ref_roles": [
    {
      "context": "arability, recall the tower is the countable directed union $\\mathcal{P}=\\bigcup_{\\lambda\\in\\mathbb{N}}P_\\lambda$ (Def.~\\ref{definition:appB_symbolic_state_space}), and each level $P_\\lambda$ is bounded in complexity ($\\le\\lambda$) and operator norm ($\\le\\lambda$), hence totally bo",
      "label": "definition:appB_symbolic_state_space",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "appendix_symbolic_reflexive_validation.tex",
      "target_line": 103,
      "target_type": "definition"
    },
    {
      "context": "thcal{O}}(x_t,y_t)\\to 0$, with the induced metric $\\bar d_{\\mathcal{O}}([x],[y])=\\lim_t d_{\\mathcal{O}}(x_t,y_t)$ (Def.~\\ref{definition:bk4_coherence_metric_on_symbolic_manifold} supplies the metric). The resulting space $\\overline{\\mathcal{P}}$ is complete and contains $\\mathcal{P}$ isometrically",
      "label": "definition:bk4_coherence_metric_on_symbolic_manifold",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "book4.tex",
      "target_line": 2363,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:appB_symbolic_state_space",
    "definition:bk4_coherence_metric_on_symbolic_manifold"
  ],
  "role": "proof",
  "type": "proof"
}

definitiondefinitionalappendix

Symbolic Chart System

definition:appB_symbolic_chart

Exact LaTeX body

\begin{definition}[Symbolic Chart System]
\label{definition:appB_symbolic_chart}
For each $\lambda$, define:
\[
\chi_\lambda(s, \rho) = (\text{encode}_\lambda(s), \text{matrix}_\lambda(\rho)) \in \mathbb{R}^{d_\lambda}
\]
These charts coordinatize the completed manifold $M$ (cf.~\ref{theorem:appB_metric_completion}).
\end{definition}

Reference roles

TargetRoleLogical support
theorem:appB_metric_completioncf_near_matchyes
Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [
    "assumption:appB_chart_compatibility",
    "lemma:appB_chart_bounds",
    "proof:appB_chart_bounds",
    "proof:bk1_atlas_final_topology_phase_space",
    "theorem:appB_smooth_atlas"
  ],
  "cites": [
    "theorem:appB_metric_completion"
  ],
  "depends_on": [
    "theorem:appB_metric_completion"
  ],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "definition:appB_symbolic_chart",
  "label": "definition:appB_symbolic_chart",
  "latex_body": "\\begin{definition}[Symbolic Chart System]\n\\label{definition:appB_symbolic_chart}\nFor each $\\lambda$, define:\n\\[\n\\chi_\\lambda(s, \\rho) = (\\text{encode}_\\lambda(s), \\text{matrix}_\\lambda(\\rho)) \\in \\mathbb{R}^{d_\\lambda}\n\\]\nThese charts coordinatize the completed manifold $M$ (cf.~\\ref{theorem:appB_metric_completion}).\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": [
      "re-read over FracturedAtlas's ChartComplex rather than constructed from an encode/matrix pair; the specific R^{d_lambda} coordinatization is not modeled, only chart-consistency."
    ],
    "record_ids": [
      "MAP-SMALLPACK-009"
    ],
    "statuses": [
      "conditional"
    ],
    "witnesses": [
      "Book9B.atlas_consistent_of_glued_and_covers"
    ]
  },
  "line": 193,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Symbolic Chart System",
  "proof_status": "definitional",
  "ref_roles": [
    {
      "context": "), \\text{matrix}_\\lambda(\\rho)) \\in \\mathbb{R}^{d_\\lambda} \\] These charts coordinatize the completed manifold $M$ (cf.~\\ref{theorem:appB_metric_completion}). \\end{definition}",
      "label": "theorem:appB_metric_completion",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "appendix_symbolic_reflexive_validation.tex",
      "target_line": 182,
      "target_type": "theorem"
    }
  ],
  "refs": [
    "theorem:appB_metric_completion"
  ],
  "role": "definition",
  "type": "definition"
}

lemmaprovenappendix

Uniform Chart Bounds

lemma:appB_chart_bounds

Exact LaTeX body

\begin{lemma}[Uniform Chart Bounds]
\label{lemma:appB_chart_bounds}
For charts $\chi_\lambda$ (Def.~\ref{definition:appB_symbolic_chart}):
\[
\sup_{x \in P_\lambda} \|D\chi_\lambda(x)\|_{\text{op}} \leq C_{\text{chart}} \cdot \lambda^{1/2}
\]
\end{lemma}

Reference roles

TargetRoleLogical support
definition:appB_symbolic_chartdefinition_anchoryes
Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [
    "assumption:appB_chart_compatibility",
    "proof:appB_smooth_atlas"
  ],
  "cites": [
    "definition:appB_symbolic_chart"
  ],
  "depends_on": [
    "definition:appB_symbolic_chart",
    "definition:appB_symbolic_energy",
    "definition:appB_symbolic_state_space"
  ],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "lemma:appB_chart_bounds",
  "label": "lemma:appB_chart_bounds",
  "latex_body": "\\begin{lemma}[Uniform Chart Bounds]\n\\label{lemma:appB_chart_bounds}\nFor charts $\\chi_\\lambda$ (Def.~\\ref{definition:appB_symbolic_chart}):\n\\[\n\\sup_{x \\in P_\\lambda} \\|D\\chi_\\lambda(x)\\|_{\\text{op}} \\leq C_{\\text{chart}} \\cdot \\lambda^{1/2}\n\\]\n\\end{lemma}",
  "lean_alignment": {
    "conditions": [
      "modeling laws are structure fields or explicit hypotheses; continuum/categorical content is NOT formalized"
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "Models only the scalar bound expression C_chart * sqrt(lambda) and proves it is nonnegative and monotone nondecreasing in lambda. The operator-norm sup over the actual charts D chi_lambda is not modeled."
    ],
    "record_ids": [
      "MAP-SMALLPACK-005"
    ],
    "statuses": [
      "conditional"
    ],
    "witnesses": [
      "SmallPack.chartBound_mono",
      "SmallPack.chartBound_nonneg"
    ]
  },
  "line": 202,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Uniform Chart Bounds",
  "proof_labels": [
    "proof:appB_chart_bounds"
  ],
  "proof_status": "proven",
  "ref_roles": [
    {
      "context": "\\begin{lemma}[Uniform Chart Bounds] \\label{lemma:appB_chart_bounds} For charts $\\chi_\\lambda$ (Def.~\\ref{definition:appB_symbolic_chart}): \\[ \\sup_{x \\in P_\\lambda} \\|D\\chi_\\lambda(x)\\|_{\\text{op}} \\leq C_{\\text{chart}} \\cdot \\lambda^{1/2} \\] \\end{lemma}",
      "label": "definition:appB_symbolic_chart",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "appendix_symbolic_reflexive_validation.tex",
      "target_line": 193,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:appB_symbolic_chart"
  ],
  "role": "lemma",
  "type": "lemma"
}

proofappendix

proof:appB_chart_bounds

proof:appB_chart_bounds

Exact LaTeX body

\begin{proof}
\label{proof:appB_chart_bounds}
\leavevmode
On the level set $P_\lambda$ the chart $\chi_\lambda(s,\rho)=(\text{encode}_\lambda(s),\text{matrix}_\lambda(\rho))$ (Def.~\ref{definition:appB_symbolic_chart}) is the product of the symbolic encoding and the operator-coordinate map, each Lipschitz with respect to the coherence norm $\|\cdot\|_\kappa$ on the bounded domain, with a Lipschitz constant $C_{\text{chart}}$ independent of $\lambda$. The domain constrains both factors by the single resolution scale $\lambda$: $\text{complexity}(s)\le\lambda$ and $\|\rho\|_{\text{op}}\le\lambda$ (Def.~\ref{definition:appB_symbolic_state_space}). The norm controlling the differential is the energy norm (Def.~\ref{definition:appB_symbolic_energy}), whose quadratic kinetic terms make it scale as the square root of the level-$\lambda$ budget; consequently $\|D\chi_\lambda(x)\|_{\text{op}}\le C_{\text{chart}}\,\lambda^{1/2}$ for every $x\in P_\lambda$. Taking the supremum over $P_\lambda$ gives the stated uniform bound.
\end{proof}

Reference roles

TargetRoleLogical support
definition:appB_symbolic_chartdefinition_anchoryes
definition:appB_symbolic_energydefinition_anchoryes
definition:appB_symbolic_state_spacedefinition_anchoryes
Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [],
  "cites": [
    "definition:appB_symbolic_chart",
    "definition:appB_symbolic_energy",
    "definition:appB_symbolic_state_space"
  ],
  "depends_on": [
    "definition:appB_symbolic_chart",
    "definition:appB_symbolic_energy",
    "definition:appB_symbolic_state_space"
  ],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "proof:appB_chart_bounds",
  "label": "proof:appB_chart_bounds",
  "latex_body": "\\begin{proof}\n\\label{proof:appB_chart_bounds}\n\\leavevmode\nOn the level set $P_\\lambda$ the chart $\\chi_\\lambda(s,\\rho)=(\\text{encode}_\\lambda(s),\\text{matrix}_\\lambda(\\rho))$ (Def.~\\ref{definition:appB_symbolic_chart}) is the product of the symbolic encoding and the operator-coordinate map, each Lipschitz with respect to the coherence norm $\\|\\cdot\\|_\\kappa$ on the bounded domain, with a Lipschitz constant $C_{\\text{chart}}$ independent of $\\lambda$. The domain constrains both factors by the single resolution scale $\\lambda$: $\\text{complexity}(s)\\le\\lambda$ and $\\|\\rho\\|_{\\text{op}}\\le\\lambda$ (Def.~\\ref{definition:appB_symbolic_state_space}). The norm controlling the differential is the energy norm (Def.~\\ref{definition:appB_symbolic_energy}), whose quadratic kinetic terms make it scale as the square root of the level-$\\lambda$ budget; consequently $\\|D\\chi_\\lambda(x)\\|_{\\text{op}}\\le C_{\\text{chart}}\\,\\lambda^{1/2}$ for every $x\\in P_\\lambda$. Taking the supremum over $P_\\lambda$ gives the stated uniform bound.\n\\end{proof}",
  "line": 209,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "",
  "proves": "lemma:appB_chart_bounds",
  "ref_roles": [
    {
      "context": "the level set $P_\\lambda$ the chart $\\chi_\\lambda(s,\\rho)=(\\text{encode}_\\lambda(s),\\text{matrix}_\\lambda(\\rho))$ (Def.~\\ref{definition:appB_symbolic_chart}) is the product of the symbolic encoding and the operator-coordinate map, each Lipschitz with respect to the coherence",
      "label": "definition:appB_symbolic_chart",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "appendix_symbolic_reflexive_validation.tex",
      "target_line": 193,
      "target_type": "definition"
    },
    {
      "context": "mbda$ (Def.~\\ref{definition:appB_symbolic_state_space}). The norm controlling the differential is the energy norm (Def.~\\ref{definition:appB_symbolic_energy}), whose quadratic kinetic terms make it scale as the square root of the level-$\\lambda$ budget; consequently $\\|D\\chi_\\",
      "label": "definition:appB_symbolic_energy",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "appendix_symbolic_reflexive_validation.tex",
      "target_line": 125,
      "target_type": "definition"
    },
    {
      "context": "s by the single resolution scale $\\lambda$: $\\text{complexity}(s)\\le\\lambda$ and $\\|\\rho\\|_{\\text{op}}\\le\\lambda$ (Def.~\\ref{definition:appB_symbolic_state_space}). The norm controlling the differential is the energy norm (Def.~\\ref{definition:appB_symbolic_energy}), whose quadrati",
      "label": "definition:appB_symbolic_state_space",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "appendix_symbolic_reflexive_validation.tex",
      "target_line": 103,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:appB_symbolic_chart",
    "definition:appB_symbolic_energy",
    "definition:appB_symbolic_state_space"
  ],
  "role": "proof",
  "type": "proof"
}

assumptiondefinitionalappendix

Smooth Chart Compatibility

assumption:appB_chart_compatibility

Exact LaTeX body

\begin{assumption}[Smooth Chart Compatibility]
\label{assumption:appB_chart_compatibility}
The symbolic charts form a compatible atlas on the completion: each $\chi_\lambda$ (Def.~\ref{definition:appB_symbolic_chart}) is a homeomorphism of an open neighborhood in $M=\overline{\mathcal{P}}$ onto an open subset of $\mathbb{R}^{d_\lambda}$, and on each overlap $P_\lambda\cap P_\mu$ the transition map $\chi_\mu\circ\chi_\lambda^{-1}$ is a $C^\infty$ diffeomorphism between its open images. This is the structural hypothesis that the multi-resolution encodings $\text{encode}_\lambda$ refine one another smoothly; the uniform first-order control of Lemma~\ref{lemma:appB_chart_bounds} supplies the $C^1$ part, and the hypothesis upgrades overlap regularity to $C^\infty$.
\end{assumption}

Reference roles

TargetRoleLogical support
definition:appB_symbolic_chartdefinition_anchoryes
lemma:appB_chart_boundsformal_dependencyyes
Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [
    "proof:appB_smooth_atlas"
  ],
  "cites": [
    "definition:appB_symbolic_chart",
    "lemma:appB_chart_bounds"
  ],
  "depends_on": [
    "definition:appB_symbolic_chart",
    "lemma:appB_chart_bounds"
  ],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "assumption:appB_chart_compatibility",
  "label": "assumption:appB_chart_compatibility",
  "latex_body": "\\begin{assumption}[Smooth Chart Compatibility]\n\\label{assumption:appB_chart_compatibility}\nThe symbolic charts form a compatible atlas on the completion: each $\\chi_\\lambda$ (Def.~\\ref{definition:appB_symbolic_chart}) is a homeomorphism of an open neighborhood in $M=\\overline{\\mathcal{P}}$ onto an open subset of $\\mathbb{R}^{d_\\lambda}$, and on each overlap $P_\\lambda\\cap P_\\mu$ the transition map $\\chi_\\mu\\circ\\chi_\\lambda^{-1}$ is a $C^\\infty$ diffeomorphism between its open images. This is the structural hypothesis that the multi-resolution encodings $\\text{encode}_\\lambda$ refine one another smoothly; the uniform first-order control of Lemma~\\ref{lemma:appB_chart_bounds} supplies the $C^1$ part, and the hypothesis upgrades overlap regularity to $C^\\infty$.\n\\end{assumption}",
  "line": 215,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Smooth Chart Compatibility",
  "proof_status": "definitional",
  "ref_roles": [
    {
      "context": "tion:appB_chart_compatibility} The symbolic charts form a compatible atlas on the completion: each $\\chi_\\lambda$ (Def.~\\ref{definition:appB_symbolic_chart}) is a homeomorphism of an open neighborhood in $M=\\overline{\\mathcal{P}}$ onto an open subset of $\\mathbb{R}^{d_\\lambda",
      "label": "definition:appB_symbolic_chart",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "appendix_symbolic_reflexive_validation.tex",
      "target_line": 193,
      "target_type": "definition"
    },
    {
      "context": "ulti-resolution encodings $\\text{encode}_\\lambda$ refine one another smoothly; the uniform first-order control of Lemma~\\ref{lemma:appB_chart_bounds} supplies the $C^1$ part, and the hypothesis upgrades overlap regularity to $C^\\infty$. \\end{assumption}",
      "label": "lemma:appB_chart_bounds",
      "logical_support": true,
      "role": "formal_dependency",
      "target_file": "appendix_symbolic_reflexive_validation.tex",
      "target_line": 202,
      "target_type": "lemma"
    }
  ],
  "refs": [
    "definition:appB_symbolic_chart",
    "lemma:appB_chart_bounds"
  ],
  "role": "assumption",
  "type": "assumption"
}

theoremprovenappendix

Smooth Atlas on Completion

theorem:appB_smooth_atlas

Exact LaTeX body

\begin{theorem}[Smooth Atlas on Completion]
\label{theorem:appB_smooth_atlas}
The metric completion $M = \overline{\mathcal{P}}$ admits a smooth manifold structure compatible with the charts $\{\chi_\lambda\}$ (cf.~\ref{definition:appB_symbolic_chart}), constructed over the completed space (cf.~\ref{theorem:appB_metric_completion}).
\end{theorem}

Reference roles

TargetRoleLogical support
definition:appB_symbolic_chartcf_near_matchyes
theorem:appB_metric_completioncf_near_matchyes
Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [
    "proof:appB_resolution_of_smoothness",
    "proof:appB_smoothness_emergence"
  ],
  "cites": [
    "definition:appB_symbolic_chart",
    "theorem:appB_metric_completion"
  ],
  "depends_on": [
    "assumption:appB_chart_compatibility",
    "definition:appB_symbolic_chart",
    "definition:appB_symbolic_state_space",
    "lemma:appB_chart_bounds",
    "lemma:appB_energy_contraction",
    "theorem:appB_metric_completion"
  ],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "theorem:appB_smooth_atlas",
  "label": "theorem:appB_smooth_atlas",
  "latex_body": "\\begin{theorem}[Smooth Atlas on Completion]\n\\label{theorem:appB_smooth_atlas}\nThe metric completion $M = \\overline{\\mathcal{P}}$ admits a smooth manifold structure compatible with the charts $\\{\\chi_\\lambda\\}$ (cf.~\\ref{definition:appB_symbolic_chart}), constructed over the completed space (cf.~\\ref{theorem:appB_metric_completion}).\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": true,
    "notes": [
      "only chart-compatibility (existence of a consistent global metric) is modeled; the smooth-manifold structure itself is not."
    ],
    "record_ids": [
      "MAP-SMALLPACK-011"
    ],
    "statuses": [
      "conditional"
    ],
    "witnesses": [
      "Book9B.atlas_consistent_of_glued_and_covers"
    ]
  },
  "line": 220,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Smooth Atlas on Completion",
  "proof_labels": [
    "proof:appB_smooth_atlas"
  ],
  "proof_status": "proven",
  "ref_roles": [
    {
      "context": "tion $M = \\overline{\\mathcal{P}}$ admits a smooth manifold structure compatible with the charts $\\{\\chi_\\lambda\\}$ (cf.~\\ref{definition:appB_symbolic_chart}), constructed over the completed space (cf.~\\ref{theorem:appB_metric_completion}). \\end{theorem}",
      "label": "definition:appB_symbolic_chart",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "appendix_symbolic_reflexive_validation.tex",
      "target_line": 193,
      "target_type": "definition"
    },
    {
      "context": "ith the charts $\\{\\chi_\\lambda\\}$ (cf.~\\ref{definition:appB_symbolic_chart}), constructed over the completed space (cf.~\\ref{theorem:appB_metric_completion}). \\end{theorem}",
      "label": "theorem:appB_metric_completion",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "appendix_symbolic_reflexive_validation.tex",
      "target_line": 182,
      "target_type": "theorem"
    }
  ],
  "refs": [
    "definition:appB_symbolic_chart",
    "theorem:appB_metric_completion"
  ],
  "role": "theorem",
  "type": "theorem"
}

proofappendix

proof:appB_smooth_atlas

proof:appB_smooth_atlas

Exact LaTeX body

\begin{proof}
\label{proof:appB_smooth_atlas}
\leavevmode
By Thm.~\ref{theorem:appB_metric_completion} the completion $M=\overline{\mathcal{P}}$ is a separable complete metric space, hence Hausdorff. By Smooth Chart Compatibility (Assumption~\ref{assumption:appB_chart_compatibility}) each chart $\chi_\lambda$ is a homeomorphism of a neighborhood in $M$ onto an open subset of $\mathbb{R}^{d_\lambda}$, so $M$ is locally Euclidean, and the charts cover $M$ because every point of $\overline{\mathcal{P}}$ is a limit of points lying in some level $P_\lambda$ (Def.~\ref{definition:appB_symbolic_state_space}). The uniform chart bounds (Lemma~\ref{lemma:appB_chart_bounds}) keep the differentials non-degenerate in the limit, so no chart collapses; and by the same assumption the transition maps $\chi_\mu\circ\chi_\lambda^{-1}$ are $C^\infty$ on overlaps. Hence $\{\chi_\lambda\}$ is a smooth atlas and $M$ carries a smooth manifold structure compatible with the charts.
\end{proof}

Reference roles

TargetRoleLogical support
assumption:appB_chart_compatibilitydefinition_anchoryes
definition:appB_symbolic_state_spacedefinition_anchoryes
lemma:appB_chart_boundsproof_supportyes
lemma:appB_energy_contractionproof_supportyes
theorem:appB_metric_completionproof_supportyes
Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [],
  "cites": [
    "assumption:appB_chart_compatibility",
    "definition:appB_symbolic_state_space",
    "lemma:appB_chart_bounds",
    "lemma:appB_energy_contraction",
    "theorem:appB_metric_completion"
  ],
  "depends_on": [
    "assumption:appB_chart_compatibility",
    "definition:appB_symbolic_state_space",
    "lemma:appB_chart_bounds",
    "lemma:appB_energy_contraction",
    "theorem:appB_metric_completion"
  ],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "proof:appB_smooth_atlas",
  "label": "proof:appB_smooth_atlas",
  "latex_body": "\\begin{proof}\n\\label{proof:appB_smooth_atlas}\n\\leavevmode\nBy Thm.~\\ref{theorem:appB_metric_completion} the completion $M=\\overline{\\mathcal{P}}$ is a separable complete metric space, hence Hausdorff. By Smooth Chart Compatibility (Assumption~\\ref{assumption:appB_chart_compatibility}) each chart $\\chi_\\lambda$ is a homeomorphism of a neighborhood in $M$ onto an open subset of $\\mathbb{R}^{d_\\lambda}$, so $M$ is locally Euclidean, and the charts cover $M$ because every point of $\\overline{\\mathcal{P}}$ is a limit of points lying in some level $P_\\lambda$ (Def.~\\ref{definition:appB_symbolic_state_space}). The uniform chart bounds (Lemma~\\ref{lemma:appB_chart_bounds}) keep the differentials non-degenerate in the limit, so no chart collapses; and by the same assumption the transition maps $\\chi_\\mu\\circ\\chi_\\lambda^{-1}$ are $C^\\infty$ on overlaps. Hence $\\{\\chi_\\lambda\\}$ is a smooth atlas and $M$ carries a smooth manifold structure compatible with the charts.\n\\end{proof}",
  "line": 224,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "",
  "proves": "theorem:appB_smooth_atlas",
  "ref_roles": [
    {
      "context": "overline{\\mathcal{P}}$ is a separable complete metric space, hence Hausdorff. By Smooth Chart Compatibility (Assumption~\\ref{assumption:appB_chart_compatibility}) each chart $\\chi_\\lambda$ is a homeomorphism of a neighborhood in $M$ onto an open subset of $\\mathbb{R}^{d_\\lambda}$,",
      "label": "assumption:appB_chart_compatibility",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "appendix_symbolic_reflexive_validation.tex",
      "target_line": 215,
      "target_type": "assumption"
    },
    {
      "context": "ts cover $M$ because every point of $\\overline{\\mathcal{P}}$ is a limit of points lying in some level $P_\\lambda$ (Def.~\\ref{definition:appB_symbolic_state_space}). The uniform chart bounds (Lemma~\\ref{lemma:appB_chart_bounds}) keep the differentials non-degenerate in the limit, so",
      "label": "definition:appB_symbolic_state_space",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "appendix_symbolic_reflexive_validation.tex",
      "target_line": 103,
      "target_type": "definition"
    },
    {
      "context": "ints lying in some level $P_\\lambda$ (Def.~\\ref{definition:appB_symbolic_state_space}). The uniform chart bounds (Lemma~\\ref{lemma:appB_chart_bounds}) keep the differentials non-degenerate in the limit, so no chart collapses; and by the same assumption the transition m",
      "label": "lemma:appB_chart_bounds",
      "logical_support": true,
      "role": "proof_support",
      "target_file": "appendix_symbolic_reflexive_validation.tex",
      "target_line": 202,
      "target_type": "lemma"
    },
    {
      "context": "",
      "label": "lemma:appB_energy_contraction",
      "logical_support": true,
      "role": "proof_support",
      "target_file": "appendix_symbolic_reflexive_validation.tex",
      "target_line": 138,
      "target_type": "lemma"
    },
    {
      "context": "\\begin{proof} \\label{proof:appB_smooth_atlas} \\leavevmode By Thm.~\\ref{theorem:appB_metric_completion} the completion $M=\\overline{\\mathcal{P}}$ is a separable complete metric space, hence Hausdorff. By Smooth Chart Compat",
      "label": "theorem:appB_metric_completion",
      "logical_support": true,
      "role": "proof_support",
      "target_file": "appendix_symbolic_reflexive_validation.tex",
      "target_line": 182,
      "target_type": "theorem"
    }
  ],
  "refs": [
    "assumption:appB_chart_compatibility",
    "definition:appB_symbolic_state_space",
    "lemma:appB_chart_bounds",
    "theorem:appB_metric_completion"
  ],
  "role": "proof",
  "type": "proof"
}

sectionsubsectionappendix

B.4 Resolution of the Continuum Disjunction

subsec:appB_continuum_resolution

Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "subsec:appB_continuum_resolution",
  "label": "subsec:appB_continuum_resolution",
  "latex_body": "",
  "line": 240,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "B.4 Resolution of the Continuum Disjunction",
  "role": "section",
  "subtype": "subsection",
  "type": "section"
}

theoremprovenappendix

Emergent Smoothness from Symbolic Discreteness

theorem:appB_smoothness_emergence

Exact LaTeX body

\begin{theorem}[Emergent Smoothness from Symbolic Discreteness]
\label{theorem:appB_smoothness_emergence}
The completed space $M = \overline{\mathcal{P}}$ is a smooth, second-countable, paracompact manifold, confirming topological regularity (cf.~\ref{axiom:bk1_topological_regularity}) and realizing the pre-geometric nature of the framework (cf.~\ref{axiom:bk1_pre_geometric_nature}).
\end{theorem}

Reference roles

TargetRoleLogical support
axiom:bk1_pre_geometric_naturecf_near_matchyes
axiom:bk1_topological_regularitycf_near_matchyes
Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [
    "proof:appB_resolution_of_smoothness"
  ],
  "cites": [
    "axiom:bk1_pre_geometric_nature",
    "axiom:bk1_topological_regularity"
  ],
  "depends_on": [
    "axiom:bk1_pre_geometric_nature",
    "axiom:bk1_topological_regularity",
    "theorem:appB_metric_completion",
    "theorem:appB_smooth_atlas"
  ],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "theorem:appB_smoothness_emergence",
  "label": "theorem:appB_smoothness_emergence",
  "latex_body": "\\begin{theorem}[Emergent Smoothness from Symbolic Discreteness]\n\\label{theorem:appB_smoothness_emergence}\nThe completed space $M = \\overline{\\mathcal{P}}$ is a smooth, second-countable, paracompact manifold, confirming topological regularity (cf.~\\ref{axiom:bk1_topological_regularity}) and realizing the pre-geometric nature of the framework (cf.~\\ref{axiom:bk1_pre_geometric_nature}).\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": [
      "Book9B.no_global_metric_without_gluing"
    ],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "the converse/obstruction direction: charts that are not glued admit no consistent global metric. Smoothness, second-countability, and paracompactness are not modeled."
    ],
    "record_ids": [
      "MAP-SMALLPACK-012"
    ],
    "statuses": [
      "conditional"
    ],
    "witnesses": [
      "Book9B.no_global_metric_without_gluing"
    ]
  },
  "line": 243,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Emergent Smoothness from Symbolic Discreteness",
  "proof_labels": [
    "proof:appB_smoothness_emergence"
  ],
  "proof_status": "proven",
  "ref_roles": [
    {
      "context": "al regularity (cf.~\\ref{axiom:bk1_topological_regularity}) and realizing the pre-geometric nature of the framework (cf.~\\ref{axiom:bk1_pre_geometric_nature}). \\end{theorem}",
      "label": "axiom:bk1_pre_geometric_nature",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 1104,
      "target_type": "axiom"
    },
    {
      "context": "M = \\overline{\\mathcal{P}}$ is a smooth, second-countable, paracompact manifold, confirming topological regularity (cf.~\\ref{axiom:bk1_topological_regularity}) and realizing the pre-geometric nature of the framework (cf.~\\ref{axiom:bk1_pre_geometric_nature}). \\end{theorem}",
      "label": "axiom:bk1_topological_regularity",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 2758,
      "target_type": "axiom"
    }
  ],
  "refs": [
    "axiom:bk1_pre_geometric_nature",
    "axiom:bk1_topological_regularity"
  ],
  "role": "theorem",
  "type": "theorem"
}

proofappendix

proof:appB_smoothness_emergence

proof:appB_smoothness_emergence

Exact LaTeX body

\begin{proof}
\label{proof:appB_smoothness_emergence}
\leavevmode
By Thm.~\ref{theorem:appB_smooth_atlas} the completion $M=\overline{\mathcal{P}}$ is a smooth manifold. It is second-countable: $M$ is a separable metric space (Thm.~\ref{theorem:appB_metric_completion}), and a separable metric space is second-countable. It is Hausdorff, being metric. A locally Euclidean, Hausdorff, second-countable space is paracompact (each such space admits a countable, locally finite refinement of every open cover). Hence $M$ is a smooth, second-countable, paracompact manifold. This realizes the topological regularity posited in Ax.~\ref{axiom:bk1_topological_regularity} and the pre-geometric construction of Ax.~\ref{axiom:bk1_pre_geometric_nature}: the continuum manifold is obtained, not assumed, from the discrete symbolic tower by metric completion.
\end{proof}

Reference roles

TargetRoleLogical support
axiom:bk1_pre_geometric_naturedefinition_anchoryes
axiom:bk1_topological_regularitydefinition_anchoryes
theorem:appB_metric_completionproof_supportyes
theorem:appB_smooth_atlasproof_supportyes
Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [],
  "cites": [
    "axiom:bk1_pre_geometric_nature",
    "axiom:bk1_topological_regularity",
    "theorem:appB_metric_completion",
    "theorem:appB_smooth_atlas"
  ],
  "depends_on": [
    "axiom:bk1_pre_geometric_nature",
    "axiom:bk1_topological_regularity",
    "theorem:appB_metric_completion",
    "theorem:appB_smooth_atlas"
  ],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "proof:appB_smoothness_emergence",
  "label": "proof:appB_smoothness_emergence",
  "latex_body": "\\begin{proof}\n\\label{proof:appB_smoothness_emergence}\n\\leavevmode\nBy Thm.~\\ref{theorem:appB_smooth_atlas} the completion $M=\\overline{\\mathcal{P}}$ is a smooth manifold. It is second-countable: $M$ is a separable metric space (Thm.~\\ref{theorem:appB_metric_completion}), and a separable metric space is second-countable. It is Hausdorff, being metric. A locally Euclidean, Hausdorff, second-countable space is paracompact (each such space admits a countable, locally finite refinement of every open cover). Hence $M$ is a smooth, second-countable, paracompact manifold. This realizes the topological regularity posited in Ax.~\\ref{axiom:bk1_topological_regularity} and the pre-geometric construction of Ax.~\\ref{axiom:bk1_pre_geometric_nature}: the continuum manifold is obtained, not assumed, from the discrete symbolic tower by metric completion.\n\\end{proof}",
  "line": 247,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "",
  "proves": "theorem:appB_smoothness_emergence",
  "ref_roles": [
    {
      "context": "topological regularity posited in Ax.~\\ref{axiom:bk1_topological_regularity} and the pre-geometric construction of Ax.~\\ref{axiom:bk1_pre_geometric_nature}: the continuum manifold is obtained, not assumed, from the discrete symbolic tower by metric completion. \\end{proof}",
      "label": "axiom:bk1_pre_geometric_nature",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 1104,
      "target_type": "axiom"
    },
    {
      "context": "Hence $M$ is a smooth, second-countable, paracompact manifold. This realizes the topological regularity posited in Ax.~\\ref{axiom:bk1_topological_regularity} and the pre-geometric construction of Ax.~\\ref{axiom:bk1_pre_geometric_nature}: the continuum manifold is obtained, not",
      "label": "axiom:bk1_topological_regularity",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 2758,
      "target_type": "axiom"
    },
    {
      "context": "mpletion $M=\\overline{\\mathcal{P}}$ is a smooth manifold. It is second-countable: $M$ is a separable metric space (Thm.~\\ref{theorem:appB_metric_completion}), and a separable metric space is second-countable. It is Hausdorff, being metric. A locally Euclidean, Hausdorff, seco",
      "label": "theorem:appB_metric_completion",
      "logical_support": true,
      "role": "proof_support",
      "target_file": "appendix_symbolic_reflexive_validation.tex",
      "target_line": 182,
      "target_type": "theorem"
    },
    {
      "context": "\\begin{proof} \\label{proof:appB_smoothness_emergence} \\leavevmode By Thm.~\\ref{theorem:appB_smooth_atlas} the completion $M=\\overline{\\mathcal{P}}$ is a smooth manifold. It is second-countable: $M$ is a separable metric space",
      "label": "theorem:appB_smooth_atlas",
      "logical_support": true,
      "role": "proof_support",
      "target_file": "appendix_symbolic_reflexive_validation.tex",
      "target_line": 220,
      "target_type": "theorem"
    }
  ],
  "refs": [
    "axiom:bk1_pre_geometric_nature",
    "axiom:bk1_topological_regularity",
    "theorem:appB_metric_completion",
    "theorem:appB_smooth_atlas"
  ],
  "role": "proof",
  "type": "proof"
}

corollaryprovenappendix

Resolution of Symbolic Smoothness

corollary:appB_resolution_of_smoothness

Exact LaTeX body

\begin{corollary}[Resolution of Symbolic Smoothness]
\label{corollary:appB_resolution_of_smoothness}
The problem posed in Scholium~\ref{scholium:bk1_resolution_of_continuum_disjunction} is resolved: smooth structure arises constructively from discrete symbolic layers under bounded observer resolution.
\end{corollary}

Reference roles

TargetRoleLogical support
scholium:bk1_resolution_of_continuum_disjunctionformal_dependencyyes
Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [],
  "cites": [
    "scholium:bk1_resolution_of_continuum_disjunction"
  ],
  "depends_on": [
    "definition:appB_symbolic_state_space",
    "lemma:appB_energy_contraction",
    "scholium:bk1_resolution_of_continuum_disjunction",
    "theorem:appB_metric_completion",
    "theorem:appB_smooth_atlas",
    "theorem:appB_smoothness_emergence",
    "theorem:appB_srv_cauchy"
  ],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "corollary:appB_resolution_of_smoothness",
  "label": "corollary:appB_resolution_of_smoothness",
  "latex_body": "\\begin{corollary}[Resolution of Symbolic Smoothness]\n\\label{corollary:appB_resolution_of_smoothness}\nThe problem posed in Scholium~\\ref{scholium:bk1_resolution_of_continuum_disjunction} is resolved: smooth structure arises constructively from discrete symbolic layers under bounded observer resolution.\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": [
      "Book9B.no_global_metric_without_gluing"
    ],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "\"smooth structure arises... under bounded observer resolution\" is re-read as its failure mode: resolution that is not consistent across charts (not Glued) yields no single global metric."
    ],
    "record_ids": [
      "MAP-SMALLPACK-013"
    ],
    "statuses": [
      "conditional"
    ],
    "witnesses": [
      "Book9B.no_global_metric_without_gluing"
    ]
  },
  "line": 253,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Resolution of Symbolic Smoothness",
  "proof_labels": [
    "proof:appB_resolution_of_smoothness"
  ],
  "proof_status": "proven",
  "ref_roles": [
    {
      "context": "llary}[Resolution of Symbolic Smoothness] \\label{corollary:appB_resolution_of_smoothness} The problem posed in Scholium~\\ref{scholium:bk1_resolution_of_continuum_disjunction} is resolved: smooth structure arises constructively from discrete symbolic layers under bounded observer resolution. \\e",
      "label": "scholium:bk1_resolution_of_continuum_disjunction",
      "logical_support": true,
      "role": "formal_dependency",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 2709,
      "target_type": "scholium"
    }
  ],
  "refs": [
    "scholium:bk1_resolution_of_continuum_disjunction"
  ],
  "role": "corollary",
  "type": "corollary"
}

proofappendix

proof:appB_resolution_of_smoothness

proof:appB_resolution_of_smoothness

Exact LaTeX body

\begin{proof}
\label{proof:appB_resolution_of_smoothness}
\leavevmode
Scholium~\ref{scholium:bk1_resolution_of_continuum_disjunction} poses the disjunction between a discrete symbolic substrate and a continuous, smooth manifold. The construction of this appendix dissolves it constructively: from the discrete, finite-complexity symbolic tower $\mathcal{P}=\bigcup_\lambda P_\lambda$ (Def.~\ref{definition:appB_symbolic_state_space}), the SRV dynamics are dissipative (Lemma~\ref{lemma:appB_energy_contraction}) and their trajectories Cauchy (Thm.~\ref{theorem:appB_srv_cauchy}); metric completion yields a separable complete space (Thm.~\ref{theorem:appB_metric_completion}) carrying a smooth, paracompact manifold structure (Thm.~\ref{theorem:appB_smooth_atlas}, Thm.~\ref{theorem:appB_smoothness_emergence}). Smoothness therefore arises \emph{from} the discrete layers under bounded observer resolution rather than being postulated beside them, which is precisely the resolution the Scholium calls for.
\end{proof}

Reference roles

TargetRoleLogical support
definition:appB_symbolic_state_spacedefinition_anchoryes
lemma:appB_energy_contractionproof_supportyes
scholium:bk1_resolution_of_continuum_disjunctionproof_supportyes
theorem:appB_metric_completionproof_supportyes
theorem:appB_smooth_atlasproof_supportyes
theorem:appB_smoothness_emergenceproof_supportyes
theorem:appB_srv_cauchyproof_supportyes
Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [],
  "cites": [
    "definition:appB_symbolic_state_space",
    "lemma:appB_energy_contraction",
    "scholium:bk1_resolution_of_continuum_disjunction",
    "theorem:appB_metric_completion",
    "theorem:appB_smooth_atlas",
    "theorem:appB_smoothness_emergence",
    "theorem:appB_srv_cauchy"
  ],
  "depends_on": [
    "definition:appB_symbolic_state_space",
    "lemma:appB_energy_contraction",
    "scholium:bk1_resolution_of_continuum_disjunction",
    "theorem:appB_metric_completion",
    "theorem:appB_smooth_atlas",
    "theorem:appB_smoothness_emergence",
    "theorem:appB_srv_cauchy"
  ],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "proof:appB_resolution_of_smoothness",
  "label": "proof:appB_resolution_of_smoothness",
  "latex_body": "\\begin{proof}\n\\label{proof:appB_resolution_of_smoothness}\n\\leavevmode\nScholium~\\ref{scholium:bk1_resolution_of_continuum_disjunction} poses the disjunction between a discrete symbolic substrate and a continuous, smooth manifold. The construction of this appendix dissolves it constructively: from the discrete, finite-complexity symbolic tower $\\mathcal{P}=\\bigcup_\\lambda P_\\lambda$ (Def.~\\ref{definition:appB_symbolic_state_space}), the SRV dynamics are dissipative (Lemma~\\ref{lemma:appB_energy_contraction}) and their trajectories Cauchy (Thm.~\\ref{theorem:appB_srv_cauchy}); metric completion yields a separable complete space (Thm.~\\ref{theorem:appB_metric_completion}) carrying a smooth, paracompact manifold structure (Thm.~\\ref{theorem:appB_smooth_atlas}, Thm.~\\ref{theorem:appB_smoothness_emergence}). Smoothness therefore arises \\emph{from} the discrete layers under bounded observer resolution rather than being postulated beside them, which is precisely the resolution the Scholium calls for.\n\\end{proof}",
  "line": 257,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "",
  "proves": "corollary:appB_resolution_of_smoothness",
  "ref_roles": [
    {
      "context": "es it constructively: from the discrete, finite-complexity symbolic tower $\\mathcal{P}=\\bigcup_\\lambda P_\\lambda$ (Def.~\\ref{definition:appB_symbolic_state_space}), the SRV dynamics are dissipative (Lemma~\\ref{lemma:appB_energy_contraction}) and their trajectories Cauchy (Thm.~\\ref",
      "label": "definition:appB_symbolic_state_space",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "appendix_symbolic_reflexive_validation.tex",
      "target_line": 103,
      "target_type": "definition"
    },
    {
      "context": "}=\\bigcup_\\lambda P_\\lambda$ (Def.~\\ref{definition:appB_symbolic_state_space}), the SRV dynamics are dissipative (Lemma~\\ref{lemma:appB_energy_contraction}) and their trajectories Cauchy (Thm.~\\ref{theorem:appB_srv_cauchy}); metric completion yields a separable complete spac",
      "label": "lemma:appB_energy_contraction",
      "logical_support": true,
      "role": "proof_support",
      "target_file": "appendix_symbolic_reflexive_validation.tex",
      "target_line": 138,
      "target_type": "lemma"
    },
    {
      "context": "\\begin{proof} \\label{proof:appB_resolution_of_smoothness} \\leavevmode Scholium~\\ref{scholium:bk1_resolution_of_continuum_disjunction} poses the disjunction between a discrete symbolic substrate and a continuous, smooth manifold. The construction of this",
      "label": "scholium:bk1_resolution_of_continuum_disjunction",
      "logical_support": true,
      "role": "proof_support",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 2709,
      "target_type": "scholium"
    },
    {
      "context": "eir trajectories Cauchy (Thm.~\\ref{theorem:appB_srv_cauchy}); metric completion yields a separable complete space (Thm.~\\ref{theorem:appB_metric_completion}) carrying a smooth, paracompact manifold structure (Thm.~\\ref{theorem:appB_smooth_atlas}, Thm.~\\ref{theorem:appB_smooth",
      "label": "theorem:appB_metric_completion",
      "logical_support": true,
      "role": "proof_support",
      "target_file": "appendix_symbolic_reflexive_validation.tex",
      "target_line": 182,
      "target_type": "theorem"
    },
    {
      "context": "able complete space (Thm.~\\ref{theorem:appB_metric_completion}) carrying a smooth, paracompact manifold structure (Thm.~\\ref{theorem:appB_smooth_atlas}, Thm.~\\ref{theorem:appB_smoothness_emergence}). Smoothness therefore arises \\emph{from} the discrete layers under bound",
      "label": "theorem:appB_smooth_atlas",
      "logical_support": true,
      "role": "proof_support",
      "target_file": "appendix_symbolic_reflexive_validation.tex",
      "target_line": 220,
      "target_type": "theorem"
    },
    {
      "context": ":appB_metric_completion}) carrying a smooth, paracompact manifold structure (Thm.~\\ref{theorem:appB_smooth_atlas}, Thm.~\\ref{theorem:appB_smoothness_emergence}). Smoothness therefore arises \\emph{from} the discrete layers under bounded observer resolution rather than being postu",
      "label": "theorem:appB_smoothness_emergence",
      "logical_support": true,
      "role": "proof_support",
      "target_file": "appendix_symbolic_reflexive_validation.tex",
      "target_line": 243,
      "target_type": "theorem"
    },
    {
      "context": "ace}), the SRV dynamics are dissipative (Lemma~\\ref{lemma:appB_energy_contraction}) and their trajectories Cauchy (Thm.~\\ref{theorem:appB_srv_cauchy}); metric completion yields a separable complete space (Thm.~\\ref{theorem:appB_metric_completion}) carrying a smooth, pa",
      "label": "theorem:appB_srv_cauchy",
      "logical_support": true,
      "role": "proof_support",
      "target_file": "appendix_symbolic_reflexive_validation.tex",
      "target_line": 160,
      "target_type": "theorem"
    }
  ],
  "refs": [
    "definition:appB_symbolic_state_space",
    "lemma:appB_energy_contraction",
    "scholium:bk1_resolution_of_continuum_disjunction",
    "theorem:appB_metric_completion",
    "theorem:appB_smooth_atlas",
    "theorem:appB_smoothness_emergence",
    "theorem:appB_srv_cauchy"
  ],
  "role": "proof",
  "type": "proof"
}

remarkappendix

Executable Resolution of Smoothness

remark:appB_executable_resolution_smoothness

Exact LaTeX body

\begin{remark}[Executable Resolution of Smoothness]
\label{remark:appB_executable_resolution_smoothness}
The theoretical results presented here are verified through executable Python simulations included with this appendix. 
Rather than appealing to numerical coincidence, these simulations implement the SRV flow and symbolic metric directly, 
demonstrating that $\varphi$ arises as a coherence-preserving attractor and that symbolic curvature is observable via compression behavior.
This fulfills the symbolic resolution of the continuum disjunction proposed in Scholium~\ref{scholium:bk1_resolution_of_continuum_disjunction}.
\end{remark}

Reference roles

TargetRoleLogical support
scholium:bk1_resolution_of_continuum_disjunctionformal_dependencyyes
Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [],
  "cites": [
    "scholium:bk1_resolution_of_continuum_disjunction"
  ],
  "depends_on": [
    "scholium:bk1_resolution_of_continuum_disjunction"
  ],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "remark:appB_executable_resolution_smoothness",
  "label": "remark:appB_executable_resolution_smoothness",
  "latex_body": "\\begin{remark}[Executable Resolution of Smoothness]\n\\label{remark:appB_executable_resolution_smoothness}\nThe theoretical results presented here are verified through executable Python simulations included with this appendix. \nRather than appealing to numerical coincidence, these simulations implement the SRV flow and symbolic metric directly, \ndemonstrating that $\\varphi$ arises as a coherence-preserving attractor and that symbolic curvature is observable via compression behavior.\nThis fulfills the symbolic resolution of the continuum disjunction proposed in Scholium~\\ref{scholium:bk1_resolution_of_continuum_disjunction}.\n\\end{remark}",
  "line": 263,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Executable Resolution of Smoothness",
  "ref_roles": [
    {
      "context": "vable via compression behavior. This fulfills the symbolic resolution of the continuum disjunction proposed in Scholium~\\ref{scholium:bk1_resolution_of_continuum_disjunction}. \\end{remark}",
      "label": "scholium:bk1_resolution_of_continuum_disjunction",
      "logical_support": true,
      "role": "formal_dependency",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 2709,
      "target_type": "scholium"
    }
  ],
  "refs": [
    "scholium:bk1_resolution_of_continuum_disjunction"
  ],
  "role": "remark",
  "type": "remark"
}

sectionsubsectionappendix

B.5 Consequences for Machine Learning

subsec:appB_ml_consequences

Reference roles

TargetRoleLogical support
remark:bk7_unnamed_remark_03navigationno
Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [],
  "cites": [
    "remark:bk7_unnamed_remark_03"
  ],
  "depends_on": [
    "remark:bk7_unnamed_remark_03"
  ],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "subsec:appB_ml_consequences",
  "label": "subsec:appB_ml_consequences",
  "latex_body": "",
  "line": 272,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "B.5 Consequences for Machine Learning",
  "ref_roles": [
    {
      "context": "",
      "label": "remark:bk7_unnamed_remark_03",
      "logical_support": false,
      "role": "navigation",
      "target_file": "book7.tex",
      "target_line": 440,
      "target_type": "remark"
    }
  ],
  "role": "section",
  "subtype": "subsection",
  "type": "section"
}

remarkappendix

SRV and Embodied Predictive Geometry

remark:appB_embodied_predictive_geometry

Exact LaTeX body

\begin{remark}[SRV and Embodied Predictive Geometry]
\label{remark:appB_embodied_predictive_geometry}
The drift-reflection formalism
(Def.~\ref{definition:bk1_drift_field};
Def.~\ref{definition:bk1_reflection_operator}) applies to symbolic computation
and embodied prediction in biological and artificial agents.
Under SRV, a sensorimotor loop that injects perturbations (drift) and contracts
prediction error through internal models (reflection) traces a Cauchy path in
observer metric $d_{\mathcal{O}}$, constructing a smooth manifold of embodied
states.
Kinesthetic sense is one example.
More broadly, SRV predicts continuous felt geometry across vestibular balance,
active touch, and visuo-motor alignment, consistent with
sensorimotor-contingency theory.
These links suggest that the symbolic manifold may provide a unifying geometry
for diverse forms of embodied cognition.
\end{remark}

Reference roles

TargetRoleLogical support
definition:bk1_drift_fielddefinition_anchoryes
definition:bk1_reflection_operatordefinition_anchoryes
Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [],
  "cites": [
    "definition:bk1_drift_field",
    "definition:bk1_reflection_operator"
  ],
  "depends_on": [
    "definition:bk1_drift_field",
    "definition:bk1_reflection_operator"
  ],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "remark:appB_embodied_predictive_geometry",
  "label": "remark:appB_embodied_predictive_geometry",
  "latex_body": "\\begin{remark}[SRV and Embodied Predictive Geometry]\n\\label{remark:appB_embodied_predictive_geometry}\nThe drift-reflection formalism\n(Def.~\\ref{definition:bk1_drift_field};\nDef.~\\ref{definition:bk1_reflection_operator}) applies to symbolic computation\nand embodied prediction in biological and artificial agents.\nUnder SRV, a sensorimotor loop that injects perturbations (drift) and contracts\nprediction error through internal models (reflection) traces a Cauchy path in\nobserver metric $d_{\\mathcal{O}}$, constructing a smooth manifold of embodied\nstates.\nKinesthetic sense is one example.\nMore broadly, SRV predicts continuous felt geometry across vestibular balance,\nactive touch, and visuo-motor alignment, consistent with\nsensorimotor-contingency theory.\nThese links suggest that the symbolic manifold may provide a unifying geometry\nfor diverse forms of embodied cognition.\n\\end{remark}",
  "line": 283,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "SRV and Embodied Predictive Geometry",
  "ref_roles": [
    {
      "context": "and Embodied Predictive Geometry] \\label{remark:appB_embodied_predictive_geometry} The drift-reflection formalism (Def.~\\ref{definition:bk1_drift_field}; Def.~\\ref{definition:bk1_reflection_operator}) applies to symbolic computation and embodied prediction in biological a",
      "label": "definition:bk1_drift_field",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 1198,
      "target_type": "definition"
    },
    {
      "context": "l{remark:appB_embodied_predictive_geometry} The drift-reflection formalism (Def.~\\ref{definition:bk1_drift_field}; Def.~\\ref{definition:bk1_reflection_operator}) applies to symbolic computation and embodied prediction in biological and artificial agents. Under SRV, a sensorimotor",
      "label": "definition:bk1_reflection_operator",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 1209,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:bk1_drift_field",
    "definition:bk1_reflection_operator"
  ],
  "role": "remark",
  "type": "remark"
}

sectionsubsectionappendix

B.6 Scholium: The Synthetic Resolution

scholium:appB_synthetic_resolution

Reference roles

TargetRoleLogical support
definition:bk1_reflection_operatornavigationno
Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [],
  "cites": [
    "definition:bk1_reflection_operator"
  ],
  "depends_on": [
    "definition:bk1_reflection_operator"
  ],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "scholium:appB_synthetic_resolution",
  "label": "scholium:appB_synthetic_resolution",
  "latex_body": "",
  "line": 302,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "B.6 Scholium: The Synthetic Resolution",
  "ref_roles": [
    {
      "context": "",
      "label": "definition:bk1_reflection_operator",
      "logical_support": false,
      "role": "navigation",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 1209,
      "target_type": "definition"
    }
  ],
  "role": "section",
  "subtype": "subsection",
  "type": "section"
}

sectionsubsectionappendix

Technical Note

subsec:appB_technical_note

Complete structured record
{
  "book": "appendix_symbolic_reflexive_validation",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "appendix_symbolic_reflexive_validation.tex",
  "id": "subsec:appB_technical_note",
  "label": "subsec:appB_technical_note",
  "latex_body": "",
  "line": 323,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Technical Note",
  "role": "section",
  "subtype": "subsection",
  "type": "section"
}

sectionsectionsource_support

Trace 1: Symbolic Drift Stability

section:trace1_symbolic_drift_stability

Complete structured record
{
  "book": "trace1",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "trace1.tex",
  "id": "section:trace1_symbolic_drift_stability",
  "label": "section:trace1_symbolic_drift_stability",
  "latex_body": "",
  "line": 1,
  "macros_used": [],
  "matter_region": "source_support",
  "matter_role": "source_support",
  "name": "Trace 1: Symbolic Drift Stability",
  "role": "section",
  "subtype": "section",
  "type": "section"
}

sectionsubsectionsource_support

1 Objective

subsection:trace1_objective

Complete structured record
{
  "book": "trace1",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "trace1.tex",
  "id": "subsection:trace1_objective",
  "label": "subsection:trace1_objective",
  "latex_body": "",
  "line": 10,
  "macros_used": [],
  "matter_region": "source_support",
  "matter_role": "source_support",
  "name": "1 Objective",
  "role": "section",
  "subtype": "subsection",
  "type": "section"
}

sectionsubsectionsource_support

2 Validation Setup

subsection:trace1_validation_setup

Complete structured record
{
  "book": "trace1",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "trace1.tex",
  "id": "subsection:trace1_validation_setup",
  "label": "subsection:trace1_validation_setup",
  "latex_body": "",
  "line": 15,
  "macros_used": [],
  "matter_region": "source_support",
  "matter_role": "source_support",
  "name": "2 Validation Setup",
  "role": "section",
  "subtype": "subsection",
  "type": "section"
}

sectionsubsectionsource_support

3 Symbolic Responses

subsection:trace1_symbolic_responses

Complete structured record
{
  "book": "trace1",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "trace1.tex",
  "id": "subsection:trace1_symbolic_responses",
  "label": "subsection:trace1_symbolic_responses",
  "latex_body": "",
  "line": 26,
  "macros_used": [],
  "matter_region": "source_support",
  "matter_role": "source_support",
  "name": "3 Symbolic Responses",
  "role": "section",
  "subtype": "subsection",
  "type": "section"
}

sectionsubsectionsource_support

4 Observations

subsection:trace1_observations

Complete structured record
{
  "book": "trace1",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "trace1.tex",
  "id": "subsection:trace1_observations",
  "label": "subsection:trace1_observations",
  "latex_body": "",
  "line": 34,
  "macros_used": [],
  "matter_region": "source_support",
  "matter_role": "source_support",
  "name": "4 Observations",
  "role": "section",
  "subtype": "subsection",
  "type": "section"
}

sectionsubsectionsource_support

5 Conclusion

subsection:trace1_conclusion

Complete structured record
{
  "book": "trace1",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "trace1.tex",
  "id": "subsection:trace1_conclusion",
  "label": "subsection:trace1_conclusion",
  "latex_body": "",
  "line": 41,
  "macros_used": [],
  "matter_region": "source_support",
  "matter_role": "source_support",
  "name": "5 Conclusion",
  "role": "section",
  "subtype": "subsection",
  "type": "section"
}

sectionsubsectionsource_support

6 Theory Linkage

subsection:trace1_theory_linkage

Complete structured record
{
  "book": "trace1",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "trace1.tex",
  "id": "subsection:trace1_theory_linkage",
  "label": "subsection:trace1_theory_linkage",
  "latex_body": "",
  "line": 46,
  "macros_used": [],
  "matter_region": "source_support",
  "matter_role": "source_support",
  "name": "6 Theory Linkage",
  "role": "section",
  "subtype": "subsection",
  "type": "section"
}

sectionsectionsource_support

Trace 2: Symbolic Entropy Growth

section:trace2_symbolic_entropy_growth

Complete structured record
{
  "book": "trace2",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "trace2.tex",
  "id": "section:trace2_symbolic_entropy_growth",
  "label": "section:trace2_symbolic_entropy_growth",
  "latex_body": "",
  "line": 1,
  "macros_used": [],
  "matter_region": "source_support",
  "matter_role": "source_support",
  "name": "Trace 2: Symbolic Entropy Growth",
  "role": "section",
  "subtype": "section",
  "type": "section"
}