api-design rubric can request mutually-incompatible changes: remove @[expose] + add a rfl _apply/unfold lemma

[cameronfreer]

🤖 issue written by Claude Code and revised by Codex during a coding session that encountered this issue twice

Summary

For the same definition, the api-design rubric has asked to both:

1. remove @[expose] — "consumers can unfold the body instead of using a stable API"; and
2. add a public normal-form / _apply lemma proved by rfl — e.g. directingMeasure_apply,
   shiftRV_apply, consRV_zero.

In the Lean module system these two requests are mutually incompatible when the requested public
lemma needs to unfold the hidden definition. A public (exported) theorem whose proof unfolds a
definition's body, which every rfl _apply/unfold lemma does, requires that definition to be
@[expose]. Removing @[expose] makes the requested lemma fail to compile:

error: Not a definitional equality: the left-hand side
  directingMeasure μ X ω
is not definitionally equal to the right-hand side
  (condDistrib (X 0) id μ) ω
Note: This theorem is exported from the current module. This requires that all definitions that
need to be unfolded to prove this theorem must be exposed.

So one cannot satisfy both bullets for the same definition. This is not a complaint about _apply
lemmas or @[simp] lemmas in general. The conflict is specifically: hide the body and export a
body-unfolding normal form.

Where it occurred

• TauCeti#558 (directingMeasure): api-design asked to remove @[expose] and add
  @[simp] directingMeasure_apply : directingMeasure … = @condDistrib …. Incompatible. Resolved by
  removing @[expose] and relying on the property lemmas (isProbabilityMeasure_directingMeasure,
  measurable_tailProcess_directingMeasure_coe, directingMeasure_ae_eq_condExp) instead of an
  unfold lemma; documented in a code comment. (Merged.)
• TauCeti#560 (processShift / processCons / processTail / prefixCylinder / indProd):
  api-design asked to remove @[expose] and add shiftRV_apply, consRV_zero, consRV_succ,
  tailRV_apply, indProd_apply, etc. For these purely computational defs the only characterization
  IS the rfl _apply lemma, so removing @[expose] would leave them uncharacterizable. Resolved by
  keeping @[expose] and adding the _apply @[simp] lemmas; documented in a code comment.

The underlying distinction

Two kinds of definitions need different api-design guidance:

1. Computational defs (e.g. processShift X m ω n = X (m + n) ω): the characteristic API is the
   rfl _apply lemma. → Keep @[expose]; add @[simp] _apply lemmas. Removing @[expose]
   cannot be paired with the requested lemmas. For small projections, shifts, constructors,
   reindexing maps, and other computational adapters, @[expose] is not a code smell; it is how the
   module publicly promises definitional behavior.
2. Property-characterized defs (e.g. directingMeasure, characterized by probability /
   measurability / condExp lemmas, not its body): → Remove @[expose]; add the property lemmas.
   A _apply/unfold lemma is then impossible and should not be requested.

There is a related @[simp] distinction. A @[simp] theorem can be appropriate in either style, but
its right-hand side should be an intended public normal form. For a computational definition, that may
be the unfolded body. For a property-characterized definition, the simp/normal-form theorem should be
a property, constructor/destructor, or iff-style characterization, not an implementation-unfolding
lemma.

Suggested rubric refinement

The api-design rubric should not request both "remove @[expose]" and "add a rfl unfold/_apply
lemma" for the same definition. Instead:

• Computational def, API = the unfold: ask to keep @[expose] and add @[simp] _apply lemmas.
• Non-body characterization available: ask to remove @[expose] and add the property lemmas (and
  do not ask for an unfold lemma).

Concrete review rule:

Before asking to remove @[expose], check whether the same review asks for an rfl _apply or
unfold lemma. If yes, either keep @[expose], or replace the requested lemma with a non-unfolding
semantic characterization.

Private helper lemmas are not the issue here. A private proof may unfold whatever is locally
available. The problem is specifically the exported/public API requested from contributors.

Pointers

• TauCeti#558 (resolved by removing @[expose], property lemmas).
• TauCeti#560 (resolved by keeping @[expose], _apply lemmas).

[cameronfreer]

🤖 update written by Codex based on updated findings from a Claude Code coding session

Follow-up nuance from TauCeti#560: this is specifically about exported rfl / definitional-equality unfold lemmas. Some non-rfl characteristic lemmas can still be exported after removing @[expose] if they are proved propositionally, e.g. by simp only [theDef]/extensionality rather than rfl.

So the rubric refinement should probably distinguish:

• rfl _apply lemmas exposing the body: require @[expose];
• propositional characterization lemmas proved by ordinary reasoning: may work without @[expose];
• property-characterized defs: prefer no @[expose] and use those non-rfl characterization/property lemmas.

The bad request is not “remove @[expose] plus any public lemma”; it is “remove @[expose] plus require an exported lemma whose proof depends on definitional unfolding.”