axiomdefinitionalappendix

PS--C4 (Ray invariance)

axiom:appC_psc4

Exact LaTeX body

\begin{axiom}[PS--C4 (Ray invariance)]
\label{axiom:appC_psc4}
$\mathcal{C}_{\Obs}(e^{i\theta} \tilde\psi_{\Obs}, \Pi)
= \mathcal{C}_{\Obs}(\tilde\psi_{\Obs}, \Pi)$ \quad (cf.~\ref{definition:appC_coherence_functional}).
The corresponding complex homogeneity is phase-faithful: amplitudes scale through
$\overline a a=|a|^2$, not through the real shadow $a^2$.
\end{axiom}

Reference roles

TargetRoleLogical support
definition:appC_coherence_functionalcf_near_matchyes
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [
    "definition:appC_coherence_functional"
  ],
  "depends_on": [
    "definition:appC_coherence_functional"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "axiom:appC_psc4",
  "label": "axiom:appC_psc4",
  "latex_body": "\\begin{axiom}[PS--C4 (Ray invariance)]\n\\label{axiom:appC_psc4}\n$\\mathcal{C}_{\\Obs}(e^{i\\theta} \\tilde\\psi_{\\Obs}, \\Pi)\n= \\mathcal{C}_{\\Obs}(\\tilde\\psi_{\\Obs}, \\Pi)$ \\quad (cf.~\\ref{definition:appC_coherence_functional}).\nThe corresponding complex homogeneity is phase-faithful: amplitudes scale through\n$\\overline a a=|a|^2$, not through the real shadow $a^2$.\n\\end{axiom}",
  "lean_alignment": {
    "conditions": [
      "Gleason-type uniqueness (axioms force the Born form in d>=3) and PS-C5 stay open; only the forward direction Born => axioms is certified",
      "continuum charge/action integrals stay open; the discrete conservation mechanism is certified"
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "The Born form is phase-invariant (ray invariance).",
      "The exact kernel supports the phase-faithful correction without certifying the PS axiom as derived."
    ],
    "record_ids": [
      "MAP-APPENDIX_DUAL_HORIZON-044",
      "Q-COMPLEX-06"
    ],
    "statuses": [
      "exact"
    ],
    "witnesses": [
      "Book7QuantumGleason.complex_phase_refutes_real_degreeTwo",
      "Book7QuantumGleason.vectorExpectation_globalPhase",
      "Book7QuantumGleason.vectorExpectation_smul",
      "Born.psc4_ray_invariance"
    ]
  },
  "line": 612,
  "macros_used": [
    "Obs"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "PS--C4 (Ray invariance)",
  "proof_status": "definitional",
  "ref_roles": [
    {
      "context": "_psc4} $\\mathcal{C}_{\\Obs}(e^{i\\theta} \\tilde\\psi_{\\Obs}, \\Pi) = \\mathcal{C}_{\\Obs}(\\tilde\\psi_{\\Obs}, \\Pi)$ \\quad (cf.~\\ref{definition:appC_coherence_functional}). The corresponding complex homogeneity is phase-faithful: amplitudes scale through $\\overline a a=|a|^2$, not through",
      "label": "definition:appC_coherence_functional",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 361,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:appC_coherence_functional"
  ],
  "role": "axiom",
  "type": "axiom"
}

axiomdefinitionalappendix

PS--C5 (Resolution-limited distinguishability)

axiom:appC_psc5

Exact LaTeX body

\begin{axiom}[PS--C5 (Resolution-limited distinguishability)]
\label{axiom:appC_psc5}
If $\Pi_1 \perp \Pi_2$ and $\| \Pi_1 - \Pi_2 \| > \epsilon_{\Obs}$,
then both coherence values cannot equal 1 for the same pure state (cf.~\ref{definition:appC_coherence_functional}).
\end{axiom}

Reference roles

TargetRoleLogical support
definition:appC_coherence_functionalcf_near_matchyes
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "assumption:appC_bounded_discernibility",
    "remark:appC_psc3prime_open_route"
  ],
  "cites": [
    "definition:appC_coherence_functional"
  ],
  "depends_on": [
    "definition:appC_coherence_functional"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "axiom:appC_psc5",
  "label": "axiom:appC_psc5",
  "latex_body": "\\begin{axiom}[PS--C5 (Resolution-limited distinguishability)]\n\\label{axiom:appC_psc5}\nIf $\\Pi_1 \\perp \\Pi_2$ and $\\| \\Pi_1 - \\Pi_2 \\| > \\epsilon_{\\Obs}$,\nthen both coherence values cannot equal 1 for the same pure state (cf.~\\ref{definition:appC_coherence_functional}).\n\\end{axiom}",
  "lean_alignment": {
    "conditions": [
      "PS-C3-prime supplied as a cross-frame budget law",
      "PS-C5 supplied as a separated-orthogonal exclusivity law",
      "coherence values bounded in the unit interval"
    ],
    "countermodels": [
      "AppendixCoherenceAxioms.boundedness_does_not_force_resolution_distinguishability"
    ],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "Typed resolution axiom excludes simultaneous unit coherence for separated orthogonal questions. Countermodel confirms ordinary [0,1] boundedness does not derive PS-C5; it remains an explicit physical axiom."
    ],
    "record_ids": [
      "MAP-APPENDIX_DUAL_HORIZON-050"
    ],
    "statuses": [
      "conditional"
    ],
    "witnesses": [
      "AppendixCoherenceAxioms.boundedness_does_not_force_resolution_distinguishability",
      "AppendixCoherenceAxioms.separated_orthogonal_questions_not_both_maximal"
    ]
  },
  "line": 620,
  "macros_used": [
    "Obs"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "PS--C5 (Resolution-limited distinguishability)",
  "proof_status": "definitional",
  "ref_roles": [
    {
      "context": "_2$ and $\\| \\Pi_1 - \\Pi_2 \\| > \\epsilon_{\\Obs}$, then both coherence values cannot equal 1 for the same pure state (cf.~\\ref{definition:appC_coherence_functional}). \\end{axiom}",
      "label": "definition:appC_coherence_functional",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 361,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:appC_coherence_functional"
  ],
  "role": "axiom",
  "type": "axiom"
}

axiomdefinitionalappendix

PS--C6 (Pure-state calibration)

axiom:appC_psc6

Exact LaTeX body

\begin{axiom}[PS--C6 (Pure-state calibration)]
\label{axiom:appC_psc6}
If the observer representation $\tilde\psi_{\Obs}$ represents the normalized pure
state $\psi\in\Horizon$ at the working resolution and
$P_\psi:=|\psi\rangle\langle\psi|$, then
\[
\mathcal{C}_{\Obs}(\tilde\psi_{\Obs},P_\psi)=1.
\]
Equivalently, the question whose range is precisely the represented ray is
answered with full coherence by that represented pure state.
\end{axiom}
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "appendix_dual_horizon.tex",
  "id": "axiom:appC_psc6",
  "label": "axiom:appC_psc6",
  "latex_body": "\\begin{axiom}[PS--C6 (Pure-state calibration)]\n\\label{axiom:appC_psc6}\nIf the observer representation $\\tilde\\psi_{\\Obs}$ represents the normalized pure\nstate $\\psi\\in\\Horizon$ at the working resolution and\n$P_\\psi:=|\\psi\\rangle\\langle\\psi|$, then\n\\[\n\\mathcal{C}_{\\Obs}(\\tilde\\psi_{\\Obs},P_\\psi)=1.\n\\]\nEquivalently, the question whose range is precisely the represented ray is\nanswered with full coherence by that represented pure state.\n\\end{axiom}",
  "lean_alignment": {
    "conditions": [
      "Gleason-type uniqueness (axioms force the Born form in d>=3) and PS-C5 stay open; only the forward direction Born => axioms is certified",
      "continuum charge/action integrals stay open; the discrete conservation mechanism is certified"
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "The Born form calibrates: a pure state answers its own question with coherence 1."
    ],
    "record_ids": [
      "MAP-APPENDIX_DUAL_HORIZON-045"
    ],
    "statuses": [
      "exact"
    ],
    "witnesses": [
      "Born.psc6_calibration"
    ]
  },
  "line": 626,
  "macros_used": [
    "Horizon",
    "Obs"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "PS--C6 (Pure-state calibration)",
  "proof_status": "definitional",
  "refs": [],
  "role": "axiom",
  "type": "axiom"
}

sectionsubsectionappendix

Preparatory Lemmas

subsec:appC_born_lemmas

Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "appendix_dual_horizon.tex",
  "id": "subsec:appC_born_lemmas",
  "label": "subsec:appC_born_lemmas",
  "latex_body": "",
  "line": 638,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Preparatory Lemmas",
  "role": "section",
  "subtype": "subsection",
  "type": "section"
}

lemmaprovenappendix

Finite orthogonal additivity gives a Gleason frame function

lemma:appC_sigma_additivity

Exact LaTeX body

\begin{lemma}[Finite orthogonal additivity gives a Gleason frame function]
\label{lemma:appC_sigma_additivity}
Let $\dim\Horizon=d<\infty$ and fix an observer-state representation
$\tilde\psi_{\Obs}$. Define
$\mu_\psi(\Pi):=\mathcal{C}_{\Obs}(\tilde\psi_{\Obs},\Pi)$.
Boundedness (PS--C1) and within-frame additivity (PS--C3, now
Cor.~\ref{axiom:appC_psc3}, established as
Thm.~\ref{theorem:appC_orthogonal_additivity}) imply that $\mu_\psi$ is a
normalized nonnegative finitely additive measure on $Proj(\Horizon)$; equivalently, its restriction to
rank-one projectors is a normalized frame function. Since $\Horizon$ is finite
dimensional, every orthogonal family of nonzero projectors is finite, so finite
orthogonal additivity is also countable additivity in the only sense required by
finite-dimensional Gleason theory.
\end{lemma}

Reference roles

TargetRoleLogical support
axiom:appC_psc3formal_dependencyyes
theorem:appC_orthogonal_additivityformal_dependencyyes
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "proof:appC_born_rule"
  ],
  "cites": [
    "axiom:appC_psc3",
    "theorem:appC_orthogonal_additivity"
  ],
  "depends_on": [
    "axiom:appC_psc3",
    "theorem:appC_orthogonal_additivity"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "lemma:appC_sigma_additivity",
  "label": "lemma:appC_sigma_additivity",
  "latex_body": "\\begin{lemma}[Finite orthogonal additivity gives a Gleason frame function]\n\\label{lemma:appC_sigma_additivity}\nLet $\\dim\\Horizon=d<\\infty$ and fix an observer-state representation\n$\\tilde\\psi_{\\Obs}$. Define\n$\\mu_\\psi(\\Pi):=\\mathcal{C}_{\\Obs}(\\tilde\\psi_{\\Obs},\\Pi)$.\nBoundedness (PS--C1) and within-frame additivity (PS--C3, now\nCor.~\\ref{axiom:appC_psc3}, established as\nThm.~\\ref{theorem:appC_orthogonal_additivity}) imply that $\\mu_\\psi$ is a\nnormalized nonnegative finitely additive measure on $Proj(\\Horizon)$; equivalently, its restriction to\nrank-one projectors is a normalized frame function. Since $\\Horizon$ is finite\ndimensional, every orthogonal family of nonzero projectors is finite, so finite\northogonal additivity is also countable additivity in the only sense required by\nfinite-dimensional Gleason theory.\n\\end{lemma}",
  "lean_alignment": {
    "conditions": [
      "continuum/categorical content is NOT formalized; static and finite-discrete kernels only",
      "modeling laws are structure fields or explicit hypotheses"
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": false,
    "notes": [
      "Only the finite-dimensional remark is realized: since the frame-index type is a Fintype, summing mu_conservation over Finset.univ already covers every orthogonal family a finite-dimensional Horizon can present. The Gleason-frame-function / normalized-measure identification itself is not separately formalized."
    ],
    "record_ids": [
      "MAP-APPENDIX_DUAL_HORIZON-011"
    ],
    "statuses": [
      "open_bridge"
    ],
    "witnesses": [
      "AppendixDH.mu_conservation"
    ]
  },
  "line": 641,
  "macros_used": [
    "Horizon",
    "Obs"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Finite orthogonal additivity gives a Gleason frame function",
  "proof_labels": [
    "proof:appC_sigma_additivity"
  ],
  "proof_status": "proven",
  "ref_roles": [
    {
      "context": "si(\\Pi):=\\mathcal{C}_{\\Obs}(\\tilde\\psi_{\\Obs},\\Pi)$. Boundedness (PS--C1) and within-frame additivity (PS--C3, now Cor.~\\ref{axiom:appC_psc3}, established as Thm.~\\ref{theorem:appC_orthogonal_additivity}) imply that $\\mu_\\psi$ is a normalized nonnegative finite",
      "label": "axiom:appC_psc3",
      "logical_support": true,
      "role": "formal_dependency",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 591,
      "target_type": "corollary"
    },
    {
      "context": "s},\\Pi)$. Boundedness (PS--C1) and within-frame additivity (PS--C3, now Cor.~\\ref{axiom:appC_psc3}, established as Thm.~\\ref{theorem:appC_orthogonal_additivity}) imply that $\\mu_\\psi$ is a normalized nonnegative finitely additive measure on $Proj(\\Horizon)$; equivalently, its res",
      "label": "theorem:appC_orthogonal_additivity",
      "logical_support": true,
      "role": "formal_dependency",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 504,
      "target_type": "theorem"
    }
  ],
  "refs": [
    "axiom:appC_psc3",
    "theorem:appC_orthogonal_additivity"
  ],
  "role": "lemma",
  "type": "lemma"
}

proofappendix

proof:appC_sigma_additivity

proof:appC_sigma_additivity

Exact LaTeX body

\begin{proof}
\label{proof:appC_sigma_additivity}
By PS--C1, $0\le \mu_\psi(\Pi)\le 1$ for all projectors $\Pi$. By
Corollary~\ref{axiom:appC_psc3}, applied to the one-element decomposition
$\{\mathbbm{1}\}$, $\mu_\psi(\mathbbm{1})=1$; applying
Theorem~\ref{theorem:appC_orthogonal_additivity} to the empty sum gives
$\mu_\psi(0)=0$. For any mutually orthogonal finite family
$\{\Pi_i\}_{i=1}^n$, Theorem~\ref{theorem:appC_orthogonal_additivity} gives
\[
\mu_\psi\!\left(\sum_{i=1}^n \Pi_i\right)=\sum_{i=1}^n \mu_\psi(\Pi_i).
\]
If $\{P_i\}_{i=1}^d$ is an orthonormal rank-one resolution of the identity, then
$\sum_i\mu_\psi(P_i)=\mu_\psi(\mathbbm{1})=1$, which is exactly the normalized
frame-function condition. Finally, an orthogonal family of nonzero subspaces in a
$d$-dimensional Hilbert space has cardinality at most $d$; hence no additional
countable-additivity condition remains to be checked.
\end{proof}

Reference roles

TargetRoleLogical support
axiom:appC_psc3proof_supportyes
theorem:appC_orthogonal_additivityproof_supportyes
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [
    "axiom:appC_psc3",
    "theorem:appC_orthogonal_additivity"
  ],
  "depends_on": [
    "axiom:appC_psc3",
    "theorem:appC_orthogonal_additivity"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "proof:appC_sigma_additivity",
  "label": "proof:appC_sigma_additivity",
  "latex_body": "\\begin{proof}\n\\label{proof:appC_sigma_additivity}\nBy PS--C1, $0\\le \\mu_\\psi(\\Pi)\\le 1$ for all projectors $\\Pi$. By\nCorollary~\\ref{axiom:appC_psc3}, applied to the one-element decomposition\n$\\{\\mathbbm{1}\\}$, $\\mu_\\psi(\\mathbbm{1})=1$; applying\nTheorem~\\ref{theorem:appC_orthogonal_additivity} to the empty sum gives\n$\\mu_\\psi(0)=0$. For any mutually orthogonal finite family\n$\\{\\Pi_i\\}_{i=1}^n$, Theorem~\\ref{theorem:appC_orthogonal_additivity} gives\n\\[\n\\mu_\\psi\\!\\left(\\sum_{i=1}^n \\Pi_i\\right)=\\sum_{i=1}^n \\mu_\\psi(\\Pi_i).\n\\]\nIf $\\{P_i\\}_{i=1}^d$ is an orthonormal rank-one resolution of the identity, then\n$\\sum_i\\mu_\\psi(P_i)=\\mu_\\psi(\\mathbbm{1})=1$, which is exactly the normalized\nframe-function condition. Finally, an orthogonal family of nonzero subspaces in a\n$d$-dimensional Hilbert space has cardinality at most $d$; hence no additional\ncountable-additivity condition remains to be checked.\n\\end{proof}",
  "line": 656,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "",
  "proves": "lemma:appC_sigma_additivity",
  "ref_roles": [
    {
      "context": "{proof} \\label{proof:appC_sigma_additivity} By PS--C1, $0\\le \\mu_\\psi(\\Pi)\\le 1$ for all projectors $\\Pi$. By Corollary~\\ref{axiom:appC_psc3}, applied to the one-element decomposition $\\{\\mathbbm{1}\\}$, $\\mu_\\psi(\\mathbbm{1})=1$; applying Theorem~\\ref{theorem:a",
      "label": "axiom:appC_psc3",
      "logical_support": true,
      "role": "proof_support",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 591,
      "target_type": "corollary"
    },
    {
      "context": "iom:appC_psc3}, applied to the one-element decomposition $\\{\\mathbbm{1}\\}$, $\\mu_\\psi(\\mathbbm{1})=1$; applying Theorem~\\ref{theorem:appC_orthogonal_additivity} to the empty sum gives $\\mu_\\psi(0)=0$. For any mutually orthogonal finite family $\\{\\Pi_i\\}_{i=1}^n$, Theorem~\\ref{the",
      "label": "theorem:appC_orthogonal_additivity",
      "logical_support": true,
      "role": "proof_support",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 504,
      "target_type": "theorem"
    }
  ],
  "refs": [
    "axiom:appC_psc3",
    "theorem:appC_orthogonal_additivity"
  ],
  "role": "proof",
  "type": "proof"
}

lemmaprovenappendix

Unitary covariance of the measure family

lemma:appC_unitary_invariance

Exact LaTeX body

\begin{lemma}[Unitary covariance of the measure family]
\label{lemma:appC_unitary_invariance}
For every unitary $U$ and projector $\Pi$,
\[
\mu_{U\psi}(U\Pi U^\dagger)=\mu_\psi(\Pi),
\]
where $\mu_\psi(\Pi):=\mathcal{C}_{\Obs}(\tilde\psi_{\Obs},\Pi)$ and
$\mu_{U\psi}$ denotes the assignment associated with the transformed observer
representation $U\tilde\psi_{\Obs}$.
\end{lemma}
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "appendix_dual_horizon.tex",
  "id": "lemma:appC_unitary_invariance",
  "label": "lemma:appC_unitary_invariance",
  "latex_body": "\\begin{lemma}[Unitary covariance of the measure family]\n\\label{lemma:appC_unitary_invariance}\nFor every unitary $U$ and projector $\\Pi$,\n\\[\n\\mu_{U\\psi}(U\\Pi U^\\dagger)=\\mu_\\psi(\\Pi),\n\\]\nwhere $\\mu_\\psi(\\Pi):=\\mathcal{C}_{\\Obs}(\\tilde\\psi_{\\Obs},\\Pi)$ and\n$\\mu_{U\\psi}$ denotes the assignment associated with the transformed observer\nrepresentation $U\\tilde\\psi_{\\Obs}$.\n\\end{lemma}",
  "lean_alignment": {
    "conditions": [
      "Gleason-type uniqueness (axioms force the Born form in d>=3) and PS-C5 stay open; only the forward direction Born => axioms is certified",
      "continuum charge/action integrals stay open; the discrete conservation mechanism is certified"
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "The measure family is unitary-covariant - same kernel as PS-C2."
    ],
    "record_ids": [
      "MAP-APPENDIX_DUAL_HORIZON-043"
    ],
    "statuses": [
      "exact"
    ],
    "witnesses": [
      "Born.psc2_unitary_covariance"
    ]
  },
  "line": 674,
  "macros_used": [
    "Obs"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Unitary covariance of the measure family",
  "proof_labels": [
    "proof:appC_unitary_invariance"
  ],
  "proof_status": "proven",
  "refs": [],
  "role": "lemma",
  "type": "lemma"
}

proofappendix

proof:appC_unitary_invariance

proof:appC_unitary_invariance

Exact LaTeX body

\begin{proof}
\label{proof:appC_unitary_invariance}
This is precisely PS--C2 written in measure notation:
\[
\mu_{U\psi}(U\Pi U^\dagger)
=\mathcal{C}_{\Obs}(U\tilde\psi_{\Obs},U\Pi U^\dagger)
=\mathcal{C}_{\Obs}(\tilde\psi_{\Obs},\Pi)
=\mu_\psi(\Pi).
\]
Ray invariance PS--C4 ensures that this statement depends only on the ray of the
state representation and not on its arbitrary global phase.
\end{proof}
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "appendix_dual_horizon.tex",
  "id": "proof:appC_unitary_invariance",
  "label": "proof:appC_unitary_invariance",
  "latex_body": "\\begin{proof}\n\\label{proof:appC_unitary_invariance}\nThis is precisely PS--C2 written in measure notation:\n\\[\n\\mu_{U\\psi}(U\\Pi U^\\dagger)\n=\\mathcal{C}_{\\Obs}(U\\tilde\\psi_{\\Obs},U\\Pi U^\\dagger)\n=\\mathcal{C}_{\\Obs}(\\tilde\\psi_{\\Obs},\\Pi)\n=\\mu_\\psi(\\Pi).\n\\]\nRay invariance PS--C4 ensures that this statement depends only on the ray of the\nstate representation and not on its arbitrary global phase.\n\\end{proof}",
  "line": 685,
  "macros_used": [
    "Obs"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "",
  "proves": "lemma:appC_unitary_invariance",
  "refs": [],
  "role": "proof",
  "type": "proof"
}

sectionsubsectionappendix

Main Theorem

subsec:appC_born_theorem

Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "appendix_dual_horizon.tex",
  "id": "subsec:appC_born_theorem",
  "label": "subsec:appC_born_theorem",
  "latex_body": "",
  "line": 698,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Main Theorem",
  "role": "section",
  "subtype": "subsection",
  "type": "section"
}

theoremprovenappendix

Observer-relative Born Rule

theorem:appC_born_rule

Exact LaTeX body

\begin{theorem}[Observer-relative Born Rule]
\label{theorem:appC_born_rule}
Let $\dim \Horizon = d \geq 3$, let $\psi\in\Horizon$ be normalized, and suppose
PS--C1--PS--C6 hold for the observer representation $\tilde\psi_{\Obs}$. Then for
any rank-one projector $\Pi_a = |a\rangle \langle a|$,
\[
\mathcal{C}_{\Obs}(\tilde\psi_{\Obs}, \Pi_a)
= |\langle a | \psi \rangle|^2 .
\]
More generally, for every projector $\Pi\in Proj(\Horizon)$,
\[
\mathcal{C}_{\Obs}(\tilde\psi_{\Obs},\Pi)=\operatorname{tr}(P_\psi\Pi),
\qquad P_\psi:=|\psi\rangle\langle\psi|.
\]
\end{theorem}
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "proof:appC_mixed_states",
    "proof:appC_qubit_case",
    "remark:appC_psc3prime_open_route",
    "remark:bk7_pisu_status",
    "scholium:bk7_born_as_hilbert_cross_section",
    "subsec:bk7_pisu_implications"
  ],
  "cites": [],
  "depends_on": [
    "lemma:appC_sigma_additivity"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "theorem:appC_born_rule",
  "label": "theorem:appC_born_rule",
  "latex_body": "\\begin{theorem}[Observer-relative Born Rule]\n\\label{theorem:appC_born_rule}\nLet $\\dim \\Horizon = d \\geq 3$, let $\\psi\\in\\Horizon$ be normalized, and suppose\nPS--C1--PS--C6 hold for the observer representation $\\tilde\\psi_{\\Obs}$. Then for\nany rank-one projector $\\Pi_a = |a\\rangle \\langle a|$,\n\\[\n\\mathcal{C}_{\\Obs}(\\tilde\\psi_{\\Obs}, \\Pi_a)\n= |\\langle a | \\psi \\rangle|^2 .\n\\]\nMore generally, for every projector $\\Pi\\in Proj(\\Horizon)$,\n\\[\n\\mathcal{C}_{\\Obs}(\\tilde\\psi_{\\Obs},\\Pi)=\\operatorname{tr}(P_\\psi\\Pi),\n\\qquad P_\\psi:=|\\psi\\rangle\\langle\\psi|.\n\\]\n\\end{theorem}",
  "lean_alignment": {
    "conditions": [
      "Gleason-type uniqueness (axioms force the Born form in d>=3) and PS-C5 stay open; only the forward direction Born => axioms is certified",
      "continuum charge/action integrals stay open; the discrete conservation mechanism is certified"
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "The broader appendix argument remains human mathematics; neither formal half-bridge is mislabeled as the classical theorem.",
      "The rank-one Born value taken as the coherence functional, computed on the qubit and bounded by 1; Gleason-type uniqueness (axioms force this form in d>=3) stays a counsel-permanent open."
    ],
    "record_ids": [
      "MAP-APPENDIX_DUAL_HORIZON-046",
      "Q-BORN-07"
    ],
    "statuses": [
      "conditional",
      "interpretive"
    ],
    "witnesses": [
      "Born.coh_le_one",
      "Born.qubit_born"
    ]
  },
  "line": 701,
  "macros_used": [
    "Horizon",
    "Obs"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Observer-relative Born Rule",
  "proof_labels": [
    "proof:appC_born_rule"
  ],
  "proof_status": "proven",
  "refs": [],
  "role": "theorem",
  "type": "theorem"
}

proofappendix

proof:appC_born_rule

proof:appC_born_rule

Exact LaTeX body

\begin{proof}
\label{proof:appC_born_rule}
Set $\mu_\psi(\Pi)=\mathcal{C}_{\Obs}(\tilde\psi_{\Obs},\Pi)$. By
Lemma~\ref{lemma:appC_sigma_additivity}, $\mu_\psi$ is a normalized nonnegative
frame function on the projectors of a Hilbert space of dimension at least three.
Finite-dimensional Gleason's theorem therefore gives a unique positive trace-one
operator $W_\psi$ such that
\[
\mu_\psi(\Pi)=\operatorname{tr}(W_\psi\Pi)
\quad\text{for every }\Pi\in Proj(\Horizon).
\]
By PS--C6, $1=\mu_\psi(P_\psi)=\operatorname{tr}(W_\psi P_\psi)
=\langle\psi,W_\psi\psi\rangle$. Write the spectral decomposition
$W_\psi=\sum_j p_j |u_j\rangle\langle u_j|$, with $p_j\ge0$ and
$\sum_j p_j=1$. Then
\[
1=\sum_j p_j |\langle u_j,\psi\rangle|^2 \le \sum_j p_j=1.
\]
Equality is possible only when every eigenvector with $p_j>0$ is colinear with
$\psi$. Hence $W_\psi=P_\psi$. Consequently
\[
\mathcal{C}_{\Obs}(\tilde\psi_{\Obs},\Pi)
=\operatorname{tr}(P_\psi\Pi)
\]
for all projectors $\Pi$. Taking $\Pi=\Pi_a=|a\rangle\langle a|$ gives
\[
\operatorname{tr}(P_\psi\Pi_a)=\langle a,P_\psi a\rangle
=|\langle a|\psi\rangle|^2,
\]
which is the Born rule.
\end{proof}

Reference roles

TargetRoleLogical support
lemma:appC_sigma_additivityproof_supportyes
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [
    "lemma:appC_sigma_additivity"
  ],
  "depends_on": [
    "lemma:appC_sigma_additivity"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "proof:appC_born_rule",
  "label": "proof:appC_born_rule",
  "latex_body": "\\begin{proof}\n\\label{proof:appC_born_rule}\nSet $\\mu_\\psi(\\Pi)=\\mathcal{C}_{\\Obs}(\\tilde\\psi_{\\Obs},\\Pi)$. By\nLemma~\\ref{lemma:appC_sigma_additivity}, $\\mu_\\psi$ is a normalized nonnegative\nframe function on the projectors of a Hilbert space of dimension at least three.\nFinite-dimensional Gleason's theorem therefore gives a unique positive trace-one\noperator $W_\\psi$ such that\n\\[\n\\mu_\\psi(\\Pi)=\\operatorname{tr}(W_\\psi\\Pi)\n\\quad\\text{for every }\\Pi\\in Proj(\\Horizon).\n\\]\nBy PS--C6, $1=\\mu_\\psi(P_\\psi)=\\operatorname{tr}(W_\\psi P_\\psi)\n=\\langle\\psi,W_\\psi\\psi\\rangle$. Write the spectral decomposition\n$W_\\psi=\\sum_j p_j |u_j\\rangle\\langle u_j|$, with $p_j\\ge0$ and\n$\\sum_j p_j=1$. Then\n\\[\n1=\\sum_j p_j |\\langle u_j,\\psi\\rangle|^2 \\le \\sum_j p_j=1.\n\\]\nEquality is possible only when every eigenvector with $p_j>0$ is colinear with\n$\\psi$. Hence $W_\\psi=P_\\psi$. Consequently\n\\[\n\\mathcal{C}_{\\Obs}(\\tilde\\psi_{\\Obs},\\Pi)\n=\\operatorname{tr}(P_\\psi\\Pi)\n\\]\nfor all projectors $\\Pi$. Taking $\\Pi=\\Pi_a=|a\\rangle\\langle a|$ gives\n\\[\n\\operatorname{tr}(P_\\psi\\Pi_a)=\\langle a,P_\\psi a\\rangle\n=|\\langle a|\\psi\\rangle|^2,\n\\]\nwhich is the Born rule.\n\\end{proof}",
  "line": 717,
  "macros_used": [
    "Horizon",
    "Obs"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "",
  "proves": "theorem:appC_born_rule",
  "ref_roles": [
    {
      "context": "\\begin{proof} \\label{proof:appC_born_rule} Set $\\mu_\\psi(\\Pi)=\\mathcal{C}_{\\Obs}(\\tilde\\psi_{\\Obs},\\Pi)$. By Lemma~\\ref{lemma:appC_sigma_additivity}, $\\mu_\\psi$ is a normalized nonnegative frame function on the projectors of a Hilbert space of dimension at least three",
      "label": "lemma:appC_sigma_additivity",
      "logical_support": true,
      "role": "proof_support",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 641,
      "target_type": "lemma"
    }
  ],
  "refs": [
    "lemma:appC_sigma_additivity"
  ],
  "role": "proof",
  "type": "proof"
}

corollaryprovenappendix

Qubit case \texorpdfstring{$d = 2$}{d = 2}

corollary:appC_qubit_case

Exact LaTeX body

\begin{corollary}[Qubit case \texorpdfstring{$d = 2$}{d = 2}]
\label{corollary:appC_qubit_case}
Let $V\cong\mathbb{C}^2$ be a qubit subspace. If the qubit coherence assignment is
the restriction of a PS--C1--PS--C6 assignment on an embedding
$\widehat\Horizon=V\oplus\mathbb{C}$ with represented state
$\widehat\psi=\psi\oplus0$, then for every qubit rank-one projector
$\Pi_a\in Proj(V)$,
\[
\mathcal{C}_{\Obs}(\tilde\psi_{\Obs},\Pi_a)=|\langle a|\psi\rangle|^2.
\]
\end{corollary}
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [],
  "depends_on": [
    "theorem:appC_born_rule"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "corollary:appC_qubit_case",
  "label": "corollary:appC_qubit_case",
  "latex_body": "\\begin{corollary}[Qubit case \\texorpdfstring{$d = 2$}{d = 2}]\n\\label{corollary:appC_qubit_case}\nLet $V\\cong\\mathbb{C}^2$ be a qubit subspace. If the qubit coherence assignment is\nthe restriction of a PS--C1--PS--C6 assignment on an embedding\n$\\widehat\\Horizon=V\\oplus\\mathbb{C}$ with represented state\n$\\widehat\\psi=\\psi\\oplus0$, then for every qubit rank-one projector\n$\\Pi_a\\in Proj(V)$,\n\\[\n\\mathcal{C}_{\\Obs}(\\tilde\\psi_{\\Obs},\\Pi_a)=|\\langle a|\\psi\\rangle|^2.\n\\]\n\\end{corollary}",
  "lean_alignment": {
    "conditions": [
      "Gleason-type uniqueness (axioms force the Born form in d>=3) and PS-C5 stay open; only the forward direction Born => axioms is certified",
      "The human proof uses an explicit higher-rank extension; Lean certifies the lower-rank obstruction but not this full extension argument.",
      "continuum charge/action integrals stay open; the discrete conservation mechanism is certified"
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "The human proof uses an explicit higher-rank extension; Lean certifies the lower-rank obstruction but not this full extension argument.",
      "The qubit Born value equals the squared amplitude, computed on C^2."
    ],
    "record_ids": [
      "MAP-APPENDIX_DUAL_HORIZON-047",
      "REVIEW-003"
    ],
    "statuses": [
      "conditional",
      "exact"
    ],
    "witnesses": [
      "Book7GleasonBoundary.rank_two_frame_axioms_do_not_force_born",
      "Born.qubit_born"
    ]
  },
  "line": 749,
  "macros_used": [
    "Horizon",
    "Obs"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Qubit case \\texorpdfstring{$d = 2$}{d = 2}",
  "proof_labels": [
    "proof:appC_qubit_case"
  ],
  "proof_status": "proven",
  "refs": [],
  "role": "corollary",
  "type": "corollary"
}

proofappendix

proof:appC_qubit_case

proof:appC_qubit_case

Exact LaTeX body

\begin{proof}
\label{proof:appC_qubit_case}
Extend the qubit projector to $\widehat\Pi_a=\Pi_a\oplus0$ on
$\widehat\Horizon$. The hypotheses place the extended assignment in dimension
$3$, so Theorem~\ref{theorem:appC_born_rule} gives
$\widehat{\mathcal C}_{\Obs}(\widehat{\tilde\psi}_{\Obs},\widehat\Pi_a)
=\operatorname{tr}(|\widehat\psi\rangle\langle\widehat\psi|\widehat\Pi_a)
=|\langle a|\psi\rangle|^2$. Restricting back to $V$ gives the claimed qubit
formula. The extension hypothesis is essential: without it, two-dimensional
Hilbert space admits contextual dispersion-free frame assignments not excluded by
Gleason's theorem alone.
\end{proof}

Reference roles

TargetRoleLogical support
theorem:appC_born_ruleproof_supportyes
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [
    "theorem:appC_born_rule"
  ],
  "depends_on": [
    "theorem:appC_born_rule"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "proof:appC_qubit_case",
  "label": "proof:appC_qubit_case",
  "latex_body": "\\begin{proof}\n\\label{proof:appC_qubit_case}\nExtend the qubit projector to $\\widehat\\Pi_a=\\Pi_a\\oplus0$ on\n$\\widehat\\Horizon$. The hypotheses place the extended assignment in dimension\n$3$, so Theorem~\\ref{theorem:appC_born_rule} gives\n$\\widehat{\\mathcal C}_{\\Obs}(\\widehat{\\tilde\\psi}_{\\Obs},\\widehat\\Pi_a)\n=\\operatorname{tr}(|\\widehat\\psi\\rangle\\langle\\widehat\\psi|\\widehat\\Pi_a)\n=|\\langle a|\\psi\\rangle|^2$. Restricting back to $V$ gives the claimed qubit\nformula. The extension hypothesis is essential: without it, two-dimensional\nHilbert space admits contextual dispersion-free frame assignments not excluded by\nGleason's theorem alone.\n\\end{proof}",
  "line": 761,
  "macros_used": [
    "Horizon",
    "Obs"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "",
  "proves": "corollary:appC_qubit_case",
  "ref_roles": [
    {
      "context": "hat\\Pi_a=\\Pi_a\\oplus0$ on $\\widehat\\Horizon$. The hypotheses place the extended assignment in dimension $3$, so Theorem~\\ref{theorem:appC_born_rule} gives $\\widehat{\\mathcal C}_{\\Obs}(\\widehat{\\tilde\\psi}_{\\Obs},\\widehat\\Pi_a) =\\operatorname{tr}(|\\widehat\\psi\\rangle\\l",
      "label": "theorem:appC_born_rule",
      "logical_support": true,
      "role": "proof_support",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 701,
      "target_type": "theorem"
    }
  ],
  "refs": [
    "theorem:appC_born_rule"
  ],
  "role": "proof",
  "type": "proof"
}

corollaryprovenappendix

Mixed states

corollary:appC_mixed_states

Exact LaTeX body

\begin{corollary}[Mixed states]
\label{corollary:appC_mixed_states}
Assume, in addition, that the observer coherence budget is affine under classical
mixtures of preparations. If
$\rho = \sum_i p_i |\psi_i\rangle\langle\psi_i|$ with $p_i\ge0$ and
$\sum_i p_i=1$, then for every projector $\Pi_a$,
\[
\mathcal{C}_{\Obs}(\tilde\rho_{\Obs}, \Pi_a) = \operatorname{tr}(\rho \Pi_a).
\]
\end{corollary}
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [],
  "depends_on": [
    "theorem:appC_born_rule"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "corollary:appC_mixed_states",
  "label": "corollary:appC_mixed_states",
  "latex_body": "\\begin{corollary}[Mixed states]\n\\label{corollary:appC_mixed_states}\nAssume, in addition, that the observer coherence budget is affine under classical\nmixtures of preparations. If\n$\\rho = \\sum_i p_i |\\psi_i\\rangle\\langle\\psi_i|$ with $p_i\\ge0$ and\n$\\sum_i p_i=1$, then for every projector $\\Pi_a$,\n\\[\n\\mathcal{C}_{\\Obs}(\\tilde\\rho_{\\Obs}, \\Pi_a) = \\operatorname{tr}(\\rho \\Pi_a).\n\\]\n\\end{corollary}",
  "lean_alignment": {
    "conditions": [
      "Gleason-type uniqueness (axioms force the Born form in d>=3) and PS-C5 stay open; only the forward direction Born => axioms is certified",
      "The affine-mixture premise is visible in the prose but the mixed-state construction is not part of the current Lean receipt.",
      "continuum charge/action integrals stay open; the discrete conservation mechanism is certified"
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "The affine-mixture premise is visible in the prose but the mixed-state construction is not part of the current Lean receipt.",
      "The mixed-state coherence is affine in the mixing weights, matching tr(rho Pi_a)."
    ],
    "record_ids": [
      "MAP-APPENDIX_DUAL_HORIZON-048",
      "REVIEW-004"
    ],
    "statuses": [
      "conditional"
    ],
    "witnesses": [
      "Born.cohMix_nonneg",
      "Born.mixed_affine"
    ]
  },
  "line": 774,
  "macros_used": [
    "Obs"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Mixed states",
  "proof_labels": [
    "proof:appC_mixed_states"
  ],
  "proof_status": "proven",
  "refs": [],
  "role": "corollary",
  "type": "corollary"
}

proofappendix

proof:appC_mixed_states

proof:appC_mixed_states

Exact LaTeX body

\begin{proof}
\label{proof:appC_mixed_states}
Affineness of the observer budget gives
\[
\mathcal{C}_{\Obs}(\tilde\rho_{\Obs},\Pi_a)
=\sum_i p_i\mathcal{C}_{\Obs}(\widetilde{\psi_i}_{\Obs},\Pi_a).
\]
By Theorem~\ref{theorem:appC_born_rule}, each pure component contributes
$\mathcal{C}_{\Obs}(\widetilde{\psi_i}_{\Obs},\Pi_a)
=\operatorname{tr}(|\psi_i\rangle\langle\psi_i|\Pi_a)$. Therefore
\[
\mathcal{C}_{\Obs}(\tilde\rho_{\Obs},\Pi_a)
=\sum_i p_i\operatorname{tr}(|\psi_i\rangle\langle\psi_i|\Pi_a)
=\operatorname{tr}\!\left(\sum_i p_i|\psi_i\rangle\langle\psi_i|\Pi_a\right)
=\operatorname{tr}(\rho\Pi_a).
\]
\end{proof}

Reference roles

TargetRoleLogical support
theorem:appC_born_ruleproof_supportyes
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [
    "theorem:appC_born_rule"
  ],
  "depends_on": [
    "theorem:appC_born_rule"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "proof:appC_mixed_states",
  "label": "proof:appC_mixed_states",
  "latex_body": "\\begin{proof}\n\\label{proof:appC_mixed_states}\nAffineness of the observer budget gives\n\\[\n\\mathcal{C}_{\\Obs}(\\tilde\\rho_{\\Obs},\\Pi_a)\n=\\sum_i p_i\\mathcal{C}_{\\Obs}(\\widetilde{\\psi_i}_{\\Obs},\\Pi_a).\n\\]\nBy Theorem~\\ref{theorem:appC_born_rule}, each pure component contributes\n$\\mathcal{C}_{\\Obs}(\\widetilde{\\psi_i}_{\\Obs},\\Pi_a)\n=\\operatorname{tr}(|\\psi_i\\rangle\\langle\\psi_i|\\Pi_a)$. Therefore\n\\[\n\\mathcal{C}_{\\Obs}(\\tilde\\rho_{\\Obs},\\Pi_a)\n=\\sum_i p_i\\operatorname{tr}(|\\psi_i\\rangle\\langle\\psi_i|\\Pi_a)\n=\\operatorname{tr}\\!\\left(\\sum_i p_i|\\psi_i\\rangle\\langle\\psi_i|\\Pi_a\\right)\n=\\operatorname{tr}(\\rho\\Pi_a).\n\\]\n\\end{proof}",
  "line": 785,
  "macros_used": [
    "Obs"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "",
  "proves": "corollary:appC_mixed_states",
  "ref_roles": [
    {
      "context": "athcal{C}_{\\Obs}(\\tilde\\rho_{\\Obs},\\Pi_a) =\\sum_i p_i\\mathcal{C}_{\\Obs}(\\widetilde{\\psi_i}_{\\Obs},\\Pi_a). \\] By Theorem~\\ref{theorem:appC_born_rule}, each pure component contributes $\\mathcal{C}_{\\Obs}(\\widetilde{\\psi_i}_{\\Obs},\\Pi_a) =\\operatorname{tr}(|\\psi_i\\rangle",
      "label": "theorem:appC_born_rule",
      "logical_support": true,
      "role": "proof_support",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 701,
      "target_type": "theorem"
    }
  ],
  "refs": [
    "theorem:appC_born_rule"
  ],
  "role": "proof",
  "type": "proof"
}

sectionsubsectionappendix

Interpretation Within Principia Symbolica

subsec:appC_born_interpretation_ps

Reference roles

TargetRoleLogical support
definition:bk2_symbolic_free_energynavigationno
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "definition:appC_observer_token_space"
  ],
  "cites": [
    "definition:bk2_symbolic_free_energy"
  ],
  "depends_on": [
    "definition:bk2_symbolic_free_energy"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "subsec:appC_born_interpretation_ps",
  "label": "subsec:appC_born_interpretation_ps",
  "latex_body": "",
  "lean_alignment": {
    "conditions": [],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": false,
    "notes": [
      "The emergence-of-randomness and free-energy language is an observer interpretation, not the finite observer-lowering theorem itself."
    ],
    "record_ids": [
      "REVIEW-005"
    ],
    "statuses": [
      "interpretive"
    ],
    "witnesses": []
  },
  "line": 803,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Interpretation Within Principia Symbolica",
  "ref_roles": [
    {
      "context": "",
      "label": "definition:bk2_symbolic_free_energy",
      "logical_support": false,
      "role": "navigation",
      "target_file": "book2.tex",
      "target_line": 135,
      "target_type": "definition"
    }
  ],
  "role": "section",
  "subtype": "subsection",
  "type": "section"
}

sectionsubsectionappendix

Implications and Outlook

subsec:appC_born_outlook

Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "appendix_dual_horizon.tex",
  "id": "subsec:appC_born_outlook",
  "label": "subsec:appC_born_outlook",
  "latex_body": "",
  "lean_alignment": {
    "conditions": [],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": false,
    "notes": [
      "The resolution-limit outlook is intentionally synthetic and empirical-facing; it should remain outside exact kernel projection unless separately witnessed."
    ],
    "record_ids": [
      "REVIEW-006"
    ],
    "statuses": [
      "interpretive"
    ],
    "witnesses": []
  },
  "line": 814,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Implications and Outlook",
  "role": "section",
  "subtype": "subsection",
  "type": "section"
}

sectionsubsectionappendix

Preamble

subsec:appC_time_preamble_rigorous

Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "appendix_dual_horizon.tex",
  "id": "subsec:appC_time_preamble_rigorous",
  "label": "subsec:appC_time_preamble_rigorous",
  "latex_body": "",
  "line": 829,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Preamble",
  "role": "section",
  "subtype": "subsection",
  "type": "section"
}

sectionsubsectionappendix

Critique of the Entropic Arrow

subsec:appC_time_critique_rigorous

Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "appendix_dual_horizon.tex",
  "id": "subsec:appC_time_critique_rigorous",
  "label": "subsec:appC_time_critique_rigorous",
  "latex_body": "",
  "line": 833,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Critique of the Entropic Arrow",
  "role": "section",
  "subtype": "subsection",
  "type": "section"
}

sectionsubsectionappendix

The Geometric Engine of Irreversibility

subsec:appC_time_geometric_engine_final

Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "appendix_dual_horizon.tex",
  "id": "subsec:appC_time_geometric_engine_final",
  "label": "subsec:appC_time_geometric_engine_final",
  "latex_body": "",
  "line": 837,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "The Geometric Engine of Irreversibility",
  "role": "section",
  "subtype": "subsection",
  "type": "section"
}

definitiondefinitionalappendix

Reflective State Space \(\mathcal{S}_O\)

definition:appC_reflective_state_space

Exact LaTeX body

\begin{definition}[Reflective State Space \(\mathcal{S}_O\)]
\label{definition:appC_reflective_state_space}
A Bounded Observer \(\Obs\) (cf.~\ref{definition:bk4_bounded_observer}) does not simply perceive a state \(x \in \manifold\) (cf.~\ref{definition:bk1_symbolic_manifold}). It perceives a state within the context of its own history, \(H_t\). The true state space is not \(\manifold\), but the \textbf{Reflective State Space} \(\mathcal{S}_O = \manifold \times \mathcal{H}\), where \(\mathcal{H}\) is the space of possible observer histories. A state is a tuple \((x, H_t)\).
\end{definition}

Reference roles

TargetRoleLogical support
definition:bk1_symbolic_manifoldcf_near_matchyes
definition:bk4_bounded_observercf_near_matchyes
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [
    "definition:bk1_symbolic_manifold",
    "definition:bk4_bounded_observer"
  ],
  "depends_on": [
    "definition:bk1_symbolic_manifold",
    "definition:bk4_bounded_observer"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "definition:appC_reflective_state_space",
  "label": "definition:appC_reflective_state_space",
  "latex_body": "\\begin{definition}[Reflective State Space \\(\\mathcal{S}_O\\)]\n\\label{definition:appC_reflective_state_space}\nA Bounded Observer \\(\\Obs\\) (cf.~\\ref{definition:bk4_bounded_observer}) does not simply perceive a state \\(x \\in \\manifold\\) (cf.~\\ref{definition:bk1_symbolic_manifold}). It perceives a state within the context of its own history, \\(H_t\\). The true state space is not \\(\\manifold\\), but the \\textbf{Reflective State Space} \\(\\mathcal{S}_O = \\manifold \\times \\mathcal{H}\\), where \\(\\mathcal{H}\\) is the space of possible observer histories. A state is a tuple \\((x, H_t)\\).\n\\end{definition}",
  "line": 841,
  "macros_used": [
    "Obs",
    "manifold"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Reflective State Space \\(\\mathcal{S}_O\\)",
  "proof_status": "definitional",
  "ref_roles": [
    {
      "context": "Observer \\(\\Obs\\) (cf.~\\ref{definition:bk4_bounded_observer}) does not simply perceive a state \\(x \\in \\manifold\\) (cf.~\\ref{definition:bk1_symbolic_manifold}). It perceives a state within the context of its own history, \\(H_t\\). The true state space is not \\(\\manifold\\), but t",
      "label": "definition:bk1_symbolic_manifold",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 1188,
      "target_type": "definition"
    },
    {
      "context": "flective State Space \\(\\mathcal{S}_O\\)] \\label{definition:appC_reflective_state_space} A Bounded Observer \\(\\Obs\\) (cf.~\\ref{definition:bk4_bounded_observer}) does not simply perceive a state \\(x \\in \\manifold\\) (cf.~\\ref{definition:bk1_symbolic_manifold}). It perceives a stat",
      "label": "definition:bk4_bounded_observer",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book4.tex",
      "target_line": 427,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:bk1_symbolic_manifold",
    "definition:bk4_bounded_observer"
  ],
  "role": "definition",
  "type": "definition"
}

axiomdefinitionalappendix

The Axiom of Memory

axiom:appC_axiom_of_memory

Exact LaTeX body

\begin{axiom}[The Axiom of Memory]
\label{axiom:appC_axiom_of_memory}
Every act of differentiation, \(\delta^O\), by a Bounded Observer \(\Obs\) necessarily alters its history. If \(\delta^O\) maps a state \((x_0, H_{t_0})\) to \((x_1, H_{t_1})\), then \(H_{t_1} \neq H_{t_0}\). Specifically, \(H_{t_1}\) contains the trace of the operation that led from \(x_0\) to \(x_1\). This act of recording is metabolically non-zero, incurring a minimal cost in Symbolic Free Energy \(\Delta{\freeenergy}_{\text{mem}} > 0\) (cf.~\ref{definition:bk2_symbolic_free_energy}).
\end{axiom}

Reference roles

TargetRoleLogical support
definition:bk2_symbolic_free_energycf_near_matchyes
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "proof:appC_fundamental_irreversibility",
    "proof:appD_titans_as_arrow_of_time",
    "proposition:appC_conditional_minimality_2x2",
    "scholium:appC_time_as_memory",
    "scholium:appD_axiom_of_memory_titans"
  ],
  "cites": [
    "definition:bk2_symbolic_free_energy"
  ],
  "depends_on": [
    "definition:bk2_symbolic_free_energy"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "axiom:appC_axiom_of_memory",
  "label": "axiom:appC_axiom_of_memory",
  "latex_body": "\\begin{axiom}[The Axiom of Memory]\n\\label{axiom:appC_axiom_of_memory}\nEvery act of differentiation, \\(\\delta^O\\), by a Bounded Observer \\(\\Obs\\) necessarily alters its history. If \\(\\delta^O\\) maps a state \\((x_0, H_{t_0})\\) to \\((x_1, H_{t_1})\\), then \\(H_{t_1} \\neq H_{t_0}\\). Specifically, \\(H_{t_1}\\) contains the trace of the operation that led from \\(x_0\\) to \\(x_1\\). This act of recording is metabolically non-zero, incurring a minimal cost in Symbolic Free Energy \\(\\Delta{\\freeenergy}_{\\text{mem}} > 0\\) (cf.~\\ref{definition:bk2_symbolic_free_energy}).\n\\end{axiom}",
  "lean_alignment": {
    "conditions": [
      "continuum/categorical content is NOT formalized; static and finite-discrete kernels only",
      "modeling laws are structure fields or explicit hypotheses"
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "History-change on every act is proved as a theorem from the strictly increasing order parameter carried by MemoryAct, upgrading the source's postulated axiom to a derived consequence of the monotone-order model."
    ],
    "record_ids": [
      "MAP-APPENDIX_DUAL_HORIZON-013"
    ],
    "statuses": [
      "exact"
    ],
    "witnesses": [
      "AppendixDH.memoryAct_hist_changes"
    ]
  },
  "line": 846,
  "macros_used": [
    "Obs",
    "freeenergy"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "The Axiom of Memory",
  "proof_status": "definitional",
  "ref_roles": [
    {
      "context": "metabolically non-zero, incurring a minimal cost in Symbolic Free Energy \\(\\Delta{\\freeenergy}_{\\text{mem}} > 0\\) (cf.~\\ref{definition:bk2_symbolic_free_energy}). \\end{axiom}",
      "label": "definition:bk2_symbolic_free_energy",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book2.tex",
      "target_line": 135,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:bk2_symbolic_free_energy"
  ],
  "role": "axiom",
  "type": "axiom"
}

theoremprovenappendix

Fundamental Irreversibility of Reflective Observation

theorem:appC_fundamental_irreversibility_final

Exact LaTeX body

\begin{theorem}[Fundamental Irreversibility of Reflective Observation]
\label{theorem:appC_fundamental_irreversibility_final}
Any symbolic process involving a state change perceived by a Bounded Observer (cf.~\ref{definition:bk4_bounded_observer}) is fundamentally irreversible: each observation incurs a non-recoverable cost in Symbolic Free Energy (cf.~\ref{definition:bk2_symbolic_free_energy}).
\end{theorem}

Reference roles

TargetRoleLogical support
definition:bk2_symbolic_free_energycf_near_matchyes
definition:bk4_bounded_observercf_near_matchyes
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "corollary:appC_emergence_of_time_arrow_final",
    "proof:appD_titans_as_arrow_of_time",
    "scholium:bk4_irreversibility_as_trace"
  ],
  "cites": [
    "definition:bk2_symbolic_free_energy",
    "definition:bk4_bounded_observer"
  ],
  "depends_on": [
    "axiom:appC_axiom_of_memory",
    "definition:bk2_symbolic_free_energy",
    "definition:bk4_bounded_observer"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "theorem:appC_fundamental_irreversibility_final",
  "label": "theorem:appC_fundamental_irreversibility_final",
  "latex_body": "\\begin{theorem}[Fundamental Irreversibility of Reflective Observation]\n\\label{theorem:appC_fundamental_irreversibility_final}\nAny symbolic process involving a state change perceived by a Bounded Observer (cf.~\\ref{definition:bk4_bounded_observer}) is fundamentally irreversible: each observation incurs a non-recoverable cost in Symbolic Free Energy (cf.~\\ref{definition:bk2_symbolic_free_energy}).\n\\end{theorem}",
  "lean_alignment": {
    "conditions": [
      "continuum/categorical content is NOT formalized; static and finite-discrete kernels only",
      "modeling laws are structure fields or explicit hypotheses"
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "Every act incurs strictly positive cost, direct from the MemoryAct.cost_pos field."
    ],
    "record_ids": [
      "MAP-APPENDIX_DUAL_HORIZON-014"
    ],
    "statuses": [
      "exact"
    ],
    "witnesses": [
      "AppendixDH.memoryAct_irreversible"
    ]
  },
  "line": 851,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Fundamental Irreversibility of Reflective Observation",
  "proof_labels": [
    "proof:appC_fundamental_irreversibility"
  ],
  "proof_status": "proven",
  "ref_roles": [
    {
      "context": "d_observer}) is fundamentally irreversible: each observation incurs a non-recoverable cost in Symbolic Free Energy (cf.~\\ref{definition:bk2_symbolic_free_energy}). \\end{theorem}",
      "label": "definition:bk2_symbolic_free_energy",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book2.tex",
      "target_line": 135,
      "target_type": "definition"
    },
    {
      "context": "C_fundamental_irreversibility_final} Any symbolic process involving a state change perceived by a Bounded Observer (cf.~\\ref{definition:bk4_bounded_observer}) is fundamentally irreversible: each observation incurs a non-recoverable cost in Symbolic Free Energy (cf.~\\ref{defini",
      "label": "definition:bk4_bounded_observer",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book4.tex",
      "target_line": 427,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:bk2_symbolic_free_energy",
    "definition:bk4_bounded_observer"
  ],
  "role": "theorem",
  "type": "theorem"
}

proofappendix

proof:appC_fundamental_irreversibility

proof:appC_fundamental_irreversibility

Exact LaTeX body

\begin{proof}
\label{proof:appC_fundamental_irreversibility}
\leavevmode

\begin{enumerate}
    \item Consider a process that takes the system from state \(A\) to state \(B\). In the Reflective State Space, this is a transition from \((x_A, H_A)\) to \((x_B, H_B)\). By the Axiom of Memory (Axiom~\ref{axiom:appC_axiom_of_memory}), the history is updated, so \(H_B\) contains the record of the A\(\to\)B transformation.

    \item Now, consider a "reverse" process that takes the system from state \(B\) back to a state geometrically indistinguishable from \(A\). Let this new state be \(A'\). In the base manifold \(\manifold\), we have \(x_{A'} = x_A\).

    \item However, in the full Reflective State Space, the new state is \((x_{A'}, H_{A'})\). The reverse process is also an act of differentiation that must be recorded. Therefore, the new history \(H_{A'}\) contains the record of the B\(\to\)A' transformation. It is necessarily different from the original history, \(H_{A'} \neq H_A\).

    \item The full initial and final states are \((x_A, H_A)\) and \((x_{A'}, H_{A'})\). Since \(x_{A'} = x_A\) but \(H_{A'} \neq H_A\), the full system state is not restored.
    \[
    (x_A, H_A) \neq (x_{A'}, H_{A'})
    \]
    \item The process is irreversible. The difference between the initial and final states lies not in the geometric position on the base manifold, but in the accumulated history within the observer. This is a fundamental asymmetry.
\end{enumerate}
\end{proof}

Reference roles

TargetRoleLogical support
axiom:appC_axiom_of_memorydefinition_anchoryes
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [
    "axiom:appC_axiom_of_memory"
  ],
  "depends_on": [
    "axiom:appC_axiom_of_memory"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "proof:appC_fundamental_irreversibility",
  "label": "proof:appC_fundamental_irreversibility",
  "latex_body": "\\begin{proof}\n\\label{proof:appC_fundamental_irreversibility}\n\\leavevmode\n\n\\begin{enumerate}\n    \\item Consider a process that takes the system from state \\(A\\) to state \\(B\\). In the Reflective State Space, this is a transition from \\((x_A, H_A)\\) to \\((x_B, H_B)\\). By the Axiom of Memory (Axiom~\\ref{axiom:appC_axiom_of_memory}), the history is updated, so \\(H_B\\) contains the record of the A\\(\\to\\)B transformation.\n\n    \\item Now, consider a \"reverse\" process that takes the system from state \\(B\\) back to a state geometrically indistinguishable from \\(A\\). Let this new state be \\(A'\\). In the base manifold \\(\\manifold\\), we have \\(x_{A'} = x_A\\).\n\n    \\item However, in the full Reflective State Space, the new state is \\((x_{A'}, H_{A'})\\). The reverse process is also an act of differentiation that must be recorded. Therefore, the new history \\(H_{A'}\\) contains the record of the B\\(\\to\\)A' transformation. It is necessarily different from the original history, \\(H_{A'} \\neq H_A\\).\n\n    \\item The full initial and final states are \\((x_A, H_A)\\) and \\((x_{A'}, H_{A'})\\). Since \\(x_{A'} = x_A\\) but \\(H_{A'} \\neq H_A\\), the full system state is not restored.\n    \\[\n    (x_A, H_A) \\neq (x_{A'}, H_{A'})\n    \\]\n    \\item The process is irreversible. The difference between the initial and final states lies not in the geometric position on the base manifold, but in the accumulated history within the observer. This is a fundamental asymmetry.\n\\end{enumerate}\n\\end{proof}",
  "line": 856,
  "macros_used": [
    "manifold"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "",
  "proves": "theorem:appC_fundamental_irreversibility_final",
  "ref_roles": [
    {
      "context": "n the Reflective State Space, this is a transition from \\((x_A, H_A)\\) to \\((x_B, H_B)\\). By the Axiom of Memory (Axiom~\\ref{axiom:appC_axiom_of_memory}), the history is updated, so \\(H_B\\) contains the record of the A\\(\\to\\)B transformation. \\item Now, consider a \"r",
      "label": "axiom:appC_axiom_of_memory",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 846,
      "target_type": "axiom"
    }
  ],
  "refs": [
    "axiom:appC_axiom_of_memory"
  ],
  "role": "proof",
  "type": "proof"
}

corollaryprovenappendix

The Emergence of the Arrow of Time

corollary:appC_emergence_of_time_arrow_final

Exact LaTeX body

\begin{corollary}[The Emergence of the Arrow of Time]
\label{corollary:appC_emergence_of_time_arrow_final}
The fundamental irreversibility established in
Theorem~\ref{theorem:appC_fundamental_irreversibility_final} induces a directed
partial order on observer-accessible reflective states. Along any nontrivial
observed path, the order parameter
\[
N(H):=\text{the number of recorded differentiation traces in }H
\]
is strictly increasing; if symbolic free-energy minimization selects admissible
successor states, the selected direction is the direction in which records are
accumulated and unrecoverable memory cost has already been paid.
\end{corollary}

Reference roles

TargetRoleLogical support
theorem:appC_fundamental_irreversibility_finalformal_dependencyyes
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [
    "theorem:appC_fundamental_irreversibility_final"
  ],
  "depends_on": [
    "theorem:appC_fundamental_irreversibility_final"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "corollary:appC_emergence_of_time_arrow_final",
  "label": "corollary:appC_emergence_of_time_arrow_final",
  "latex_body": "\\begin{corollary}[The Emergence of the Arrow of Time]\n\\label{corollary:appC_emergence_of_time_arrow_final}\nThe fundamental irreversibility established in\nTheorem~\\ref{theorem:appC_fundamental_irreversibility_final} induces a directed\npartial order on observer-accessible reflective states. Along any nontrivial\nobserved path, the order parameter\n\\[\nN(H):=\\text{the number of recorded differentiation traces in }H\n\\]\nis strictly increasing; if symbolic free-energy minimization selects admissible\nsuccessor states, the selected direction is the direction in which records are\naccumulated and unrecoverable memory cost has already been paid.\n\\end{corollary}",
  "lean_alignment": {
    "conditions": [
      "continuum/categorical content is NOT formalized; static and finite-discrete kernels only",
      "modeling laws are structure fields or explicit hypotheses"
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "The order parameter accumulates by at least n over n steps, hence the history never returns to an earlier value along any nontrivial path -- the discrete/finite kernel of the induced directed order and arrow of time."
    ],
    "record_ids": [
      "MAP-APPENDIX_DUAL_HORIZON-015"
    ],
    "statuses": [
      "exact"
    ],
    "witnesses": [
      "AppendixDH.memoryAct_no_return",
      "AppendixDH.memoryAct_order_iterate"
    ]
  },
  "line": 875,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "The Emergence of the Arrow of Time",
  "proof_labels": [
    "proof:appC_emergence_of_time_arrow_final"
  ],
  "proof_status": "proven",
  "ref_roles": [
    {
      "context": "ow of Time] \\label{corollary:appC_emergence_of_time_arrow_final} The fundamental irreversibility established in Theorem~\\ref{theorem:appC_fundamental_irreversibility_final} induces a directed partial order on observer-accessible reflective states. Along any nontrivial observed path, the orde",
      "label": "theorem:appC_fundamental_irreversibility_final",
      "logical_support": true,
      "role": "formal_dependency",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 851,
      "target_type": "theorem"
    }
  ],
  "refs": [
    "theorem:appC_fundamental_irreversibility_final"
  ],
  "role": "corollary",
  "type": "corollary"
}

proofappendix

proof:appC_emergence_of_time_arrow_final

proof:appC_emergence_of_time_arrow_final

Exact LaTeX body

\begin{proof}
\label{proof:appC_emergence_of_time_arrow_final}
Let $(x_n,H_n)$ be a path generated by nontrivial acts of observer
differentiation. By the Axiom of Memory, each step appends a new trace to the
history and incurs positive cost $\Delta{\freeenergy}_{\text{mem}}>0$. Hence
$N(H_{n+1})=N(H_n)+1$ for every observed step, so $N$ is strictly increasing along
the path. A reverse path that restored the base point $x_n$ would still have a
history containing the additional forward and reverse records, and therefore
would have larger $N$ than the original state. Thus the relation
$(x,H)\prec(x',H')$ iff $H'$ contains the records of $H$ plus at least one new
record is transitive, antisymmetric up to equality of histories, and nontrivial;
it defines an observer-relative temporal orientation. When the dynamics also
minimize symbolic free energy among admissible successors, this orientation is
the direction along which the system pays and accumulates the non-recoverable
memory costs. That oriented accumulation is the arrow of time.
\end{proof}
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "appendix_dual_horizon.tex",
  "id": "proof:appC_emergence_of_time_arrow_final",
  "label": "proof:appC_emergence_of_time_arrow_final",
  "latex_body": "\\begin{proof}\n\\label{proof:appC_emergence_of_time_arrow_final}\nLet $(x_n,H_n)$ be a path generated by nontrivial acts of observer\ndifferentiation. By the Axiom of Memory, each step appends a new trace to the\nhistory and incurs positive cost $\\Delta{\\freeenergy}_{\\text{mem}}>0$. Hence\n$N(H_{n+1})=N(H_n)+1$ for every observed step, so $N$ is strictly increasing along\nthe path. A reverse path that restored the base point $x_n$ would still have a\nhistory containing the additional forward and reverse records, and therefore\nwould have larger $N$ than the original state. Thus the relation\n$(x,H)\\prec(x',H')$ iff $H'$ contains the records of $H$ plus at least one new\nrecord is transitive, antisymmetric up to equality of histories, and nontrivial;\nit defines an observer-relative temporal orientation. When the dynamics also\nminimize symbolic free energy among admissible successors, this orientation is\nthe direction along which the system pays and accumulates the non-recoverable\nmemory costs. That oriented accumulation is the arrow of time.\n\\end{proof}",
  "line": 889,
  "macros_used": [
    "freeenergy"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "",
  "proves": "corollary:appC_emergence_of_time_arrow_final",
  "refs": [],
  "role": "proof",
  "type": "proof"
}

scholiumappendix

Time as the Accumulation of Memory

scholium:appC_time_as_memory

Exact LaTeX body

\begin{scholium}[Time as the Accumulation of Memory]
\label{scholium:appC_time_as_memory}
This derivation reframes the Arrow of Time. It is not about the universe expanding or entropy increasing. It is about the simple, profound fact that a system capable of knowing cannot "un-know." Every observation, every reflection (cf.~\ref{definition:bk1_reflection_operator}), every act of differentiation leaves a trace, as required by the Axiom of Memory (cf.~\ref{axiom:appC_axiom_of_memory}). Time is the continuous accumulation of these traces. It is the ever-growing distinction between "what was" and "what is," a distinction that exists only for a system that remembers. The irreversibility is not in the world, but in the memory of it.
\end{scholium}

Reference roles

TargetRoleLogical support
axiom:appC_axiom_of_memorycf_near_matchyes
definition:bk1_reflection_operatorcf_near_matchyes
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "scholium:appC_symbolic_geometric_equivalence"
  ],
  "cites": [
    "axiom:appC_axiom_of_memory",
    "definition:bk1_reflection_operator"
  ],
  "depends_on": [
    "axiom:appC_axiom_of_memory",
    "definition:bk1_reflection_operator"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "scholium:appC_time_as_memory",
  "label": "scholium:appC_time_as_memory",
  "latex_body": "\\begin{scholium}[Time as the Accumulation of Memory]\n\\label{scholium:appC_time_as_memory}\nThis derivation reframes the Arrow of Time. It is not about the universe expanding or entropy increasing. It is about the simple, profound fact that a system capable of knowing cannot \"un-know.\" Every observation, every reflection (cf.~\\ref{definition:bk1_reflection_operator}), every act of differentiation leaves a trace, as required by the Axiom of Memory (cf.~\\ref{axiom:appC_axiom_of_memory}). Time is the continuous accumulation of these traces. It is the ever-growing distinction between \"what was\" and \"what is,\" a distinction that exists only for a system that remembers. The irreversibility is not in the world, but in the memory of it.\n\\end{scholium}",
  "line": 906,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Time as the Accumulation of Memory",
  "ref_roles": [
    {
      "context": "inition:bk1_reflection_operator}), every act of differentiation leaves a trace, as required by the Axiom of Memory (cf.~\\ref{axiom:appC_axiom_of_memory}). Time is the continuous accumulation of these traces. It is the ever-growing distinction between \"what was\" and \"what",
      "label": "axiom:appC_axiom_of_memory",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 846,
      "target_type": "axiom"
    },
    {
      "context": "t the simple, profound fact that a system capable of knowing cannot \"un-know.\" Every observation, every reflection (cf.~\\ref{definition:bk1_reflection_operator}), every act of differentiation leaves a trace, as required by the Axiom of Memory (cf.~\\ref{axiom:appC_axiom_of_memory}",
      "label": "definition:bk1_reflection_operator",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 1209,
      "target_type": "definition"
    }
  ],
  "refs": [
    "axiom:appC_axiom_of_memory",
    "definition:bk1_reflection_operator"
  ],
  "role": "scholium",
  "type": "scholium"
}

sectionsectionappendix

\texorpdfstring{Structural Derivations of $\varphi$ Across Symbolic Modalities

section:appendix_dual_horizon.tex:911

Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "appendix_dual_horizon.tex",
  "id": "section:appendix_dual_horizon.tex:911",
  "label": "",
  "latex_body": "",
  "line": 911,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "\\texorpdfstring{Structural Derivations of $\\varphi$ Across Symbolic Modalities",
  "role": "section",
  "subtype": "section",
  "type": "section"
}

definitiondefinitionalappendix

Symbolic Potential Function

definition:appC_lagrangian_potential

Exact LaTeX body

\begin{definition}[Symbolic Potential Function]
\label{definition:appC_lagrangian_potential}
Define the symbolic potential governing recursive learning as:
\[
V(C) = \frac{1}{2} \left(C - \frac{1}{C} \right)^2
\]
This encodes the symbolic tension between drift (\textit{cf.} Def.~\ref{definition:bk6_drift_operator_complete}) and reflection (Def.~\ref{definition:bk6_reflection_operator_complete}), as defined in Book VI.
\end{definition}

Reference roles

TargetRoleLogical support
definition:bk6_drift_operator_completecf_near_matchyes
definition:bk6_reflection_operator_completecf_near_matchyes
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "theorem:appC_phi_from_lagrangian"
  ],
  "cites": [
    "definition:bk6_drift_operator_complete",
    "definition:bk6_reflection_operator_complete"
  ],
  "depends_on": [
    "definition:bk6_drift_operator_complete",
    "definition:bk6_reflection_operator_complete"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "definition:appC_lagrangian_potential",
  "label": "definition:appC_lagrangian_potential",
  "latex_body": "\\begin{definition}[Symbolic Potential Function]\n\\label{definition:appC_lagrangian_potential}\nDefine the symbolic potential governing recursive learning as:\n\\[\nV(C) = \\frac{1}{2} \\left(C - \\frac{1}{C} \\right)^2\n\\]\nThis encodes the symbolic tension between drift (\\textit{cf.} Def.~\\ref{definition:bk6_drift_operator_complete}) and reflection (Def.~\\ref{definition:bk6_reflection_operator_complete}), as defined in Book VI.\n\\end{definition}",
  "lean_alignment": {
    "conditions": [
      "continuum/categorical content is NOT formalized; static and finite-discrete kernels only",
      "modeling laws are structure fields or explicit hypotheses"
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "V(C) = (1/2)(C - 1/C)^2 kept exactly; nonnegativity is unconditional, the zero-locus characterization (V(C)=0 iff C=1) is proved for C > 0."
    ],
    "record_ids": [
      "MAP-APPENDIX_DUAL_HORIZON-016"
    ],
    "statuses": [
      "conditional"
    ],
    "witnesses": [
      "AppendixDH.V_eq_zero_iff",
      "AppendixDH.V_nonneg"
    ]
  },
  "line": 921,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Symbolic Potential Function",
  "proof_status": "definitional",
  "ref_roles": [
    {
      "context": "(C) = \\frac{1}{2} \\left(C - \\frac{1}{C} \\right)^2 \\] This encodes the symbolic tension between drift (\\textit{cf.} Def.~\\ref{definition:bk6_drift_operator_complete}) and reflection (Def.~\\ref{definition:bk6_reflection_operator_complete}), as defined in Book VI. \\end{definition}",
      "label": "definition:bk6_drift_operator_complete",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book6.tex",
      "target_line": 926,
      "target_type": "definition"
    },
    {
      "context": "he symbolic tension between drift (\\textit{cf.} Def.~\\ref{definition:bk6_drift_operator_complete}) and reflection (Def.~\\ref{definition:bk6_reflection_operator_complete}), as defined in Book VI. \\end{definition}",
      "label": "definition:bk6_reflection_operator_complete",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book6.tex",
      "target_line": 937,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:bk6_drift_operator_complete",
    "definition:bk6_reflection_operator_complete"
  ],
  "role": "definition",
  "type": "definition"
}

theoremprovenappendix

Emergence of $\varphi$ from Lagrangian Equilibrium

theorem:appC_phi_from_lagrangian

Exact LaTeX body

\begin{theorem}[Emergence of $\varphi$ from Lagrangian Equilibrium]
\label{theorem:appC_phi_from_lagrangian}
Let $(C_n)_{n\ge0}$ be the positive stroboscopic complexity sequence selected by
the drift--reflection balance associated with
Def.~\ref{definition:appC_lagrangian_potential}. Assume the balanced two-step
closure
\[
C_{n+1}=C_n+C_{n-1},\qquad C_0>0,\quad C_1>0,
\]
which says that each new symbolic state preserves the current differentiated
content while reintegrating the immediately preceding memory trace. Then the
successive growth ratios
\[
\lambda_n:=\frac{C_{n+1}}{C_n}
\]
converge to the golden ratio
$\varphi=(1+\sqrt5)/2$.
\end{theorem}

Reference roles

TargetRoleLogical support
definition:appC_lagrangian_potentialdefinition_anchoryes
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "proof:appC_phi_min_growth",
    "remark:bk5_curvature_vs_chaos"
  ],
  "cites": [
    "definition:appC_lagrangian_potential"
  ],
  "depends_on": [
    "definition:appC_lagrangian_potential",
    "definition:bk1_stage_composite_operator",
    "definition:bk6_drift_operator_complete",
    "definition:bk6_reflection_operator_complete"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "theorem:appC_phi_from_lagrangian",
  "label": "theorem:appC_phi_from_lagrangian",
  "latex_body": "\\begin{theorem}[Emergence of $\\varphi$ from Lagrangian Equilibrium]\n\\label{theorem:appC_phi_from_lagrangian}\nLet $(C_n)_{n\\ge0}$ be the positive stroboscopic complexity sequence selected by\nthe drift--reflection balance associated with\nDef.~\\ref{definition:appC_lagrangian_potential}. Assume the balanced two-step\nclosure\n\\[\nC_{n+1}=C_n+C_{n-1},\\qquad C_0>0,\\quad C_1>0,\n\\]\nwhich says that each new symbolic state preserves the current differentiated\ncontent while reintegrating the immediately preceding memory trace. Then the\nsuccessive growth ratios\n\\[\n\\lambda_n:=\\frac{C_{n+1}}{C_n}\n\\]\nconverge to the golden ratio\n$\\varphi=(1+\\sqrt5)/2$.\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": [
      "Witnessed only for the canonical positive-initial-data instance C_n=fib(n+1) (C_0=C_1=1); generalizing to arbitrary C_0,C_1>0 is not attempted."
    ],
    "record_ids": [
      "MAP-APPENDIX_DUAL_HORIZON-033"
    ],
    "statuses": [
      "conditional"
    ],
    "witnesses": [
      "Book7B.shiftedFib_ratio_tendsto_goldenRatio"
    ]
  },
  "line": 930,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Emergence of $\\varphi$ from Lagrangian Equilibrium",
  "proof_labels": [
    "proof:appC_phi_from_lagrangian"
  ],
  "proof_status": "proven",
  "ref_roles": [
    {
      "context": "n\\ge0}$ be the positive stroboscopic complexity sequence selected by the drift--reflection balance associated with Def.~\\ref{definition:appC_lagrangian_potential}. Assume the balanced two-step closure \\[ C_{n+1}=C_n+C_{n-1},\\qquad C_0>0,\\quad C_1>0, \\] which says that each new symb",
      "label": "definition:appC_lagrangian_potential",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 921,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:appC_lagrangian_potential"
  ],
  "role": "theorem",
  "type": "theorem"
}

proofappendix

proof:appC_phi_from_lagrangian

proof:appC_phi_from_lagrangian

Exact LaTeX body

\begin{proof}
\label{proof:appC_phi_from_lagrangian}
The recurrence has characteristic polynomial $r^2-r-1=0$, with roots
$\varphi=(1+\sqrt5)/2$ and $\widehat\varphi=(1-\sqrt5)/2=-\varphi^{-1}$. Hence
\[
C_n=A\varphi^n+B\widehat\varphi^{\,n}
\]
for constants $A,B$ determined by $C_0,C_1$. Since
$A=(C_1-\widehat\varphi C_0)/(\varphi-\widehat\varphi)$ and
$C_0,C_1>0$ while $\widehat\varphi<0$, we have $A>0$. Therefore
\[
\lambda_n=\frac{C_{n+1}}{C_n}
=\frac{A\varphi^{n+1}+B\widehat\varphi^{\,n+1}}
       {A\varphi^n+B\widehat\varphi^{\,n}}
\longrightarrow \varphi,
\]
because $|\widehat\varphi|<\varphi$. Equivalently, any positive fixed ratio
$\lambda$ for the two-step closure must satisfy
$\lambda=1+1/\lambda$, and the unique positive solution is $\varphi$.
\end{proof}

Reference roles

TargetRoleLogical support
definition:bk1_stage_composite_operatordefinition_anchoryes
definition:bk6_drift_operator_completedefinition_anchoryes
definition:bk6_reflection_operator_completedefinition_anchoryes
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [
    "definition:bk1_stage_composite_operator",
    "definition:bk6_drift_operator_complete",
    "definition:bk6_reflection_operator_complete"
  ],
  "depends_on": [
    "definition:bk1_stage_composite_operator",
    "definition:bk6_drift_operator_complete",
    "definition:bk6_reflection_operator_complete"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "proof:appC_phi_from_lagrangian",
  "label": "proof:appC_phi_from_lagrangian",
  "latex_body": "\\begin{proof}\n\\label{proof:appC_phi_from_lagrangian}\nThe recurrence has characteristic polynomial $r^2-r-1=0$, with roots\n$\\varphi=(1+\\sqrt5)/2$ and $\\widehat\\varphi=(1-\\sqrt5)/2=-\\varphi^{-1}$. Hence\n\\[\nC_n=A\\varphi^n+B\\widehat\\varphi^{\\,n}\n\\]\nfor constants $A,B$ determined by $C_0,C_1$. Since\n$A=(C_1-\\widehat\\varphi C_0)/(\\varphi-\\widehat\\varphi)$ and\n$C_0,C_1>0$ while $\\widehat\\varphi<0$, we have $A>0$. Therefore\n\\[\n\\lambda_n=\\frac{C_{n+1}}{C_n}\n=\\frac{A\\varphi^{n+1}+B\\widehat\\varphi^{\\,n+1}}\n       {A\\varphi^n+B\\widehat\\varphi^{\\,n}}\n\\longrightarrow \\varphi,\n\\]\nbecause $|\\widehat\\varphi|<\\varphi$. Equivalently, any positive fixed ratio\n$\\lambda$ for the two-step closure must satisfy\n$\\lambda=1+1/\\lambda$, and the unique positive solution is $\\varphi$.\n\\end{proof}",
  "line": 949,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "",
  "proves": "theorem:appC_phi_from_lagrangian",
  "ref_roles": [
    {
      "context": "",
      "label": "definition:bk1_stage_composite_operator",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 520,
      "target_type": "definition"
    },
    {
      "context": "",
      "label": "definition:bk6_drift_operator_complete",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "book6.tex",
      "target_line": 926,
      "target_type": "definition"
    },
    {
      "context": "",
      "label": "definition:bk6_reflection_operator_complete",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "book6.tex",
      "target_line": 937,
      "target_type": "definition"
    }
  ],
  "refs": [],
  "role": "proof",
  "type": "proof"
}

scholiumappendix

scholium:appendix_dual_horizon.tex:970

scholium:appendix_dual_horizon.tex:970

Exact LaTeX body

\begin{scholium}
This derivation reveals $\varphi$ as a symbolic equilibrium point: the unique attractor balancing forward momentum (drift, Def.~\ref{definition:bk6_drift_operator_complete}) and reflective curvature (Def.~\ref{definition:bk6_reflection_operator_complete}). It constitutes a primitive emergence structure \textit{(cf.} Emergence Operator, Def.~\ref{definition:bk1_stage_composite_operator}).
\end{scholium}
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "appendix_dual_horizon.tex",
  "id": "scholium:appendix_dual_horizon.tex:970",
  "label": "",
  "latex_body": "\\begin{scholium}\nThis derivation reveals $\\varphi$ as a symbolic equilibrium point: the unique attractor balancing forward momentum (drift, Def.~\\ref{definition:bk6_drift_operator_complete}) and reflective curvature (Def.~\\ref{definition:bk6_reflection_operator_complete}). It constitutes a primitive emergence structure \\textit{(cf.} Emergence Operator, Def.~\\ref{definition:bk1_stage_composite_operator}).\n\\end{scholium}",
  "line": 970,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "",
  "refs": [
    "definition:bk1_stage_composite_operator",
    "definition:bk6_drift_operator_complete",
    "definition:bk6_reflection_operator_complete"
  ],
  "role": "scholium",
  "type": "scholium"
}

definitiondefinitionalappendix

Bounded Observation Frame

definition:appC_bounded_observation_frame

Exact LaTeX body

\begin{definition}[Bounded Observation Frame]
\label{definition:appC_bounded_observation_frame}
Let $\mathcal{H}$ be a separable Hilbert space. Define the observer-relative frame (Def.~\ref{definition:bk4_observer_kernel_convolution_map}):
\[
F_\delta(t) = \{x \in \mathcal{H} : \|x - x_0(t)\| \leq \delta\}
\]
with $x_0(t)$ the current observer state and $\delta$ their perceptual radius (see also bounded observer kernel in Def.~\ref{definition:bk1_bounded_observer}).
\end{definition}

Reference roles

TargetRoleLogical support
definition:bk1_bounded_observerdefinition_anchoryes
definition:bk4_observer_kernel_convolution_mapdefinition_anchoryes
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [
    "definition:bk1_bounded_observer",
    "definition:bk4_observer_kernel_convolution_map"
  ],
  "depends_on": [
    "definition:bk1_bounded_observer",
    "definition:bk4_observer_kernel_convolution_map"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "definition:appC_bounded_observation_frame",
  "label": "definition:appC_bounded_observation_frame",
  "latex_body": "\\begin{definition}[Bounded Observation Frame]\n\\label{definition:appC_bounded_observation_frame}\nLet $\\mathcal{H}$ be a separable Hilbert space. Define the observer-relative frame (Def.~\\ref{definition:bk4_observer_kernel_convolution_map}):\n\\[\nF_\\delta(t) = \\{x \\in \\mathcal{H} : \\|x - x_0(t)\\| \\leq \\delta\\}\n\\]\nwith $x_0(t)$ the current observer state and $\\delta$ their perceptual radius (see also bounded observer kernel in Def.~\\ref{definition:bk1_bounded_observer}).\n\\end{definition}",
  "lean_alignment": {
    "conditions": [
      "continuum/Hilbert/PDE-on-manifold content stays open; chart-complex restatements carry Glued as a named hypothesis where the source consumes compatibility",
      "modeling laws are structure fields or explicit hypotheses"
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": false,
    "notes": [
      "Frame modeled as a Finset rather than a Hilbert-space metric ball."
    ],
    "record_ids": [
      "MAP-APPENDIX_DUAL_HORIZON-034"
    ],
    "statuses": [
      "open_bridge"
    ],
    "witnesses": [
      "Book7B.complexity_card_le"
    ]
  },
  "line": 977,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Bounded Observation Frame",
  "proof_status": "definitional",
  "ref_roles": [
    {
      "context": "with $x_0(t)$ the current observer state and $\\delta$ their perceptual radius (see also bounded observer kernel in Def.~\\ref{definition:bk1_bounded_observer}). \\end{definition}",
      "label": "definition:bk1_bounded_observer",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 27,
      "target_type": "definition"
    },
    {
      "context": "ppC_bounded_observation_frame} Let $\\mathcal{H}$ be a separable Hilbert space. Define the observer-relative frame (Def.~\\ref{definition:bk4_observer_kernel_convolution_map}): \\[ F_\\delta(t) = \\{x \\in \\mathcal{H} : \\|x - x_0(t)\\| \\leq \\delta\\} \\] with $x_0(t)$ the current observer state and $",
      "label": "definition:bk4_observer_kernel_convolution_map",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "book4.tex",
      "target_line": 143,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:bk1_bounded_observer",
    "definition:bk4_observer_kernel_convolution_map"
  ],
  "role": "definition",
  "type": "definition"
}

definitiondefinitionalappendix

Complexity Measure

definition:appC_complexity_measure

Exact LaTeX body

\begin{definition}[Complexity Measure]
\label{definition:appC_complexity_measure}
The complexity $C(t)$ of the agent’s symbolic representation is:
\[
C(t) = \dim\left(\text{span}(F_\delta(t) \cap \text{learned\_basis}(t))\right)
\]
cf. recursive emergence in Def.~\ref{definition:bk1_stage_composite_operator}.
\end{definition}

Reference roles

TargetRoleLogical support
definition:bk1_stage_composite_operatorcf_near_matchyes
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [
    "definition:bk1_stage_composite_operator"
  ],
  "depends_on": [
    "definition:bk1_stage_composite_operator"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "definition:appC_complexity_measure",
  "label": "definition:appC_complexity_measure",
  "latex_body": "\\begin{definition}[Complexity Measure]\n\\label{definition:appC_complexity_measure}\nThe complexity $C(t)$ of the agent’s symbolic representation is:\n\\[\nC(t) = \\dim\\left(\\text{span}(F_\\delta(t) \\cap \\text{learned\\_basis}(t))\\right)\n\\]\ncf. recursive emergence in Def.~\\ref{definition:bk1_stage_composite_operator}.\n\\end{definition}",
  "lean_alignment": {
    "conditions": [
      "continuum/Hilbert/PDE-on-manifold content stays open; chart-complex restatements carry Glued as a named hypothesis where the source consumes compatibility",
      "modeling laws are structure fields or explicit hypotheses"
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": false,
    "notes": [
      "Finset.card of an intersection stands in for dim(span(...)); genuine linear-algebra dimension is not modeled."
    ],
    "record_ids": [
      "MAP-APPENDIX_DUAL_HORIZON-035"
    ],
    "statuses": [
      "open_bridge"
    ],
    "witnesses": [
      "Book7B.complexity_card_le"
    ]
  },
  "line": 986,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Complexity Measure",
  "proof_status": "definitional",
  "ref_roles": [
    {
      "context": "s: \\[ C(t) = \\dim\\left(\\text{span}(F_\\delta(t) \\cap \\text{learned\\_basis}(t))\\right) \\] cf. recursive emergence in Def.~\\ref{definition:bk1_stage_composite_operator}. \\end{definition}",
      "label": "definition:bk1_stage_composite_operator",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 520,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:bk1_stage_composite_operator"
  ],
  "role": "definition",
  "type": "definition"
}

definitiondefinitionalappendix

Frame Curvature Operator $K_t$

definition:appC_frame_curvature_operator

Exact LaTeX body

\begin{definition}[Frame Curvature Operator $K_t$]
\label{definition:appC_frame_curvature_operator}
The curvature of evolving frames is defined symbolically as:
\[
K_t(v) = \lim_{h \to 0} \frac{P_{F_\delta(t+h)}(v) - P_{F_\delta(t)}(v)}{h}
\]
This parallels the symbolic curvature tensor in Def.~\ref{definition:bk6_symbolic_curvature_tensor}.
\end{definition}

Reference roles

TargetRoleLogical support
definition:bk6_symbolic_curvature_tensordefinition_anchoryes
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [
    "definition:bk6_symbolic_curvature_tensor"
  ],
  "depends_on": [
    "definition:bk6_symbolic_curvature_tensor"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "definition:appC_frame_curvature_operator",
  "label": "definition:appC_frame_curvature_operator",
  "latex_body": "\\begin{definition}[Frame Curvature Operator $K_t$]\n\\label{definition:appC_frame_curvature_operator}\nThe curvature of evolving frames is defined symbolically as:\n\\[\nK_t(v) = \\lim_{h \\to 0} \\frac{P_{F_\\delta(t+h)}(v) - P_{F_\\delta(t)}(v)}{h}\n\\]\nThis parallels the symbolic curvature tensor in Def.~\\ref{definition:bk6_symbolic_curvature_tensor}.\n\\end{definition}",
  "line": 998,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Frame Curvature Operator $K_t$",
  "proof_status": "definitional",
  "ref_roles": [
    {
      "context": "m_{h \\to 0} \\frac{P_{F_\\delta(t+h)}(v) - P_{F_\\delta(t)}(v)}{h} \\] This parallels the symbolic curvature tensor in Def.~\\ref{definition:bk6_symbolic_curvature_tensor}. \\end{definition}",
      "label": "definition:bk6_symbolic_curvature_tensor",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "book6.tex",
      "target_line": 16,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:bk6_symbolic_curvature_tensor"
  ],
  "role": "definition",
  "type": "definition"
}

lemmaprovenappendix

Banach Space of Curvature Flows

lemma:appC_banach_space_of_curvature_flows

Exact LaTeX body

\begin{lemma}[Banach Space of Curvature Flows]
\label{lemma:appC_banach_space_of_curvature_flows}
Fix a finite observation interval $[0,T]$. Let
$\mathcal{L}(\mathcal{H})$ denote the bounded operators on the Hilbert space and
let
\[
\operatorname{Lip}([0,T],\mathcal{L}(\mathcal{H}))
:=\{K:[0,T]\to\mathcal{L}(\mathcal{H}) : K\text{ is Lipschitz}\}
\]
with norm
\[
\|K\|_{\operatorname{Lip}}
:=\sup_{t\in[0,T]}\|K_t\|_{\mathrm{op}}
+\sup_{s\ne t}\frac{\|K_t-K_s\|_{\mathrm{op}}}{|t-s|}.
\]
Then $\operatorname{Lip}([0,T],\mathcal{L}(\mathcal{H}))$ is a Banach space. The
admissible bounded-observer curvature flows satisfying
\[
\|K_t-K_s\|_{\mathrm{op}}\le C_1\delta |t-s|\qquad(s,t\in[0,T])
\]
form a closed complete subset of this Banach space.
\end{lemma}
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "appendix_dual_horizon.tex",
  "id": "lemma:appC_banach_space_of_curvature_flows",
  "label": "lemma:appC_banach_space_of_curvature_flows",
  "latex_body": "\\begin{lemma}[Banach Space of Curvature Flows]\n\\label{lemma:appC_banach_space_of_curvature_flows}\nFix a finite observation interval $[0,T]$. Let\n$\\mathcal{L}(\\mathcal{H})$ denote the bounded operators on the Hilbert space and\nlet\n\\[\n\\operatorname{Lip}([0,T],\\mathcal{L}(\\mathcal{H}))\n:=\\{K:[0,T]\\to\\mathcal{L}(\\mathcal{H}) : K\\text{ is Lipschitz}\\}\n\\]\nwith norm\n\\[\n\\|K\\|_{\\operatorname{Lip}}\n:=\\sup_{t\\in[0,T]}\\|K_t\\|_{\\mathrm{op}}\n+\\sup_{s\\ne t}\\frac{\\|K_t-K_s\\|_{\\mathrm{op}}}{|t-s|}.\n\\]\nThen $\\operatorname{Lip}([0,T],\\mathcal{L}(\\mathcal{H}))$ is a Banach space. The\nadmissible bounded-observer curvature flows satisfying\n\\[\n\\|K_t-K_s\\|_{\\mathrm{op}}\\le C_1\\delta |t-s|\\qquad(s,t\\in[0,T])\n\\]\nform a closed complete subset of this Banach space.\n\\end{lemma}",
  "lean_alignment": {
    "conditions": [
      "complete normed target for ambient bounded continuous flows",
      "one common Lipschitz constant across the sequence",
      "pointwise convergence of the flow sequence"
    ],
    "countermodels": [
      "AppendixCurvatureFlows.pointwise_convergence_alone_does_not_preserve_bound"
    ],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "Analytic kernel: bounded continuous flows into a complete normed target are complete in the uniform ambient metric, and a shared Lipschitz bound—including the printed C1*delta bound—passes to pointwise limits. A countermodel shows pointwise convergence without a common bound is insufficient. The exact custom Lipschitz norm and bounded-operator specialization are not reconstructed."
    ],
    "record_ids": [
      "MAP-APPENDIX_DUAL_HORIZON-052"
    ],
    "statuses": [
      "conditional"
    ],
    "witnesses": [
      "AppendixCurvatureFlows.boundedContinuousFlow_cauchy_converges",
      "AppendixCurvatureFlows.observer_bound_closed_under_pointwise_limit",
      "AppendixCurvatureFlows.pointwise_convergence_alone_does_not_preserve_bound",
      "AppendixCurvatureFlows.pointwise_limit_preserves_lipschitz_bound"
    ]
  },
  "line": 1007,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Banach Space of Curvature Flows",
  "proof_labels": [
    "proof:appC_banach_space_of_curvature_flows"
  ],
  "proof_status": "proven",
  "refs": [],
  "role": "lemma",
  "type": "lemma"
}

proofappendix

proof:appC_banach_space_of_curvature_flows

proof:appC_banach_space_of_curvature_flows

Exact LaTeX body

\begin{proof}
\label{proof:appC_banach_space_of_curvature_flows}
Let $(K^{(m)})$ be a Cauchy sequence in the Lipschitz norm. Then it is Cauchy in
the uniform operator norm, and since $\mathcal{L}(\mathcal{H})$ is Banach, there
exists a uniform limit $K:[0,T]\to\mathcal{L}(\mathcal{H})$. The Lipschitz
seminorms of $K^{(m)}-K^{(\ell)}$ also converge to zero, so for every $s\ne t$
the quotients
\[
\frac{(K^{(m)}_t-K^{(m)}_s)-(K^{(\ell)}_t-K^{(\ell)}_s)}{|t-s|}
\]
are Cauchy in operator norm uniformly over $s,t$. Passing to the uniform limit
shows that $K$ has finite Lipschitz seminorm and that
$\|K^{(m)}-K\|_{\operatorname{Lip}}\to0$. Thus the space is complete.
If each $K^{(m)}$ satisfies
$\|K^{(m)}_t-K^{(m)}_s\|_{\mathrm{op}}\le C_1\delta |t-s|$, uniform convergence
permits passage to the limit, giving the same inequality for $K$. Hence the
admissible class is closed and therefore complete.
\end{proof}
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "appendix_dual_horizon.tex",
  "id": "proof:appC_banach_space_of_curvature_flows",
  "label": "proof:appC_banach_space_of_curvature_flows",
  "latex_body": "\\begin{proof}\n\\label{proof:appC_banach_space_of_curvature_flows}\nLet $(K^{(m)})$ be a Cauchy sequence in the Lipschitz norm. Then it is Cauchy in\nthe uniform operator norm, and since $\\mathcal{L}(\\mathcal{H})$ is Banach, there\nexists a uniform limit $K:[0,T]\\to\\mathcal{L}(\\mathcal{H})$. The Lipschitz\nseminorms of $K^{(m)}-K^{(\\ell)}$ also converge to zero, so for every $s\\ne t$\nthe quotients\n\\[\n\\frac{(K^{(m)}_t-K^{(m)}_s)-(K^{(\\ell)}_t-K^{(\\ell)}_s)}{|t-s|}\n\\]\nare Cauchy in operator norm uniformly over $s,t$. Passing to the uniform limit\nshows that $K$ has finite Lipschitz seminorm and that\n$\\|K^{(m)}-K\\|_{\\operatorname{Lip}}\\to0$. Thus the space is complete.\nIf each $K^{(m)}$ satisfies\n$\\|K^{(m)}_t-K^{(m)}_s\\|_{\\mathrm{op}}\\le C_1\\delta |t-s|$, uniform convergence\npermits passage to the limit, giving the same inequality for $K$. Hence the\nadmissible class is closed and therefore complete.\n\\end{proof}",
  "line": 1030,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "",
  "proves": "lemma:appC_banach_space_of_curvature_flows",
  "refs": [],
  "role": "proof",
  "type": "proof"
}

definitiondefinitionalappendix

Sustainable Growth Rate

definition:appC_sustainable_growth_rate

Exact LaTeX body

\begin{definition}[Sustainable Growth Rate]
\label{definition:appC_sustainable_growth_rate}
A growth rate $\lambda>1$ is \emph{sustainable} for a bounded recursive observer if
there exists a positive complexity sequence $(C_n)$ with finite asymptotic ratio
\[
\lambda=\lim_{n\to\infty}\frac{C_{n+1}}{C_n}
\]
and satisfying the drift--reflection retention constraint
\[
C_{n+1}\ge C_n+C_{n-1}\qquad(n\ge1).
\]
Equality is the minimal balanced closure: the next state preserves current
symbolic content and exactly one previous memory trace, with no superfluous
expansion.
\end{definition}
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "theorem:appC_phi_min_growth",
    "theorem:appC_phi_minimized_entropy_per_complexity"
  ],
  "cites": [],
  "depends_on": [],
  "file": "appendix_dual_horizon.tex",
  "id": "definition:appC_sustainable_growth_rate",
  "label": "definition:appC_sustainable_growth_rate",
  "latex_body": "\\begin{definition}[Sustainable Growth Rate]\n\\label{definition:appC_sustainable_growth_rate}\nA growth rate $\\lambda>1$ is \\emph{sustainable} for a bounded recursive observer if\nthere exists a positive complexity sequence $(C_n)$ with finite asymptotic ratio\n\\[\n\\lambda=\\lim_{n\\to\\infty}\\frac{C_{n+1}}{C_n}\n\\]\nand satisfying the drift--reflection retention constraint\n\\[\nC_{n+1}\\ge C_n+C_{n-1}\\qquad(n\\ge1).\n\\]\nEquality is the minimal balanced closure: the next state preserves current\nsymbolic content and exactly one previous memory trace, with no superfluous\nexpansion.\n\\end{definition}",
  "lean_alignment": {
    "conditions": [
      "continuum/categorical content is NOT formalized; static and finite-discrete kernels only",
      "modeling laws are structure fields or explicit hypotheses"
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "Reframed algebraically from the source's asymptotic-ratio condition to the fixed-point inequality theta >= 1 + 1/theta (the same inequality theorem:appC_phi_minimal_curvature_parameter states verbatim for the curvature parameter) -- an explicit honesty gap against the source's limit-of-sequence phrasing."
    ],
    "record_ids": [
      "MAP-APPENDIX_DUAL_HORIZON-017"
    ],
    "statuses": [
      "constructed"
    ],
    "witnesses": [
      "AppendixDH.sustainable_phi"
    ]
  },
  "line": 1052,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Sustainable Growth Rate",
  "proof_status": "definitional",
  "refs": [],
  "role": "definition",
  "type": "definition"
}

theoremprovenappendix

Golden Ratio as Minimal Sustainable Growth Rate

theorem:appC_phi_min_growth

Exact LaTeX body

\begin{theorem}[Golden Ratio as Minimal Sustainable Growth Rate]
\label{theorem:appC_phi_min_growth}
Among all sustainable growth rates in the sense of
Def.~\ref{definition:appC_sustainable_growth_rate}, the least possible value is
$\varphi$.
\end{theorem}

Reference roles

TargetRoleLogical support
definition:appC_sustainable_growth_ratedefinition_anchoryes
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "proof:appC_phi_minimized_entropy_per_complexity"
  ],
  "cites": [
    "definition:appC_sustainable_growth_rate"
  ],
  "depends_on": [
    "definition:appC_sustainable_growth_rate",
    "theorem:appC_phi_from_lagrangian"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "theorem:appC_phi_min_growth",
  "label": "theorem:appC_phi_min_growth",
  "latex_body": "\\begin{theorem}[Golden Ratio as Minimal Sustainable Growth Rate]\n\\label{theorem:appC_phi_min_growth}\nAmong all sustainable growth rates in the sense of\nDef.~\\ref{definition:appC_sustainable_growth_rate}, the least possible value is\n$\\varphi$.\n\\end{theorem}",
  "lean_alignment": {
    "conditions": [
      "continuum/categorical content is NOT formalized; static and finite-discrete kernels only",
      "modeling laws are structure fields or explicit hypotheses"
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "phi is the least value satisfying the algebraic reframing of Sustainable; not a statement about limits of sequences of ratios."
    ],
    "record_ids": [
      "MAP-APPENDIX_DUAL_HORIZON-018"
    ],
    "statuses": [
      "conditional"
    ],
    "witnesses": [
      "AppendixDH.sustainable_ge_phi"
    ]
  },
  "line": 1068,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Golden Ratio as Minimal Sustainable Growth Rate",
  "proof_labels": [
    "proof:appC_phi_min_growth"
  ],
  "proof_status": "proven",
  "ref_roles": [
    {
      "context": "al Sustainable Growth Rate] \\label{theorem:appC_phi_min_growth} Among all sustainable growth rates in the sense of Def.~\\ref{definition:appC_sustainable_growth_rate}, the least possible value is $\\varphi$. \\end{theorem}",
      "label": "definition:appC_sustainable_growth_rate",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 1052,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:appC_sustainable_growth_rate"
  ],
  "role": "theorem",
  "type": "theorem"
}

proofappendix

proof:appC_phi_min_growth

proof:appC_phi_min_growth

Exact LaTeX body

\begin{proof}
\label{proof:appC_phi_min_growth}
Let $\lambda$ be sustainable and let $(C_n)$ witness sustainability. Divide
$C_{n+1}\ge C_n+C_{n-1}$ by $C_n>0$ and pass to the limit:
\[
\lambda=\lim_{n\to\infty}\frac{C_{n+1}}{C_n}
\ge 1+\lim_{n\to\infty}\frac{C_{n-1}}{C_n}
=1+\frac{1}{\lambda}.
\]
Thus $\lambda^2-\lambda-1\ge0$. Since $\lambda>0$, this implies
$\lambda\ge(1+\sqrt5)/2=\varphi$. The equality recurrence
$C_{n+1}=C_n+C_{n-1}$ with $C_0,C_1>0$ has asymptotic ratio $\varphi$ by
Theorem~\ref{theorem:appC_phi_from_lagrangian}; hence the lower bound is sharp.
Therefore the minimal sustainable growth rate is $\varphi$.
\end{proof}

Reference roles

TargetRoleLogical support
theorem:appC_phi_from_lagrangianproof_supportyes
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [
    "theorem:appC_phi_from_lagrangian"
  ],
  "depends_on": [
    "theorem:appC_phi_from_lagrangian"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "proof:appC_phi_min_growth",
  "label": "proof:appC_phi_min_growth",
  "latex_body": "\\begin{proof}\n\\label{proof:appC_phi_min_growth}\nLet $\\lambda$ be sustainable and let $(C_n)$ witness sustainability. Divide\n$C_{n+1}\\ge C_n+C_{n-1}$ by $C_n>0$ and pass to the limit:\n\\[\n\\lambda=\\lim_{n\\to\\infty}\\frac{C_{n+1}}{C_n}\n\\ge 1+\\lim_{n\\to\\infty}\\frac{C_{n-1}}{C_n}\n=1+\\frac{1}{\\lambda}.\n\\]\nThus $\\lambda^2-\\lambda-1\\ge0$. Since $\\lambda>0$, this implies\n$\\lambda\\ge(1+\\sqrt5)/2=\\varphi$. The equality recurrence\n$C_{n+1}=C_n+C_{n-1}$ with $C_0,C_1>0$ has asymptotic ratio $\\varphi$ by\nTheorem~\\ref{theorem:appC_phi_from_lagrangian}; hence the lower bound is sharp.\nTherefore the minimal sustainable growth rate is $\\varphi$.\n\\end{proof}",
  "line": 1075,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "",
  "proves": "theorem:appC_phi_min_growth",
  "ref_roles": [
    {
      "context": "5)/2=\\varphi$. The equality recurrence $C_{n+1}=C_n+C_{n-1}$ with $C_0,C_1>0$ has asymptotic ratio $\\varphi$ by Theorem~\\ref{theorem:appC_phi_from_lagrangian}; hence the lower bound is sharp. Therefore the minimal sustainable growth rate is $\\varphi$. \\end{proof}",
      "label": "theorem:appC_phi_from_lagrangian",
      "logical_support": true,
      "role": "proof_support",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 930,
      "target_type": "theorem"
    }
  ],
  "refs": [
    "theorem:appC_phi_from_lagrangian"
  ],
  "role": "proof",
  "type": "proof"
}

definitiondefinitionalappendix

Complexity Growth Operator $G$

definition:appC_complexity_growth_operator

Exact LaTeX body

\begin{definition}[Complexity Growth Operator $G$]
\label{definition:appC_complexity_growth_operator}
Work in $\mathbb{R}^2$ with any norm, encoding a two-step symbolic state
as $(C_n,C_{n-1})^T$. Define the balanced complexity growth operator
\[
G\begin{pmatrix}x\\y\end{pmatrix}
=\begin{pmatrix}x+y\\x\end{pmatrix},
\qquad
G=\begin{pmatrix}1&1\\1&0\end{pmatrix}.
\]
This is the linear operator form of the minimal drift--reflection closure
$C_{n+1}=C_n+C_{n-1}$.
\end{definition}
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "theorem:appC_phi_as_spectral_radius"
  ],
  "cites": [],
  "depends_on": [],
  "file": "appendix_dual_horizon.tex",
  "id": "definition:appC_complexity_growth_operator",
  "label": "definition:appC_complexity_growth_operator",
  "latex_body": "\\begin{definition}[Complexity Growth Operator $G$]\n\\label{definition:appC_complexity_growth_operator}\nWork in $\\mathbb{R}^2$ with any norm, encoding a two-step symbolic state\nas $(C_n,C_{n-1})^T$. Define the balanced complexity growth operator\n\\[\nG\\begin{pmatrix}x\\\\y\\end{pmatrix}\n=\\begin{pmatrix}x+y\\\\x\\end{pmatrix},\n\\qquad\nG=\\begin{pmatrix}1&1\\\\1&0\\end{pmatrix}.\n\\]\nThis is the linear operator form of the minimal drift--reflection closure\n$C_{n+1}=C_n+C_{n-1}$.\n\\end{definition}",
  "line": 1094,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Complexity Growth Operator $G$",
  "proof_status": "definitional",
  "refs": [],
  "role": "definition",
  "type": "definition"
}

theoremprovenappendix

Spectral Radius of $G$ Equals $\varphi$

theorem:appC_phi_as_spectral_radius

Exact LaTeX body

\begin{theorem}[Spectral Radius of $G$ Equals $\varphi$]
\label{theorem:appC_phi_as_spectral_radius}
For $G$ defined in Def.~\ref{definition:appC_complexity_growth_operator},
\[
\rho(G)=\lim_{n \to \infty} \|G^n\|^{1/n} = \varphi .
\]
\end{theorem}

Reference roles

TargetRoleLogical support
definition:appC_complexity_growth_operatordefinition_anchoryes
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "remark:bk5_curvature_vs_chaos"
  ],
  "cites": [
    "definition:appC_complexity_growth_operator"
  ],
  "depends_on": [
    "definition:appC_complexity_growth_operator"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "theorem:appC_phi_as_spectral_radius",
  "label": "theorem:appC_phi_as_spectral_radius",
  "latex_body": "\\begin{theorem}[Spectral Radius of $G$ Equals $\\varphi$]\n\\label{theorem:appC_phi_as_spectral_radius}\nFor $G$ defined in Def.~\\ref{definition:appC_complexity_growth_operator},\n\\[\n\\rho(G)=\\lim_{n \\to \\infty} \\|G^n\\|^{1/n} = \\varphi .\n\\]\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 scalar growth-rate content of rho(G)=phi is witnessed by the same golden-ratio limit; the operator G and its spectral radius/operator norm are not modeled."
    ],
    "record_ids": [
      "MAP-APPENDIX_DUAL_HORIZON-036"
    ],
    "statuses": [
      "conditional"
    ],
    "witnesses": [
      "Book7B.shiftedFib_ratio_tendsto_goldenRatio"
    ]
  },
  "line": 1108,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Spectral Radius of $G$ Equals $\\varphi$",
  "proof_labels": [
    "proof:appC_phi_as_spectral_radius"
  ],
  "proof_status": "proven",
  "ref_roles": [
    {
      "context": "n{theorem}[Spectral Radius of $G$ Equals $\\varphi$] \\label{theorem:appC_phi_as_spectral_radius} For $G$ defined in Def.~\\ref{definition:appC_complexity_growth_operator}, \\[ \\rho(G)=\\lim_{n \\to \\infty} \\|G^n\\|^{1/n} = \\varphi . \\] \\end{theorem}",
      "label": "definition:appC_complexity_growth_operator",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 1094,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:appC_complexity_growth_operator"
  ],
  "role": "theorem",
  "type": "theorem"
}

proofappendix

proof:appC_phi_as_spectral_radius

proof:appC_phi_as_spectral_radius

Exact LaTeX body

\begin{proof}
\label{proof:appC_phi_as_spectral_radius}
The characteristic polynomial of $G$ is
\[
\det\!\begin{pmatrix}1-\mu&1\\1&-\mu\end{pmatrix}
=\mu^2-\mu-1.
\]
Its eigenvalues are $\varphi=(1+\sqrt5)/2$ and
$\widehat\varphi=(1-\sqrt5)/2=-\varphi^{-1}$. Hence the spectral radius is
$\rho(G)=\max\{|\varphi|,|\widehat\varphi|\}=\varphi$. Since $G$ is a finite
matrix, Gelfand's formula gives $\rho(G)=\lim_{n\to\infty}\|G^n\|^{1/n}$ for any
matrix norm.
\end{proof}
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "appendix_dual_horizon.tex",
  "id": "proof:appC_phi_as_spectral_radius",
  "label": "proof:appC_phi_as_spectral_radius",
  "latex_body": "\\begin{proof}\n\\label{proof:appC_phi_as_spectral_radius}\nThe characteristic polynomial of $G$ is\n\\[\n\\det\\!\\begin{pmatrix}1-\\mu&1\\\\1&-\\mu\\end{pmatrix}\n=\\mu^2-\\mu-1.\n\\]\nIts eigenvalues are $\\varphi=(1+\\sqrt5)/2$ and\n$\\widehat\\varphi=(1-\\sqrt5)/2=-\\varphi^{-1}$. Hence the spectral radius is\n$\\rho(G)=\\max\\{|\\varphi|,|\\widehat\\varphi|\\}=\\varphi$. Since $G$ is a finite\nmatrix, Gelfand's formula gives $\\rho(G)=\\lim_{n\\to\\infty}\\|G^n\\|^{1/n}$ for any\nmatrix norm.\n\\end{proof}",
  "line": 1116,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "",
  "proves": "theorem:appC_phi_as_spectral_radius",
  "refs": [],
  "role": "proof",
  "type": "proof"
}

