ProductVisible
plain-language theorem explainer
A prior on fugacity and action is product-visible when it depends only on the physical Boltzmann product weight. The R18 booking-gauge wall cites this class to package ledger-internal candidates (label indifference, product gluing, insertion stationarity, orbit accounting). The definition is an existential factorisation: some predicate of the product map alone decides the prior.
Claim. Fix a bound $B\in\mathbb{N}$. A predicate $P$ on pairs $(a,S)$, with $a$ a fugacity assignment $\mathbb{N}^3\to\mathbb{R}$ and $S$ an action on bounded complexes of size at most $B$, is product-visible if there exists a predicate $Q$ on maps from those complexes to $\mathbb{R}$ such that $P(a,S)$ holds if and only if $Q$ holds of $K\mapsto w(a,K)\,e^{-S(K)}$, where $w$ is the fugacity weight.
background
The ambient module is the Gap-2 necessary-reasons census: richer RecognitionLedger / posting-layer structure is assumed to force the Gauge Counting Principle for physical class mass (equivalently $\nu=1/|\mathrm{Aut}|$). Each candidate reason is scored THEOREM, OPEN, MODEL, or REFUTED.
The physical Boltzmann product is the pointwise weight $w(a,K),e^{-S(K)}$ on a bounded complex $K$, with $w$ the fugacity weight from the Gap-2 gauge-volume layer and $S$ the action. Rebooking is the gauge $(a,S)\mapsto(t\cdot a,,S+\log t)$, which leaves that product unchanged. Product-visible priors are those whose truth value is a function of the product alone; the doc-comment notes that ledger-internal candidates (label indifference of the weight, gluing of the product, insertion stationarity, orbit accounting) all have this shape.
Upstream scaffolding supplies the fugacity weight and the bounded-complex carrier; the definition itself does not invoke the bridge ratio $K$ or the PRC stage chain.
proof idea
Pure definition, no proof obligations. Unpack as an existential: a witness predicate $Q$ on real-valued functions of bounded complexes, together with a biconditional that $P(a,S)$ holds exactly when $Q$ holds of the Boltzmann product map $K\mapsto w(a,K),e^{-S(K)}$. Instantiation in downstream lemmas is by obtain \langle Q, hQ\rangle := hP and rewriting through that biconditional.
why it matters
This class is the input type for the R18 block of the necessary-reasons census. Downstream, every product-visible prior is shown rebooking-invariant (the gauge step preserves the product pointwise), and no satisfiable product-visible prior can force the Gibbs numerator $a\equiv 1$. Those two facts assemble into the typed R18 wall: over every cap with a two-point complex, product-visible sits inside rebooking-invariant, and neither class selects unit fugacity.
In framework terms this closes a ledger-internal route to the Gauge Counting Principle: priors that only see the physical weight cannot pin $a\equiv 1$. The module honesty note records the residual OPEN as action-first priors that pin $S$ independently of the measure. The definition therefore marks the boundary between refuted product-only selectors and the surviving action-first residual.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.