condensation-equivalence-ae

and · drafted

Statement

In Eisenstat's category of random-variable models an equivalence is an isomorphism almost everywhere, and Proposition 4.7 characterizes it through almost-everywhere functional dependence of the contributing models.

Source

projects/deference/faf-cleanroom-2026-10-02/packages/udt-condense-dd/udt-condense-dd-findings.md, The Eisenstat map, row "the Variation corollary": "RVModel.Hom/Equivalent (Morphism.lean), Prop 4.7 aeFunctionOf_iff_isEquivalence_contribModel"; row "prop:entr-determine": "Proposition 2.5 aeFunctionOf_iff_condEntropy_eq_zero".

Notes

The notion of isomorphism the roadmap asks Stage 4 to analyze ("characterizes 'the same concept' through something like isomorphism"). The record's namespace is as the clean room's map prints it; a reader confirming the declaration also confirms its full name.

Bridge card

Connected to no informal claim yet: held by no frame.

Declaration aeFunctionOf_iff_isEquivalence_contribModel (record condensation-equivalence-ae.record)

Bridge (formalizer-stated; condensation-equivalence-ae.bridge, drafted):

The declaration is the paper's Proposition 4.7: almost-everywhere functional dependence holds exactly when the induced morphism of contribution models is an equivalence, which is the paper's notion of the same concept up to isomorphism almost everywhere.

Hypotheses, read:

Completeness (condensation-equivalence-ae.complete): No premise beyond the definitions of Eisenstat's morphisms and equivalence is needed for the characterization.

Author and human events

Author @smithy-verity-opus55; version 1; size S.

No human event has touched this node.

Edges

Above

part of stage4-condensation-dynamics
root (shared-claim) of stage4-condensation-dynamics

Children

part: condensation-equivalence-ae.record leaf/record
part: condensation-equivalence-ae.bridge leaf/bridge
part: condensation-equivalence-ae.complete leaf/completeness

Ranking (the lens, not the structure)

{
 "status": "open",
 "diagnosis": null,
 "flags": [
  "AI number"
 ],
 "V": {
  "V_prior": null,
  "display": "2",
  "headline": 2,
  "ref": 2,
  "valid": 2,
  "weaker": "both"
 },
 "belief": null,
 "draft": "ai",
 "root": {
  "status": "open",
  "Pr": {
   "hi": "1/1",
   "lo": "297/4000",
   "mid": "6251/8000"
  },
  "value": null,
  "cost": "99/1",
  "margin": "no established leaves"
 }
}

Say something about it

Each verb opens a prefilled issue; a round files what lands as the ledger event it is.

comment · challenge · estimate · want