SupportQuotientReflectsIndependence
plain-language theorem explainer
A quotient map q from abstract events to support-bearing events reflects independence when independence of the images forces independence of the sources. Anyone building support-disjoint independence or support extraction through a canonical support quotient cites this certificate. It is a single-field Prop structure; propositional uniqueness is immediate (Subsingleton by rfl).
Claim. Fix types $\mathrm{Event}$ and $\mathrm{Atom}$ with decidable equality on atoms, and equip $\mathrm{Event}$ with a configuration-space structure (empty config, join, consistency, independence). Let $q:\mathrm{Event}\to\mathrm{SupportEvent}(\mathrm{Atom})$ send each event to a finite-support carrier. The reflection certificate asserts: for all $a,b$, if $q(a)$ and $q(b)$ are independent in the support configuration space, then $a$ and $b$ are independent in the source configuration space.
background
In the Unified Forcing Chain module, T0–T8 are forced from the Recognition Composition Law plus normalization and calibration. Mid-chain bookkeeping needs a clean notion of when two configurations share no predicates, so that cost and ledger structure can be extracted without double-counting.
A configuration space supplies empty config, binary join, consistency, and an independence relation (no shared predicates), with join a commutative monoid and independence symmetric. The canonical model is the support event: a finite set of atoms, with join as union and independence as disjointness of supports. Thus on support events, independence is not an extra axiom; it is set-theoretic disjointness.
An arbitrary event type need not present independence that way. Mapping into the support carrier via a quotient $q$ lets one pull the concrete disjointness semantics back. The missing piece for inheritance is exactly reflection: independence after $q$ must imply independence before $q$.
proof idea
This declaration is a Prop-valued structure with one field: the universal implication that independence of $q(a)$ and $q(b)$ yields independence of $a$ and $b$. There is no computational body beyond packaging that predicate.
A companion instance proves that any two such certificates are propositionally equal (Subsingleton), by rfl on the unique Prop field. Downstream theorems assume an inhabitant of this structure and discharge the reflection hypothesis by projection, rather than re-proving the implication inline.
why it matters
The certificate is the exact remaining independence condition so an arbitrary event system inherits support-disjoint independence from its canonical support quotient. It feeds supportDisjointIndependence_of_supportQuotient (quotient reflecting independence induces support-disjoint independence for the extracted support map) and the full SupportExtractionThroughQuotient bundle, assembled by support_extraction_through_quotient from quotient-map, reflection, and cost-preservation surfaces.
That extraction path replaces a primitive support map with a theorem-backed map through SupportEvent. The same surface appears among the dependencies of the T5→T6 self-similarity bridge certificate, which routes unique $J$ into the forced scale ratio $\varphi$ once hierarchy data are realized. In the forcing chain, clean independence under quotienting keeps ledger and cost structure coherent before self-similarity (T6) and the eight-tick / $D=3$ steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.