and
plain-language theorem explainer
Conjunction of two extension-stable predicates on finite traces is again extension-stable. Anyone assembling the first Primitive Recognition Calculus logic layer cites this connective. The construction is pointwise logical and; stability is inherited componentwise from the two factors.
Claim. If $P$ and $Q$ are predicates on finite traces that persist under trace extension, then the pointwise conjunction $T \mapsto P(T) \land Q(T)$ is likewise a predicate that persists under every extension $T \preceq U$.
background
In the Primitive Recognition Calculus (PRC) first logic pass, a proposition is not an arbitrary Prop: it is a TracePredicate, a predicate on finite traces together with a stability witness. Stability means: if the predicate holds on $T$ and $U$ extends $T$, then it holds on $U$. That forces truth to be monotone along the directed system of growing observation records.
The ambient module builds the Boolean skeleton of that logic (truth, falsity, conjunction, disjunction, implication, negation, and quantifiers over traces). Conjunction is the first nontrivial binary connective: it must return another stable predicate, not merely a raw Prop.
Upstream, the only structural input is the TracePredicate record itself (holds plus stable). Name collisions elsewhere in the graph (Clifford and, various unit gauges $U$, field towers $T$) are unrelated to this connective.
proof idea
Define the holder as ordinary pointwise conjunction on traces. For stability, take an extension $T \preceq U$ and a proof that both conjuncts hold on $T$. Project the pair, apply each factor's own stability lemma along the same extension, and reassemble the pair on $U$. No extra lemmas; pure structure packing.
why it matters
This is the meet operation in the PRC stable-predicate lattice. Downstream introduction and projection rules (and_intro, and_left, and the rest of the TraceLogic API) sit on top of it, so every compound stable assertion in the first logic pass factors through this definition.
In the broader Recognition stack the stable-trace logic is the linguistic layer for statements that must survive longer observation windows (eight-tick cadence, defect traces, cost identities). The connective itself is pure foundation: it does not encode $J$, $\varphi$, or the forcing chain, but it is what lets those claims be stated as stable propositions rather than one-off Props.
Graph edges into Action/Euler–Lagrange modules are name-collision noise on the identifier and; the real consumers are the TraceLogic intro/elim lemmas and any PRC development that conjoins stable constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.