definitiondefinitionalappendix

Complexity--Entropy Tradeoff

definition:appC_complexity_entropy_tradeof

Exact LaTeX body

\begin{definition}[Complexity--Entropy Tradeoff]
\label{definition:appC_complexity_entropy_tradeof}
For a sustainable asymptotic growth factor $\lambda$, define the normalized
one-step symbolic inefficiency
\[
\mathcal{I}(\lambda):=\lambda+\frac{1}{\lambda}.
\]
The first term records forward expansion cost; the second records the reflective
memory load required by bounded retention. This is the dimensionless
entropy-per-complexity overhead associated with one asymptotic drift--reflection
step.
\end{definition}
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "theorem:appC_phi_minimized_entropy_per_complexity"
  ],
  "cites": [],
  "depends_on": [],
  "file": "appendix_dual_horizon.tex",
  "id": "definition:appC_complexity_entropy_tradeof",
  "label": "definition:appC_complexity_entropy_tradeof",
  "latex_body": "\\begin{definition}[Complexity--Entropy Tradeoff]\n\\label{definition:appC_complexity_entropy_tradeof}\nFor a sustainable asymptotic growth factor $\\lambda$, define the normalized\none-step symbolic inefficiency\n\\[\n\\mathcal{I}(\\lambda):=\\lambda+\\frac{1}{\\lambda}.\n\\]\nThe first term records forward expansion cost; the second records the reflective\nmemory load required by bounded retention. This is the dimensionless\nentropy-per-complexity overhead associated with one asymptotic drift--reflection\nstep.\n\\end{definition}",
  "line": 1133,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Complexity--Entropy Tradeoff",
  "proof_status": "definitional",
  "refs": [],
  "role": "definition",
  "type": "definition"
}

