Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Shared Canonical Arena Peers

Abstract

Five frozen causal peers reuse the separation template on two existing canonical arenas.

The intervention catalog contains four new peers and its gold shadow; the observation-intervention catalog contains one new peer and its gold shadow. Each occurrence uses exactly the two finite readouts of its declared law. No anchors, carrier copies, or theorem-truth readouts enter the bundles.

Definition 1.1 (Finite intervention object arena).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/SharedArenaPeers.finiteInterventionArena

Formalization. D5/S3/ConceptDynamics/InformationEscape/SharedArenaPeers.finiteInterventionArena (✓ std3).

Source. Repository-derived.

Commentary.

The intervention registrations enumerate the finite SCM object arena used by their declared readouts.

Definition 1.2 (Finite intervention law arena).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/SharedArenaPeers.finiteInterventionLawArena

Formalization. D5/S3/ConceptDynamics/InformationEscape/SharedArenaPeers.finiteInterventionLawArena (✓ std3).

Source. Repository-derived.

Commentary.

The homogeneous finite signature turns intervention and counterfactual codes into the separation law.

Definition 1.3 (Finite observation object arena).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/SharedArenaPeers.finiteObservationInterventionArena

Formalization. D5/S3/ConceptDynamics/InformationEscape/SharedArenaPeers.finiteObservationInterventionArena (✓ std3).

Source. Repository-derived.

Commentary.

The observation-intervention registrations enumerate the finite directional SCM object arena.

Definition 1.4 (Finite observation law arena).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/SharedArenaPeers.finiteObservationInterventionLawArena

Formalization. D5/S3/ConceptDynamics/InformationEscape/SharedArenaPeers.finiteObservationInterventionLawArena (✓ std3).

Source. Repository-derived.

Commentary.

The same homogeneous signature records observation and intervention code separation.

Definition 1.5 (Intervention code readouts).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/SharedArenaPeers.icIntCode

Formalization. D5/S3/ConceptDynamics/InformationEscape/SharedArenaPeers.icIntCode (✓ std3).

Source. Repository-derived.

Commentary.

Marginal and counterfactual outcome tables are encoded as the two public finite readout functions.

Definition 1.6 (Counterfactual code readout).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/SharedArenaPeers.icCFCode

Formalization. D5/S3/ConceptDynamics/InformationEscape/SharedArenaPeers.icCFCode (✓ std3).

Source. Repository-derived.

Commentary.

The joint outcome table supplies the second intervention readout.

Definition 1.7 (Observation code readout).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/SharedArenaPeers.oiObsCode

Formalization. D5/S3/ConceptDynamics/InformationEscape/SharedArenaPeers.oiObsCode (✓ std3).

Source. Repository-derived.

Commentary.

The observation code branches on the direction field and projects the root and child fields.

Definition 1.8 (Intervention code readout).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/SharedArenaPeers.oiIntCode

Formalization. D5/S3/ConceptDynamics/InformationEscape/SharedArenaPeers.oiIntCode (✓ std3).

Source. Repository-derived.

Commentary.

The intervention code branches on the direction field and projects the corresponding causal field.

Theorem 1.9 (Counterfactual kernel strictness).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/SharedArenaPeers.finer_bridge

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscape/SharedArenaPeers.finer_bridge (✓ std3). ∎

Source. Repository-derived.

Commentary.

The collapse identity supplies inclusion; the remaining law is separation.

Theorem 1.10 (Variation on a coupling fiber).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/SharedArenaPeers.fiber_bridge

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscape/SharedArenaPeers.fiber_bridge (✓ std3). ∎

Source. Repository-derived.

Commentary.

Introducing or eliminating the common marginal label preserves the separation law.

Theorem 1.11 (Failure of identifiability).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/SharedArenaPeers.not_identifiable_bridge

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscape/SharedArenaPeers.not_identifiable_bridge (✓ std3). ∎

Source. Repository-derived.

Commentary.

The factorization criterion converts failure of identifiability into a separated pair.

Theorem 1.12 (Target-relative sufficiency).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/SharedArenaPeers.target_bridge

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscape/SharedArenaPeers.target_bridge (✓ std3). ∎

Source. Repository-derived.

Commentary.

Universal sufficiency factorization identifies the failed counterfactual upgrade.

Theorem 1.13 (Full intervention profile strictness).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/SharedArenaPeers.profile_bridge

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscape/SharedArenaPeers.profile_bridge (✓ std3). ∎

Source. Repository-derived.

Commentary.

The null-action coordinate supplies observational inclusion; strictness supplies separation.

Theorem 1.14 (Intervention law sensitivity).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/SharedArenaPeers.intervention_law_sensitive

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscape/SharedArenaPeers.intervention_law_sensitive (✓ std3). ∎

Source. Repository-derived.

Commentary.

The actual realization satisfies the law and a constant realization of the same signature fails it.

Theorem 1.15 (Observation law sensitivity).

Lean statement: D5/S3/ConceptDynamics/InformationEscape/SharedArenaPeers.observation_law_sensitive

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscape/SharedArenaPeers.observation_law_sensitive (✓ std3). ∎

Source. Repository-derived.

Commentary.

The actual realization satisfies the law and a constant realization of the same signature fails it.

Reg.Catalogs.SharedArenaPeers imports the genuine registration leaves and owns both complete catalogs and their maximal seal. The seal reports a redundant verdict: every occurrence is certified trivial in its catalog and carries one finite IE-C007 zero-unique-capture record (intervention full 0 and without 0; observation-intervention full 24 and without 24). Each catalog publishes a redundancy certificate, no occurrence receives positive admission, system irredundancy is refuted for this root, and the census query certifies triviality for all seven occurrences.

References