Dual Horizon – A Formal Proof by Elimination — page 1 of 3

{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "remark:bk9_grace_flow_geometric_witness",
    "sec:bk1_prefatio"
  ],
  "cites": [
    "definition:bk4_bounded_observer",
    "definition:bk6_drift_operator_complete",
    "definition:bk6_reflection_operator_complete",
    "scholium:appC_two_modalities_one_root",
    "sec:appC_proof_by_elimination",
    "sec:appC_proof_observational",
    "theorem:bk1_dual_horizon_necessity_theorem"
  ],
  "depends_on": [
    "definition:bk4_bounded_observer",
    "definition:bk6_drift_operator_complete",
    "definition:bk6_reflection_operator_complete",
    "theorem:bk1_dual_horizon_necessity_theorem"
  ],
  "file": "appendix_dual_horizon.tex",
  "forward_ref_roles": [
    {
      "context": "",
      "label": "scholium:appC_two_modalities_one_root",
      "line_distance": 267,
      "role": "navigation",
      "target_line": 270,
      "target_type": "scholium"
    },
    {
      "context": "",
      "label": "sec:appC_proof_by_elimination",
      "line_distance": 141,
      "role": "navigation",
      "target_line": 144,
      "target_type": "section"
    },
    {
      "context": "",
      "label": "sec:appC_proof_observational",
      "line_distance": 96,
      "role": "navigation",
      "target_line": 99,
      "target_type": "section"
    }
  ],
  "forward_refs": [
    "scholium:appC_two_modalities_one_root",
    "sec:appC_proof_by_elimination",
    "sec:appC_proof_observational"
  ],
  "id": "sec:appC_dual_horizon",
  "label": "sec:appC_dual_horizon",
  "latex_body": "",
  "line": 3,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Dual Horizon – A Formal Proof by Elimination",
  "ref_roles": [
    {
      "context": "",
      "label": "definition:bk4_bounded_observer",
      "logical_support": false,
      "role": "navigation",
      "target_file": "book4.tex",
      "target_line": 427,
      "target_type": "definition"
    },
    {
      "context": "",
      "label": "definition:bk6_drift_operator_complete",
      "logical_support": false,
      "role": "navigation",
      "target_file": "book6.tex",
      "target_line": 926,
      "target_type": "definition"
    },
    {
      "context": "",
      "label": "definition:bk6_reflection_operator_complete",
      "logical_support": false,
      "role": "navigation",
      "target_file": "book6.tex",
      "target_line": 937,
      "target_type": "definition"
    },
    {
      "context": "",
      "label": "scholium:appC_two_modalities_one_root",
      "logical_support": false,
      "role": "forward_navigation",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 270,
      "target_type": "scholium"
    },
    {
      "context": "",
      "label": "sec:appC_proof_by_elimination",
      "logical_support": false,
      "role": "forward_navigation",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 144,
      "target_type": "section"
    },
    {
      "context": "",
      "label": "sec:appC_proof_observational",
      "logical_support": false,
      "role": "forward_navigation",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 99,
      "target_type": "section"
    },
    {
      "context": "",
      "label": "theorem:bk1_dual_horizon_necessity_theorem",
      "logical_support": false,
      "role": "navigation",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 775,
      "target_type": "theorem"
    }
  ],
  "role": "section",
  "subtype": "chapter",
  "type": "section"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [
    "assumption:appC_emergence_coupling",
    "assumption:appC_emergence_domination",
    "remark:appC_domination_open_route",
    "sec:appC_born_rule",
    "sec:appC_proof_by_elimination",
    "sec:appC_proof_observational"
  ],
  "depends_on": [],
  "file": "appendix_dual_horizon.tex",
  "forward_ref_roles": [
    {
      "context": "",
      "label": "assumption:appC_emergence_coupling",
      "line_distance": 190,
      "role": "navigation",
      "target_line": 197,
      "target_type": "assumption"
    },
    {
      "context": "",
      "label": "assumption:appC_emergence_domination",
      "line_distance": 56,
      "role": "navigation",
      "target_line": 63,
      "target_type": "assumption"
    },
    {
      "context": "",
      "label": "remark:appC_domination_open_route",
      "line_distance": 244,
      "role": "navigation",
      "target_line": 251,
      "target_type": "remark"
    },
    {
      "context": "",
      "label": "sec:appC_born_rule",
      "line_distance": 301,
      "role": "navigation",
      "target_line": 308,
      "target_type": "section"
    },
    {
      "context": "",
      "label": "sec:appC_proof_by_elimination",
      "line_distance": 137,
      "role": "navigation",
      "target_line": 144,
      "target_type": "section"
    },
    {
      "context": "",
      "label": "sec:appC_proof_observational",
      "line_distance": 92,
      "role": "navigation",
      "target_line": 99,
      "target_type": "section"
    }
  ],
  "forward_refs": [
    "assumption:appC_emergence_coupling",
    "assumption:appC_emergence_domination",
    "remark:appC_domination_open_route",
    "sec:appC_born_rule",
    "sec:appC_proof_by_elimination",
    "sec:appC_proof_observational"
  ],
  "id": "subsec:appC_methodological_logical_framework",
  "label": "subsec:appC_methodological_logical_framework",
  "latex_body": "",
  "line": 7,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "C.0.1 Method: two eliminations, one root",
  "ref_roles": [
    {
      "context": "",
      "label": "assumption:appC_emergence_coupling",
      "logical_support": false,
      "role": "forward_navigation",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 197,
      "target_type": "assumption"
    },
    {
      "context": "",
      "label": "assumption:appC_emergence_domination",
      "logical_support": false,
      "role": "forward_navigation",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 63,
      "target_type": "assumption"
    },
    {
      "context": "",
      "label": "remark:appC_domination_open_route",
      "logical_support": false,
      "role": "forward_navigation",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 251,
      "target_type": "remark"
    },
    {
      "context": "",
      "label": "sec:appC_born_rule",
      "logical_support": false,
      "role": "forward_navigation",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 308,
      "target_type": "section"
    },
    {
      "context": "",
      "label": "sec:appC_proof_by_elimination",
      "logical_support": false,
      "role": "forward_navigation",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 144,
      "target_type": "section"
    },
    {
      "context": "",
      "label": "sec:appC_proof_observational",
      "logical_support": false,
      "role": "forward_navigation",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 99,
      "target_type": "section"
    }
  ],
  "role": "section",
  "subtype": "subsection",
  "type": "section"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "appendix_dual_horizon.tex",
  "id": "sec:appC_formal_statement_dual_horizon_thesis",
  "label": "sec:appC_formal_statement_dual_horizon_thesis",
  "latex_body": "",
  "line": 10,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Formal Statement: Dual Horizon as Effective Signature",
  "role": "section",
  "subtype": "section",
  "type": "section"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [
    "definition:bk1_symbolic_manifold",
    "definition:bk4_bounded_observer",
    "definition:bk4_observer_kernel_convolution_map",
    "definition:bk6_drift_operator_complete",
    "definition:bk6_reflection_operator_complete"
  ],
  "depends_on": [
    "definition:bk1_symbolic_manifold",
    "definition:bk4_bounded_observer",
    "definition:bk4_observer_kernel_convolution_map",
    "definition:bk6_drift_operator_complete",
    "definition:bk6_reflection_operator_complete"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "definition:appC_observer_visible_system",
  "label": "definition:appC_observer_visible_system",
  "latex_body": "\\begin{definition}[Observer-visible symbolic system]\n\\label{definition:appC_observer_visible_system}\nA \\emph{bounded symbolic dynamical system} is a tuple\n\\((\\manifold, g, \\drift, R_{\\mathrm{stab}}, \\Obs)\\), where \\(\\manifold\\) is a\nsymbolic manifold (cf.~\\ref{definition:bk1_symbolic_manifold}) with metric \\(g\\),\n\\(\\drift\\) is the drift field (cf.~\\ref{definition:bk6_drift_operator_complete}),\n\\(R_{\\mathrm{stab}}\\) is the stabilizing reflection field\n(cf.~\\ref{definition:bk6_reflection_operator_complete}), and \\(\\Obs\\) is a Bounded\nObserver (cf.~\\ref{definition:bk4_bounded_observer}) with resolution threshold\n\\(\\epsilon_{\\Obs}\\). The \\emph{observer-visible domain} \\(\\Omega\\subseteq\\manifold\\)\nis the region resolved by \\(\\Obs\\) above \\(\\epsilon_{\\Obs}\\), carrying the\nresolution-weighted observer measure \\(\\mu_{\\Obs}\\) induced by the observer kernel\n(cf.~\\ref{definition:bk4_observer_kernel_convolution_map}).\n\\end{definition}",
  "line": 12,
  "macros_used": [
    "Obs",
    "drift",
    "manifold"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Observer-visible symbolic system",
  "proof_status": "definitional",
  "ref_roles": [
    {
      "context": "system} is a tuple \\((\\manifold, g, \\drift, R_{\\mathrm{stab}}, \\Obs)\\), where \\(\\manifold\\) is a symbolic manifold (cf.~\\ref{definition:bk1_symbolic_manifold}) with metric \\(g\\), \\(\\drift\\) is the drift field (cf.~\\ref{definition:bk6_drift_operator_complete}), \\(R_{\\mathrm{stab",
      "label": "definition:bk1_symbolic_manifold",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 1188,
      "target_type": "definition"
    },
    {
      "context": "izing reflection field (cf.~\\ref{definition:bk6_reflection_operator_complete}), and \\(\\Obs\\) is a Bounded Observer (cf.~\\ref{definition:bk4_bounded_observer}) with resolution threshold \\(\\epsilon_{\\Obs}\\). The \\emph{observer-visible domain} \\(\\Omega\\subseteq\\manifold\\) is the",
      "label": "definition:bk4_bounded_observer",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book4.tex",
      "target_line": 427,
      "target_type": "definition"
    },
    {
      "context": "\\epsilon_{\\Obs}\\), carrying the resolution-weighted observer measure \\(\\mu_{\\Obs}\\) induced by the observer kernel (cf.~\\ref{definition:bk4_observer_kernel_convolution_map}). \\end{definition}",
      "label": "definition:bk4_observer_kernel_convolution_map",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book4.tex",
      "target_line": 143,
      "target_type": "definition"
    },
    {
      "context": "a symbolic manifold (cf.~\\ref{definition:bk1_symbolic_manifold}) with metric \\(g\\), \\(\\drift\\) is the drift field (cf.~\\ref{definition:bk6_drift_operator_complete}), \\(R_{\\mathrm{stab}}\\) is the stabilizing reflection field (cf.~\\ref{definition:bk6_reflection_operator_complete}), an",
      "label": "definition:bk6_drift_operator_complete",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book6.tex",
      "target_line": 926,
      "target_type": "definition"
    },
    {
      "context": "ield (cf.~\\ref{definition:bk6_drift_operator_complete}), \\(R_{\\mathrm{stab}}\\) is the stabilizing reflection field (cf.~\\ref{definition:bk6_reflection_operator_complete}), and \\(\\Obs\\) is a Bounded Observer (cf.~\\ref{definition:bk4_bounded_observer}) with resolution threshold \\(\\epsilon_{",
      "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:bk1_symbolic_manifold",
    "definition:bk4_bounded_observer",
    "definition:bk4_observer_kernel_convolution_map",
    "definition:bk6_drift_operator_complete",
    "definition:bk6_reflection_operator_complete"
  ],
  "role": "definition",
  "type": "definition"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "remark:appC_horizon_realizations"
  ],
  "cites": [],
  "depends_on": [],
  "file": "appendix_dual_horizon.tex",
  "id": "definition:appC_horizon_fluxes",
  "label": "definition:appC_horizon_fluxes",
  "latex_body": "\\begin{definition}[Generative and stabilizing horizon fluxes]\n\\label{definition:appC_horizon_fluxes}\nOn the observer-visible domain \\(\\Omega\\) define the \\emph{generative flux}\n\\[\nG_{\\Obs}(\\Omega) := \\int_\\Omega \\big(\\nabla\\!\\cdot\\drift\\big)_+ \\, d\\mu_{\\Obs},\n\\qquad (x)_+ := \\max\\{x,0\\},\n\\]\nand the \\emph{stabilizing flux}\n\\[\nC_{\\Obs}(\\Omega) := \\int_\\Omega \\big(-\\nabla\\!\\cdot R_{\\mathrm{stab}}\\big)_+ \\, d\\mu_{\\Obs}.\n\\]\nThus \\(G_{\\Obs}\\) accumulates the observer-visible rate at which Drift \\emph{sources}\nnovelty (positive divergence) and \\(C_{\\Obs}\\) the rate at which stabilizing\nReflection \\emph{sinks} it (negative divergence). Up to the divergence theorem,\n\\(\\int_\\Omega \\nabla\\!\\cdot\\drift \\, d\\mu_{\\Obs}\\) is the net Drift flux across the\nresolution boundary \\(\\partial\\Omega\\) --- the observer's \\emph{horizon} --- and\n\\(G_{\\Obs}\\) retains only its sourcing part; symmetrically for \\(C_{\\Obs}\\). This is\nthe precise sense in which the two are horizon-effects, defined independently of how\nmany geometric horizons realize them.\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": [
      "Only the pointwise real identity x = max(x,0)-max(-x,0) underlying the divergence-theorem remark is modeled; the observer measure and manifold integrals G_Obs, C_Obs themselves are not."
    ],
    "record_ids": [
      "MAP-APPENDIX_DUAL_HORIZON-032"
    ],
    "statuses": [
      "open_bridge"
    ],
    "witnesses": [
      "Book7B.posPart_sub_negPart"
    ]
  },
  "line": 27,
  "macros_used": [
    "Obs",
    "drift"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Generative and stabilizing horizon fluxes",
  "proof_status": "definitional",
  "refs": [],
  "role": "definition",
  "type": "definition"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "theorem:appC_dual_horizon_signature"
  ],
  "cites": [
    "definition:bk1_stage_composite_operator",
    "definition:bk2_symbolic_free_energy"
  ],
  "depends_on": [
    "definition:bk1_stage_composite_operator",
    "definition:bk2_symbolic_free_energy"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "definition:appC_bounded_reflexive_emergence",
  "label": "definition:appC_bounded_reflexive_emergence",
  "latex_body": "\\begin{definition}[Bounded reflexive emergence]\n\\label{definition:appC_bounded_reflexive_emergence}\nThe system exhibits \\emph{bounded reflexive emergence} on \\(\\Omega\\) over a\nsymbolic-time interval \\(I\\) if the observer-visible emergence functional\n\\(\\Delta\\Phi_{\\Obs}\\) --- the net gain over \\(I\\) of retained, resolved coherent\nstructure produced by the coupled action of \\(\\drift\\) and \\(R_{\\mathrm{stab}}\\) (the\nstage-composite emergence of Def.~\\ref{definition:bk1_stage_composite_operator},\nmeasured as stabilized reduction of symbolic free energy \\(\\freeenergy\\),\ncf.~\\ref{definition:bk2_symbolic_free_energy}) --- satisfies\n\\[\n\\Delta\\Phi_{\\Obs}(\\drift, R_{\\mathrm{stab}}) \\;\\ge\\; \\tau_E \\;>\\; 0\n\\]\nfor an observer-fixed emergence threshold \\(\\tau_E\\).\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": [
      "Modeled as the hypothesis pair (0 < tauE, tauE <= deltaPhi) taken by dual_horizon_signature, rather than as a standalone named Prop."
    ],
    "record_ids": [
      "MAP-APPENDIX_DUAL_HORIZON-001"
    ],
    "statuses": [
      "constructed"
    ],
    "witnesses": [
      "AppendixDH.dual_horizon_signature"
    ]
  },
  "line": 48,
  "macros_used": [
    "Obs",
    "drift",
    "freeenergy"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Bounded reflexive emergence",
  "proof_status": "definitional",
  "ref_roles": [
    {
      "context": "structure produced by the coupled action of \\(\\drift\\) and \\(R_{\\mathrm{stab}}\\) (the stage-composite emergence of Def.~\\ref{definition:bk1_stage_composite_operator}, measured as stabilized reduction of symbolic free energy \\(\\freeenergy\\), cf.~\\ref{definition:bk2_symbolic_free_energy",
      "label": "definition:bk1_stage_composite_operator",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 520,
      "target_type": "definition"
    },
    {
      "context": "definition:bk1_stage_composite_operator}, measured as stabilized reduction of symbolic free energy \\(\\freeenergy\\), cf.~\\ref{definition:bk2_symbolic_free_energy}) --- satisfies \\[ \\Delta\\Phi_{\\Obs}(\\drift, R_{\\mathrm{stab}}) \\;\\ge\\; \\tau_E \\;>\\; 0 \\] for an observer-fixed emergenc",
      "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:bk1_stage_composite_operator",
    "definition:bk2_symbolic_free_energy"
  ],
  "role": "definition",
  "type": "definition"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "proof:appC_dual_horizon_biconditional",
    "proof:appC_dual_horizon_signature_geometric",
    "remark:appC_domination_open_route",
    "subsec:appC_methodological_logical_framework",
    "theorem:appC_dual_horizon_biconditional",
    "theorem:appC_dual_horizon_signature"
  ],
  "cites": [
    "definition:appC_observer_coherence_budget"
  ],
  "depends_on": [],
  "file": "appendix_dual_horizon.tex",
  "forward_ref_roles": [
    {
      "context": "(\\Omega)\\,\\big\\}. \\] This is symbolic-budget bookkeeping, not a dynamical postulate (cf. the token-budget bound of Def.~\\ref{definition:appC_observer_coherence_budget}): retained novelty visible to \\(\\Obs\\) can be neither more than was generated nor more than was stabilized, so it is bo",
      "label": "definition:appC_observer_coherence_budget",
      "line_distance": 388,
      "role": "interpretive_bridge",
      "target_line": 451,
      "target_type": "definition"
    }
  ],
  "forward_refs": [
    "definition:appC_observer_coherence_budget"
  ],
  "id": "assumption:appC_emergence_domination",
  "label": "assumption:appC_emergence_domination",
  "latex_body": "\\begin{assumption}[Emergence Domination]\n\\label{assumption:appC_emergence_domination}\nObserver-visible emergence cannot exceed the budget of the \\emph{binding} flux:\nthere is a finite gain constant \\(\\Lambda=\\Lambda(\\epsilon_{\\Obs})\\) with\n\\[\n\\Delta\\Phi_{\\Obs}(\\drift, R_{\\mathrm{stab}})\n\\;\\le\\; \\Lambda \\cdot \\min\\big\\{\\,G_{\\Obs}(\\Omega),\\, C_{\\Obs}(\\Omega)\\,\\big\\}.\n\\]\nThis is symbolic-budget bookkeeping, not a dynamical postulate (cf. the token-budget\nbound of Def.~\\ref{definition:appC_observer_coherence_budget}): retained novelty\nvisible to \\(\\Obs\\) can be neither more than was generated nor more than was\nstabilized, so it is bounded by the smaller of the two. Where one flux vanishes, no\nemergence above the floor is available.\n\\end{assumption}",
  "line": 63,
  "macros_used": [
    "Obs",
    "drift"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Emergence Domination",
  "proof_status": "definitional",
  "ref_roles": [
    {
      "context": "(\\Omega)\\,\\big\\}. \\] This is symbolic-budget bookkeeping, not a dynamical postulate (cf. the token-budget bound of Def.~\\ref{definition:appC_observer_coherence_budget}): retained novelty visible to \\(\\Obs\\) can be neither more than was generated nor more than was stabilized, so it is bo",
      "label": "definition:appC_observer_coherence_budget",
      "logical_support": false,
      "role": "forward_interpretive_bridge",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 451,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:appC_observer_coherence_budget"
  ],
  "role": "assumption",
  "type": "assumption"
}

{
  "book": "appendix_dual_horizon",
  "canonical_status": "expansion_of",
  "canonical_target": "theorem:bk1_dual_horizon_necessity_theorem",
  "certificate_tier": "A",
  "cited_by": [
    "proof:appC_dual_horizon_biconditional",
    "proof:bk1_proof_of_dual_horizon_necessity_theorem",
    "remark:appC_horizon_realizations",
    "sec:appC_proof_by_elimination",
    "sec:appC_proof_observational",
    "theorem:bk1_dual_horizon_necessity_theorem"
  ],
  "cites": [
    "assumption:appC_emergence_domination",
    "definition:appC_bounded_reflexive_emergence",
    "sec:appC_proof_by_elimination",
    "sec:appC_proof_observational",
    "theorem:bk1_dual_horizon_necessity_theorem"
  ],
  "depends_on": [
    "assumption:appC_emergence_domination",
    "definition:appC_bounded_reflexive_emergence",
    "theorem:bk1_dual_horizon_necessity_theorem"
  ],
  "file": "appendix_dual_horizon.tex",
  "forward_ref_roles": [
    {
      "context": "nal}), and geometrically, from Emergence Domination (Assumption~\\ref{assumption:appC_emergence_domination}; Proof~II, \\S\\ref{sec:appC_proof_by_elimination}). \\end{theorem}",
      "label": "sec:appC_proof_by_elimination",
      "line_distance": 66,
      "role": "navigation",
      "target_line": 144,
      "target_type": "section"
    },
    {
      "context": "se components. The conclusion is established twice below: observationally, from Bounded Observability alone (Proof~I, \\S\\ref{sec:appC_proof_observational}), and geometrically, from Emergence Domination (Assumption~\\ref{assumption:appC_emergence_domination}; Proof~II, \\S\\ref",
      "label": "sec:appC_proof_observational",
      "line_distance": 21,
      "role": "navigation",
      "target_line": 99,
      "target_type": "section"
    }
  ],
  "forward_refs": [
    "sec:appC_proof_by_elimination",
    "sec:appC_proof_observational"
  ],
  "id": "theorem:appC_dual_horizon_signature",
  "label": "theorem:appC_dual_horizon_signature",
  "latex_body": "\\begin{theorem}[Dual Horizon Necessity (Effective Signature)]\n\\label{theorem:appC_dual_horizon_signature}\nThis is the expanded, realization-invariant form of the canonical Book~I theorem\n(Thm.~\\ref{theorem:bk1_dual_horizon_necessity_theorem}); Book~I carries the\nstatement of record, and what follows is its full derivation and defense.\nLet \\((\\manifold, g, \\drift, R_{\\mathrm{stab}}, \\Obs)\\) be a bounded symbolic\ndynamical system that exhibits bounded reflexive emergence on \\(\\Omega\\)\n(Def.~\\ref{definition:appC_bounded_reflexive_emergence}). Then\n\\[\nG_{\\Obs}(\\Omega) > 0 \\qquad\\text{and}\\qquad C_{\\Obs}(\\Omega) > 0 .\n\\]\nThat is, the observer-visible flux carries a \\emph{dual effective horizon signature}\non the shared domain \\(\\Omega\\): one positive/generative and one\nnegative/stabilizing component, invariant under the geometric realization of those\ncomponents. The conclusion is established twice below: observationally, from Bounded\nObservability alone (Proof~I, \\S\\ref{sec:appC_proof_observational}), and\ngeometrically, from Emergence Domination\n(Assumption~\\ref{assumption:appC_emergence_domination}; Proof~II,\n\\S\\ref{sec:appC_proof_by_elimination}).\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 via the Emergence Domination route (Proof II of the source): bounded reflexive emergence plus the DualHorizonBalance sandwich forces min(G,C) > 0, hence G > 0 and C > 0. The source's alternative Proof I 'from Bounded Observability alone' is not modeled since that assumption is not given with enough precision in the packet."
    ],
    "record_ids": [
      "MAP-APPENDIX_DUAL_HORIZON-002"
    ],
    "statuses": [
      "conditional"
    ],
    "witnesses": [
      "AppendixDH.dual_horizon_signature"
    ]
  },
  "line": 78,
  "macros_used": [
    "Obs",
    "drift",
    "manifold"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Dual Horizon Necessity (Effective Signature)",
  "proof_labels": [
    "proof:appC_dual_horizon_signature_observational",
    "proof:appC_dual_horizon_signature_geometric"
  ],
  "proof_status": "proven",
  "ref_roles": [
    {
      "context": "ability alone (Proof~I, \\S\\ref{sec:appC_proof_observational}), and geometrically, from Emergence Domination (Assumption~\\ref{assumption:appC_emergence_domination}; Proof~II, \\S\\ref{sec:appC_proof_by_elimination}). \\end{theorem}",
      "label": "assumption:appC_emergence_domination",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 63,
      "target_type": "assumption"
    },
    {
      "context": "rm{stab}}, \\Obs)\\) be a bounded symbolic dynamical system that exhibits bounded reflexive emergence on \\(\\Omega\\) (Def.~\\ref{definition:appC_bounded_reflexive_emergence}). Then \\[ G_{\\Obs}(\\Omega) > 0 \\qquad\\text{and}\\qquad C_{\\Obs}(\\Omega) > 0 . \\] That is, the observer-visible flux carr",
      "label": "definition:appC_bounded_reflexive_emergence",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 48,
      "target_type": "definition"
    },
    {
      "context": "nal}), and geometrically, from Emergence Domination (Assumption~\\ref{assumption:appC_emergence_domination}; Proof~II, \\S\\ref{sec:appC_proof_by_elimination}). \\end{theorem}",
      "label": "sec:appC_proof_by_elimination",
      "logical_support": false,
      "role": "forward_navigation",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 144,
      "target_type": "section"
    },
    {
      "context": "se components. The conclusion is established twice below: observationally, from Bounded Observability alone (Proof~I, \\S\\ref{sec:appC_proof_observational}), and geometrically, from Emergence Domination (Assumption~\\ref{assumption:appC_emergence_domination}; Proof~II, \\S\\ref",
      "label": "sec:appC_proof_observational",
      "logical_support": false,
      "role": "forward_navigation",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 99,
      "target_type": "section"
    },
    {
      "context": "rem:appC_dual_horizon_signature} This is the expanded, realization-invariant form of the canonical Book~I theorem (Thm.~\\ref{theorem:bk1_dual_horizon_necessity_theorem}); Book~I carries the statement of record, and what follows is its full derivation and defense. Let \\((\\manifold, g, \\dr",
      "label": "theorem:bk1_dual_horizon_necessity_theorem",
      "logical_support": true,
      "role": "canonical_anchor",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 775,
      "target_type": "theorem"
    }
  ],
  "refs": [
    "assumption:appC_emergence_domination",
    "definition:appC_bounded_reflexive_emergence",
    "sec:appC_proof_by_elimination",
    "sec:appC_proof_observational",
    "theorem:bk1_dual_horizon_necessity_theorem"
  ],
  "role": "theorem",
  "type": "theorem"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "scholium:appC_two_modalities_one_root",
    "sec:appC_dual_horizon",
    "subsec:appC_methodological_logical_framework",
    "theorem:appC_dual_horizon_signature"
  ],
  "cites": [
    "theorem:appC_dual_horizon_signature"
  ],
  "depends_on": [
    "theorem:appC_dual_horizon_signature"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "sec:appC_proof_observational",
  "label": "sec:appC_proof_observational",
  "latex_body": "",
  "line": 99,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Proof I --- Observational Elimination",
  "ref_roles": [
    {
      "context": "",
      "label": "theorem:appC_dual_horizon_signature",
      "logical_support": false,
      "role": "navigation",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 78,
      "target_type": "theorem"
    }
  ],
  "role": "section",
  "subtype": "section",
  "type": "section"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "appendix_dual_horizon.tex",
  "id": "proof:appC_dual_horizon_signature_observational",
  "label": "proof:appC_dual_horizon_signature_observational",
  "latex_body": "\\begin{proof}[Proof of Theorem~\\ref{theorem:appC_dual_horizon_signature} (observational modality)]\n\\label{proof:appC_dual_horizon_signature_observational}\n\\leavevmode\n\nAssume bounded reflexive emergence, \\(\\Delta\\Phi_{\\Obs}\\ge\\tau_E>0\\): over \\(I\\) the\nobserver registers and \\emph{retains} new coherent structure on \\(\\Omega\\). We\neliminate, in turn, the three ways the dual signature can fail --- novelty that never\ncrosses the horizon, novelty that crosses but is never stabilized, and the two alive\nyet never meeting on a single observer's domain.\n\n\\textbf{Case A (no observer-visible generation): \\(G_{\\Obs}(\\Omega)=0\\).} No novelty\nis sourced across the horizon into \\(\\Omega\\) that the observer can resolve above\n\\(\\epsilon_{\\Obs}\\). Over \\(I\\) it therefore registers no \\emph{new} differentiated\ncontent --- only rearrangement below resolution, bare repetition, or decay. Retained\nnew structure presupposes registered new content; with none, \\(\\Delta\\Phi_{\\Obs}\\)\ncannot rise to \\(\\tau_E\\). One cannot retain what was never observed to enter.\nContradiction.\n\n\\textbf{Case B (no observer-visible stabilization): \\(C_{\\Obs}(\\Omega)=0\\).} Novelty\nis sourced but nothing contracts or integrates it on \\(\\Omega\\). Relative to finite\nresolution \\(\\epsilon_{\\Obs}\\), unintegrated novelty disperses or saturates the\nobserver's channel: it may be registered transiently but is not \\emph{retained} as\nstable identity \\(\\identity\\) across \\(I\\). Since \\(\\Delta\\Phi_{\\Obs}\\) counts\nretained structure, it stays below \\(\\tau_E\\). Novelty seen but not kept is not\nemergence. Contradiction.\n\n\\textbf{Case C (generation and stabilization in different observer patches).} Suppose\nboth occur in \\(\\manifold\\) but not within one resolved domain \\(\\Omega\\). The\nobserver integrates emergence over a single \\(\\Omega\\); on it, the absent\ncontribution lies outside the patch or below \\(\\epsilon_{\\Obs}\\), so that \\(\\Omega\\)\nreduces to Case~A or Case~B. No single bounded observer registers coupled becoming.\nContradiction.\n\nIn each case the observer fails to register retained emergence, contradicting\n\\(\\Delta\\Phi_{\\Obs}\\ge\\tau_E\\). Hence both an observer-visible generative contribution\nand an observer-visible stabilizing contribution must be present on the shared\n\\(\\Omega\\); that is, \\(G_{\\Obs}(\\Omega)>0\\) and \\(C_{\\Obs}(\\Omega)>0\\).\n\\end{proof}",
  "line": 105,
  "macros_used": [
    "Obs",
    "identity",
    "manifold"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Proof of Theorem~\\ref{theorem:appC_dual_horizon_signature} (observational modality)",
  "proves": "theorem:appC_dual_horizon_signature",
  "refs": [
    "theorem:appC_dual_horizon_signature"
  ],
  "role": "proof",
  "type": "proof"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "scholium:appC_two_modalities_one_root",
    "sec:appC_dual_horizon",
    "subsec:appC_methodological_logical_framework",
    "theorem:appC_dual_horizon_signature"
  ],
  "cites": [
    "theorem:appC_dual_horizon_signature"
  ],
  "depends_on": [
    "theorem:appC_dual_horizon_signature"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "sec:appC_proof_by_elimination",
  "label": "sec:appC_proof_by_elimination",
  "latex_body": "",
  "line": 144,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Proof II --- Effective-Signature (Geometric)",
  "ref_roles": [
    {
      "context": "",
      "label": "theorem:appC_dual_horizon_signature",
      "logical_support": false,
      "role": "navigation",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 78,
      "target_type": "theorem"
    }
  ],
  "role": "section",
  "subtype": "section",
  "type": "section"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [
    "assumption:appC_emergence_domination"
  ],
  "depends_on": [
    "assumption:appC_emergence_domination"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "proof:appC_dual_horizon_signature_geometric",
  "label": "proof:appC_dual_horizon_signature_geometric",
  "latex_body": "\\begin{proof}[Proof of Theorem~\\ref{theorem:appC_dual_horizon_signature} (geometric modality)]\n\\label{proof:appC_dual_horizon_signature_geometric}\n\\leavevmode\n\nAssume bounded reflexive emergence, \\(\\Delta\\Phi_{\\Obs}\\ge\\tau_E>0\\). The dual\nsignature ``\\(G_{\\Obs}(\\Omega)>0\\) and \\(C_{\\Obs}(\\Omega)>0\\)'' can fail in exactly\nthree ways; we eliminate each.\n\n\\textbf{Case A (no generative flux on \\(\\Omega\\)): \\(G_{\\Obs}(\\Omega)=0\\).} Then\n\\(\\min\\{G_{\\Obs},C_{\\Obs}\\}=0\\), and Emergence Domination\n(Assumption~\\ref{assumption:appC_emergence_domination}) gives\n\\(\\Delta\\Phi_{\\Obs}\\le \\Lambda\\cdot 0 = 0 < \\tau_E\\), contradicting emergence.\nSymbolically: Drift may be formally nonzero, yet it sources no observer-visible\nnovelty across the horizon --- transport below \\(\\epsilon_{\\Obs}\\), bare repetition,\nor collapse --- so no new structure arises to be retained.\n\n\\textbf{Case B (no stabilizing flux on \\(\\Omega\\)): \\(C_{\\Obs}(\\Omega)=0\\).} Again\n\\(\\min=0\\) and \\(\\Delta\\Phi_{\\Obs}\\le 0<\\tau_E\\), a contradiction. Symbolically:\nnovelty is generated but never contracted or integrated; symbolic free energy\n\\(\\freeenergy\\) is not stably reduced, and the differentiated content disperses below\nresolution before it can register as retained identity (\\(\\identity\\)). Generation\nwithout a sink is flux, not emergence.\n\n\\textbf{Case C (no shared domain).} Suppose instead that both signs occur somewhere\nin \\(\\manifold\\) --- \\((\\nabla\\!\\cdot\\drift)_+>0\\) on some region and\n\\((-\\nabla\\!\\cdot R_{\\mathrm{stab}})_+>0\\) on another --- but their observer-visible\nsupports do not both meet a common \\(\\Omega\\). Then on the domain over which \\(\\Obs\\)\nactually integrates emergence, at least one integrand vanishes\n\\(\\mu_{\\Obs}\\)-almost everywhere, so \\(G_{\\Obs}(\\Omega)=0\\) or\n\\(C_{\\Obs}(\\Omega)=0\\), returning us to Case A or B. Uncoupled generation and\nstabilization, however vigorous in separate observer patches, produce no reflexive\nemergence for \\(\\Obs\\).\n\nIn every case \\(\\Delta\\Phi_{\\Obs}<\\tau_E\\), contradicting the hypothesis. Hence both\nfluxes are strictly positive on a shared \\(\\Omega\\): the dual effective signature is\nnecessary.\n\\end{proof}",
  "line": 148,
  "macros_used": [
    "Obs",
    "drift",
    "freeenergy",
    "identity",
    "manifold"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Proof of Theorem~\\ref{theorem:appC_dual_horizon_signature} (geometric modality)",
  "proves": "theorem:appC_dual_horizon_signature",
  "ref_roles": [
    {
      "context": "lux on \\(\\Omega\\)): \\(G_{\\Obs}(\\Omega)=0\\).} Then \\(\\min\\{G_{\\Obs},C_{\\Obs}\\}=0\\), and Emergence Domination (Assumption~\\ref{assumption:appC_emergence_domination}) gives \\(\\Delta\\Phi_{\\Obs}\\le \\Lambda\\cdot 0 = 0 < \\tau_E\\), contradicting emergence. Symbolically: Drift may be formal",
      "label": "assumption:appC_emergence_domination",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 63,
      "target_type": "assumption"
    }
  ],
  "refs": [
    "assumption:appC_emergence_domination",
    "theorem:appC_dual_horizon_signature"
  ],
  "role": "proof",
  "type": "proof"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [
    "axiom:appC_psc3prime"
  ],
  "depends_on": [],
  "file": "appendix_dual_horizon.tex",
  "forward_ref_roles": [
    {
      "context": "",
      "label": "axiom:appC_psc3prime",
      "line_distance": 338,
      "role": "navigation",
      "target_line": 528,
      "target_type": "axiom"
    }
  ],
  "forward_refs": [
    "axiom:appC_psc3prime"
  ],
  "id": "subsec:appC_conclusion_of_proof_by_elimination",
  "label": "subsec:appC_conclusion_of_proof_by_elimination",
  "latex_body": "",
  "line": 190,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Sufficiency and the Conditional Biconditional",
  "ref_roles": [
    {
      "context": "",
      "label": "axiom:appC_psc3prime",
      "logical_support": false,
      "role": "forward_navigation",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 528,
      "target_type": "axiom"
    }
  ],
  "role": "section",
  "subtype": "section",
  "type": "section"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "proof:appC_dual_horizon_biconditional",
    "subsec:appC_methodological_logical_framework",
    "theorem:appC_dual_horizon_biconditional"
  ],
  "cites": [],
  "depends_on": [],
  "file": "appendix_dual_horizon.tex",
  "id": "assumption:appC_emergence_coupling",
  "label": "assumption:appC_emergence_coupling",
  "latex_body": "\\begin{assumption}[Emergence Coupling lower bound]\n\\label{assumption:appC_emergence_coupling}\nThere is a coupling gain \\(\\kappa=\\kappa(\\epsilon_{\\Obs})>0\\) such that, when both\nfluxes are present and interact on the shared domain \\(\\Omega\\),\n\\[\n\\Delta\\Phi_{\\Obs}(\\drift, R_{\\mathrm{stab}})\n\\;\\ge\\; \\kappa\\cdot\\min\\big\\{\\,G_{\\Obs}(\\Omega),\\, C_{\\Obs}(\\Omega)\\,\\big\\}.\n\\]\nNecessarily \\(\\kappa\\le\\Lambda\\), since both bounds hold simultaneously.\n\\end{assumption}",
  "line": 197,
  "macros_used": [
    "Obs",
    "drift"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Emergence Coupling lower bound",
  "proof_status": "definitional",
  "refs": [],
  "role": "assumption",
  "type": "assumption"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "scholium:appC_two_horizons_co_constitutive"
  ],
  "cites": [
    "assumption:appC_emergence_coupling",
    "assumption:appC_emergence_domination"
  ],
  "depends_on": [
    "assumption:appC_emergence_coupling",
    "assumption:appC_emergence_domination",
    "theorem:appC_dual_horizon_signature"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "theorem:appC_dual_horizon_biconditional",
  "label": "theorem:appC_dual_horizon_biconditional",
  "latex_body": "\\begin{theorem}[Emergence is sandwiched by the dual signature]\n\\label{theorem:appC_dual_horizon_biconditional}\nUnder Emergence Domination and Emergence Coupling\n(Assumptions~\\ref{assumption:appC_emergence_domination},~\\ref{assumption:appC_emergence_coupling}),\nwrite \\(m:=\\min\\{G_{\\Obs}(\\Omega),C_{\\Obs}(\\Omega)\\}\\). Then\n\\[\n\\kappa\\, m \\;\\le\\; \\Delta\\Phi_{\\Obs}(\\drift,R_{\\mathrm{stab}}) \\;\\le\\; \\Lambda\\, m .\n\\]\nConsequently:\n\\begin{enumerate}[label=(\\roman*)]\n\\item \\emph{(Sufficiency)} \\(m \\ge \\tau_E/\\kappa \\;\\Rightarrow\\; \\Delta\\Phi_{\\Obs}\\ge\\tau_E\\);\n\\item \\emph{(Necessity)} \\(\\Delta\\Phi_{\\Obs}\\ge\\tau_E \\;\\Rightarrow\\; m \\ge \\tau_E/\\Lambda > 0\\).\n\\end{enumerate}\nIn the tight-bookkeeping case \\(\\kappa=\\Lambda=:\\Gamma\\) the two collapse to an exact\nbiconditional, \\(\\;\\Delta\\Phi_{\\Obs}\\ge\\tau_E \\iff m\\ge\\tau_E/\\Gamma\\).\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": [
      "The full sandwich kappa*m <= deltaPhi <= Lambda*m, sufficiency, necessity, and the tight kappa=Lambda biconditional are all proved unconditionally from the DualHorizonBalance data."
    ],
    "record_ids": [
      "MAP-APPENDIX_DUAL_HORIZON-003"
    ],
    "statuses": [
      "exact"
    ],
    "witnesses": [
      "AppendixDH.dualHorizon_necessity",
      "AppendixDH.dualHorizon_necessity_pos",
      "AppendixDH.dualHorizon_sufficiency",
      "AppendixDH.dualHorizon_tight_biconditional"
    ]
  },
  "line": 208,
  "macros_used": [
    "Obs",
    "drift"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Emergence is sandwiched by the dual signature",
  "proof_labels": [
    "proof:appC_dual_horizon_biconditional"
  ],
  "proof_status": "proven",
  "ref_roles": [
    {
      "context": "conditional} Under Emergence Domination and Emergence Coupling (Assumptions~\\ref{assumption:appC_emergence_domination},~\\ref{assumption:appC_emergence_coupling}), write \\(m:=\\min\\{G_{\\Obs}(\\Omega),C_{\\Obs}(\\Omega)\\}\\). Then \\[ \\kappa\\, m \\;\\le\\; \\Delta\\Phi_{\\Obs}(\\drift,R_{\\mathr",
      "label": "assumption:appC_emergence_coupling",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 197,
      "target_type": "assumption"
    },
    {
      "context": "gnature] \\label{theorem:appC_dual_horizon_biconditional} Under Emergence Domination and Emergence Coupling (Assumptions~\\ref{assumption:appC_emergence_domination},~\\ref{assumption:appC_emergence_coupling}), write \\(m:=\\min\\{G_{\\Obs}(\\Omega),C_{\\Obs}(\\Omega)\\}\\). Then \\[ \\kappa\\, m",
      "label": "assumption:appC_emergence_domination",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 63,
      "target_type": "assumption"
    }
  ],
  "refs": [
    "assumption:appC_emergence_coupling",
    "assumption:appC_emergence_domination"
  ],
  "role": "theorem",
  "type": "theorem"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [
    "assumption:appC_emergence_coupling",
    "assumption:appC_emergence_domination",
    "theorem:appC_dual_horizon_signature"
  ],
  "depends_on": [
    "assumption:appC_emergence_coupling",
    "assumption:appC_emergence_domination",
    "theorem:appC_dual_horizon_signature"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "proof:appC_dual_horizon_biconditional",
  "label": "proof:appC_dual_horizon_biconditional",
  "latex_body": "\\begin{proof}\n\\label{proof:appC_dual_horizon_biconditional}\nThe sandwich is the conjunction of\nAssumptions~\\ref{assumption:appC_emergence_domination}\nand~\\ref{assumption:appC_emergence_coupling}. For (i),\n\\(\\Delta\\Phi_{\\Obs}\\ge\\kappa m\\ge\\kappa\\cdot(\\tau_E/\\kappa)=\\tau_E\\). For (ii),\n\\(\\tau_E\\le\\Delta\\Phi_{\\Obs}\\le\\Lambda m\\) gives \\(m\\ge\\tau_E/\\Lambda>0\\); positivity\nof \\(m\\) recovers Theorem~\\ref{theorem:appC_dual_horizon_signature}. When\n\\(\\kappa=\\Lambda=\\Gamma\\) the lower and upper thresholds coincide at\n\\(\\tau_E/\\Gamma\\), yielding the biconditional.\n\\end{proof}",
  "line": 224,
  "macros_used": [
    "Obs"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "",
  "proves": "theorem:appC_dual_horizon_biconditional",
  "ref_roles": [
    {
      "context": "al_horizon_biconditional} The sandwich is the conjunction of Assumptions~\\ref{assumption:appC_emergence_domination} and~\\ref{assumption:appC_emergence_coupling}. For (i), \\(\\Delta\\Phi_{\\Obs}\\ge\\kappa m\\ge\\kappa\\cdot(\\tau_E/\\kappa)=\\tau_E\\). For (ii), \\(\\tau_E\\le\\Delta\\Phi_{\\Obs}\\",
      "label": "assumption:appC_emergence_coupling",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 197,
      "target_type": "assumption"
    },
    {
      "context": "\\begin{proof} \\label{proof:appC_dual_horizon_biconditional} The sandwich is the conjunction of Assumptions~\\ref{assumption:appC_emergence_domination} and~\\ref{assumption:appC_emergence_coupling}. For (i), \\(\\Delta\\Phi_{\\Obs}\\ge\\kappa m\\ge\\kappa\\cdot(\\tau_E/\\kappa)=\\tau",
      "label": "assumption:appC_emergence_domination",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 63,
      "target_type": "assumption"
    },
    {
      "context": "r (ii), \\(\\tau_E\\le\\Delta\\Phi_{\\Obs}\\le\\Lambda m\\) gives \\(m\\ge\\tau_E/\\Lambda>0\\); positivity of \\(m\\) recovers Theorem~\\ref{theorem:appC_dual_horizon_signature}. When \\(\\kappa=\\Lambda=\\Gamma\\) the lower and upper thresholds coincide at \\(\\tau_E/\\Gamma\\), yielding the biconditiona",
      "label": "theorem:appC_dual_horizon_signature",
      "logical_support": true,
      "role": "proof_support",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 78,
      "target_type": "theorem"
    }
  ],
  "refs": [
    "assumption:appC_emergence_coupling",
    "assumption:appC_emergence_domination",
    "theorem:appC_dual_horizon_signature"
  ],
  "role": "proof",
  "type": "proof"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [
    "definition:appC_horizon_fluxes",
    "theorem:appC_dual_horizon_signature"
  ],
  "depends_on": [
    "definition:appC_horizon_fluxes",
    "theorem:appC_dual_horizon_signature"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "remark:appC_horizon_realizations",
  "label": "remark:appC_horizon_realizations",
  "latex_body": "\\begin{remark}[Invariance under horizon realization]\n\\label{remark:appC_horizon_realizations}\nBoth fluxes are integrals of positive parts of divergences against \\(\\mu_{\\Obs}\\);\nnothing in Definition~\\ref{definition:appC_horizon_fluxes} or\nTheorem~\\ref{theorem:appC_dual_horizon_signature} counts horizons. The same\nsignature \\((G_{\\Obs}>0,\\,C_{\\Obs}>0)\\) is produced by (i) a single\ngenerative/dissipative horizon pair; (ii) several same-sign horizons, whose positive\nparts simply add; (iii) one sign-changing curvature field, whose positive and\nnegative divergence parts feed \\(G_{\\Obs}\\) and \\(C_{\\Obs}\\) respectively; (iv) a\nsmooth, delocalized source--sink field with no isolated horizon at all. The theorem\ntherefore does not fail on multi-horizon or sign-changing configurations --- the\nliability of the literal reading --- because ``dual'' is a property of the\nobserver-visible flux signature, not of the geometry that realizes it.\n\\end{remark}",
  "line": 236,
  "macros_used": [
    "Obs"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Invariance under horizon realization",
  "ref_roles": [
    {
      "context": "_realizations} Both fluxes are integrals of positive parts of divergences against \\(\\mu_{\\Obs}\\); nothing in Definition~\\ref{definition:appC_horizon_fluxes} or Theorem~\\ref{theorem:appC_dual_horizon_signature} counts horizons. The same signature \\((G_{\\Obs}>0,\\,C_{\\Obs}>0)\\)",
      "label": "definition:appC_horizon_fluxes",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 27,
      "target_type": "definition"
    },
    {
      "context": "tive parts of divergences against \\(\\mu_{\\Obs}\\); nothing in Definition~\\ref{definition:appC_horizon_fluxes} or Theorem~\\ref{theorem:appC_dual_horizon_signature} counts horizons. The same signature \\((G_{\\Obs}>0,\\,C_{\\Obs}>0)\\) is produced by (i) a single generative/dissipative ho",
      "label": "theorem:appC_dual_horizon_signature",
      "logical_support": true,
      "role": "formal_dependency",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 78,
      "target_type": "theorem"
    }
  ],
  "refs": [
    "definition:appC_horizon_fluxes",
    "theorem:appC_dual_horizon_signature"
  ],
  "role": "remark",
  "type": "remark"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "scholium:appC_two_modalities_one_root",
    "subsec:appC_methodological_logical_framework"
  ],
  "cites": [
    "assumption:appC_emergence_domination",
    "axiom:appC_psc3prime",
    "definition:bk4_observer_kernel_convolution_map"
  ],
  "depends_on": [
    "assumption:appC_emergence_domination",
    "definition:bk4_observer_kernel_convolution_map"
  ],
  "file": "appendix_dual_horizon.tex",
  "forward_ref_roles": [
    {
      "context": "e of the observer, not in the definition of emergence --- the same status, and the same debt, as PS--C3\\(^\\prime\\) (Ax.~\\ref{axiom:appC_psc3prime}). Proof~I incurs no such debt: it reaches the same conclusion from finite resolution \\(\\epsilon_{\\Obs}\\) directly, whic",
      "label": "axiom:appC_psc3prime",
      "line_distance": 277,
      "role": "proof_below",
      "target_line": 528,
      "target_type": "axiom"
    }
  ],
  "forward_refs": [
    "axiom:appC_psc3prime"
  ],
  "id": "remark:appC_domination_open_route",
  "label": "remark:appC_domination_open_route",
  "latex_body": "\\begin{remark}[Open derivation route for Emergence Domination]\n\\label{remark:appC_domination_open_route}\nEmergence Domination (Assumption~\\ref{assumption:appC_emergence_domination}) is the\nsingle posited plank of Proof~II, and it is where any residual circularity would\nhide: were \\(\\Delta\\Phi_{\\Obs}\\), \\(G_{\\Obs}\\), \\(C_{\\Obs}\\) not independently\nmeasured, the bound would be analytic and the theorem would prove only what it\nassumed. The route that would make it synthetic runs through \\emph{finite observer\nbandwidth}: the bounded-observer kernel\n(cf.~\\ref{definition:bk4_observer_kernel_convolution_map}) has finite throughput\nacross the resolution boundary \\(\\partial\\Omega\\), so it cannot retain coherent\nnovelty faster than the binding flux carries it across the horizon --- which is exactly\n\\(\\Delta\\Phi_{\\Obs}\\le\\Lambda\\min\\{G_{\\Obs},C_{\\Obs}\\}\\). We record this as open.\nUntil it is discharged, Domination stands as a labelled premise grounded in the\nfinitude of the observer, not in the definition of emergence --- the same status, and\nthe same debt, as PS--C3\\(^\\prime\\) (Ax.~\\ref{axiom:appC_psc3prime}). Proof~I incurs no\nsuch debt: it reaches the same conclusion from finite resolution \\(\\epsilon_{\\Obs}\\)\ndirectly, which is why the two proofs are worth keeping side by side.\n\\end{remark}",
  "line": 251,
  "macros_used": [
    "Obs"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Open derivation route for Emergence Domination",
  "ref_roles": [
    {
      "context": "n derivation route for Emergence Domination] \\label{remark:appC_domination_open_route} Emergence Domination (Assumption~\\ref{assumption:appC_emergence_domination}) is the single posited plank of Proof~II, and it is where any residual circularity would hide: were \\(\\Delta\\Phi_{\\Obs}",
      "label": "assumption:appC_emergence_domination",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 63,
      "target_type": "assumption"
    },
    {
      "context": "e of the observer, not in the definition of emergence --- the same status, and the same debt, as PS--C3\\(^\\prime\\) (Ax.~\\ref{axiom:appC_psc3prime}). Proof~I incurs no such debt: it reaches the same conclusion from finite resolution \\(\\epsilon_{\\Obs}\\) directly, whic",
      "label": "axiom:appC_psc3prime",
      "logical_support": false,
      "role": "forward_proof_below",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 528,
      "target_type": "axiom"
    },
    {
      "context": "The route that would make it synthetic runs through \\emph{finite observer bandwidth}: the bounded-observer kernel (cf.~\\ref{definition:bk4_observer_kernel_convolution_map}) has finite throughput across the resolution boundary \\(\\partial\\Omega\\), so it cannot retain coherent novelty faster t",
      "label": "definition:bk4_observer_kernel_convolution_map",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book4.tex",
      "target_line": 143,
      "target_type": "definition"
    }
  ],
  "refs": [
    "assumption:appC_emergence_domination",
    "axiom:appC_psc3prime",
    "definition:bk4_observer_kernel_convolution_map"
  ],
  "role": "remark",
  "type": "remark"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "sec:appC_dual_horizon"
  ],
  "cites": [
    "remark:appC_domination_open_route",
    "sec:appC_proof_by_elimination",
    "sec:appC_proof_observational",
    "theorem:appC_modal_transference"
  ],
  "depends_on": [
    "remark:appC_domination_open_route"
  ],
  "file": "appendix_dual_horizon.tex",
  "forward_ref_roles": [
    {
      "context": "in two carriers, the observational and the geometric, and their agreement is precisely a \\emph{transference test} (Thm.~\\ref{theorem:appC_modal_transference}) of the Dual Horizon necessity against its own mode of presentation. That the invariant survives the carrier swap is th",
      "label": "theorem:appC_modal_transference",
      "line_distance": 1251,
      "role": "downstream_application",
      "target_line": 1521,
      "target_type": "theorem"
    }
  ],
  "forward_refs": [
    "theorem:appC_modal_transference"
  ],
  "id": "scholium:appC_two_modalities_one_root",
  "label": "scholium:appC_two_modalities_one_root",
  "latex_body": "\\begin{scholium}[Two Modalities, One Root]\n\\label{scholium:appC_two_modalities_one_root}\nThe necessity has now been proved twice: observationally\n(\\S\\ref{sec:appC_proof_observational}, by what a bounded observer can register and\nretain) and geometrically (\\S\\ref{sec:appC_proof_by_elimination}, by the flux\nsignature on the manifold). These are not independent confirmations. Both proofs\nfinally rest on the same fact --- the finitude of the observer: Proof~I on finite\nresolution \\(\\epsilon_{\\Obs}\\), Proof~II on finite bandwidth across \\(\\partial\\Omega\\)\n(Remark~\\ref{remark:appC_domination_open_route}). They are therefore two\n\\emph{presentations} of one invariant in two carriers, the observational and the\ngeometric, and their agreement is precisely a \\emph{transference test}\n(Thm.~\\ref{theorem:appC_modal_transference}) of the Dual Horizon necessity against its\nown mode of presentation. That the invariant survives the carrier swap is the\nappendix's strongest internal evidence that the dual signature belongs to the symbolic\nstructure and not to either proof's framing. The earlier metaphysical trilemma ---\n``solely generative / solely dissipative / neither'' --- is the degenerate, prose-bound\nancestor of Proof~I, recovered as the corners \\(C_{\\Obs}=0\\), \\(G_{\\Obs}=0\\),\n\\(G_{\\Obs}=C_{\\Obs}=0\\); its rehabilitation as Proof~I now carries Case~C, which the\nmetaphysical reading missed.\n\\end{scholium}",
  "line": 270,
  "macros_used": [
    "Obs"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Two Modalities, One Root",
  "ref_roles": [
    {
      "context": "erver: Proof~I on finite resolution \\(\\epsilon_{\\Obs}\\), Proof~II on finite bandwidth across \\(\\partial\\Omega\\) (Remark~\\ref{remark:appC_domination_open_route}). They are therefore two \\emph{presentations} of one invariant in two carriers, the observational and the geometric, an",
      "label": "remark:appC_domination_open_route",
      "logical_support": true,
      "role": "application",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 251,
      "target_type": "remark"
    },
    {
      "context": "ionally (\\S\\ref{sec:appC_proof_observational}, by what a bounded observer can register and retain) and geometrically (\\S\\ref{sec:appC_proof_by_elimination}, by the flux signature on the manifold). These are not independent confirmations. Both proofs finally rest on the same",
      "label": "sec:appC_proof_by_elimination",
      "logical_support": false,
      "role": "navigation",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 144,
      "target_type": "section"
    },
    {
      "context": "es, One Root] \\label{scholium:appC_two_modalities_one_root} The necessity has now been proved twice: observationally (\\S\\ref{sec:appC_proof_observational}, by what a bounded observer can register and retain) and geometrically (\\S\\ref{sec:appC_proof_by_elimination}, by the f",
      "label": "sec:appC_proof_observational",
      "logical_support": false,
      "role": "navigation",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 99,
      "target_type": "section"
    },
    {
      "context": "in two carriers, the observational and the geometric, and their agreement is precisely a \\emph{transference test} (Thm.~\\ref{theorem:appC_modal_transference}) of the Dual Horizon necessity against its own mode of presentation. That the invariant survives the carrier swap is th",
      "label": "theorem:appC_modal_transference",
      "logical_support": false,
      "role": "forward_downstream_application",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 1521,
      "target_type": "theorem"
    }
  ],
  "refs": [
    "remark:appC_domination_open_route",
    "sec:appC_proof_by_elimination",
    "sec:appC_proof_observational",
    "theorem:appC_modal_transference"
  ],
  "role": "scholium",
  "type": "scholium"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "scholium:appC_symbolic_geometric_equivalence"
  ],
  "cites": [
    "definition:bk1_drift_field",
    "definition:bk7_symbolic_reflexive_validation_srv",
    "theorem:appC_dual_horizon_biconditional"
  ],
  "depends_on": [
    "definition:bk1_drift_field",
    "definition:bk7_symbolic_reflexive_validation_srv",
    "theorem:appC_dual_horizon_biconditional"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "scholium:appC_two_horizons_co_constitutive",
  "label": "scholium:appC_two_horizons_co_constitutive",
  "latex_body": "\\begin{scholium}[The Two Horizons as Co-Constitutive]\n\\label{scholium:appC_two_horizons_co_constitutive}\nCo-constitution is now a theorem about a bound, not a metaphor. Because the emergence\nfunctional is sandwiched between \\(\\kappa\\) and \\(\\Lambda\\) times\n\\(\\min\\{G_{\\Obs},C_{\\Obs}\\}\\) (Theorem~\\ref{theorem:appC_dual_horizon_biconditional}),\nthe binding term is the \\emph{smaller} of the two fluxes: neither generation nor\nstabilization can carry observer-visible becoming alone, and they constrain emergence\nsymmetrically and inseparably. Drift (cf.~\\ref{definition:bk1_drift_field}) supplies\nthe novelty that Reflection retains; Reflection supplies the contraction that turns\nnovelty into structure. Their coupling on a shared bounded-observer domain --- formally\nenacted as Symbolic Reflexive Validation\n(cf.~\\ref{definition:bk7_symbolic_reflexive_validation_srv}) --- is the crucible of\nsymbolic existence and becoming. The dual horizon is not two objects in the world but the two-signed\nsignature any world must present to a Bounded Observer in order to be seen to emerge at\nall.\n\\end{scholium}",
  "line": 291,
  "macros_used": [
    "Obs"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "The Two Horizons as Co-Constitutive",
  "ref_roles": [
    {
      "context": "ation can carry observer-visible becoming alone, and they constrain emergence symmetrically and inseparably. Drift (cf.~\\ref{definition:bk1_drift_field}) supplies the novelty that Reflection retains; Reflection supplies the contraction that turns novelty into structure. T",
      "label": "definition:bk1_drift_field",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 1198,
      "target_type": "definition"
    },
    {
      "context": "tructure. Their coupling on a shared bounded-observer domain --- formally enacted as Symbolic Reflexive Validation (cf.~\\ref{definition:bk7_symbolic_reflexive_validation_srv}) --- is the crucible of symbolic existence and becoming. The dual horizon is not two objects in the world but the two-s",
      "label": "definition:bk7_symbolic_reflexive_validation_srv",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book7.tex",
      "target_line": 1441,
      "target_type": "definition"
    },
    {
      "context": "the emergence functional is sandwiched between \\(\\kappa\\) and \\(\\Lambda\\) times \\(\\min\\{G_{\\Obs},C_{\\Obs}\\}\\) (Theorem~\\ref{theorem:appC_dual_horizon_biconditional}), the binding term is the \\emph{smaller} of the two fluxes: neither generation nor stabilization can carry observer-vis",
      "label": "theorem:appC_dual_horizon_biconditional",
      "logical_support": true,
      "role": "formal_dependency",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 208,
      "target_type": "theorem"
    }
  ],
  "refs": [
    "definition:bk1_drift_field",
    "definition:bk7_symbolic_reflexive_validation_srv",
    "theorem:appC_dual_horizon_biconditional"
  ],
  "role": "scholium",
  "type": "scholium"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "subsec:appC_methodological_logical_framework"
  ],
  "cites": [
    "definition:bk1_bounded_observer"
  ],
  "depends_on": [
    "definition:bk1_bounded_observer"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "sec:appC_born_rule",
  "label": "sec:appC_born_rule",
  "latex_body": "",
  "line": 308,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Born Rule – A Formal Derivation",
  "ref_roles": [
    {
      "context": "",
      "label": "definition:bk1_bounded_observer",
      "logical_support": false,
      "role": "navigation",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 27,
      "target_type": "definition"
    }
  ],
  "role": "section",
  "subtype": "section",
  "type": "section"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [
    "axiom:appC_psc3prime",
    "definition:bk1_bounded_observer",
    "subsec:appC_born_additivity_derivation",
    "subsec:appC_born_axioms",
    "theorem:appC_orthogonal_additivity"
  ],
  "depends_on": [
    "definition:bk1_bounded_observer"
  ],
  "file": "appendix_dual_horizon.tex",
  "forward_ref_roles": [
    {
      "context": "server-token disjointness, while its cross-frame content---non-contextuality---is isolated and posited as PS-C3$'$ (Ax.~\\ref{axiom:appC_psc3prime}). The derivation thus reduces Gleason's additivity hypothesis to finite-budget bookkeeping plus a single, explicitly la",
      "label": "axiom:appC_psc3prime",
      "line_distance": 216,
      "role": "teaser",
      "target_line": 528,
      "target_type": "axiom"
    },
    {
      "context": "ly satisfies. The additivity once carried as PS-C3 splits in two: its \\emph{within-frame} content is \\emph{proved} in \\S\\ref{subsec:appC_born_additivity_derivation} (Thm.~\\ref{theorem:appC_orthogonal_additivity}) from observer-token disjointness, while its cross-frame content---non-c",
      "label": "subsec:appC_born_additivity_derivation",
      "line_distance": 97,
      "role": "navigation",
      "target_line": 409,
      "target_type": "section"
    },
    {
      "context": "tructure] \\label{remark:appC_born_rule_dependency} This derivation proceeds from the coherence constraints PS-C1--C5 (\\S\\ref{subsec:appC_born_axioms}) to Gleason's hypotheses, and thence to the Born Rule. The structural constraints PS-C1, PS-C2, PS-C4, PS-C5 are conseq",
      "label": "subsec:appC_born_axioms",
      "line_distance": 260,
      "role": "navigation",
      "target_line": 572,
      "target_type": "section"
    },
    {
      "context": "splits in two: its \\emph{within-frame} content is \\emph{proved} in \\S\\ref{subsec:appC_born_additivity_derivation} (Thm.~\\ref{theorem:appC_orthogonal_additivity}) from observer-token disjointness, while its cross-frame content---non-contextuality---is isolated and posited as PS-C3",
      "label": "theorem:appC_orthogonal_additivity",
      "line_distance": 192,
      "role": "teaser",
      "target_line": 504,
      "target_type": "theorem"
    }
  ],
  "forward_refs": [
    "axiom:appC_psc3prime",
    "subsec:appC_born_additivity_derivation",
    "subsec:appC_born_axioms",
    "theorem:appC_orthogonal_additivity"
  ],
  "id": "remark:appC_born_rule_dependency",
  "label": "remark:appC_born_rule_dependency",
  "latex_body": "\\begin{remark}[Derivation Structure]\n\\label{remark:appC_born_rule_dependency}\nThis derivation proceeds from the coherence constraints PS-C1--C5\n(\\S\\ref{subsec:appC_born_axioms}) to Gleason's hypotheses, and thence to\nthe Born Rule. The structural constraints PS-C1, PS-C2, PS-C4, PS-C5 are\nconsequences of bounded observation (Def.~\\ref{definition:bk1_bounded_observer}),\nnot ad hoc quantum postulates: each encodes a constraint that any\nfinite-resolution observer necessarily satisfies. The additivity once carried as\nPS-C3 splits in two: its \\emph{within-frame} content is \\emph{proved} in\n\\S\\ref{subsec:appC_born_additivity_derivation}\n(Thm.~\\ref{theorem:appC_orthogonal_additivity}) from observer-token disjointness,\nwhile its cross-frame content---non-contextuality---is isolated and posited as\nPS-C3$'$ (Ax.~\\ref{axiom:appC_psc3prime}). The derivation thus reduces Gleason's\nadditivity hypothesis to finite-budget bookkeeping plus a single, explicitly\nlabelled non-contextuality axiom, and is grounded in the PS foundational framework\nrather than in the Hilbert space structure it explains; the Born conclusion is\nconditional on PS-C3$'$.\n\\end{remark}",
  "lean_alignment": {
    "conditions": [
      "The remark correctly exposes PS-C3-prime, but its broader assertion that the other PS-C constraints follow from bounded observation is a human mathematical claim not certified by the current Lean companion."
    ],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": false,
    "notes": [
      "The remark correctly exposes PS-C3-prime, but its broader assertion that the other PS-C constraints follow from bounded observation is a human mathematical claim not certified by the current Lean companion."
    ],
    "record_ids": [
      "REVIEW-001"
    ],
    "statuses": [
      "conditional"
    ],
    "witnesses": []
  },
  "line": 312,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Derivation Structure",
  "ref_roles": [
    {
      "context": "server-token disjointness, while its cross-frame content---non-contextuality---is isolated and posited as PS-C3$'$ (Ax.~\\ref{axiom:appC_psc3prime}). The derivation thus reduces Gleason's additivity hypothesis to finite-budget bookkeeping plus a single, explicitly la",
      "label": "axiom:appC_psc3prime",
      "logical_support": false,
      "role": "forward_teaser",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 528,
      "target_type": "axiom"
    },
    {
      "context": "e to the Born Rule. The structural constraints PS-C1, PS-C2, PS-C4, PS-C5 are consequences of bounded observation (Def.~\\ref{definition:bk1_bounded_observer}), not ad hoc quantum postulates: each encodes a constraint that any finite-resolution observer necessarily satisfies. T",
      "label": "definition:bk1_bounded_observer",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 27,
      "target_type": "definition"
    },
    {
      "context": "ly satisfies. The additivity once carried as PS-C3 splits in two: its \\emph{within-frame} content is \\emph{proved} in \\S\\ref{subsec:appC_born_additivity_derivation} (Thm.~\\ref{theorem:appC_orthogonal_additivity}) from observer-token disjointness, while its cross-frame content---non-c",
      "label": "subsec:appC_born_additivity_derivation",
      "logical_support": false,
      "role": "forward_navigation",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 409,
      "target_type": "section"
    },
    {
      "context": "tructure] \\label{remark:appC_born_rule_dependency} This derivation proceeds from the coherence constraints PS-C1--C5 (\\S\\ref{subsec:appC_born_axioms}) to Gleason's hypotheses, and thence to the Born Rule. The structural constraints PS-C1, PS-C2, PS-C4, PS-C5 are conseq",
      "label": "subsec:appC_born_axioms",
      "logical_support": false,
      "role": "forward_navigation",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 572,
      "target_type": "section"
    },
    {
      "context": "splits in two: its \\emph{within-frame} content is \\emph{proved} in \\S\\ref{subsec:appC_born_additivity_derivation} (Thm.~\\ref{theorem:appC_orthogonal_additivity}) from observer-token disjointness, while its cross-frame content---non-contextuality---is isolated and posited as PS-C3",
      "label": "theorem:appC_orthogonal_additivity",
      "logical_support": false,
      "role": "forward_teaser",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 504,
      "target_type": "theorem"
    }
  ],
  "refs": [
    "axiom:appC_psc3prime",
    "definition:bk1_bounded_observer",
    "subsec:appC_born_additivity_derivation",
    "subsec:appC_born_axioms",
    "theorem:appC_orthogonal_additivity"
  ],
  "role": "remark",
  "type": "remark"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [
    "definition:bk1_bounded_observer",
    "definition:bk6_symbolic_curvature_tensor"
  ],
  "depends_on": [
    "definition:bk1_bounded_observer",
    "definition:bk6_symbolic_curvature_tensor"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "sec:appC_born_preamble",
  "label": "sec:appC_born_preamble",
  "latex_body": "",
  "line": 331,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Preamble",
  "ref_roles": [
    {
      "context": "",
      "label": "definition:bk1_bounded_observer",
      "logical_support": false,
      "role": "navigation",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 27,
      "target_type": "definition"
    },
    {
      "context": "",
      "label": "definition:bk6_symbolic_curvature_tensor",
      "logical_support": false,
      "role": "navigation",
      "target_file": "book6.tex",
      "target_line": 16,
      "target_type": "definition"
    }
  ],
  "role": "section",
  "subtype": "subsection",
  "type": "section"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "scholium:bk4_emergence_of_classical_calculus"
  ],
  "cites": [
    "definition:bk1_bounded_observer"
  ],
  "depends_on": [
    "definition:bk1_bounded_observer"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "subsec:appC_born_observer_structures",
  "label": "subsec:appC_born_observer_structures",
  "latex_body": "",
  "line": 340,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Observer Data Structures in the Quantum Regime",
  "ref_roles": [
    {
      "context": "",
      "label": "definition:bk1_bounded_observer",
      "logical_support": false,
      "role": "navigation",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 27,
      "target_type": "definition"
    }
  ],
  "role": "section",
  "subtype": "subsection",
  "type": "section"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "definition:appC_observer_token_space"
  ],
  "cites": [
    "definition:bk4_bounded_observer"
  ],
  "depends_on": [
    "definition:bk4_bounded_observer"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "definition:appC_frame_space",
  "label": "definition:appC_frame_space",
  "latex_body": "\\begin{definition}[Frame space of $\\Obs$]\n\\label{definition:appC_frame_space}\nFor a bounded observer $\\Obs$ (cf.~\\ref{definition:bk4_bounded_observer}), define\n\\[\nF_{Obs} \\subseteq Proj(\\Horizon)\n\\]\nas the \\emph{frame space}: the maximal set of mutually orthogonal projections\nwhose outcomes are classically discernible given the observer’s resolution threshold\n$\\epsilon_{\\Obs}$.\n\\end{definition}",
  "line": 350,
  "macros_used": [
    "Horizon",
    "Obs"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Frame space of $\\Obs$",
  "proof_status": "definitional",
  "ref_roles": [
    {
      "context": "\\begin{definition}[Frame space of $\\Obs$] \\label{definition:appC_frame_space} For a bounded observer $\\Obs$ (cf.~\\ref{definition:bk4_bounded_observer}), define \\[ F_{Obs} \\subseteq Proj(\\Horizon) \\] as the \\emph{frame space}: the maximal set of mutually orthogonal proje",
      "label": "definition:bk4_bounded_observer",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "book4.tex",
      "target_line": 427,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:bk4_bounded_observer"
  ],
  "role": "definition",
  "type": "definition"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "axiom:appC_psc1",
    "axiom:appC_psc2",
    "axiom:appC_psc3",
    "axiom:appC_psc4",
    "axiom:appC_psc5",
    "definition:appC_observer_coherence_budget",
    "subsec:appC_born_axioms"
  ],
  "cites": [
    "definition:bk1_bounded_observer"
  ],
  "depends_on": [
    "definition:bk1_bounded_observer"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "definition:appC_coherence_functional",
  "label": "definition:appC_coherence_functional",
  "latex_body": "\\begin{definition}[Coherence functional]\n\\label{definition:appC_coherence_functional}\nFor a Bounded Observer $\\Obs$ (cf.~\\ref{definition:bk1_bounded_observer}), the \\emph{coherence assignment functional} is\n\\[\n\\mathcal{C}_{Obs}: Proj(\\Horizon) \\times \\Horizon \\to [0,1], \\quad\n(\\Pi, \\psi) \\mapsto \\mathcal{C}_{\\Obs}(\\tilde\\psi_{\\Obs}, \\Pi),\n\\]\nwhere $\\tilde\\psi_{\\Obs}$ is the observer’s internal (fuzzy) representation\nof the external state $\\psi \\in \\Horizon$.\n\\end{definition}",
  "line": 361,
  "macros_used": [
    "Horizon",
    "Obs"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Coherence functional",
  "proof_status": "definitional",
  "ref_roles": [
    {
      "context": "begin{definition}[Coherence functional] \\label{definition:appC_coherence_functional} For a Bounded Observer $\\Obs$ (cf.~\\ref{definition:bk1_bounded_observer}), the \\emph{coherence assignment functional} is \\[ \\mathcal{C}_{Obs}: Proj(\\Horizon) \\times \\Horizon \\to [0,1], \\quad (",
      "label": "definition:bk1_bounded_observer",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "scholium_symbolicum.tex",
      "target_line": 27,
      "target_type": "definition"
    }
  ],
  "refs": [
    "definition:bk1_bounded_observer"
  ],
  "role": "definition",
  "type": "definition"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [],
  "depends_on": [],
  "file": "appendix_dual_horizon.tex",
  "id": "remark:appC_observer_lowering_boundary",
  "label": "remark:appC_observer_lowering_boundary",
  "latex_body": "\\begin{remark}[Formal correspondence at the observer boundary]\n\\label{remark:appC_observer_lowering_boundary}\nThe machine-checked companion supplies two complementary Gleason-facing\nhalf-bridges, separated by an observer boundary.  In the source-to-readout direction,\na normalized pure-state vector determines its Hermitian rank-one density and lowers\nthrough a fixed observer kernel to a Born-compatible resolved readout.  In the\nreadout-to-representation direction, explicitly certified conjugate-linear, linear,\nand Hermitian cross laws construct a sesquilinear representation of the available\nvalues.  The second construction represents the readout; it is not an inverse that\nrecovers the originating vector or process state.\n\nThe seam is genuinely lossy.  Global phase is forgotten, so distinct normalized\nvectors can yield the same density and the same fixed-kernel observer record.\nExplicit counterexamples further show that arbitrary coherent frame readouts and\narbitrary normalized resolution records need not determine an upstream Hermitian\nstate.  Finite partial trace provides another exact lowering: it preserves trace and\nall represented local-observer expectations while discarding access to the full joint\noperator.\n\nTemporal direction is already present in the companion's Cost of Cacophony backbone.\nSimultaneous finite-support compression obeys the certified norm-fracture bounds, and\nthe diagonal witness has a strictly positive representability gap.  A staged path is\ninstead accounted for as an ordered sum of per-step displacements; its transport cost\nis paid by free-energy decrease in the certified JKO step.  Under the stated\nsummability, completeness, or Lyapunov-descent premises, those directed stages\nconverge.  Thus time is not merely a metaphor here: it is the parameter by which one\nsimultaneous obstruction is re-expressed as sequential transport with an explicit cost\nand convergence contract.\n\nWhat remains functionally interpretive is the physical specialization: mapping quantum decoherence\nand noise as the continued unfolding of this general directed cost-and-loss geometry.\nThe exact temporal transport results, exact partial-trace reduction, and exact\nphase-collision boundary ground that operational, testable reading without collapsing the mapped domains into one another.\nThis status distinction neither rejects the human mathematical argument under\nPS--C1--PS--C6 nor reduces its observer interpretation to the finite Lean model.\n\\end{remark}",
  "lean_alignment": {
    "conditions": [
      "Explicit conjugate-linear/linear Hermitian cross laws, or a retained reduced-state matrix certified Hermitian.",
      "Summable per-step displacement bounds and completeness, or a nonnegative potential with positive linear descent control."
    ],
    "countermodels": [
      "Book7QuantumGleason.completeFrameCoherence_does_not_supply_hermitian_certificate",
      "Book7QuantumGleason.quantumResolution_does_not_force_reducedState_isHermitian",
      "Book7QuantumGleason.quantumResolution_without_matrixHermiticity_does_not_supply_certificate"
    ],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "Convergence is certified under explicit preservation/descent contracts, not inferred from staging alone.",
      "First of two complementary Gleason-facing half-bridges. The construction is forward and preserves upstream Hermiticity without strengthening the observer certificate.",
      "Second complementary Gleason-facing half-bridge. It represents the certified observer-level values and is not an inverse recovering the originating source.",
      "The failure is information loss across the observer boundary, not a missing certificate field.",
      "The implication is formally false, not awaiting proof.",
      "The physical quantum specialization is functionally interpretive: an operational, testable map rather than a kernel identity. The general temporal cost-and-transport arrow, partial-trace reduction, and phase-collision boundary are exact or explicitly conditional.",
      "This is an exact reduction/regrouping theorem, not a certified temporal channel or distinguishability monotonicity law.",
      "This is the Cost of Cacophony-facing geometric obstruction: compression regime and support geometry determine a certified cost boundary.",
      "This is the proved non-injectivity of observer lowering.",
      "Time supplies an ordered transport coordinate with explicit accumulated cost; this is not merely literary temporal language."
    ],
    "record_ids": [
      "C-COMPRESSION-13",
      "C-CONVERGENCE-15",
      "C-STAGING-14",
      "Q-DECOHERENCE-12",
      "Q-FRAME-03",
      "Q-HERMITIAN-05",
      "Q-LOWER-01",
      "Q-PARTIAL-11",
      "Q-PHASE-02",
      "Q-RESOLVE-04"
    ],
    "statuses": [
      "conditional",
      "constructed",
      "exact",
      "interpretive",
      "refuted"
    ],
    "witnesses": [
      "Book4QuantumMeasurement.jointExpectation_local_eq_reduced",
      "Book4QuantumMeasurement.trace_partialTraceEnvironment",
      "Book5.axisCostOn_le_card_rpow_mul_lpCostOn",
      "Book5.diagonalDecoherence_formula",
      "Book5.diagonalDecoherence_pos",
      "Book5.lpCostOn_le_axisCostOn",
      "Book7QuantumGleason.completeFrameCoherence_does_not_supply_hermitian_certificate",
      "Book7QuantumGleason.hermitian_reconstruction_from_certificate",
      "Book7QuantumGleason.pureStateDensity_globalPhase",
      "Book7QuantumGleason.pureStateDensity_isHermitian",
      "Book7QuantumGleason.pureStateToResolution_globalPhase",
      "Book7QuantumGleason.pureStateToResolution_reducedState_isHermitian",
      "Book7QuantumGleason.pureState_forward_chain",
      "Book7QuantumGleason.pureState_lowering_not_injective",
      "Book7QuantumGleason.quantumResolution_does_not_force_reducedState_isHermitian",
      "Book7QuantumGleason.quantumResolution_to_hermitian_certificate",
      "Book7QuantumGleason.quantumResolution_without_matrixHermiticity_does_not_supply_certificate",
      "ScholiumA.ChainedApprox.cauchySeq",
      "ScholiumA.ChainedApprox.exists_limit_with_tail_bound",
      "ScholiumA.chainedApprox_telescope",
      "ScholiumD.jko_step_freeEnergy_le",
      "ScholiumD.jko_step_transport_cost_le_energy_drop",
      "cauchy_forcing_completion"
    ]
  },
  "line": 372,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Formal correspondence at the observer boundary",
  "refs": [],
  "role": "remark",
  "type": "remark"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "remark:appC_born_rule_dependency",
    "subsec:appC_born_axioms"
  ],
  "cites": [
    "axiom:appC_psc3prime"
  ],
  "depends_on": [],
  "file": "appendix_dual_horizon.tex",
  "forward_ref_roles": [
    {
      "context": "",
      "label": "axiom:appC_psc3prime",
      "line_distance": 119,
      "role": "navigation",
      "target_line": 528,
      "target_type": "axiom"
    }
  ],
  "forward_refs": [
    "axiom:appC_psc3prime"
  ],
  "id": "subsec:appC_born_additivity_derivation",
  "label": "subsec:appC_born_additivity_derivation",
  "latex_body": "",
  "line": 409,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Interpretive-Budget Additivity from Bounded Discernibility",
  "ref_roles": [
    {
      "context": "",
      "label": "axiom:appC_psc3prime",
      "logical_support": false,
      "role": "forward_navigation",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 528,
      "target_type": "axiom"
    }
  ],
  "role": "section",
  "subtype": "subsection",
  "type": "section"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "proof:appC_orthogonal_token_separation"
  ],
  "cites": [
    "axiom:appC_psc5"
  ],
  "depends_on": [],
  "file": "appendix_dual_horizon.tex",
  "forward_ref_roles": [
    {
      "context": "resolved outcomes receive distinct tokens. This is the content later codified, at the resolution scale, as PS--C5 (Ax.~\\ref{axiom:appC_psc5}). \\end{assumption}",
      "label": "axiom:appC_psc5",
      "line_distance": 196,
      "role": "teaser",
      "target_line": 620,
      "target_type": "axiom"
    }
  ],
  "forward_refs": [
    "axiom:appC_psc5"
  ],
  "id": "assumption:appC_bounded_discernibility",
  "label": "assumption:appC_bounded_discernibility",
  "latex_body": "\\begin{assumption}[Bounded discernibility]\n\\label{assumption:appC_bounded_discernibility}\nA single resolved observer token is assigned to at most one of any two mutually\northogonal (hence mutually exclusive) outcome subspaces: orthogonal resolved outcomes\nreceive distinct tokens. This is the content later codified, at the resolution scale,\nas PS--C5 (Ax.~\\ref{axiom:appC_psc5}).\n\\end{assumption}",
  "line": 424,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Bounded discernibility",
  "proof_status": "definitional",
  "ref_roles": [
    {
      "context": "resolved outcomes receive distinct tokens. This is the content later codified, at the resolution scale, as PS--C5 (Ax.~\\ref{axiom:appC_psc5}). \\end{assumption}",
      "label": "axiom:appC_psc5",
      "logical_support": false,
      "role": "forward_teaser",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 620,
      "target_type": "axiom"
    }
  ],
  "refs": [
    "axiom:appC_psc5"
  ],
  "role": "assumption",
  "type": "assumption"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [
    "definition:appC_frame_space",
    "subsec:appC_born_interpretation_ps"
  ],
  "depends_on": [
    "definition:appC_frame_space"
  ],
  "file": "appendix_dual_horizon.tex",
  "forward_ref_roles": [
    {
      "context": "tokens} produced when $\\Obs$ applies its collapse/refinement map (the observer-context realization of $R_\\lambda$, cf.~\\ref{subsec:appC_born_interpretation_ps}) to $\\mathfrak{F}$. For any projector $\\Pi$ obtained by coarse-graining elements of $\\mathfrak{F}$, set \\[ T_\\Obs(\\Pi)",
      "label": "subsec:appC_born_interpretation_ps",
      "line_distance": 371,
      "role": "navigation",
      "target_line": 803,
      "target_type": "section"
    }
  ],
  "forward_refs": [
    "subsec:appC_born_interpretation_ps"
  ],
  "id": "definition:appC_observer_token_space",
  "label": "definition:appC_observer_token_space",
  "latex_body": "\\begin{definition}[Observer token space for a projective frame]\n\\label{definition:appC_observer_token_space}\nLet $\\dim\\Horizon < \\infty$ and let\n\\[\n\\mathfrak{F} = \\{\\Pi_i\\}_{i=1}^{n} \\subseteq Proj(\\Horizon),\n\\qquad \\Pi_i \\Pi_j = 0\\ (i \\neq j),\\qquad \\sum_i \\Pi_i = \\mathbbm{1},\n\\]\nbe a complete orthogonal frame discernible to the Bounded Observer $\\Obs$\n(cf.~\\ref{definition:appC_frame_space}). Let $\\mathcal{T}_\\Obs(\\mathfrak{F})$ denote\nthe finite set of \\emph{observer-resolvable outcome tokens} produced when $\\Obs$\napplies its collapse/refinement map (the observer-context realization of $R_\\lambda$,\ncf.~\\ref{subsec:appC_born_interpretation_ps}) to $\\mathfrak{F}$. For any projector\n$\\Pi$ obtained by coarse-graining elements of $\\mathfrak{F}$, set\n\\[\nT_\\Obs(\\Pi) := \\{\\, t \\in \\mathcal{T}_\\Obs(\\mathfrak{F}) :\n\\text{the outcome resolved by } t \\text{ lies in } \\operatorname{im}(\\Pi) \\,\\}.\n\\]\n\\end{definition}",
  "line": 432,
  "macros_used": [
    "Horizon",
    "Obs"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Observer token space for a projective frame",
  "proof_status": "definitional",
  "ref_roles": [
    {
      "context": "j),\\qquad \\sum_i \\Pi_i = \\mathbbm{1}, \\] be a complete orthogonal frame discernible to the Bounded Observer $\\Obs$ (cf.~\\ref{definition:appC_frame_space}). Let $\\mathcal{T}_\\Obs(\\mathfrak{F})$ denote the finite set of \\emph{observer-resolvable outcome tokens} produced when",
      "label": "definition:appC_frame_space",
      "logical_support": true,
      "role": "cf_near_match",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 350,
      "target_type": "definition"
    },
    {
      "context": "tokens} produced when $\\Obs$ applies its collapse/refinement map (the observer-context realization of $R_\\lambda$, cf.~\\ref{subsec:appC_born_interpretation_ps}) to $\\mathfrak{F}$. For any projector $\\Pi$ obtained by coarse-graining elements of $\\mathfrak{F}$, set \\[ T_\\Obs(\\Pi)",
      "label": "subsec:appC_born_interpretation_ps",
      "logical_support": false,
      "role": "forward_navigation",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 803,
      "target_type": "section"
    }
  ],
  "refs": [
    "definition:appC_frame_space",
    "subsec:appC_born_interpretation_ps"
  ],
  "role": "definition",
  "type": "definition"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "assumption:appC_emergence_domination",
    "proof:appC_orthogonal_additivity",
    "proof:appC_psc3",
    "remark:appC_born_honest_reduction"
  ],
  "cites": [
    "definition:appC_coherence_functional"
  ],
  "depends_on": [
    "definition:appC_coherence_functional"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "definition:appC_observer_coherence_budget",
  "label": "definition:appC_observer_coherence_budget",
  "latex_body": "\\begin{definition}[Observer coherence budget]\n\\label{definition:appC_observer_coherence_budget}\nA Bounded Observer $\\Obs$ in state $\\tilde\\psi_{\\Obs}$ carries a finite\n\\emph{coherence budget}\n\\[\n\\mu_{\\Obs,\\tilde\\psi} : \\mathcal{P}\\big(\\mathcal{T}_\\Obs(\\mathfrak{F})\\big) \\to [0,1],\n\\qquad\n\\mu_{\\Obs,\\tilde\\psi}(\\varnothing) = 0,\\quad\n\\mu_{\\Obs,\\tilde\\psi}\\big(\\mathcal{T}_\\Obs(\\mathfrak{F})\\big) = 1,\n\\]\nwhich is finitely additive on disjoint token sets:\n$A \\cap B = \\varnothing \\Rightarrow\n\\mu_{\\Obs,\\tilde\\psi}(A \\sqcup B) = \\mu_{\\Obs,\\tilde\\psi}(A) + \\mu_{\\Obs,\\tilde\\psi}(B)$.\nThis is not a quantum-probability axiom but finite symbolic-budget conservation:\ndisjoint resolved tokens cannot consume the same bounded interpretive resource twice.\nThe coherence functional (cf.~\\ref{definition:appC_coherence_functional}) admits the\ntoken-budget representation\n\\[\n\\mathcal{C}_{\\Obs}(\\tilde\\psi_{\\Obs}, \\Pi) = \\mu_{\\Obs,\\tilde\\psi}\\big(T_\\Obs(\\Pi)\\big).\n\\]\n\\end{definition}",
  "line": 451,
  "macros_used": [
    "Obs"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Observer coherence budget",
  "proof_status": "definitional",
  "ref_roles": [
    {
      "context": "on: disjoint resolved tokens cannot consume the same bounded interpretive resource twice. The coherence functional (cf.~\\ref{definition:appC_coherence_functional}) admits the token-budget representation \\[ \\mathcal{C}_{\\Obs}(\\tilde\\psi_{\\Obs}, \\Pi) = \\mu_{\\Obs,\\tilde\\psi}\\big(T_\\Ob",
      "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": "definition",
  "type": "definition"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "proof:appC_coarse_graining_tokens",
    "remark:appC_born_honest_reduction"
  ],
  "cites": [],
  "depends_on": [
    "assumption:appC_bounded_discernibility"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "lemma:appC_orthogonal_token_separation",
  "label": "lemma:appC_orthogonal_token_separation",
  "latex_body": "\\begin{lemma}[Orthogonal token separation]\n\\label{lemma:appC_orthogonal_token_separation}\nIf $\\Pi\\,\\Xi = 0$ then $T_\\Obs(\\Pi) \\cap T_\\Obs(\\Xi) = \\varnothing$.\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": true,
    "notes": [
      "Tokens resolving to distinct indices are disjoint, proved directly from the resolving-function model rather than from an operator-orthogonality hypothesis."
    ],
    "record_ids": [
      "MAP-APPENDIX_DUAL_HORIZON-005"
    ],
    "statuses": [
      "exact"
    ],
    "witnesses": [
      "AppendixDH.orthogonal_token_separation"
    ]
  },
  "line": 473,
  "macros_used": [
    "Obs"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Orthogonal token separation",
  "proof_labels": [
    "proof:appC_orthogonal_token_separation"
  ],
  "proof_status": "proven",
  "refs": [],
  "role": "lemma",
  "type": "lemma"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [
    "assumption:appC_bounded_discernibility"
  ],
  "depends_on": [
    "assumption:appC_bounded_discernibility"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "proof:appC_orthogonal_token_separation",
  "label": "proof:appC_orthogonal_token_separation",
  "latex_body": "\\begin{proof}\n\\label{proof:appC_orthogonal_token_separation}\nOrthogonality gives $\\operatorname{im}(\\Pi) \\cap \\operatorname{im}(\\Xi) = \\{0\\}$.\nWere a token $t$ to lie in both $T_\\Obs(\\Pi)$ and $T_\\Obs(\\Xi)$, the single outcome\nresolved by $t$ would simultaneously be a $\\Pi$-outcome and an $\\Xi$-outcome,\ni.e.\\ the observer would assign one resolved token to two mutually orthogonal\n(hence mutually exclusive) subspaces. This violates bounded discernibility\n(Assumption~\\ref{assumption:appC_bounded_discernibility}). Hence the token sets are disjoint.\n\\end{proof}",
  "line": 478,
  "macros_used": [
    "Obs"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "",
  "proves": "lemma:appC_orthogonal_token_separation",
  "ref_roles": [
    {
      "context": "token to two mutually orthogonal (hence mutually exclusive) subspaces. This violates bounded discernibility (Assumption~\\ref{assumption:appC_bounded_discernibility}). Hence the token sets are disjoint. \\end{proof}",
      "label": "assumption:appC_bounded_discernibility",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 424,
      "target_type": "assumption"
    }
  ],
  "refs": [
    "assumption:appC_bounded_discernibility"
  ],
  "role": "proof",
  "type": "proof"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "proof:appC_orthogonal_additivity",
    "remark:appC_born_honest_reduction"
  ],
  "cites": [],
  "depends_on": [
    "lemma:appC_orthogonal_token_separation"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "lemma:appC_coarse_graining_tokens",
  "label": "lemma:appC_coarse_graining_tokens",
  "latex_body": "\\begin{lemma}[Coarse-graining of orthogonal tokens]\n\\label{lemma:appC_coarse_graining_tokens}\nIf $\\Pi_i \\Pi_j = 0$ for $i \\neq j$, then\n$T_\\Obs\\!\\big(\\sum_i \\Pi_i\\big) = \\bigsqcup_i T_\\Obs(\\Pi_i)$.\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": true,
    "notes": [
      "Coarse-graining a set of frame indices resolves to exactly the Finset.biUnion of the individual token sets."
    ],
    "record_ids": [
      "MAP-APPENDIX_DUAL_HORIZON-006"
    ],
    "statuses": [
      "exact"
    ],
    "witnesses": [
      "AppendixDH.tokensOfSet_eq_biUnion"
    ]
  },
  "line": 488,
  "macros_used": [
    "Obs"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Coarse-graining of orthogonal tokens",
  "proof_labels": [
    "proof:appC_coarse_graining_tokens"
  ],
  "proof_status": "proven",
  "refs": [],
  "role": "lemma",
  "type": "lemma"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [
    "lemma:appC_orthogonal_token_separation"
  ],
  "depends_on": [
    "lemma:appC_orthogonal_token_separation"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "proof:appC_coarse_graining_tokens",
  "label": "proof:appC_coarse_graining_tokens",
  "latex_body": "\\begin{proof}\n\\label{proof:appC_coarse_graining_tokens}\nThe projector $\\sum_i \\Pi_i$ encodes the coarse-grained question\n``did the resolved outcome fall in $\\bigcup_i \\operatorname{im}(\\Pi_i)$?'' A token\nanswers affirmatively exactly when it lies in some $T_\\Obs(\\Pi_i)$, so\n$T_\\Obs(\\sum_i \\Pi_i) = \\bigcup_i T_\\Obs(\\Pi_i)$. By\nLemma~\\ref{lemma:appC_orthogonal_token_separation} the $T_\\Obs(\\Pi_i)$ are pairwise\ndisjoint, so the union is disjoint.\n\\end{proof}",
  "line": 494,
  "macros_used": [
    "Obs"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "",
  "proves": "lemma:appC_coarse_graining_tokens",
  "ref_roles": [
    {
      "context": "firmatively exactly when it lies in some $T_\\Obs(\\Pi_i)$, so $T_\\Obs(\\sum_i \\Pi_i) = \\bigcup_i T_\\Obs(\\Pi_i)$. By Lemma~\\ref{lemma:appC_orthogonal_token_separation} the $T_\\Obs(\\Pi_i)$ are pairwise disjoint, so the union is disjoint. \\end{proof}",
      "label": "lemma:appC_orthogonal_token_separation",
      "logical_support": true,
      "role": "proof_support",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 473,
      "target_type": "lemma"
    }
  ],
  "refs": [
    "lemma:appC_orthogonal_token_separation"
  ],
  "role": "proof",
  "type": "proof"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "lemma:appC_sigma_additivity",
    "proof:appC_psc3",
    "proof:appC_sigma_additivity",
    "remark:appC_born_honest_reduction",
    "remark:appC_born_rule_dependency"
  ],
  "cites": [],
  "depends_on": [
    "definition:appC_observer_coherence_budget",
    "lemma:appC_coarse_graining_tokens"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "theorem:appC_orthogonal_additivity",
  "label": "theorem:appC_orthogonal_additivity",
  "latex_body": "\\begin{theorem}[Orthogonal additivity from bounded discernibility]\n\\label{theorem:appC_orthogonal_additivity}\nLet $\\Obs$ be a Bounded Observer with finite coherence budget\n$\\mu_{\\Obs,\\tilde\\psi}$. For any finite mutually orthogonal family\n$\\{\\Pi_i\\}_{i=1}^n \\subseteq Proj(\\Horizon)$,\n\\[\n\\mathcal{C}_{\\Obs}\\!\\Big(\\tilde\\psi_{\\Obs}, \\sum_i \\Pi_i\\Big)\n= \\sum_i \\mathcal{C}_{\\Obs}(\\tilde\\psi_{\\Obs}, \\Pi_i).\n\\]\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": [
      "Binary additivity is extended by induction to any finite pairwise-disjoint indexed family, then combined with the token-resolution model to give additivity of mu over any finite orthogonal family."
    ],
    "record_ids": [
      "MAP-APPENDIX_DUAL_HORIZON-008"
    ],
    "statuses": [
      "exact"
    ],
    "witnesses": [
      "AppendixDH.mu_biUnion_eq_sum",
      "AppendixDH.orthogonal_additivity"
    ]
  },
  "line": 504,
  "macros_used": [
    "Horizon",
    "Obs"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Orthogonal additivity from bounded discernibility",
  "proof_labels": [
    "proof:appC_orthogonal_additivity"
  ],
  "proof_status": "proven",
  "refs": [],
  "role": "theorem",
  "type": "theorem"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [
    "definition:appC_observer_coherence_budget",
    "lemma:appC_coarse_graining_tokens"
  ],
  "depends_on": [
    "definition:appC_observer_coherence_budget",
    "lemma:appC_coarse_graining_tokens"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "proof:appC_orthogonal_additivity",
  "label": "proof:appC_orthogonal_additivity",
  "latex_body": "\\begin{proof}\n\\label{proof:appC_orthogonal_additivity}\nBy the token-budget representation (Def.~\\ref{definition:appC_observer_coherence_budget}),\n$\\mathcal{C}_{\\Obs}(\\tilde\\psi_{\\Obs}, \\sum_i \\Pi_i)\n= \\mu_{\\Obs,\\tilde\\psi}\\big(T_\\Obs(\\sum_i \\Pi_i)\\big)$. By\nLemma~\\ref{lemma:appC_coarse_graining_tokens},\n$T_\\Obs(\\sum_i \\Pi_i) = \\bigsqcup_i T_\\Obs(\\Pi_i)$. Finite additivity of the budget\nover disjoint token sets gives\n$\\mu_{\\Obs,\\tilde\\psi}(\\bigsqcup_i T_\\Obs(\\Pi_i))\n= \\sum_i \\mu_{\\Obs,\\tilde\\psi}(T_\\Obs(\\Pi_i))$, and applying the representation once\nmore yields $\\sum_i \\mathcal{C}_{\\Obs}(\\tilde\\psi_{\\Obs}, \\Pi_i)$.\n\\end{proof}",
  "line": 515,
  "macros_used": [
    "Obs"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "",
  "proves": "theorem:appC_orthogonal_additivity",
  "ref_roles": [
    {
      "context": "\\begin{proof} \\label{proof:appC_orthogonal_additivity} By the token-budget representation (Def.~\\ref{definition:appC_observer_coherence_budget}), $\\mathcal{C}_{\\Obs}(\\tilde\\psi_{\\Obs}, \\sum_i \\Pi_i) = \\mu_{\\Obs,\\tilde\\psi}\\big(T_\\Obs(\\sum_i \\Pi_i)\\big)$. By Lemma",
      "label": "definition:appC_observer_coherence_budget",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 451,
      "target_type": "definition"
    },
    {
      "context": ", $\\mathcal{C}_{\\Obs}(\\tilde\\psi_{\\Obs}, \\sum_i \\Pi_i) = \\mu_{\\Obs,\\tilde\\psi}\\big(T_\\Obs(\\sum_i \\Pi_i)\\big)$. By Lemma~\\ref{lemma:appC_coarse_graining_tokens}, $T_\\Obs(\\sum_i \\Pi_i) = \\bigsqcup_i T_\\Obs(\\Pi_i)$. Finite additivity of the budget over disjoint token sets gives $\\m",
      "label": "lemma:appC_coarse_graining_tokens",
      "logical_support": true,
      "role": "proof_support",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 488,
      "target_type": "lemma"
    }
  ],
  "refs": [
    "definition:appC_observer_coherence_budget",
    "lemma:appC_coarse_graining_tokens"
  ],
  "role": "proof",
  "type": "proof"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "definition:bk7_contextuality_defect",
    "remark:appC_born_rule_dependency",
    "remark:appC_domination_open_route",
    "remark:bk7_pisu_status",
    "subsec:appC_born_additivity_derivation",
    "subsec:appC_born_axioms",
    "subsec:appC_conclusion_of_proof_by_elimination",
    "subsec:bk7_pisu_implications"
  ],
  "cites": [],
  "depends_on": [],
  "file": "appendix_dual_horizon.tex",
  "id": "axiom:appC_psc3prime",
  "label": "axiom:appC_psc3prime",
  "latex_body": "\\begin{axiom}[PS--C3$'$ (Non-contextual token budget)]\n\\label{axiom:appC_psc3prime}\nLet $\\mathfrak{F}, \\mathfrak{F}'$ be complete orthogonal frames discernible to $\\Obs$,\nand let $\\Pi \\in Proj(\\Horizon)$ be obtained by coarse-graining elements of\n$\\mathfrak{F}$ and also of $\\mathfrak{F}'$, with token realizations\n$T^{\\mathfrak{F}}_\\Obs(\\Pi)$ and $T^{\\mathfrak{F}'}_\\Obs(\\Pi)$. Then the budget\nassigns them equal measure,\n\\[\n\\mu_{\\Obs,\\tilde\\psi}\\big(T^{\\mathfrak{F}}_\\Obs(\\Pi)\\big)\n= \\mu_{\\Obs,\\tilde\\psi}\\big(T^{\\mathfrak{F}'}_\\Obs(\\Pi)\\big);\n\\]\nequivalently, $\\mathcal{C}_{\\Obs}(\\tilde\\psi_\\Obs,\\Pi)$ is well defined independently of\nthe complete frame within which $\\Obs$ poses the question $\\Pi$.\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.bounded_budget_does_not_force_noncontextuality"
    ],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": true,
    "notes": [
      "Typed noncontextuality axiom: a budget satisfying NoncontextualAt gives equal values for the same question across frames. Countermodel confirms unit-interval boundedness does not derive frame independence, matching the source declaration that PS-C3-prime is posited."
    ],
    "record_ids": [
      "MAP-APPENDIX_DUAL_HORIZON-049"
    ],
    "statuses": [
      "conditional"
    ],
    "witnesses": [
      "AppendixCoherenceAxioms.bounded_budget_does_not_force_noncontextuality",
      "AppendixCoherenceAxioms.noncontextual_budget_frame_independent"
    ]
  },
  "line": 528,
  "macros_used": [
    "Horizon",
    "Obs"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "PS--C3$'$ (Non-contextual token budget)",
  "proof_status": "definitional",
  "refs": [],
  "role": "axiom",
  "type": "axiom"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [
    "definition:appC_observer_coherence_budget",
    "lemma:appC_coarse_graining_tokens",
    "lemma:appC_orthogonal_token_separation",
    "theorem:appC_orthogonal_additivity"
  ],
  "depends_on": [
    "definition:appC_observer_coherence_budget",
    "lemma:appC_coarse_graining_tokens",
    "lemma:appC_orthogonal_token_separation",
    "theorem:appC_orthogonal_additivity"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "remark:appC_born_honest_reduction",
  "label": "remark:appC_born_honest_reduction",
  "latex_body": "\\begin{remark}[What is proved, and what is posited]\n\\label{remark:appC_born_honest_reduction}\nLemma~\\ref{lemma:appC_orthogonal_token_separation},\nLemma~\\ref{lemma:appC_coarse_graining_tokens}, and\nTheorem~\\ref{theorem:appC_orthogonal_additivity} establish additivity of the budget\n\\emph{within any single frame}; this is bookkeeping, derived from token disjointness.\nThe frame-independence of the representation\n$\\mathcal{C}_{\\Obs}(\\tilde\\psi_\\Obs,\\Pi) = \\mu_{\\Obs,\\tilde\\psi}(T_\\Obs(\\Pi))$ across\nframes -- PS--C3$'$ -- is the PS form of non-contextuality and is posited, not derived.\nThe Born derivation therefore reduces Gleason's additivity hypothesis to two\ningredients: finite-budget conservation on disjoint tokens\n(Def.~\\ref{definition:appC_observer_coherence_budget}, a bookkeeping principle) and\nnon-contextuality of the budget (PS--C3$'$, the physical content).\n\\end{remark}",
  "line": 543,
  "macros_used": [
    "Obs"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "What is proved, and what is posited",
  "ref_roles": [
    {
      "context": "erefore reduces Gleason's additivity hypothesis to two ingredients: finite-budget conservation on disjoint tokens (Def.~\\ref{definition:appC_observer_coherence_budget}, a bookkeeping principle) and non-contextuality of the budget (PS--C3$'$, the physical content). \\end{remark}",
      "label": "definition:appC_observer_coherence_budget",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 451,
      "target_type": "definition"
    },
    {
      "context": "nd what is posited] \\label{remark:appC_born_honest_reduction} Lemma~\\ref{lemma:appC_orthogonal_token_separation}, Lemma~\\ref{lemma:appC_coarse_graining_tokens}, and Theorem~\\ref{theorem:appC_orthogonal_additivity} establish additivity of the budget \\emph{within any single frame}",
      "label": "lemma:appC_coarse_graining_tokens",
      "logical_support": true,
      "role": "formal_dependency",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 488,
      "target_type": "lemma"
    },
    {
      "context": "\\begin{remark}[What is proved, and what is posited] \\label{remark:appC_born_honest_reduction} Lemma~\\ref{lemma:appC_orthogonal_token_separation}, Lemma~\\ref{lemma:appC_coarse_graining_tokens}, and Theorem~\\ref{theorem:appC_orthogonal_additivity} establish additivi",
      "label": "lemma:appC_orthogonal_token_separation",
      "logical_support": true,
      "role": "formal_dependency",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 473,
      "target_type": "lemma"
    },
    {
      "context": "duction} Lemma~\\ref{lemma:appC_orthogonal_token_separation}, Lemma~\\ref{lemma:appC_coarse_graining_tokens}, and Theorem~\\ref{theorem:appC_orthogonal_additivity} establish additivity of the budget \\emph{within any single frame}; this is bookkeeping, derived from token disjointness",
      "label": "theorem:appC_orthogonal_additivity",
      "logical_support": true,
      "role": "formal_dependency",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 504,
      "target_type": "theorem"
    }
  ],
  "refs": [
    "definition:appC_observer_coherence_budget",
    "lemma:appC_coarse_graining_tokens",
    "lemma:appC_orthogonal_token_separation",
    "theorem:appC_orthogonal_additivity"
  ],
  "role": "remark",
  "type": "remark"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [
    "axiom:appC_psc5",
    "theorem:appC_born_rule"
  ],
  "depends_on": [],
  "file": "appendix_dual_horizon.tex",
  "forward_ref_roles": [
    {
      "context": "sc3prime_open_route} A future derivation could proceed through resolution-limited frame distinguishability (PS--C5, Ax.~\\ref{axiom:appC_psc5}): if two discernible frames agree on $\\Pi$ up to the observer threshold $\\epsilon_\\Obs$, the budgets they assign $\\Pi$",
      "label": "axiom:appC_psc5",
      "line_distance": 62,
      "role": "teaser",
      "target_line": 620,
      "target_type": "axiom"
    },
    {
      "context": "ent limit. We record this as open. That $\\dim\\Horizon \\ge 3$ enters in the same place it enters Gleason's theorem (Thm.~\\ref{theorem:appC_born_rule}) is structural evidence the route is the right one; until it is completed, PS--C3$'$ stands as an axiom and the Born co",
      "label": "theorem:appC_born_rule",
      "line_distance": 143,
      "role": "teaser",
      "target_line": 701,
      "target_type": "theorem"
    }
  ],
  "forward_refs": [
    "axiom:appC_psc5",
    "theorem:appC_born_rule"
  ],
  "id": "remark:appC_psc3prime_open_route",
  "label": "remark:appC_psc3prime_open_route",
  "latex_body": "\\begin{remark}[Open derivation route for PS--C3$'$]\n\\label{remark:appC_psc3prime_open_route}\nA future derivation could proceed through resolution-limited frame distinguishability\n(PS--C5, Ax.~\\ref{axiom:appC_psc5}): if two discernible frames agree on $\\Pi$ up to the\nobserver threshold $\\epsilon_\\Obs$, the budgets they assign $\\Pi$ must agree up to a\nmodulus controlled by $\\epsilon_\\Obs$, and a continuity-plus-density argument over the\nframe manifold -- connected for $\\dim\\Horizon \\ge 3$ -- might then force exact equality\nin the $\\epsilon_\\Obs \\to 0$ refinement limit. We record this as open. That\n$\\dim\\Horizon \\ge 3$ enters in the same place it enters Gleason's theorem\n(Thm.~\\ref{theorem:appC_born_rule}) is structural evidence the route is the right one;\nuntil it is completed, PS--C3$'$ stands as an axiom and the Born conclusion is\nconditional on it.\n\\end{remark}",
  "lean_alignment": {
    "conditions": [],
    "countermodels": [],
    "full_record": "bib/principia_lean_alignment.json",
    "kernel_certified": false,
    "notes": [
      "The existing continuity-plus-density route is explicitly speculative and distinct from the now-refuted direct frame-readout lift; later editing should keep those two boundaries separate."
    ],
    "record_ids": [
      "REVIEW-002"
    ],
    "statuses": [
      "open_bridge"
    ],
    "witnesses": [
      "Book7QuantumGleason.completeFrameCoherence_does_not_supply_hermitian_certificate"
    ]
  },
  "line": 558,
  "macros_used": [
    "Horizon",
    "Obs"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Open derivation route for PS--C3$'$",
  "ref_roles": [
    {
      "context": "sc3prime_open_route} A future derivation could proceed through resolution-limited frame distinguishability (PS--C5, Ax.~\\ref{axiom:appC_psc5}): if two discernible frames agree on $\\Pi$ up to the observer threshold $\\epsilon_\\Obs$, the budgets they assign $\\Pi$",
      "label": "axiom:appC_psc5",
      "logical_support": false,
      "role": "forward_teaser",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 620,
      "target_type": "axiom"
    },
    {
      "context": "ent limit. We record this as open. That $\\dim\\Horizon \\ge 3$ enters in the same place it enters Gleason's theorem (Thm.~\\ref{theorem:appC_born_rule}) is structural evidence the route is the right one; until it is completed, PS--C3$'$ stands as an axiom and the Born co",
      "label": "theorem:appC_born_rule",
      "logical_support": false,
      "role": "forward_teaser",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 701,
      "target_type": "theorem"
    }
  ],
  "refs": [
    "axiom:appC_psc5",
    "theorem:appC_born_rule"
  ],
  "role": "remark",
  "type": "remark"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "remark:appC_born_rule_dependency"
  ],
  "cites": [
    "axiom:appC_psc3prime",
    "definition:appC_coherence_functional",
    "subsec:appC_born_additivity_derivation"
  ],
  "depends_on": [
    "axiom:appC_psc3prime",
    "definition:appC_coherence_functional"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "subsec:appC_born_axioms",
  "label": "subsec:appC_born_axioms",
  "latex_body": "",
  "line": 572,
  "macros_used": [],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "Coherence Axioms (PS–C)",
  "ref_roles": [
    {
      "context": "",
      "label": "axiom:appC_psc3prime",
      "logical_support": false,
      "role": "navigation",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 528,
      "target_type": "axiom"
    },
    {
      "context": "",
      "label": "definition:appC_coherence_functional",
      "logical_support": false,
      "role": "navigation",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 361,
      "target_type": "definition"
    },
    {
      "context": "",
      "label": "subsec:appC_born_additivity_derivation",
      "logical_support": false,
      "role": "navigation",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 409,
      "target_type": "section"
    }
  ],
  "role": "section",
  "subtype": "subsection",
  "type": "section"
}

{
  "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_psc1",
  "label": "axiom:appC_psc1",
  "latex_body": "\\begin{axiom}[PS--C1 (Boundedness)]\n\\label{axiom:appC_psc1}\n$0 \\leq \\mathcal{C}_{\\Obs}(\\tilde\\psi_{\\Obs}, \\Pi) \\leq 1$ \\quad (cf.~\\ref{definition:appC_coherence_functional})\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": [
      "Boundedness is derived as a theorem from mu_nonneg plus finite additivity (mu(full) = mu(A) + mu(full\\A) >= mu(A)), rather than postulated as a separate axiom."
    ],
    "record_ids": [
      "MAP-APPENDIX_DUAL_HORIZON-009"
    ],
    "statuses": [
      "exact"
    ],
    "witnesses": [
      "AppendixDH.mu_le_one"
    ]
  },
  "line": 580,
  "macros_used": [
    "Obs"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "PS--C1 (Boundedness)",
  "proof_status": "definitional",
  "ref_roles": [
    {
      "context": "om}[PS--C1 (Boundedness)] \\label{axiom:appC_psc1} $0 \\leq \\mathcal{C}_{\\Obs}(\\tilde\\psi_{\\Obs}, \\Pi) \\leq 1$ \\quad (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"
}

{
  "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_psc2",
  "label": "axiom:appC_psc2",
  "latex_body": "\\begin{axiom}[PS--C2 (Unitary covariance)]\n\\label{axiom:appC_psc2}\n$\\mathcal{C}_{\\Obs}(U \\tilde\\psi_{\\Obs}, U \\Pi U^\\dagger)\n= \\mathcal{C}_{\\Obs}(\\tilde\\psi_{\\Obs}, \\Pi)$ \\quad (cf.~\\ref{definition:appC_coherence_functional})\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 coherence form satisfies unitary covariance; forward direction of the Born rule."
    ],
    "record_ids": [
      "MAP-APPENDIX_DUAL_HORIZON-042"
    ],
    "statuses": [
      "exact"
    ],
    "witnesses": [
      "Born.psc2_unitary_covariance"
    ]
  },
  "line": 585,
  "macros_used": [
    "Obs"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "PS--C2 (Unitary covariance)",
  "proof_status": "definitional",
  "ref_roles": [
    {
      "context": "sc2} $\\mathcal{C}_{\\Obs}(U \\tilde\\psi_{\\Obs}, U \\Pi U^\\dagger) = \\mathcal{C}_{\\Obs}(\\tilde\\psi_{\\Obs}, \\Pi)$ \\quad (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"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [
    "lemma:appC_sigma_additivity",
    "proof:appC_sigma_additivity"
  ],
  "cites": [
    "definition:appC_coherence_functional"
  ],
  "depends_on": [
    "definition:appC_coherence_functional",
    "definition:appC_observer_coherence_budget",
    "theorem:appC_orthogonal_additivity"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "axiom:appC_psc3",
  "label": "axiom:appC_psc3",
  "latex_body": "\\begin{corollary}[PS--C3 (Conservation of interpretive budget)]\n\\label{axiom:appC_psc3}\nFor any complete orthogonal decomposition $\\{\\Pi_i\\}$ of $\\mathbbm{1}$ (cf.~\\ref{definition:appC_coherence_functional}):\n\\[\n\\sum_i \\mathcal{C}_{\\Obs}(\\tilde\\psi_{\\Obs}, \\Pi_i) = 1.\n\\]\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": [
      "Conservation (sum over all frame indices = 1) is derived given the added hypothesis that the frame's coarse-graining of every index covers the full admissible token set (tokensOfSet Finset.univ = full); this hypothesis is implicit-by-construction in the source's discernible complete frame but must be stated explicitly here."
    ],
    "record_ids": [
      "MAP-APPENDIX_DUAL_HORIZON-010"
    ],
    "statuses": [
      "conditional"
    ],
    "witnesses": [
      "AppendixDH.mu_conservation"
    ]
  },
  "line": 591,
  "macros_used": [
    "Obs"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "PS--C3 (Conservation of interpretive budget)",
  "proof_labels": [
    "proof:appC_psc3"
  ],
  "proof_status": "proven",
  "ref_roles": [
    {
      "context": "terpretive budget)] \\label{axiom:appC_psc3} For any complete orthogonal decomposition $\\{\\Pi_i\\}$ of $\\mathbbm{1}$ (cf.~\\ref{definition:appC_coherence_functional}): \\[ \\sum_i \\mathcal{C}_{\\Obs}(\\tilde\\psi_{\\Obs}, \\Pi_i) = 1. \\] \\end{corollary}",
      "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": "corollary",
  "type": "corollary"
}

{
  "book": "appendix_dual_horizon",
  "cited_by": [],
  "cites": [
    "definition:appC_observer_coherence_budget",
    "theorem:appC_orthogonal_additivity"
  ],
  "depends_on": [
    "definition:appC_observer_coherence_budget",
    "theorem:appC_orthogonal_additivity"
  ],
  "file": "appendix_dual_horizon.tex",
  "id": "proof:appC_psc3",
  "label": "proof:appC_psc3",
  "latex_body": "\\begin{proof}\n\\label{proof:appC_psc3}\nApply Theorem~\\ref{theorem:appC_orthogonal_additivity} to the complete frame\n$\\sum_i \\Pi_i = \\mathbbm{1}$:\n$\\sum_i \\mathcal{C}_{\\Obs}(\\tilde\\psi_{\\Obs}, \\Pi_i)\n= \\mathcal{C}_{\\Obs}(\\tilde\\psi_{\\Obs}, \\mathbbm{1})\n= \\mu_{\\Obs,\\tilde\\psi}\\big(T_\\Obs(\\mathbbm{1})\\big)\n= \\mu_{\\Obs,\\tilde\\psi}\\big(\\mathcal{T}_\\Obs(\\mathfrak{F})\\big) = 1$,\nusing the token-budget representation\n(Def.~\\ref{definition:appC_observer_coherence_budget}) and the normalization\n$\\mu_{\\Obs,\\tilde\\psi}(\\mathcal{T}_\\Obs(\\mathfrak{F})) = 1$.\n\\end{proof}",
  "line": 599,
  "macros_used": [
    "Obs"
  ],
  "matter_region": "appendix",
  "matter_role": "appendix_expansion",
  "name": "",
  "proves": "axiom:appC_psc3",
  "ref_roles": [
    {
      "context": "\\big) = \\mu_{\\Obs,\\tilde\\psi}\\big(\\mathcal{T}_\\Obs(\\mathfrak{F})\\big) = 1$, using the token-budget representation (Def.~\\ref{definition:appC_observer_coherence_budget}) and the normalization $\\mu_{\\Obs,\\tilde\\psi}(\\mathcal{T}_\\Obs(\\mathfrak{F})) = 1$. \\end{proof}",
      "label": "definition:appC_observer_coherence_budget",
      "logical_support": true,
      "role": "definition_anchor",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 451,
      "target_type": "definition"
    },
    {
      "context": "\\begin{proof} \\label{proof:appC_psc3} Apply Theorem~\\ref{theorem:appC_orthogonal_additivity} to the complete frame $\\sum_i \\Pi_i = \\mathbbm{1}$: $\\sum_i \\mathcal{C}_{\\Obs}(\\tilde\\psi_{\\Obs}, \\Pi_i) = \\mathcal{C}_",
      "label": "theorem:appC_orthogonal_additivity",
      "logical_support": true,
      "role": "proof_support",
      "target_file": "appendix_dual_horizon.tex",
      "target_line": 504,
      "target_type": "theorem"
    }
  ],
  "refs": [
    "definition:appC_observer_coherence_budget",
    "theorem:appC_orthogonal_additivity"
  ],
  "role": "proof",
  "type": "proof"
}