canonical_support_induced_config_space
plain-language theorem explainer
For any decidable atom type, finite-support recognition events form a configuration space whose independence relation is exactly disjoint support. Anyone assembling the support-event aggregate projection or the canonical distinction-atom universe cites this certificate. The proof is a two-field term constructor that installs the two support-disjointness lemmas.
Claim. For every type $A$ of atoms with decidable equality, the finite-support recognition events on $A$ carry a support-induced configuration-space structure: two events $a,b$ are independent in the cost-from-distinction sense if and only if their supports are disjoint, and that disjointness supplies the aggregate-projection compatibility interface.
background
The Unified Forcing Chain module derives T-1 through T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. Early in that chain one needs a concrete configuration space on which cost, independence, and aggregation are well-defined.
SupportInducedConfigSpace is the Prop-valued certificate for that space: the carrier is finite-support events on a decidable atom type, and ConfigSpace.Independent is identified with disjoint support. The two fields are an iff linking independence to support-disjointness, and a witness that disjoint support feeds the aggregate projection interface.
Upstream cost infrastructure (J-cost on recognition events, multiplicative-recognizer derived cost, rung-coarsen multiset cost) supplies the scalar work that later projections will sum. The present certificate only fixes the combinatorial independence relation those projections require.
proof idea
Term-mode structure constructor. The independent_iff field is filled by supportEvent_independent_iff_support_disjoint (independence of support events iff disjoint supports). The support_independence field is filled by supportEvent_support_disjoint_independence (disjoint support yields the aggregate-projection compatibility interface). No further tactics or rewriting.
why it matters
This is the canonical configuration-space certificate used by three parents in the same module. canonical_support_event_aggregate_projection installs it as support_induced and then attaches the scalar work projection (disjoint-support joins map to scalar addition). canonical_distinction_atom_universe uses it as support_carrier when building the atom universe from a bare distinction. That universe sits under the absolute-floor / T-1 side of the forcing chain.
It also appears in the dependency cone of t5_to_t6_bridge_holds, the bridge from unique J (T5) to the self-similar fixed point $\varphi$ (T6). Without a support-induced config space, the ledger events that carry the discrete self-similarity hierarchy have no certified independence relation, so the aggregate cost that forces $\varphi$ cannot be stated.
In the primer landmarks this is scaffolding under T3–T4 (ledger and recognition) rather than a direct T5–T8 statement: it makes the event carrier on which those later steps act.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.