theoremprovenappendix

$\varphi$ Minimizes Entropy-per-Complexity

theorem:appC_phi_minimized_entropy_per_complexity

Exact LaTeX body

\begin{theorem}[$\varphi$ Minimizes Entropy-per-Complexity]
\label{theorem:appC_phi_minimized_entropy_per_complexity}
Among all sustainable growth rates $\lambda$ in the sense of
Def.~\ref{definition:appC_sustainable_growth_rate}, the inefficiency
$\mathcal{I}(\lambda)$ of Def.~\ref{definition:appC_complexity_entropy_tradeof} is
minimized at $\lambda=\varphi$.
\end{theorem}

Reference roles

TargetRoleLogical support
definition:appC_complexity_entropy_tradeofdefinition_anchoryes
definition:appC_sustainable_growth_ratedefinition_anchoryes
Complete structured record
{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [
    "definition:appC_complexity_entropy_tradeof",
    "definition:appC_sustainable_growth_rate"
  ],
  "depends_on": [
    "definition:appC_complexity_entropy_tradeof",
    "definition:appC_sustainable_growth_rate",
    "theorem:appC_phi_min_growth"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "theorem:appC_phi_minimized_entropy_per_complexity",
  "label": "theorem:appC_phi_minimized_entropy_per_complexity",
  "latex_body": "\\begin{theorem}[$\\varphi$ Minimizes Entropy-per-Complexity]\n\\label{theorem:appC_phi_minimized_entropy_per_complexity}\nAmong all sustainable growth rates $\\lambda$ in the sense of\nDef.~\\ref{definition:appC_sustainable_growth_rate}, the inefficiency\n$\\mathcal{I}(\\lambda)$ of Def.~\\ref{definition:appC_complexity_entropy_tradeof} is\nminimized at $\\lambda=\\varphi$.\n\\end{theorem}",
  "lean_alignment": {
    "conditions": [
      "continuum/categorical content is NOT formalized; static and finite-discrete kernels only",
      "modeling laws are structure fields or explicit hypotheses"
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "Proved among Sustainable rates (the algebraic reframing), not among all sustainable-in-the-source's-asymptotic-sense rates."
    ],
    "record_ids": [
      "MAP-APPENDIX_DUAL_HORIZON-021"
    ],
    "statuses": [
      "conditional"
    ],
    "witnesses": [
      "AppendixDH.kappa_min_at_phi"
    ]
  },
  "line": 1146,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "$\\varphi$ Minimizes Entropy-per-Complexity",
  "proof_labels": [
    "proof:appC_phi_minimized_entropy_per_complexity"
  ],
  "proof_status": "proven",
  "ref_roles": [
    {
      "context": "da$ in the sense of Def.~\\ref{definition:appC_sustainable_growth_rate}, the inefficiency $\\mathcal{I}(\\lambda)$ of Def.~\\ref{definition:appC_complexity_entropy_tradeof} is minimized at $\\lambda=\\varphi$. \\end{theorem}",
      "label": "definition:appC_complexity_entropy_tradeof",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 1133,
      "target_type": "definition"
    },
    {
      "context": "el{theorem:appC_phi_minimized_entropy_per_complexity} Among all sustainable growth rates $\\lambda$ in the sense of Def.~\\ref{definition:appC_sustainable_growth_rate}, the inefficiency $\\mathcal{I}(\\lambda)$ of Def.~\\ref{definition:appC_complexity_entropy_tradeof} is minimized at $\\lam",
      "label": "definition:appC_sustainable_growth_rate",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 1052,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:appC_complexity_entropy_tradeof",
    "definition:appC_sustainable_growth_rate"
  ],
  "role": "theorem",
  "type": "theorem"
}