Elegant joint measurement inflation identities
Abstract
Exact upstream inflation marginal consumers for the continuous triangle model.
Theorem 1.1 (Three-node triangle block).
Lean statement: D5/S3/Quantum/Entanglement/ElegantJointMeasurementInflation.triangle_identity_renamed
Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ElegantJointMeasurementInflation.triangle_identity_renamed (✓ std3). ∎
Source. Repository-derived.
Commentary.
The first three upstream nodes factor from the seven-node remainder and contribute the original p at the observed outcomes. Independent source supports are checked after arbitrary injective source-copy renaming.
Theorem 1.2 (Singleton marginal block).
Lean statement: D5/S3/Quantum/Entanglement/ElegantJointMeasurementInflation.singleton_identity_renamed
Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ElegantJointMeasurementInflation.singleton_identity_renamed (✓ std3). ∎
Source. Repository-derived.
Commentary.
A singleton outcome factors from its eight-node remainder and contributes the two-outcome marginal sum of p. The identity is valid for arbitrary continuous response models.